search

ariadne-cps / ariadne

C++ framework for rigorous computation on cyber-physical systems
http://www.ariadne-cps.org
GNU General Public License v3.0
28 stars 9 forks source link

Inconsistent time domain returned by flow sets #289

Closed lgeretti closed 6 years ago

lgeretti commented 6 years ago

Our integrators currently return a time domain that might be [0, h] for Picard time-invariant flows, or [t, t+h] for Series flows. We should either guarantee a common domain (the latter), or in alternative modify any evolver code to rely on the actual bounds of the flow to extract the reach/evolve sets.

pietercollins commented 6 years ago

Currently, we are (sufficiently) consistent; time-invariant flow-steps always use initial time 0 (other initial times can be computed from this by translation), and time-dependent flows use the given initial time. I think it's good at the user level to statically distinguish between the time-independent and time-dependent cases, which is why the time arguments differ.
When we have a proper lambda-calculus, we could distinguish the cases by the arguments of the function. I would be happy (at some point) to only support time-dependent parametrised differential equations, and provide simple wrappers to support the other cases.

lgeretti commented 6 years ago

However, for the case at hand of DIs, the dynamics is currently time-independent and yet using TaylorSeriesIntegrator would return a flow that uses the initial time, while using TaylorPicardIntegrator doesn't. Since the time domain also affects the construction of the w functions, it would be significantly cleaner to have a consistent domain for the flow between the two integrators.

lgeretti commented 6 years ago

It would be sufficient, I guess, to treat the DI case as intrinsically time-dependent and use the time-dependent flow both for the Series and Picard integrators. What do you think @pietercollins ?

pietercollins commented 6 years ago

Yes, this latter is the approach to use, as introducing the inputs puts us in the time-dependent case anyway. Both integrators now support the same functionality.

lgeretti commented 6 years ago

Ok, then I'll close this issue.