Execution of any step is expressed as a transition between formally defined states of an Alvis model. States of a model and transitions among them are represented using a labelled transition system (LTS graph for short).

Definition 1. For a pair of states $S$, $S'$ we say that $S'$ is directly reachable from $S$ iff there exists a step $t$ such that $S-t\to S'$.

Definition 2. For a pair of states $S$, $S'$ we say that $S'$ is reachable from $S$ iff there exist a sequence of states $S^1,\dots,S^{k+1}$ and a sequence of steps $t^1,\dots,t^k$ such that $S = S^1 -t^1\to S^2 -t^2\to\dots -t^k\to S{^k+1} = S'$.

The set of all states that are reachable from the initial state $S_0$ is denoted by $\mathcal{R}(S_0)$.

Definition 3. A Labelled Transition System is a tuple LTS = (S, A, →, s_0), where:

• S is the set of states,
• A is the set of actions,
• → ⊆ S × A × S is the transition relation,
• s_0 is the initial state.

For an Alvis model we have:

• S = R(S_0),
• A = T - the set of all possible steps for a given model,
• E = {(S, t, S'): S–t→S' ∧ S, S' ∈ R(S_0)}
• S_0 is the initial state.

agent X1 {
  loop {        -- 1 
    out p; }}   -- 2

agent X2 {
  loop {        -- 1 
    in q; }}    -- 2

Go back