protocon/examplesoln/TokenRingFiveState.prot at trunk · ProtocolConvergence/protocon · 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
46
47
48
49
50
51
52

// Token-passing around a unidirectional ring
// using 5 states per process

constant N := 3;

variable x[N] < 5;

// There exists one token in the ring.
(future & shadow)
  (unique i < N :
   i==0
   &&
   (false
    || x[i-1]> 1 && x[i]> 1
    || x[i-1]<=1 && x[i]==0
    || x[i-1]==1 && x[i]==1
   )
   ||
   i!=0
   &&
   (false
    || x[i-1]==0 && x[i]> 1
    || x[i-1]==1 && x[i]!=1
    || x[i-1]>=2 && x[i]<=1
   )
  );

process Bot[i < 1]
{
  read:  x[i-1];
  write: x[i];

  direct action:
    ( x[i-1]==0 && x[i]==0 --> x[i]:=1; )
    ( x[i-1]==1 && x[i]<=1 --> x[i]:=2; )
    ( x[i-1]> 1 && x[i]> 1 --> x[i]:=0; )
    ;
}

process P[i <- map tid < N-1 : tid+1]
{
  read:  x[i-1];
  write: x[i];

  direct action:
    ( x[i-1]==0 && x[i]> 1 --> x[i]:=x[i]/4; )
    ( x[i-1]==1 && x[i]!=1 --> x[i]:=1; )
    ( x[i-1]==2 && x[i]<=1 --> x[i]:=2+x[i]; )
    ( x[i-1]>=3 && x[i]<=1 --> x[i]:=4; )
    ;
}