Component graphs are one of the main ways to understand the dynamics of a system. As such, it is important to understand what they show or not. A component graph is defined as a set of disjoint components, each being a subset of the reachable states. Components are linked by the transitions allowing to reach one from another. Which yields a graph. For instance, a transition \(C_1 \stackrel{a}{\longrightarrow} C_2\) means that some states of \(C_2\) can be reached from some states of \(C_1\) firing action \(a\). Let us insist on the word some. Most states of \(C_1\) may lead to other states of \(C_1\) thought potentially any action. But among the states of \(C_1\), some are exits and can lead out of \(C_1\). Similarly, some states of \(C_2\) are entries and may be reached from the outside of \(C_2\).
Traps
Component graphs are usually built by splitting the set of reachable states with respect to properties. Depending on the properties, we cannot guaranty that the paths exhibited in a component graph are all feasible. Indeed, a path \(C_1 \stackrel{a_1}{\longrightarrow} C_2 \stackrel{a_2}{\longrightarrow} C_3\) only means that some states of \(C_1\) lead to \(C_2\) and some states of \(C_2\) lead to \(C_3\). But it may occur that the entries of \(C_2\) reachable from \(C_1\) through \(a_1\) do not allow to reach the exits of \(C_2\) from which \(C_3\) can be reached through \(a_2\). In this case, we say that \(C_2\) has a trap: entering \(C_2\) through \(a_1\) from \(C_1\) is a trap because it does not guarantee that every exit can be reached, and thus the pas through this edge \(C_1 \stackrel{a_1}{\longrightarrow} C_2\) is misleading. More precisely, every edge \(t\) towards a component \(C\) defines the subset \(C_t \subseteq C\) of states reachable through \(t\). If \(C_t\) does not include all the exits of \(C\), then it is a trap.
ecco shows these traps in several ways:
- table
nodeshas a columntrapsthat lists the components from which a trap exists - table
edgeshas a columntrapthat is BooleanTruewhen an arc leads into a trap - when component graphs are displayed, components with traps are labelled with symbol ⬖ and trap-edges are drawn as dotted lines
ecco also provides method untrap() to split a component into its traps so they appear separated and leave no ambiguity
Macro-dynamics
A component graph is often regarded as a presentation of the main dynamics of a system, or its macro-dynamics. However, if some node as traps, this may be misleading as this macro-dynamics shows paths that cannot be realised. As long as no more that direct reachability from one component to another is considered, there is no problem: if a transition exists, reachability is guaranteed (in the “some-to-some” sense). But as soon as a sequence of transitions is considered, it cannot considered as a real dynamics if it goes through a trap-edge. More precisely, this path may exist but the component graph is not an evidence of this, and the path may not exist as well. Moreover, note that when a path enters a trap-component through a non-trap-edge, it is guaranteed that every exit is actually reachable and the trap has been avoided.
So, reading a component graphs requires care, and traps should be considered closely before to draw any conclusion about the macro-dynamics.
Sequences
One recurring question, is whether a sequence of properties is observable in a systems dynamics. Splitting the state space against these properties and searching the requested sequence in the component graph is okay as long as traps can be avoided.
A safer way to check a sequence of CTL properties \(P_1, P_2, \dots\) is to check whether \(P_1 \land EF(P_2)\) holds, because this property characterises the states when \(P_1\) holds and from which \(P_2\) is reachable. But this does not guarantees that the reached states where \(P_2\) holds can then allow to reach \(P_3\). To do so, we should check \(P_1 \land EF(P_2 \land EF (P_3))\).
In general, the full sequence may no hold, and it can be tedious to check which parts of such a sequence can be realised.
Moreover, this method works with CTL properties, but not with functional properties (at least it cannot be directly translated as there is no equivalent to \(EF\)).
ecco provides method search() to help in this analysis.
This is still rough around the edges but it shall be refined in the future.