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.
130 lines
5.0 KiB
130 lines
5.0 KiB
// model of randomised consensus
|
|
|
|
mdp
|
|
|
|
const int N = 3; // num processes
|
|
const int MAX = 4; // num rounds (R)
|
|
|
|
// need to turn these into local copies later so the reading phase is complete?
|
|
formula leaders_agree1 = (p1=1 | r1<max(r1,r2,r3)) & (p2=1 | r2<max(r1,r2,r3)) & (p3=1 | r3<max(r1,r2,r3));
|
|
formula leaders_agree2 = (p1=2 | r1<max(r1,r2,r3)) & (p2=2 | r2<max(r1,r2,r3)) & (p3=2 | r3<max(r1,r2,r3));
|
|
|
|
formula decide1 = leaders_agree1 & (p1=1 | r1<max(r1,r2,r3)-1) & (p2=1 | r2<max(r1,r2,r3)-1) & (p3=1 | r3<max(r1,r2,r3)-1);
|
|
formula decide2 = leaders_agree2 & (p1=2 | r1<max(r1,r2,r3)-1) & (p2=2 | r2<max(r1,r2,r3)-1) & (p3=2 | r3<max(r1,r2,r3)-1);
|
|
|
|
module process1
|
|
|
|
s1 : [0..5]; // local state
|
|
// 0 initialise/read registers
|
|
// 1 finish reading registers (make a decision)
|
|
// 1 warn of change
|
|
// 2 enter shared coin protocol
|
|
// 4 finished
|
|
// 5 error (reached max round and cannot decide)
|
|
r1 : [0..MAX]; // round of the process
|
|
p1 : [0..2]; // preference (0 corresponds to null)
|
|
|
|
// nondeterministic choice as to initial preference
|
|
[] s1=0 & r1=0 -> (p1'=1) & (r1'=1);
|
|
[] s1=0 & r1=0 -> (p1'=2) & (r1'=1);
|
|
|
|
// read registers (currently does nothing because read vs from other processes
|
|
[] s1=0 & r1>0 & r1<=MAX -> (s1'=1);
|
|
// maxke a decision
|
|
[] s1=1 & decide1 -> (s1'=4) & (p1'=1);
|
|
[] s1=1 & decide2 -> (s1'=4) & (p1'=2);
|
|
[] s1=1 & r1<MAX & leaders_agree1 & !decide1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
|
|
[] s1=1 & r1<MAX & leaders_agree2 & !decide2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
|
|
[] s1=1 & r1<MAX & !(leaders_agree1 | leaders_agree2) -> (s1'=2) & (p1'=0);
|
|
[] s1=1 & r1=MAX & !(decide1 | decide2) -> (s1'=5); // run out of rounds so error
|
|
// enter the coin procotol for the current round
|
|
[coin1_s1_start] s1=2 & r1=1 -> (s1'=3);
|
|
[coin2_s1_start] s1=2 & r1=2 -> (s1'=3);
|
|
[coin3_s1_start] s1=2 & r1=3 -> (s1'=3);
|
|
// get response from the coin protocol
|
|
[coin1_s1_p1] s1=3 & r1=1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
|
|
[coin1_s1_p2] s1=3 & r1=1 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
|
|
[coin2_s1_p1] s1=3 & r1=2 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
|
|
[coin2_s1_p2] s1=3 & r1=2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
|
|
[coin3_s1_p1] s1=3 & r1=3 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
|
|
[coin3_s1_p2] s1=3 & r1=3 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
|
|
// done so loop
|
|
[done] s1>=4 -> true;
|
|
|
|
endmodule
|
|
|
|
module process2 = process1[ s1=s2,
|
|
p1=p2,p2=p3,p3=p1,
|
|
r1=r2,r2=r3,r3=r1,
|
|
coin1_s1_start=coin1_s2_start,coin2_s1_start=coin2_s2_start,coin3_s1_start=coin3_s2_start,
|
|
coin1_s1_p1=coin1_s2_p1,coin2_s1_p1=coin2_s2_p1,coin3_s1_p1=coin3_s2_p1,
|
|
coin1_s1_p2=coin1_s2_p2,coin2_s1_p2=coin2_s2_p2,coin3_s1_p2=coin3_s2_p2 ]
|
|
endmodule
|
|
|
|
module process3 = process1[ s1=s3,
|
|
p1=p3,p2=p1,p3=p2,
|
|
r1=r3,r2=r1,r3=r2,
|
|
coin1_s1_start=coin1_s3_start,coin2_s1_start=coin2_s3_start,coin3_s1_start=coin3_s3_start,
|
|
coin1_s1_p1=coin1_s3_p1,coin2_s1_p1=coin2_s3_p1,coin3_s1_p1=coin3_s3_p1,
|
|
coin1_s1_p2=coin1_s3_p2,coin2_s1_p2=coin2_s3_p2,coin3_s1_p2=coin3_s3_p2 ]
|
|
endmodule
|
|
|
|
module coin1_error
|
|
|
|
c1 : [0..1]; // 1 is the error state
|
|
v1 : [0..2]; // value of the coin returned the first time
|
|
|
|
// first returned value (any processes)
|
|
[coin1_s1_p1] v1=0 -> (v1'=1);
|
|
[coin1_s2_p1] v1=0 -> (v1'=1);
|
|
[coin1_s3_p1] v1=0 -> (v1'=1);
|
|
[coin1_s1_p2] v1=0 -> (v1'=2);
|
|
[coin1_s2_p2] v1=0 -> (v1'=2);
|
|
[coin1_s3_p2] v1=0 -> (v1'=2);
|
|
// later values returned
|
|
[coin1_s1_p1] v1=1 -> true; // good behaviour
|
|
[coin1_s2_p1] v1=1 -> true; // good behaviour
|
|
[coin1_s3_p1] v1=1 -> true; // good behaviour
|
|
[coin1_s1_p2] v1=2 -> true; // good behaviour
|
|
[coin1_s2_p2] v1=2 -> true; // good behaviour
|
|
[coin1_s3_p2] v1=2 -> true; // good behaviour
|
|
[coin1_s1_p1] v1=2 -> (c1'=1); // error
|
|
[coin1_s2_p1] v1=2 -> (c1'=1); // error
|
|
[coin1_s3_p1] v1=2 -> (c1'=1); // error
|
|
[coin1_s1_p2] v1=1 -> (c1'=1); // error
|
|
[coin1_s2_p2] v1=1 -> (c1'=1); // error
|
|
[coin1_s3_p2] v1=1 -> (c1'=1); // error
|
|
|
|
endmodule
|
|
|
|
module coin2_error
|
|
|
|
c2 : [0..1]; // 1 is the error state
|
|
v2 : [0..2]; // value of the coin returned the first time
|
|
|
|
// first returned value (any processes)
|
|
[coin2_s1_p1] v2=0 -> (v2'=1);
|
|
[coin2_s2_p1] v2=0 -> (v2'=1);
|
|
[coin2_s3_p1] v2=0 -> (v2'=1);
|
|
[coin2_s1_p2] v2=0 -> (v2'=2);
|
|
[coin2_s2_p2] v2=0 -> (v2'=2);
|
|
[coin2_s3_p2] v2=0 -> (v2'=2);
|
|
// later values returned
|
|
[coin2_s1_p1] v2=1 -> true; // good behaviour
|
|
[coin2_s2_p1] v2=1 -> true; // good behaviour
|
|
[coin2_s3_p1] v2=1 -> true; // good behaviour
|
|
[coin2_s1_p2] v2=2 -> true; // good behaviour
|
|
[coin2_s2_p2] v2=2 -> true; // good behaviour
|
|
[coin2_s3_p2] v2=2 -> true; // good behaviour
|
|
[coin2_s1_p1] v2=2 -> (c2'=1); // error
|
|
[coin2_s2_p1] v2=2 -> (c2'=1); // error
|
|
[coin2_s3_p1] v2=2 -> (c2'=1); // error
|
|
[coin2_s1_p2] v2=1 -> (c2'=1); // error
|
|
[coin2_s2_p2] v2=1 -> (c2'=1); // error
|
|
[coin2_s3_p2] v2=1 -> (c2'=1); // error
|
|
|
|
endmodule
|
|
|
|
// Labels
|
|
label "one_proc_err" = (s1=5 | s2=5 | s3=5);
|
|
label "one_coin_ok" = (c1=0 | c2=0);
|