Skip to content

Commit

Permalink
Reimplemented missing checks to composite hybrid automaton class. Add…
Browse files Browse the repository at this point in the history 
…ed discrete reachability to HybridAutomaton.
  • Loading branch information
@pietercollins
pietercollins committed Oct 15, 2024
1 parent d329a7a commit 3d2233c
Show file tree
Hide file tree
Showing 7 changed files with 168 additions and 68 deletions.
11 changes: 8 additions & 3 deletions python/source/hybrid_submodule.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,16 +375,21 @@ Void export_hybrid_automaton(pybind11::module& module)
hybrid_automaton_class.def("new_transition",overload_cast<DiscreteLocation,DiscreteEvent,DiscreteLocation,ContinuousPredicate const&,EventKind>(&HybridAutomaton::new_transition));
hybrid_automaton_class.def("new_transition",overload_cast<DiscreteLocation,DiscreteEvent,DiscreteLocation,List<PrimedRealAssignment>const&>(&HybridAutomaton::new_transition));
*/
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,ContinuousPredicate const& grd,EventKind knd){return ha.new_transition(s,e,t,grd,knd);});
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,ContinuousPredicate grd,EventKind knd){return ha.new_transition(s,e,t,grd,knd);});
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,PrimedRealAssignmentMap res){return ha.new_transition(s,e,t,to_list(res));});
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,PrimedRealAssignmentMap res,ContinuousPredicate const& grd,EventKind knd){return ha.new_transition(s,e,t,to_list(res),grd,knd);});
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,ContinuousPredicate const& grd,PrimedRealAssignmentMap res,EventKind knd){return ha.new_transition(s,e,t,to_list(res),grd,knd);}); hybrid_automaton_class.def("__str__ ", &__cstr__<HybridAutomaton>);
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,PrimedRealAssignmentMap res,ContinuousPredicate grd,EventKind knd){return ha.new_transition(s,e,t,to_list(res),grd,knd);});
hybrid_automaton_class.def("new_transition",[](HybridAutomaton& ha, DiscreteLocation s,DiscreteEvent e,DiscreteLocation t,ContinuousPredicate grd,PrimedRealAssignmentMap res,EventKind knd){return ha.new_transition(s,e,t,to_list(res),grd,knd);}); hybrid_automaton_class.def("__str__ ", &__cstr__<HybridAutomaton>);
hybrid_automaton_class.def("__repr__", &__crepr__<HybridAutomaton>);

hybrid_automaton_class.def("discrete_reachability",&HybridAutomaton::discrete_reachability);
hybrid_automaton_class.def("check_reachable_modes",&HybridAutomaton::check_reachable_modes);

pybind11::class_<CompositeHybridAutomaton,pybind11::bases<HybridAutomatonInterface>>
composite_hybrid_automaton_class(module,"CompositeHybridAutomaton");
composite_hybrid_automaton_class.def(pybind11::init<const List<HybridAutomaton>&>());
composite_hybrid_automaton_class.def(pybind11::init<Identifier,const List<HybridAutomaton>&>());
composite_hybrid_automaton_class.def("discrete_reachability",&CompositeHybridAutomaton::discrete_reachability);
composite_hybrid_automaton_class.def("check_reachable_modes",&CompositeHybridAutomaton::check_reachable_modes);
composite_hybrid_automaton_class.def("__str__", &__cstr__<CompositeHybridAutomaton>);
composite_hybrid_automaton_class.def("__repr__", &__crepr__<CompositeHybridAutomaton>);
composite_hybrid_automaton_class.def("__iter__", [](CompositeHybridAutomaton const& c){return pybind11::make_iterator(c.begin(),c.end());});
Expand Down
78 changes: 42 additions & 36 deletions source/hybrid/hybrid_automaton-composite.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -632,44 +632,39 @@ CompositeHybridAutomaton::check_mode(DiscreteLocation location) const {
List<RealVariable> location_variables=catenate(state_variables,auxiliary_variables);

if(!unique(location_variables)) {
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(OverspecifiedDynamicError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<duplicates(location_variables)<<" in location "<<location<<" with defining equations "<<equations<<" and "<<dynamics<<" have more than one defining equation.");
}

Set<RealVariable> result_variables=make_set(location_variables);

Set<RealVariable> undefined_variables=difference(real_arguments(equations),result_variables);
if(!undefined_variables.empty()) {
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(UnderspecifiedDynamicError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the definition of the algebraic equations "<<equations<<" in location "<<location<<" with state variables "<<state_variables<<", but are not defined.");
}

undefined_variables=difference(real_arguments(dynamics),result_variables);
if(!undefined_variables.empty()) {
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(UnderspecifiedDynamicError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the definition of the differential equations "<<dynamics<<" in location "<<location<<" with state variables "<<state_variables<<", but are not defined.");
}

List<RealAssignment> ordered_equations=Ariadne::order(equations,make_set(state_variables));

Set<DiscreteEvent> events=this->events(location);

/*
Map<DiscreteEvent,ContinuousPredicate> const& invariants=this->invariant_predicates(location);
for(Map<DiscreteEvent,ContinuousPredicate>::ConstIterator invariant_iter=invariants.begin();
invariant_iter!=invariants.end(); ++invariant_iter)
{
DiscreteEvent action=invariant_iter->first;
const ContinuousPredicate& invariant=invariant_iter->second;
for(Set<DiscreteEvent>::Iterator event_iter=events.begin(); event_iter!=events.end(); ++event_iter) {
DiscreteEvent event=*event_iter;
const ContinuousPredicate& invariant=this->invariant_predicate(location,event);
if(!subset(real_arguments(invariant),result_variables)) {
undefined_variables=difference(real_arguments(invariant),result_variables);
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the invariant "<<invariant<<" with label \""<<action<<"\" in location "<<location<<" with variables "<<location_variables<<", but are not defined.");
ARIADNE_THROW(UnderspecifiedConstraintError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the invariant "<<invariant<<" with label \""<<events<<"\" in location "<<location<<" with variables "<<location_variables<<", but are not defined.");
}
}

Set<DiscreteEvent> events=this->events(location);
for(Set<DiscreteEvent>::ConstIterator event_iter=events.begin(); event_iter!=events.end(); ++event_iter) {
// Get transition information
DiscreteEvent event=*event_iter;
DiscreteLocation target=this->target(location,event);
Expand All @@ -679,23 +674,51 @@ CompositeHybridAutomaton::check_mode(DiscreteLocation location) const {
Set<RealVariable> target_state_variables=make_set(this->state_variables(target));
List<RealVariable> reset_variables=base(assigned(reset));

// Check kind of transitions of guard
Set<Identifier> urgent_in;
Set<Identifier> permissive_in;
for(List<HybridAutomaton>::ConstIterator component_iter=this->_components.begin();
component_iter!=this->_components.end(); ++component_iter)
{
HybridAutomaton const& component = *component_iter;
if(component.has_guard(location,event)) {
EventKind kind=component.event_kind(location,event);
if (kind == EventKind::URGENT or kind == EventKind::IMPACT) {
urgent_in.insert(component.name());
} else {
ContinuousPredicate local_guard=component.guard_predicate(location,event);
if(!is_constant(local_guard,true)) {
permissive_in.insert(component.name());
}
}
}
}
if (urgent_in.size()>1) {
ARIADNE_THROW(MultipleUrgentDeclarationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Event "<<event<<" in location "<<location<<" is declared URGENT or IMPACT by multiple components "<<urgent_in<<".");
}
if (urgent_in.size()==1 && permissive_in.size()>0) {
ARIADNE_THROW(UrgentDeclarationWithMultipleGuardsException,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Event "<<event<<" in location "<<location<<" is declared URGENT or IMPACT by component "<<*urgent_in.begin()<<", but also has a nontrivial guard in components "<<permissive_in<<"; an urgent event may only have a guard declared in the restricting component.")
}

// Check arguments of guard
if(!subset(real_arguments(guard),result_variables)) {
undefined_variables=difference(real_arguments(guard),result_variables);
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(UnderspecifiedConstraintError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the guard "<<guard<<" for event \""<<event<<"\" in location "<<location<<" with variables "<<location_variables<<", but are not defined.");
}

// Check arguments of reset
if(!subset(real_arguments(reset),result_variables)) {
undefined_variables=difference(real_arguments(reset),result_variables);
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(UnderspecifiedResetError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are used in the reset "<<reset<<" for event \""<<event<<"\" in location "<<location<<" with variables "<<location_variables<<", but are not defined.");
}

// Check duplication of reset
if(!unique(reset_variables)) {
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(OverspecifiedResetError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<duplicates(reset_variables)<<" have more than one defining equation in resets "<<reset<<" for event \""<<event<<"\" in location "<<location<<".");
}

Expand All @@ -709,22 +732,13 @@ CompositeHybridAutomaton::check_mode(DiscreteLocation location) const {

if(!subset(target_state_variables,updated_variables)) {
undefined_variables=difference(target_state_variables,updated_variables);
ARIADNE_THROW(SystemSpecificationError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
ARIADNE_THROW(UnderspecifiedResetError,"CompositeHybridAutomaton::check_mode(DiscreteLocation)",
"Variables "<<undefined_variables<<" are state variables in location "<<target<<", but are not defined in the reset "<<reset<<" for the transition \""<<event<<"\" from location "<<location<<".");
}

} // Finished checking transitions
*/
return;
}


Void
CompositeHybridAutomaton::check_reachable_modes(DiscreteLocation initial_location) const
{
Set<DiscreteLocation> initial_locations;
initial_locations.insert(initial_location);
this->check_reachable_modes(initial_locations);
return;
}


Expand All @@ -737,14 +751,6 @@ CompositeHybridAutomaton::check_reachable_modes(const Set<DiscreteLocation>& ini
}
}

Set<DiscreteLocation>
CompositeHybridAutomaton::discrete_reachability(DiscreteLocation initial_location) const
{
Set<DiscreteLocation> initial_locations;
initial_locations.insert(initial_location);
return this->discrete_reachability(initial_locations);
}

Set<DiscreteLocation>
CompositeHybridAutomaton::discrete_reachability(const Set<DiscreteLocation>& initial_locations) const
{
Expand Down
4 changes: 0 additions & 4 deletions source/hybrid/hybrid_automaton-composite.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -216,17 +216,13 @@ class CompositeHybridAutomaton
//! Includes a check for algebraic dependencies, over-defined variables, under-defined variables, and
//! variables which should be defined in a reset but are not.
Void check_mode(DiscreteLocation) const;
//! \brief Runs check_mode() in any mode reachable under the discrete dynamics from the given initial location.
Void check_reachable_modes(DiscreteLocation) const;
//! \brief Runs check_mode() in any mode reachable under the discrete dynamics from the given initial locations.
Void check_reachable_modes(const Set<DiscreteLocation>&) const;
//!@}

//!@{
//! \name Discrete reachability analysis.

//! \brief Performs a discrete reachability analysis from the given initial location.
Set<DiscreteLocation> discrete_reachability(DiscreteLocation) const;
//! \brief Performs a discrete reachability analysis from the given initial locations.
Set<DiscreteLocation> discrete_reachability(const Set<DiscreteLocation>&) const;
//!@}
Expand Down
66 changes: 63 additions & 3 deletions source/hybrid/hybrid_automaton.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,7 @@ HybridAutomaton::_new_mode(DiscreteLocation location,
for(SizeType i=0; i!=dynamic.size(); ++i) {
if(defined_variables.contains(dynamic[i].lhs.base())) {
ARIADNE_THROW(SystemSpecificationError,"HybridAutomaton::new_mode",
"Variable "<<dynamic[i].lhs.base()<<" is defined by the differential equations "<<dynamic<<" for mode "<<location<<" is already defined");
"Variable "<<dynamic[i].lhs.base()<<" defined by the differential equations "<<dynamic<<" for mode "<<location<<" is also defined in the algebraic equations "<<auxiliary);
}
defined_variables.insert(dynamic[i].lhs.base());
argument_variables.adjoin(dynamic[i].rhs.arguments());
Expand Down Expand Up @@ -437,7 +437,23 @@ HybridAutomaton::_new_update(DiscreteLocation source,
}



Void
HybridAutomaton::_new_transition(DiscreteLocation source,
DiscreteEvent event,
DiscreteLocation target,
List<PrimedRealAssignment> const& reset,
ContinuousPredicate guard,
EventKind kind)
{
if(kind==EventKind::URGENT || kind==EventKind::IMPACT) {
this->_new_action(source,!guard,event,guard,kind);
} else if(kind==EventKind::PERMISSIVE) {
this->_new_guard(source,event,guard,kind);
} else {
ARIADNE_FAIL_MSG("Unhandled event kind "<<kind);
}
this->_new_update(source,event,target,reset);
}


Set<DiscreteLocation>
Expand Down Expand Up @@ -497,7 +513,7 @@ HybridAutomaton::has_invariant(DiscreteLocation source, DiscreteEvent event) con
Bool
HybridAutomaton::has_guard(DiscreteLocation source, DiscreteEvent event) const
{
return this->has_invariant(source,event) || this->has_transition(source,event);
return this->has_partial_mode(source) && this->mode(source)._guards.has_key(event);
}


Expand Down Expand Up @@ -835,5 +851,49 @@ Void HybridAutomaton::check_mode(DiscreteLocation location) const {
}


Void HybridAutomaton::check_reachable_modes(const Set<DiscreteLocation>& initial_locations) const {
Set<DiscreteLocation> reachable_locations=this->discrete_reachability(initial_locations);
for(Set<DiscreteLocation>::ConstIterator iter=reachable_locations.begin(); iter!=reachable_locations.end(); ++iter) {
this->check_mode(*iter);
}
}

Set<DiscreteLocation> HybridAutomaton::discrete_reachability(const Set<DiscreteLocation>& initial_locations) const {
const HybridAutomaton& automaton=*this;

Set<DiscreteLocation> reached=initial_locations;
Set<DiscreteLocation> working=initial_locations;
Set<DiscreteLocation> found;

Map<DiscreteLocation,Natural> steps;
Natural step=0u;

for(Set<DiscreteLocation>::ConstIterator initial_iter=initial_locations.begin(); initial_iter!=initial_locations.end(); ++initial_iter) {
steps.insert(*initial_iter,step);
}

while(!working.empty()) {
++step;
for(Set<DiscreteLocation>::ConstIterator source_iter=working.begin(); source_iter!=working.end(); ++source_iter) {
DiscreteLocation location=*source_iter;
Set<DiscreteEvent> events=automaton.events(location);
for(Set<DiscreteEvent>::ConstIterator event_iter=events.begin(); event_iter!=events.end(); ++event_iter) {
DiscreteEvent event=*event_iter;
DiscreteLocation target=automaton.target(location,event);
if(!reached.contains(target)) {
found.insert(target);
reached.insert(target);
steps.insert(target,step);
}
}

}
working.clear();
working.swap(found);
}

return reached;
}


} // namespace Ariadne
Loading

0 comments on commit 3d2233c

Please sign in to comment.