You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
48 lines
1.5 KiB
48 lines
1.5 KiB
#const N#
|
|
// model of dining cryptographers
|
|
// gxn/dxp 15/11/06
|
|
|
|
mdp
|
|
|
|
// constants used in renaming (identities of cryptographers)
|
|
#for i=1:N#
|
|
const int p#i# = #i#;
|
|
#end#
|
|
|
|
// global variable which decides who pays
|
|
// (0 - master pays, i=1..N - cryptographer i pays)
|
|
global pay : [0..#N#];
|
|
|
|
// module for first cryptographer
|
|
module crypt1
|
|
|
|
coin1 : [0..2]; // value of its coin
|
|
s1 : [0..1]; // its status (0 = not done, 1 = done)
|
|
agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
|
|
|
|
// flip coin
|
|
[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
|
|
|
|
// make statement (once relevant coins have been flipped)
|
|
// agree (coins the same and does not pay)
|
|
[] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1);
|
|
// disagree (coins different and does not pay)
|
|
[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
|
|
// disagree (coins the same and pays)
|
|
[] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1);
|
|
// agree (coins different and pays)
|
|
[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1);
|
|
|
|
// synchronising loop when finished to avoid deadlock
|
|
[done] s1=1 -> true;
|
|
|
|
endmodule
|
|
|
|
// construct further cryptographers with renaming
|
|
#for i=2:N#
|
|
module crypt#i# = crypt1 [ coin1=coin#i#, s1=s#i#, agree1=agree#i#, p1=p#i#, coin2=coin#func(mod,i,N)+1# ] endmodule
|
|
#end#
|
|
|
|
// set of initial states
|
|
// (cryptographers in their initial state, "pay" can be anything)
|
|
init #& i=1:N# coin#i#=0&s#i#=0&agree#i#=0 #end# endinit
|