Creating an invalid initial location is not caught

[ariadne-cps]

Creating an invalid initial location is not caught

[lgeretti]

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)

---

Why can't we postpone the correctness of the definition of the automaton/system to an evaluation phase before evolution? Moreover, I think we may want to be able to overspecify behavior and possibly give a warning, if (let's say) we want to analyse the component in isolation. I'm looking at a way to provide one and only one way to define a component (and then a system), and I am willing to accept some degrees of freedom.

[lgeretti]

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)

---

There's a problem with different use-cases here. When we get a mode corresponding to a DiscreteLocation for a complete hybrid automaton (e.g. when computing system evolution), then we should not specify variables which are not used, so your example should throw an exception (or at least give a warning, since in principle we can compute the evolution). However, if the hybrid automaton is intended as a component of a larger system, then it's convenient to be able to overspecify the discrete variables, especially for inspecting the system.

I've made some initial changes: I've changed automaton.has_mode(location) to only return true if the discrete variables match exactly, and automaton.has_partial_mode(location) to return true also if location overspecifies variables in a mode. However, automaton.mode(location) works if location is overspecified, but does return only the defined discrete variables. I could then change the evolver classes to throw if the mode is overspecified.

See master-automaton for the current changes.

[lgeretti]

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)

---

If we have three automata, we compose two of them as the system under evolution, and use an initial set with locations from all three, no issue arises.

Concept example:

#!c++

AtomicHybridAutomaton first = getFirstAutomaton();
AtomicHybridAutomaton second = getSecondAutomaton();

CompositeHybridAutomaton composition({first,second});
DiscreteLocation initial_location={first|work,second|run,third|play};

A have a rather complex compositional surgery system in my macos_support branch right now, if you want to check it.

[lgeretti]

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)

---

Please could you give an example!