Skip to content

Commit

Permalink
Remove evolve/reach/reach_evolve from evolver interface (solves #552)
Browse files Browse the repository at this point in the history
  • Loading branch information
lgeretti committed May 2, 2021
1 parent 3169bd3 commit 07ca99e
Show file tree
Hide file tree
Showing 6 changed files with 24 additions and 91 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Legenda for the issue kind:

- [#538](https://github.com/ariadne-cps/ariadne/issues/538) (N) Introduce a concurrency module designed for parallel execution of internal tasks
- [#549](https://github.com/ariadne-cps/ariadne/issues/549) (N) Introduce a Least Recently Used cache utility for holding a limited number of homogeneous objects
- [#552](https://github.com/ariadne-cps/ariadne/issues/552) (C) Remove evolve/reach/reach_evolve methods from EvolverInterface, relying on orbit generation only
- [#539](https://github.com/ariadne-cps/ariadne/issues/539) (F) A segmentation fault sometimes would be issued when terminating the executable, due to logging

### 2.2
Expand Down
12 changes: 0 additions & 12 deletions source/dynamics/evolver_base.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,18 +58,6 @@ template<class SYS, class ES, class TRM> class EvolverBase

virtual Orbit<EnclosureType> orbit(const EnclosureType& initial_set, const TerminationType& termination, Semantics semantics) const = 0;

EnclosureListType evolve(const EnclosureType& initial_set, const TerminationType& termination, Semantics semantics) const {
EnclosureListType final; EnclosureListType reachable; EnclosureListType intermediate;
this->_evolution(final,reachable,intermediate,initial_set,termination,semantics); return final; }

EnclosureListType reach(const EnclosureType& initial_set, const TerminationType& termination, Semantics semantics) const {
EnclosureListType final; EnclosureListType reachable; EnclosureListType intermediate;
this->_evolution(final,reachable,intermediate,initial_set,termination,semantics); return reachable; }

Pair<EnclosureListType,EnclosureListType> reach_evolve(const EnclosureType& initial_set, const TerminationType& termination, Semantics semantics) const {
EnclosureListType final; EnclosureListType reachable; EnclosureListType intermediate;
this->_evolution(final,reachable,intermediate,initial_set,termination,semantics); return std::make_pair(reachable,final); }

//!@}

protected:
Expand Down
21 changes: 0 additions & 21 deletions source/dynamics/evolver_interface.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -87,27 +87,6 @@ class EvolverInterface
const TerminationType& time,
Semantics semantics) const = 0;

//! \brief Compute an approximation to the evolved set under the given semantics.
virtual
EnclosureListType
evolve(const EnclosureType& initial_set,
const TerminationType& time,
Semantics semantics) const = 0;

//! \brief Compute an approximation to the reachable set under the given semantics.
virtual
EnclosureListType
reach(const EnclosureType& initial_set,
const TerminationType& time,
Semantics semantics) const = 0;

//! \brief Compute an approximation to the evolved and reachable sets under the given semantics.
virtual
Pair<EnclosureListType,EnclosureListType>
reach_evolve(const EnclosureType& initial_set,
const TerminationType& time,
Semantics semantics) const = 0;

//!@}

};
Expand Down
1 change: 0 additions & 1 deletion source/dynamics/iterated_map_evolver.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,6 @@ class IteratedMapEvolver

//!@}


//!@{
//! \name Evolution using abstract sets.
//! \brief Compute an approximation to the orbit set using upper semantics.
Expand Down
66 changes: 23 additions & 43 deletions source/dynamics/reachability_analyser.tpl.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -99,17 +99,13 @@ _reach_evolve_resume(const ListSet<EnclosureType>& initial_enclosures,
StorageType& reach_cells=result.first; StorageType& evolve_cells=result.second;

for(auto initial_enclosure : initial_enclosures) {
ListSet<EnclosureType> current_reach_enclosures;
ListSet<EnclosureType> current_evolve_enclosures;

make_lpair(current_reach_enclosures,current_evolve_enclosures) = evolver.reach_evolve(initial_enclosure,time,semantics);
auto orbit = evolver.orbit(initial_enclosure,time,semantics);

for(auto enclosure : current_reach_enclosures) {
enclosure.adjoin_outer_approximation_to(reach_cells,accuracy);
}
for(auto enclosure : orbit.reach()) enclosure.adjoin_outer_approximation_to(reach_cells,accuracy);
ARIADNE_LOG_PRINTLN_AT(1,"final reach size = "<<reach_cells.size());

for(auto enclosure : current_evolve_enclosures) {
for(auto enclosure : orbit.final()) {
ARIADNE_LOG_PRINTLN_AT(2,"enclosure = "<<enclosure);
enclosure.adjoin_outer_approximation_to(evolve_cells,accuracy);
EnclosureType new_enclosure = enclosure;
Expand Down Expand Up @@ -138,7 +134,7 @@ _upper_reach(const StorageType& set,
cells.mince(accuracy);
for(auto cell : cells) {
EnclosureType initial_enclosure = evolver.enclosure(cell.box());
ListSet<EnclosureType> reach = evolver.reach(initial_enclosure,time,Semantics::UPPER);
ListSet<EnclosureType> reach = evolver.orbit(initial_enclosure,time,Semantics::UPPER).reach();
for(auto enclosure : reach) {
enclosure.adjoin_outer_approximation_to(result,accuracy);
}
Expand All @@ -158,13 +154,11 @@ _upper_evolve(const StorageType& set,
ARIADNE_LOG_SCOPE_CREATE;
GridType grid=set.grid();
StorageType result(grid,this->system()); StorageType cells=set; cells.mince(accuracy);
for(auto cell : cells) {
for (auto cell : cells) {
ARIADNE_LOG_PRINTLN_AT(1,"Evolving cell = "<<cell);
EnclosureType initial_enclosure = evolver.enclosure(cell.box());
ListSet<EnclosureType> final = evolver.evolve(initial_enclosure,time,Semantics::UPPER);
for(auto enclosure : final) {
enclosure.adjoin_outer_approximation_to(result,accuracy);
}
ListSet<EnclosureType> final = evolver.orbit(initial_enclosure,time,Semantics::UPPER).final();
for (auto enclosure : final) enclosure.adjoin_outer_approximation_to(result,accuracy);
}
ARIADNE_LOG_PRINTLN("_upper_evolve result size = "<<result.size());
return result;
Expand All @@ -187,20 +181,14 @@ _adjoin_upper_reach_evolve(StorageType& reach_cells,

ARIADNE_LOG_PRINTLN("Evolving "<<cells.size()<<" cells");
ProgressIndicator indicator(cells.size());
for(auto const& cell : cells) {
for (auto const& cell : cells) {
ARIADNE_LOG_PRINTLN_AT(1,"evolving cell = "<<cell);
EnclosureType initial_enclosure = evolver.enclosure(cell.box());
ListSet<EnclosureType> reach_enclosures;
ListSet<EnclosureType> final_enclosures;
make_lpair(reach_enclosures,final_enclosures) = evolver.reach_evolve(initial_enclosure,time,Semantics::UPPER);
ARIADNE_LOG_PRINTLN_AT(1,"computed "<<reach_enclosures.size()<<" reach enclosures and "<<final_enclosures.size()<<" final enclosures.");
auto orbit = evolver.orbit(initial_enclosure,time,Semantics::UPPER);
ARIADNE_LOG_PRINTLN_AT(1,"computed "<<orbit.reach().size()<<" reach enclosures and "<<orbit.final().size()<<" final enclosures.");

for(auto enclosure : reach_enclosures) {
enclosure.adjoin_outer_approximation_to(reach_cells,accuracy);
}
for(auto enclosure : final_enclosures) {
enclosure.adjoin_outer_approximation_to(evolve_cells,accuracy);
}
for (auto enclosure : orbit.reach()) enclosure.adjoin_outer_approximation_to(reach_cells,accuracy);
for (auto enclosure : orbit.final()) enclosure.adjoin_outer_approximation_to(evolve_cells,accuracy);
ARIADNE_LOG_SCOPE_PRINTHOLD("[" << indicator.symbol() << "] " << indicator.percentage() << "% of cells evolved.");
}

Expand Down Expand Up @@ -229,7 +217,7 @@ lower_evolve(const OvertSetInterfaceType& initial_set,
ARIADNE_LOG_PRINTLN_AT(1,"initial_cells.size()="<<initial_cells.size());
for(auto cell : initial_cells) {
EnclosureType initial_enclosure=_evolver->enclosure(cell.box());
ListSet<EnclosureType> final_enclosures=_evolver->evolve(initial_enclosure,time,Semantics::LOWER);
ListSet<EnclosureType> final_enclosures=_evolver->orbit(initial_enclosure,time,Semantics::LOWER).final();
for(auto enclosure : final_enclosures) {
enclosure.adjoin_outer_approximation_to(final_cells,grid_fineness);
}
Expand Down Expand Up @@ -258,12 +246,10 @@ lower_reach(const OvertSetInterfaceType& initial_set,
// Improve accuracy of initial set for lower computations
initial_cells.adjoin_lower_approximation(initial_set,grid_extent,grid_fineness+4);
ARIADNE_LOG_PRINTLN_AT(1,"initial_cells.size()="<<initial_cells.size());
for(auto cell : initial_cells) {
for (auto cell : initial_cells) {
EnclosureType initial_enclosure=_evolver->enclosure(cell.box());
ListSet<EnclosureType> reach_enclosures=_evolver->reach(initial_enclosure,time,Semantics::LOWER);
for(auto enclosure : reach_enclosures) {
enclosure.adjoin_outer_approximation_to(reach_cells,grid_fineness);
}
ListSet<EnclosureType> reach_enclosures=_evolver->orbit(initial_enclosure,time,Semantics::LOWER).reach();
for (auto enclosure : reach_enclosures) enclosure.adjoin_outer_approximation_to(reach_cells,grid_fineness);
}
return reach_cells;
}
Expand Down Expand Up @@ -291,17 +277,11 @@ lower_reach_evolve(const OvertSetInterfaceType& initial_set,
initial_cells.adjoin_lower_approximation(initial_set,grid_extent,grid_fineness+4);
ARIADNE_LOG_PRINTLN_AT(1,"initial_cells.size()="<<initial_cells.size());

for(auto cell : initial_cells) {
for (auto cell : initial_cells) {
EnclosureType initial_enclosure=_evolver->enclosure(cell.box());
ListSet<EnclosureType> reach_enclosures;
ListSet<EnclosureType> final_enclosures;
make_lpair(reach_enclosures,final_enclosures) = _evolver->reach_evolve(initial_enclosure,time,Semantics::LOWER);
for(auto enclosure : reach_enclosures) {
enclosure.adjoin_outer_approximation_to(reach,grid_fineness);
}
for(auto enclosure : final_enclosures) {
enclosure.adjoin_outer_approximation_to(evolve_cells,grid_fineness);
}
auto orbit = _evolver->orbit(initial_enclosure,time,Semantics::LOWER);
for (auto enclosure : orbit.reach()) enclosure.adjoin_outer_approximation_to(reach,grid_fineness);
for (auto enclosure : orbit.final()) enclosure.adjoin_outer_approximation_to(evolve_cells,grid_fineness);
}
return make_pair(reach,evolve_cells);
}
Expand Down Expand Up @@ -342,11 +322,11 @@ lower_reach(const OvertSetInterfaceType& initial_set) const

StorageType reach_cells(grid,this->system());

if(possibly(transient_time > TimeType(0))) {
if (possibly(transient_time > TimeType(0))) {
ARIADNE_LOG_PRINTLN("Computing transient evolution...");

ListSet<EnclosureType> initial_enclosures;
for(auto cell : initial_cells)
for (auto cell : initial_cells)
initial_enclosures.adjoin(_evolver->enclosure(cell.box()));

make_lpair(reach_cells,evolve_cells) =
Expand All @@ -363,7 +343,7 @@ lower_reach(const OvertSetInterfaceType& initial_set) const
}
ARIADNE_LOG_PRINTLN("Computing recurrent evolution...");

while(!evolve_cells.is_empty()) {
while (!evolve_cells.is_empty()) {

StorageType new_reach_cells(grid,this->system());
ListSet<EnclosureType> new_evolve_enclosures;
Expand Down
14 changes: 0 additions & 14 deletions source/dynamics/vector_field_evolver.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -103,20 +103,6 @@ class VectorFieldEvolver
OrbitType orbit(RealVariablesBox const& initial_set, TimeType const& time, Semantics semantics=Semantics::UPPER) const;
OrbitType orbit(RealExpressionBoundedConstraintSet const& initial_set, TimeType const& time, Semantics semantics=Semantics::UPPER) const;

using EvolverBase< VectorField, EnclosureType, TerminationType >::evolve;
using EvolverBase< VectorField, EnclosureType, TerminationType >::reach;

//! \brief Compute an approximation to the evolution set using upper semantics.
EnclosureListType evolve(const EnclosureType& initial_set, const TimeType& time) const {
EnclosureListType final; EnclosureListType reachable; EnclosureListType intermediate;
this->_evolution(final,reachable,intermediate,initial_set,time,Semantics::UPPER);
return final; }

//! \brief Compute an approximation to the reachable set under upper semantics.
EnclosureListType reach(const EnclosureType& initial_set, const TimeType& time) const {
EnclosureListType final; EnclosureListType reachable; EnclosureListType intermediate;
this->_evolution(final,reachable,intermediate,initial_set,time,Semantics::UPPER);
return reachable; }
//!@}

protected:
Expand Down

0 comments on commit 07ca99e

Please sign in to comment.