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, \to, s_0)$, where:

• $S$ is the set of states,
• $A$ is the set of actions,
• $\to\subseteq S\times A\times S$ is the transition relation,
• $s_0$ is the initial state.

For an Alvis model we have:

• $S = \mathcal{R}(S_0)$,
• $A = T$ - the set of all possible steps for a given model,
• $E = \{(S, t, S')\colon S-t\to S' \wedge S,S' \in \mathcal{R}(S_0)\}$
• $S_0$ is the initial state.

agent A {
  loop {    -- 1
    out a;  -- 2
  }
}

agent B {
  loop {    -- 1
    in b;   -- 2
  }
}

agent A, C {
  x :: Int = 5;
  out q x;       -- 1
}

agent B {
  x :: Int = 0;
  proc p1 { 
    in p1 x;     -- 1
    exit;        -- 2
  }
  proc p2 { 
    in p2 x;     -- 3
    exit;        -- 4
  }
}

Go back