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

Flow tubes and orbits #24

Open lgeretti opened 7 years ago

lgeretti commented 7 years ago

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Change evolution of continuous/hybrid systems to use flow-tube functions instead of Enclosure sets. Change Orbits to track splitting and jumping.


lgeretti commented 7 years ago

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


A flow tube is a function phi(x0,t) where x0 is the initial point. Knowing this is useful for some dynamical systems applications. It may also help with recombining. Enclosures are sets, so don't take account of where a point came from (though for reachability analysis this is no loss, and gives more scope for reductions.)

The new Orbit class (here incomplete) will allow better inspection of the computed dynamics and also enable recombining.

lgeretti commented 7 years ago

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


What is the expected advantage over enclosure sets?

lgeretti commented 7 years ago

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Possible implementation

#!c++

class FlowTube {
    ValidatedVectorFunctionModel64 _phi;
    List<Identifier> _variable_names;
  public:
    SizeType number_of_state_variables() const { return _phi.result_size(); }
    template<class X> decltype(auto) operator()(Vector<X> const& x, Scalar<X> const& t) { return phi(join(x,t)); }
    decltype(auto) space_domain() const { SizeType n=this->number_of_state_variables(); return _phi.domain()[range(0,n)]; }
    decltype(auto) time_range() const { SizeType n=this->number_of_state_variables(); return _phi.domain()[n]; }
    decltype(auto) initial_time() const { return time_range().lower(); }
    decltype(auto) final_time() const { return time_range().upper(); }
    ValidatedVectorFunctionModel64 reach_function() const;
    ValidatedVectorFunctionModel64 final_function() const;
    ValidatedImageSet initial_set() const;
    ValidatedImageSet reach_set() const;
    ValidatedImageSet final_set() const;
};

template<class E, class R=E> struct OrbitStep {
    OrbitStep* _previous;
    E _initial; R _intermediate;
    List<OrbitStep> _next;
    List<E> _final;
};

template<> class Orbit<FlowTube> {
    using ES=FlowTube;
    OrbitStep<ES> _starting;
    List<OrbitStep<ES>*> _working;
  public:
    Orbit(const ES& set);
};