Merge python-enclosure-list#543

Author: Luca Geretti

CHANGELOG.md

@@ -12,7 +12,7 @@ Legenda for the issue kind:
 
 ### 2.2
 
-*Date: /2021*
+*Date: 25/04/2021*
 
 - [#441](https://github.com/ariadne-cps/ariadne/issues/441) (N) Add support for Gnuplot output, including animated gif plot of sets and tridimensional plots for PDEs
 - [#507](https://github.com/ariadne-cps/ariadne/issues/507) (N) Add a simulator for vector field dynamics
@@ -22,6 +22,7 @@ Legenda for the issue kind:
 - [#516](https://github.com/ariadne-cps/ariadne/issues/516) (A) Add missing Python bindings for Real predicates to be used in automata specification
 - [#518](https://github.com/ariadne-cps/ariadne/issues/518) (A) Add missing Python bindings for evolver configuration and initial set assignment
 - [#520](https://github.com/ariadne-cps/ariadne/issues/520) (A) Add missing Python bindings for plotting using HybridFigure
+- [#543](https://github.com/ariadne-cps/ariadne/issues/543) (A) Add missing Python bindings for iterating across ListSet of Enclosure classes
 - [#527](https://github.com/ariadne-cps/ariadne/issues/527) (A) Allow to draw a Labelled/Hybrid orbit directly to a Labelled/Hybrid figure
 - [#492](https://github.com/ariadne-cps/ariadne/issues/492) (C) Modify SFINAE code to use C++20 concepts, currently preventing AppleClang compilation under macOS until the compiler supports Concepts
 - [#529](https://github.com/ariadne-cps/ariadne/issues/529) (C) Disallow construction of VectorField and IteratedMap from a Function, since it was broken

experimental/examples/arch/LOVO20.hpp

@@ -69,7 +69,7 @@ void LOVO20()
     RealPoint ic({1.3_dec,1.0_dec});
     Real e(0.008_dec);
     HybridSet initial_set(lotkavolterra|outside,{ic[0]-e<=x<=ic[0]+e,y==ic[1],cnt==0});
-    HybridTime evolution_time(3.64,3);
+    HybridTime evolution_time(3.64_dec,3u);
 
     StopWatch sw;
 
@@ -97,7 +97,7 @@ void LOVO20()
     else ARIADNE_LOG_PRINTLN("No final set with two transitions has been found!");
 
     ARIADNE_LOG_PRINTLN("Trajectory stays within " << (radius*100).get_d() << "% of the equilibrium for at most " <<
-                        final_bounds[cnt].upper() << " time units: " << ((definitely(final_bounds[cnt] <= 0.2_dec)) ?
+                        final_bounds[cnt].upper_bound() << " time units: " << ((definitely(final_bounds[cnt] <= 0.2_dec)) ?
                         "constraint satisfied." : "constraint not satisfied!"));
 
     ARIADNE_LOG_PRINTLN("Done in " << sw.elapsed() << " seconds.");
@@ -109,19 +109,19 @@ void LOVO20()
         instance.set_verified(1)
                 .set_execution_time(sw.elapsed())
                 .add_loss((final_bounds[x].width()*final_bounds[y].width()).get_d())
-                .add_loss(final_bounds[cnt].upper().get_d());
+                .add_loss(final_bounds[cnt].upper_bound().get_d());
     }
     instance.write();
 
     HybridAutomaton circle;
     DiscreteLocation rotate;
     RealVariable t("t");
     circle.new_mode(rotate,{let(x)=cx+radius*cos(t),let(y)=cy-radius*sin(t)},{dot(t)=1});
-    HybridSimulator simulator;
-    simulator.set_step_size(0.1);
+    HybridSimulator simulator(circle);
+    simulator.configuration().set_step_size(0.1);
     HybridRealPoint circle_initial(rotate,{t=0});
     HybridTime circle_time(2*pi,1);
-    ARIADNE_LOG_RUN_MUTED(auto circle_orbit = simulator.orbit(circle,circle_initial,circle_time));
+    ARIADNE_LOG_RUN_MUTED(auto circle_orbit = simulator.orbit(circle_initial,circle_time));
 
     ARIADNE_LOG_RUN_AT(2,plot(benchmark.name().c_str(),Axes2d(0.6<=x<=1.4,0.6<=y<=1.4), orange, orbit, black, circle_orbit));
     ARIADNE_LOG_PRINTLN("File " << benchmark.name() << ".png written.");

python/examples/hybrid/LOVO20.py

@@ -122,16 +122,16 @@ def plot_all(LOVO20_orbit,circle_orbit):
 #! [/compute_evolution]
 
 
-#! [check_number_of_events]
-def check_number_of_events(orbit):
+#! [verify]
+def verify(orbit):
 
     has_any_zero_transitions = False
     has_any_two_transitions = False
 
     for enclosure in orbit.final():
-        if (not has_any_zero_transitions) and enclosure.previous_events().size() == 0:
+        if (not has_any_zero_transitions) and len(enclosure.previous_events()) == 0:
             has_any_zero_transitions = True
-        if (not has_any_two_transitions) and enclosure.previous_events().size() == 2:
+        if (not has_any_two_transitions) and len(enclosure.previous_events()) == 2:
             has_any_two_transitions = True
 
     if has_any_zero_transitions:
@@ -144,7 +144,17 @@ def check_number_of_events(orbit):
     else:
         print("No final set with two transitions has been found!")
 
-#! [/check_number_of_events]
+    x = RealVariable("x")
+    y = RealVariable("y")
+    cnt = RealVariable("cnt")
+
+    final_bounds = orbit.final().bounding_box()
+
+    print("Trajectory stays in the reference circle for at most", final_bounds[cnt].upper_bound(), "time units: ", end='')
+    print("constraint satisfied") if final_bounds[cnt].upper_bound().raw() <= FloatDP(0.2,DoublePrecision()) else print("constraint NOT satisfied!")
+
+
+#! [/verify]
 
 #! [main]
 if __name__ == '__main__':
@@ -165,7 +175,7 @@ def check_number_of_events(orbit):
     LOVO20_orbit = evolver.orbit(initial_set,final_time,Semantics.UPPER)
 
     # Check number of events
-    #check_number_of_events(LOVO20_orbit)
+    verify(LOVO20_orbit)
 
     # Get the orbit of the circle to plot, by points
     circle_orbit = get_circle_orbit()

python/source/evolution_submodule.cpp

@@ -34,6 +34,37 @@
 
 using namespace Ariadne;
 
+Void export_labelled_drawable_2d_interface(pybind11::module& module) {
+    pybind11::class_<LabelledDrawable2dInterface> labelled_drawable_interface_class(module,"LabelledDrawable2dInterface");
+}
+
+Void export_semantics(pybind11::module& module) {
+    pybind11::enum_<Semantics> semantics_enum(module,"Semantics");
+    semantics_enum.value("UPPER", Semantics::UPPER);
+    semantics_enum.value("LOWER", Semantics::LOWER);
+    //    semantics_enum.def("__repr__" , &__cstr__<Semantics>);
+}
+
+Void export_storage(pybind11::module& module) {
+    pybind11::class_<Storage,pybind11::bases<Drawable2dInterface>> storage_class(module,"Storage");
+    pybind11::class_<LabelledStorage,pybind11::bases<LabelledDrawable2dInterface>> labelled_storage_class(module,"LabelledStorage");
+}
+
+Void export_enclosure(pybind11::module& module) {
+    pybind11::class_<Enclosure,pybind11::bases<Drawable2dInterface>> enclosure_class(module,"Enclosure");
+    enclosure_class.def("bounding_box",&Enclosure::bounding_box);
+    enclosure_class.def("__str__", &__cstr__<Enclosure>);
+    pybind11::class_<LabelledEnclosure,pybind11::bases<LabelledDrawable2dInterface,Enclosure>> labelled_enclosure_class(module,"LabelledEnclosure");
+    labelled_enclosure_class.def("bounding_box",&LabelledEnclosure::bounding_box);
+    labelled_enclosure_class.def("__str__", &__cstr__<LabelledEnclosure>);
+}
+
+template<class T> Void export_list_set(pybind11::module& module, const char* name) {
+    pybind11::class_<ListSet<T>> list_set_class(module,name);
+    list_set_class.def("__iter__", [](ListSet<T> const& l){return pybind11::make_iterator(l.begin(),l.end());});
+    list_set_class.def("size",&ListSet<T>::size);
+}
+
 
 template<class ORB>
 Void export_orbit(pybind11::module& module, const char* name)
@@ -45,15 +76,6 @@ Void export_orbit(pybind11::module& module, const char* name)
     orbit_class.def("__str__", &__cstr__<ORB>);
 }
 
-
-Void export_semantics(pybind11::module& module) {
-    pybind11::enum_<Semantics> semantics_enum(module,"Semantics");
-    semantics_enum.value("UPPER", Semantics::UPPER);
-    semantics_enum.value("LOWER", Semantics::LOWER);
-    //    semantics_enum.def("__repr__" , &__cstr__<Semantics>);
-}
-
-
 template<class SIM> Void export_simulator(pybind11::module& module, const char* name);
 
 template<> Void export_simulator<VectorFieldSimulator>(pybind11::module& module, const char* name)
@@ -65,7 +87,6 @@ template<> Void export_simulator<VectorFieldSimulator>(pybind11::module& module,
 
     auto const& reference_internal = pybind11::return_value_policy::reference_internal;
 
-    pybind11::class_<LabelledDrawable2dInterface> labelled_drawable_interface_class(module,"LabelledDrawable2dInterface");
     pybind11::class_<LabelledInterpolatedCurve,pybind11::bases<LabelledDrawable2dInterface>> labelled_interpolated_curve_class(module,"LabelledInterpolatedCurve");
 
     pybind11::class_<OrbitType,pybind11::bases<LabelledDrawable2dInterface>> simulator_orbit_class(module,"ApproximatePointOrbit");
@@ -124,10 +145,6 @@ Void export_vector_field_evolver_configuration(pybind11::module& module) {
     vector_field_evolver_configuration_class.def("__repr__",&__cstr__<ConfigurationType>);
 }
 
-Void export_labelled_storage(pybind11::module& module) {
-    pybind11::class_<LabelledStorage,pybind11::bases<LabelledDrawable2dInterface>> labelled_storage_class(module,"LabelledStorage");
-}
-
 template<class RA> Void export_safety_certificate(pybind11::module& module, const char* name) {
     typedef typename RA::StorageType StorageType;
     typedef typename RA::StateSpaceType StateSpaceType;
@@ -175,8 +192,15 @@ Void export_reachability_analyser(pybind11::module& module, const char* name)
 
 Void evolution_submodule(pybind11::module& module)
 {
+    export_labelled_drawable_2d_interface(module);
+
     export_semantics(module);
 
+    export_storage(module);
+    export_enclosure(module);
+
+    export_list_set<LabelledEnclosure>(module,"LabelledEnclosureListSet");
+
     export_simulator<VectorFieldSimulator>(module,"VectorFieldSimulator");
 
     export_evolver_interface<IteratedMapEvolver::Interface>(module, "IteratedMapEvolverInterface");
@@ -189,8 +213,6 @@ Void evolution_submodule(pybind11::module& module)
 
     export_vector_field_evolver_configuration(module);
 
-    export_labelled_storage(module);
-
     export_safety_certificate<ContinuousReachabilityAnalyser>(module,"SafetyCertificate");
     export_reachability_analyser<ContinuousReachabilityAnalyser,VectorFieldEvolver>(module,"ContinuousReachabilityAnalyser");
 }

python/source/geometry_submodule.cpp

@@ -812,8 +812,6 @@ Void export_constrained_image_set(pybind11::module& module)
     //module.def("product", (ValidatedConstrainedImageSet(*)(const ValidatedConstrainedImageSet&,const BasicSetType&)) &product);
 }
 
-
-
 Void geometry_submodule(pybind11::module& module) {
     export_drawable_interface(module);
     export_set_interface(module);

python/source/hybrid_submodule.cpp

@@ -280,10 +280,19 @@ Void export_hybrid_storage(pybind11::module& module) {
 }
 
 Void export_hybrid_enclosure(pybind11::module& module) {
+    auto const& reference_internal = pybind11::return_value_policy::reference_internal;
+
     pybind11::class_<HybridEnclosure> hybrid_enclosure_class(module,"HybridEnclosure");
+    hybrid_enclosure_class.def("previous_events", &HybridEnclosure::previous_events,reference_internal);
     hybrid_enclosure_class.def("__repr__", &__cstr__<HybridEnclosure>);
 }
 
+Void export_list_set_hybrid_enclosure(pybind11::module& module) {
+    pybind11::class_<ListSet<HybridEnclosure>> list_set_hybrid_enclosure_class(module,"HybridEnclosureListSet");
+    list_set_hybrid_enclosure_class.def("__iter__", [](ListSet<HybridEnclosure> const& l){return pybind11::make_iterator(l.begin(),l.end());});
+    list_set_hybrid_enclosure_class.def("bounding_box",&ListSet<HybridEnclosure>::bounding_box);
+}
+
 Void export_hybrid_automaton(pybind11::module& module)
 {
     // Don't use return_value_policy<copy_const_reference> since reference lifetime should not exceed automaton lifetime
@@ -293,8 +302,7 @@ Void export_hybrid_automaton(pybind11::module& module)
 
     pybind11::class_<HybridAutomatonInterface> hybrid_automaton_interface_class(module,"HybridAutomatonInterface");
 
-    pybind11::class_<HybridAutomaton,pybind11::bases<HybridAutomatonInterface>>
-        hybrid_automaton_class(module,"HybridAutomaton");
+    pybind11::class_<HybridAutomaton,pybind11::bases<HybridAutomatonInterface>> hybrid_automaton_class(module,"HybridAutomaton");
     hybrid_automaton_class.def(pybind11::init<>());
     hybrid_automaton_class.def(pybind11::init<Identifier>());
     hybrid_automaton_class.def("locations", &HybridAutomaton::locations);
@@ -520,8 +528,9 @@ Void hybrid_submodule(pybind11::module& module) {
     export_hybrid_storage(module);
     export_hybrid_enclosure(module);
 
-    export_hybrid_automaton(module);
+    export_list_set_hybrid_enclosure(module);
 
+    export_hybrid_automaton(module);
 
     export_hybrid_time(module);
     export_hybrid_termination_criterion(module);

python/source/symbolic_submodule.cpp

@@ -445,10 +445,18 @@ Void export_sets(pybind11::module& module, pybind11::class_<RealVariable>& real_
     pybind11::class_<RealVariablesBox> real_variables_box_class(module,"RealVariablesBox");
     real_variables_box_class.def(pybind11::init<Map<RealVariable,RealInterval>>());
     real_variables_box_class.def(pybind11::init<List<RealVariableInterval>>());
-//    real_variables_box_class.def(pybind11::init<Set<RealVariableInterval>>());
     real_variables_box_class.def("__getitem__", &RealVariablesBox::operator[]);
     real_variables_box_class.def("__str__",&__cstr__<RealVariablesBox>);
 
+    typedef VariablesBox<FloatDPUpperInterval> FloatDPVariablesBox;
+    pybind11::class_<FloatDPVariablesBox> floatdp_variables_box_class(module,"FloatDPVariablesBox");
+    floatdp_variables_box_class.def("__getitem__", &FloatDPVariablesBox::operator[]);
+    floatdp_variables_box_class.def("__str__",&__cstr__<FloatDPVariablesBox>);
+
+    pybind11::class_<LabelledBox<FloatDPUpperInterval>> labelled_floatdp_upper_box_class(module,"LabelledFloatDPUpperBox");
+    labelled_floatdp_upper_box_class.def("__getitem__", &LabelledBox<FloatDPUpperInterval>::operator[]);
+    labelled_floatdp_upper_box_class.def("__str__",&__cstr__<LabelledBox<FloatDPUpperInterval>>);
+
     pybind11::class_<RealExpressionConstraintSet> real_expression_constraint_set_class(module,"RealExpressionConstraintSet");
     real_expression_constraint_set_class.def(pybind11::init<List<ContinuousPredicate>>());
     real_expression_constraint_set_class.def("__str__",&__cstr__<RealExpressionConstraintSet>);

source/dynamics/enclosure.cpp

@@ -1592,31 +1592,6 @@ Void ListSet<LabelledEnclosure>::draw(CanvasInterface& cnvs, const Variables2d&
     }
 }
 
-const RealSpace LabelledSet<ListSet<Enclosure>>::space() const {
-    return (*this)[0].space();
-}
-
-const RealSpace LabelledSet<ListSet<Enclosure>>::state_space() const {
-    return (*this)[0].state_space();
-}
-
-const ListSet<Enclosure> LabelledSet<ListSet<Enclosure>>::euclidean_set() const {
-    ListSet<Enclosure> result;
-    for (SizeType i=0; i!=this->size(); ++i) {
-        result.adjoin((*this)[i].euclidean_set());
-    }
-    return result;
-}
-
-const LabelledUpperBoxType LabelledSet<ListSet<Enclosure>>::bounding_box() const {
-    if (this->empty()) { return LabelledUpperBoxType(this->space(),UpperBoxType(this->space().dimension())); }
-    UpperBoxType bbx=(*this)[0].euclidean_set().bounding_box();
-    for (SizeType i=1; i!=this->size(); ++i) {
-        bbx=hull(bbx,(*this)[i].euclidean_set().bounding_box());
-    }
-    return LabelledUpperBoxType(this->state_space(),bbx);
-}
-
 } // namespace Ariadne
 
 

source/dynamics/enclosure.hpp

@@ -446,17 +446,6 @@ template<> class ListSet<LabelledEnclosure> : public LabelledDrawable2dInterface
     virtual Void draw(CanvasInterface&, const Variables2d&) const override;
 };
 
-template<> class LabelledSet<ListSet<Enclosure>> : public ListSet<LabelledEnclosure> {
-  public:
-    LabelledSet<ListSet<Enclosure>>() : ListSet<LabelledEnclosure>() { }
-    LabelledSet<ListSet<Enclosure>>(ListSet<LabelledEnclosure> lst) : ListSet<LabelledEnclosure>(lst) { }
-
-    const RealSpace state_space() const;
-    const RealSpace space() const;
-    const ListSet<Enclosure> euclidean_set() const;
-    const LabelledUpperBoxType bounding_box() const;
-};
-
 } //namespace Ariadne
 
 #endif /* ARIADNE_ENCLOSURE_HPP */

source/dynamics/orbit.hpp

@@ -161,7 +161,7 @@ class Orbit<LabelledEnclosure>
     : public LabelledDrawable2dInterface
 {
     typedef LabelledEnclosure ES;
-    typedef LabelledSet<ListSet<Enclosure>> ESL;
+    typedef ListSet<LabelledEnclosure> ESL;
   public:
     typedef ES EnclosureType;
     typedef ESL EnclosureListType;