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→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,…,S^k+1 and a sequence of steps t^1,…,t^k such that S = S^1 –t^1→ S^2 –t^2→ … –t^k S^k+1 = S'.

The set of all states that are reachable from the initial state S_0 is denoted by 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