Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
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→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 S1,…,Sk+1 and a sequence of steps t1,…,tk such that S=S1−t1→S2−t2→⋯−tk→Sk+1=S′. | ||
- | |||
- | The set of all states that are reachable from the initial state S0 is denoted by R(S0). | ||
- | |||
- | **Definition 3.** A **Labelled Transition System** is a tuple LTS=(S,A,→,s0), where: | ||
- | * S is the set of **states**, | ||
- | * A is the set of **actions**, | ||
- | * →⊆S×A×S is the **transition relation**, | ||
- | * s0 is the **initial state**. | ||
- | |||
- | For an Alvis model we have: | ||
- | * S=R(S0), | ||
- | * A=T - the set of all possible steps for a given model, | ||
- | * E={(S,t,S′):S−t→S′∧S,S′∈R(S0)} | ||
- | * S0 is the initial state. | ||
- | |||
- | ===== Example 1 ===== | ||
- | |||
- | {{ : | ||
- | |||
- | < | ||
- | agent A { | ||
- | loop { -- 1 | ||
- | out a; -- 2 | ||
- | } | ||
- | } | ||
- | |||
- | agent B { | ||
- | loop { -- 1 | ||
- | in b; -- 2 | ||
- | } | ||
- | } | ||
- | </ | ||
- | |||
- | {{ : | ||
- | |||
- | ===== Example 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 | ||
- | } | ||
- | } | ||
- | </ | ||
- | |||
- | {{ : | ||
- | **[[: |