Functional properties

Basic sets

The most basic sets are:

• INIT the set of initial states
• DEAD the set of deadlock states
• HULL the convex hull of strongly connected components (globally to the state-space)
• ALL the set of all the reachable states

Then, for a specific component graph:

• Cn, where n is the number of a component, is the set of states of this component

Finally, for a specific RR model, name LTS is a presentation of the model itself with dedicated attributes and methods. In particular:

• LTS["act"], where act is the name if an action, is the set of states from which act can fire
• LTS["var+"], where var is the name of a variable, is the set of states where var is on
• similarly, LTS["var-"] is the set of states where var is off
• LTS["x+,y-"] is the set of states where variable x is on and y is off, and more generally any sequence of valuations can be provided

Functions and operations

The usual Python sets operations are supported: union |, intersection &, difference -, and symmetric difference ^. This is complemented with several functions:

• succ(s) is the set of all states reachable from s through a single transition
• pred(s) is the set of all states from which s can be reached through a single transition
• LTS.succ["act"](s) is the set of states that can be reached from s through one firing of action act
• LTS.pred["act"](s) is the set of states from which s can be reached through one firing of act
• past(s) is the set of states that allow to reach s, which includes s itself
• future(s) is the set of states that can be reached from s, which includes s itself
• basin(s) is the subset of past(s) from which it cannot be avoided to reach s, which include s itself. Note that any SCC in past(s) - s is not part of basin(s) because an infinite pathway that would stay in the SCC is a way to avoid reaching s
• hull(s) returns the convex hull of the SCCs included in s, which may be empty. Compared to HULL above, that is global to the state-space, this function performs a computation that is local to s
• scc(s) returns the strongly connected component including s, which may be s itself when s is actually not within an SCC
• entries(s) is the subset of s that can be reached through a single transition from its outside
• exits(s) is the subset of s from which the outside of s can be reached through a single transitions
• pick(s) returns one arbitrary state from s

Fixed point operations

Then, there are also fixed point operations. The least fixed point of a function \(f\) is obtained by applying repeatedly \(f \cup id\), where \(id\) is the identity, until a fixed point is reached. For instance, take succ for \(f\), consider the following state-space, and start from \(s = \{3\}\):

The fixed point is thus obtained after three applications of the function: \(\{3\} \mapsto \{3, 6\} \mapsto \{3, 6, 8\} \mapsto \{3, 6, 8, 5, 9\}\). Note how this least fixed point make its argument grow through the succ function. This fixed point function is available as succ_s, it can be intuitively understood as computing the set of states reachable from \(s\).

Similarly, function pred_s is available and computes the least fixed point of pred. Combined with succ_s it allows defining the function scc presented above as the intersection of succ_s and pred_s. On the example above, pred_s would build: \(\{3\} \mapsto \{3, 1, 5\} \mapsto \{3, 1, 5, 0, 8\} \mapsto \{3, 1, 5, 0, 8, 6\}\). Intersecting this final set with the one obtained from succ_s would indeed yield the SCC that contains state \(3\).

Similarly, the greatest fixed point of a function \(f\) is obtained by applying repeatedly \(f \cap id\) until a fixed point is reached. On the same example, we may start from \(s = \{0, 1, 2, 3, 4, 5, 6, 7, 8, 9\}\) and apply the greatest fixed point of succ:

The fixed point is obtained by two applications of the function: \(\{0, 1, 2, 3, 4, 5, 6, 7, 8, 9\} \mapsto \{1, 2, 3, 4, 5, 6, 7, 8, 9\} \mapsto \{3, 4, 5, 6, 7, 8, 9\}\), at each step, the states that are not reachable through succ are removed, which shrinks the set until all its states are reachable through succ from another one in the set. This fixed point is available as succ_o, as well as pred_o that is the greatest fixed point of pred. The intersection of them defines function hull: in the example above, pred_o would build \(\{0, 1, 2, 3, 4, 5, 6, 7, 8, 9\} \mapsto \{0, 1, 2, 3, 4, 5, 6, 7, 8\}\) which, intersected with the result of succ_o, would indeed yield the convex hull of the two SCCs present in this state-space.