Description
An event may only be declared URGENT or IMPACT by one component in any context. This should be checked by the check_reachable_nodes(...) method of CompositeHybridAutomaton.
Further, if an event is urgent in one component with guard g1(x)>=0, and permissive in another with guard g2(x)>=0, then compositionality requires that the event occurs as soon as g1(x)>=0 in the composed system. If at this state, g2(x)<0, then the system deadlocks. The user probably wants that the event in the composed system is urgent with guard g1(x)>=0 /\ g2(x)>=0, but we cannot allow this in the semantics. For this reason, we should probably also raise an exception in when checking a composed system. The user should define the entire constraint g1(x)>=0 && g2(x)>=0 in a single automaton.