protocon/examplesoln/TokenRingThreeState.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
53
54
55
56
57
58
59
60
61
62
63
64
65
66

// Token passing on a ring defined in
// Title: A Self-Stabilizing Algorithm with Tight Bounds for Mutual Exclusion on a Ring
// Author: Viacheslav Chernoy
// Author: Mordechai Shalom
// Author: Shmuel Zaks
// Year: 2008

constant N := 3;

variable z[N] < 3;

process Bot[i < 1]
{
  write: z[i];
  read:  z[i+1];
  direct action:
    ( (z[i]+1)%3 == z[i+1] --> z[i] := z[i]+2; )
    ;
}

process P[i <- map tid < N-2 : tid+1]
{
  read:  z[i-1];
  write: z[i];
  read:  z[i+1];
  direct action:
    (    ((z[i-1]-1)%3 == z[i+1] && z[i+1] == z[i])
      || ((z[i  ]+1)%3 == z[i-1] && z[i-1] == z[i+1])
      || ((z[i+1]-1)%3 == z[i-1] && z[i-1] == z[i])
     -->
      z[i] := z[i] + 1;
    )
    ;
}


process Top[i <- map tid < 1 : N-1]
{
  read: z[i-1];
  write: z[i];
  read: z[i+1];
  direct action:
    ( z[i-1] == z[i] && z[i] == z[i+1] || z[i-1] == (z[i]+1)%3 --> z[i] := z[i-1]+1; )
    ;
}

(future & shadow)
(
  (exists a < 3 :
   (forall i < N :
    z[i] != a))
  &&
  // One process has a token.
  (unique i < N :
   (   (i == 0 &&
        ((z[i]+1)%3 == z[i+1]))
    || (i != 0 && i != N-1 &&
        (   ((z[i-1]-1)%3 == z[i+1] && z[i+1] == z[i])
         || ((z[i  ]+1)%3 == z[i-1] && z[i-1] == z[i+1])
         || ((z[i+1]-1)%3 == z[i-1] && z[i-1] == z[i])))
    || (i == N-1 &&
        (z[i-1] == z[i] && z[i] == z[i+1] || z[i-1] == (z[i]+1)%3))
   )
  )
);