Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Test for invalid urgent events #786

Merged
merged 1 commit into from
Oct 15, 2024
Merged

Test for invalid urgent events #786

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions python/source/hybrid_submodule.cpp
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading