Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:ltsgraphs [2017/01/11 22:56]
marcin removed
+++ — (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 |}}
-**[[:alvis:manual|Go back]]**