Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:ltsgraphs [2014/01/03 16:32]
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//->//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.
-===== Example =====
-{{:alvis:alvis1.png|}}
-<code>
-agent X1 {
-  loop {        -- 1
-    out p; }}   -- 2
-agent X2 {
-  loop {        -- 1
-    in q; }}    -- 2
-</code>
-{{:alvis:alvis1lts.png|}}
-**FIXME**
-**[[:alvis:manual|Go back]]**