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.
88 lines
3.1 KiB
88 lines
3.1 KiB
// model of randomised consensus
|
|
|
|
mdp
|
|
|
|
const int N = 2; // num processes
|
|
const int MAX = 3; // num rounds (R)
|
|
const int K = 2; // Parameter for coins
|
|
|
|
// need to turn these into local copies later so the reading phase is complete?
|
|
formula leaders_agree1 = (p1=1 | r1<max(r1,r2)) & (p2=1 | r2<max(r1,r2));
|
|
formula leaders_agree2 = (p1=2 | r1<max(r1,r2)) & (p2=2 | r2<max(r1,r2));
|
|
|
|
formula decide1 = leaders_agree1 & (p1=1 | r1<max(r1,r2)-1) & (p2=1 | r2<max(r1,r2)-1);
|
|
formula decide2 = leaders_agree2 & (p1=2 | r1<max(r1,r2)-1) & (p2=2 | r2<max(r1,r2)-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);
|
|
// 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);
|
|
// done so loop
|
|
[done] s1>=4 -> true;
|
|
|
|
endmodule
|
|
|
|
module process2 = process1[ s1=s2,
|
|
p1=p2,p2=p1,
|
|
r1=r2,r2=r1,
|
|
coin1_s1_start=coin1_s2_start,coin2_s1_start=coin2_s2_start,
|
|
coin1_s1_p1=coin1_s2_p1,coin2_s1_p1=coin2_s2_p1,
|
|
coin1_s1_p2=coin1_s2_p2,coin2_s1_p2=coin2_s2_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_s1_p2] v1=0 -> (v1'=2);
|
|
[coin1_s2_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_s1_p2] v1=2 -> true; // good behaviour
|
|
[coin1_s2_p2] v1=2 -> true; // good behaviour
|
|
[coin1_s1_p1] v1=2 -> (c1'=1); // error
|
|
[coin1_s2_p1] v1=2 -> (c1'=1); // error
|
|
[coin1_s1_p2] v1=1 -> (c1'=1); // error
|
|
[coin1_s2_p2] v1=1 -> (c1'=1); // error
|
|
|
|
endmodule
|
|
|
|
// coins 2 and 3 are of no use as there are not enough rounds afterwards to decide
|
|
|
|
// Labels
|
|
label "one_proc_err" = (s1=5 | s2=5);
|
|
label "one_coin_ok" = (c1=0);
|