protocon/examplespec/DiningPhilo.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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107

// The Dining Philosophers Problem.
// See DiningPhiloRand.prot for the simpler version that allows randomization.
// This version breaks symmetry by assuming a coloring.

constant N := 3;

variable hungry[N] < 2;
variable chopstick[(2*N)] < 2;
variable cgt[(2*N)] < 2;

// Converge to a state where no philosopher is hungry or has a chopstick.
(future & future silent)
  (forall i < N : true
   && hungry[i]==0
   && chopstick[2*i  ]==0
   && chopstick[2*i+1]==0
  );

// Assume two philosophers can't have the same chopstick.
(assume & closed)
  (forall i < N :
   chopstick[2*i+1]==0 || chopstick[2*i+2]==0
  );

// Assume a coloring.
// This allows there to be a symmetric solution.
// Values cgt[2*i] and cgt[2*i+1] denote whether P[i]'s color is greater
// than   P[i-1]   and P[i+1]     respectively.
(assume & closed)
  ((forall i < N : cgt[2*i+1]!=cgt[2*i+2])
   &&
   (exists i < N : cgt[2*i] == cgt[2*i+1])
  );


process P[i < N]
{
  let L := 2*i;
  let R := 2*i+1;


  // Whether the philosopher is hungry.
  write: hungry[i];

  read: chopstick[L-1];
  write: chopstick[L];
  write: chopstick[R];
  read: chopstick[R+1];

  // Whether neighbors are hungry.
  // These are not needed in asynchronous systems.
  read: hungry[i-1];
  read: hungry[i+1];

  // Whether this philosopher's color value is greater
  // than the color values of the left and right neighbors.
  // One of these can be omitted in an asynchronous system.
  read: cgt[L];
  read: cgt[R];


  predicate HasChopsticks :=
    (chopstick[L]==1 && chopstick[R]==1);

  predicate hungry_L := hungry[i-1]==1;
  predicate hungry_R := hungry[i+1]==1;


  // Permit actions where hungry status is not changed.
  // (But only those that are not also forbidden.)
  permit:
    ( true --> hungry[i]; )
    ;

  // Can only change to be not hungry when having chopsticks.
  // The chopsticks are not given up during this step.
  permit:
    ( HasChopsticks && hungry[i]==1 --> hungry[i]:=0; _; )
    ;

  // Forbid changing position of both chopsticks at the same time.
  forbid:
    ( true --> chopstick[L]:=1-chopstick[L]; chopstick[R]:=1-chopstick[R]; )
    ;

  // The following can be uncommented for efficiency.
  // First 2:
  //   If adjacent philosopher has a greater color value,
  //   then do not grab his/her chopstick!
  // First 2 + Last 2:
  //   If adjacent philosopher has a greater color value,
  //   then do not grab any chopstick!
  forbid:
    //( cgt[L]==0 && hungry_L && chopstick[L]==0 --> chopstick[L]:=1; )
    //( cgt[R]==0 && hungry_R && chopstick[R]==0 --> chopstick[R]:=1; )
    //( cgt[L]==0 && hungry_L && chopstick[R]==0 --> chopstick[R]:=1; )
    //( cgt[R]==0 && hungry_R && chopstick[L]==0 --> chopstick[L]:=1; )
    ;

  // The following can be uncommented for efficiency.
  // Don't grab a chopstick when not hungry!
  forbid:
    //( hungry[i]==0 && chopstick[L]==0 --> chopstick[L]:=1; )
    //( hungry[i]==0 && chopstick[R]==0 --> chopstick[R]:=1; )
    ;
}