pluscal/FairProcess.tla at master · belaban/pluscal · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
---------------------------- MODULE FairProcess ----------------------------
EXTENDS Naturals, Integers, FiniteSets, Bags, Sequences, TLC
CONSTANT ids

(*

--algorithm FairProcess {
  variable x=0;

  process(id=1) {
     p0:
     while(TRUE) {
        with(m \in ids) {
           x := m;
           print x;
        }
     }
  }
}

*)
\* BEGIN TRANSLATION
VARIABLE x

vars == << x >>

ProcSet == {1}

Init == (* Global variables *)
        /\ x = 0

id == \E m \in ids:
        /\ x' = m
        /\ PrintT(x')

Next == id

Spec == Init /\ [][Next]_vars

\* END TRANSLATION

=============================================================================
\* Modification History
\* Last modified Fri Mar 27 11:41:20 CET 2015 by bela
\* Created Fri Mar 27 11:29:52 CET 2015 by bela