Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- alvis:ltsgraphs [2015/12/12 23:52]
marcin [Example]
+++ — (current)
@@ Line 1: / Line 1: @@
-====== LTS graphs ======
-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.
-===== Example 1 =====
-{{ :alvis:t016.png?320 |}}
-<code>
-agent A {
-  loop {    -- 1
-    out a;  -- 2
-  }
-}
-agent B {
-  loop {    -- 1
-    in b;   -- 2
-  }
-}
-</code>
-{{ :alvis:t016lts.png?450 |}}
-===== Example 2 =====
-{{ :alvis:t012.png?320 |}}
-<code>
-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
-  }
-}
-</code>
-{{ :alvis:t012lts.png?450 |}}
-**[[:alvis:manual|Go back]]**