Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:ltsgraphs [2015/12/12 23:38]
marcin [LTS graphs]
+++ — (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 =====
-{{:alvis:alvis1.png|}}
-<code>
-agent X1 {
-  loop {        -- 1
-    out p; }}   -- 2
-agent X2 {
-  loop {        -- 1
-    in q; }}    -- 2
-</code>
-{{:alvis:alvis1lts.png|}}
-**[[:alvis:manual|Go back]]**