/**
Modelled by Marius Mikucionis <marius@cs.aau.dk>
Some consider this to be a good model-checker benchmark...
Dining Cryptographers (from http://cryptodox.com/Dining_cryptographers_protocol)
An odd numbered group of cryptographers is enjoying dinner at a local restaurant.
Upon requesting their bill, the cryptographers are surprised to learn from their
host that payment for the dinner has already been anonymously arranged and that
the group owes nothing. They speculate that the payer might be one of
the cryptographers in the party, but then they realize that the dinner may have
been paid for by the National Security Agency, their employer. Though everybody
at the table respects each other's right to make an anonymous payment, they still
wish to know whether their meal was in fact funded by the NSA.
Problem: If it turns out that one of the cryptographers at the table is the payer,
how can he anonymously signal this fact to his peers?
Solution: Each cryptographer flips a coin privately with the member to his left
and right. Then they all stand up and annouce true if the two coins he can see
were different (head and tails) or false if the two coins were the same (head and
head). If one of the cyptographers is the payer, he states the opposite. If there
is an odd number of trues, then the NSA payed. If there is an even number, then
one of the cryptographers lied, and the check was payed by a member of the group.
Who actually payed is not revealed. If there were an even number of crytographers
the opposite would be the case; odd, a cryptographer payed, and even, the NSA payed.
*/
const int N=500; // number of cryptographers
typedef int[0, N-1] id_t; // type for cryptographer identifier
bool answer[id_t]; // first, store the coin value, and then reuse it for the answer
bool agencyPaid; // deduced answer whether the agency paid for the dinner.
chan pay; // only one process (cryptographer or agency) synchronizes here
// first we roll the coin, look at neightbor and announce the equality or inequality
broadcast chan roll, look, announce; // all cryptographers move at the same time
int sum() { // calculate the number of equalities (positive answers)
int s=0;
for(i: id_t) if (answer[i]) ++s;
return s;
}Cryptconst id_t idPaidModifyTrueToFalseModifyFalseToTrueEqualDifferentWaiterApproachdoneAnnounceEqualityLetThemLookAtNeighborRolledTheCoinGotPaidAgencyPaidNotPaidsystem Waiter, Agency, Crypt;