// The Dining Philosophers Problem allowing randomized actions. constant N := 3; variable hungry[Nat % N] <- Nat % 2; variable chopstick[Nat % (2*N)] <- Nat % 2; puppet variable b[Nat % N] <- Nat % 2; // These are more intuitively defined within P[i]. // (future & future silent) ...; // (assume & closed) ...; process P[i <- Nat % 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; predicate Avail_L := chopstick[L]==0 && chopstick[L-1]==0; predicate Avail_R := chopstick[R]==0 && chopstick[R+1]==0; // Converge to a state where no philosopher is hungry or has a chopstick. (future & future silent) (hungry[i]==0 && chopstick[L]==0 && chopstick[R]==0); // Assume two philosophers can't have the same chopstick. (assume & closed) (chopstick[L]==0 || chopstick[L-1]==0); (assume & closed) (chopstick[R]==0 || chopstick[R+1]==0); // See examplespec/DiningPhiloRand.prot for explanation. permit: ( true --> hungry[i]; ) ( Have2 -=> hungry[i]:=0; _; ) ; forbid: ( true --> chopstick[L]:=1-chopstick[L]; chopstick[R]:=1-chopstick[R]; ) ; // Unlike the {permit} and {forbid} actions, variables that are not assigned // in {puppet} actions are assumed to not change. puppet: // Use randomization to choose when nobody has a chopstick. // Note that this is the only place where the random {b[i]} value is used. ( hungry[i]==1 && Avail_L && Avail_R && b[i]==0 -=> chopstick[L]:=1; ) ( hungry[i]==1 && Avail_L && Avail_R && b[i]==1 -=> chopstick[R]:=1; ) // With one chopstick in hand, pick up a second one if it is available. ( hungry[i]==1 && chopstick[R]==1 && Avail_L -=> chopstick[L]:=1; ) ( hungry[i]==1 && chopstick[L]==1 && Avail_R -=> chopstick[R]:=1; ) // If the second chopstick is not available, put down the first one. // Note that {-=>} allows us to assume we have a chopstick to put down. ( hungry[i]==1 && chopstick[R+1]==1 -=> chopstick[L]:=0; ) ( hungry[i]==1 && chopstick[L-1]==1 -=> chopstick[R]:=0; ) // Eat. // Note that {-=>} allows us to assume we begin hungry. ( Have2 -=> hungry[i]:=0; ) // Put down chopsticks. First left, then right. The order doesn't actually // matter, but a version allowing both orders would not be synthesized. // Note that {-=>} allows us to assume we have a chopstick to put down. ( hungry[i]==0 -=> chopstick[L]:=0; ) ( hungry[i]==0 && chopstick[L]==0 -=> chopstick[R]:=0; ) ; }