protocon/examplespec/DiningPhiloRand.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

// The Dining Philosophers Problem allowing randomized actions.

constant N := 3;

variable hungry[N] < 2;
variable chopstick[(2*N)] < 2;
puppet variable b[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
  );


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];

  // Random value to influence decisions.
  random read: b[i];


  predicate Have2 := chopstick[L] + chopstick[R] == 2;


  // Permit actions where hungry status is not changed.
  // Listing {hungry[i]} after {-->} without an assignment ensures that it remains unchanged.
  // Not listing a variable or assigning it to a {_} value after {-->} means that
  // it can be changed arbitrarily as long as it does not violate any other constraints.
  permit:
    ( true --> hungry[i]; )
    //// Equivalent:
    //( true --> hungry[i]:=hungry[i]; )
    //( true --> hungry[i]:=hungry[i]; chopstick[L]:=_; chopstick[R]:=_; )
    ;

  // Forbid changing position of both chopsticks at the same time.
  // This constrains the above {permit} statement.
  forbid:
    ( true --> chopstick[L]:=1-chopstick[L]; chopstick[R]:=1-chopstick[R]; )
    ;

  // We need 2 chopsticks to eat and become not hungry.
  // Chopsticks cannot be put down during this action.
  // The {-=>} operator allows us to assume we begin hungry.
  // The {_} operator ensures the unassigned variables (the 2 chopsticks) are
  // left unchanged. The {-=>} operator protects random write variables from
  // being affected by the {_} operator.
  // ({b[i]} used to be a random write variable.)
  permit:
    ( Have2 -=> hungry[i]:=0; _; )
    //// Equivalent:
    //( Have2 -=> hungry[i]:=0; chopstick[L]; chopstick[R]; )
    //( Have2 && hungry[i]==1 --> hungry[i]:=0; chopstick[L]; chopstick[R]; )
    //( Have2 && hungry[i]==1 --> hungry[i]:=0; b[i]:=_; chopstick[L]; chopstick[R]; )
    //( Have2 && hungry[i]==1 --> hungry[i]:=0; b[i]:=_; _; )
    ;
}