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.
61 lines
1.6 KiB
61 lines
1.6 KiB
//Randomised Consensus Protocol
|
|
|
|
mdp
|
|
const double p1; // in [0.2 , 0.8]
|
|
const double p2; // in [0.2 , 0.8]
|
|
const double p3; // in [0.2 , 0.8]
|
|
const double p4; // in [0.2 , 0.8]
|
|
|
|
|
|
const int N=4;
|
|
const int K=2;
|
|
const int range = 2*(K+1)*N;
|
|
const int counter_init = (K+1)*N;
|
|
const int left = N;
|
|
const int right = 2*(K+1)*N - N;
|
|
|
|
// shared coin
|
|
global counter : [0..range] init counter_init;
|
|
|
|
module process1
|
|
|
|
// program counter
|
|
pc1 : [0..3];
|
|
// 0 - flip
|
|
// 1 - write
|
|
// 2 - check
|
|
// 3 - finished
|
|
|
|
// local coin
|
|
coin1 : [0..1];
|
|
|
|
// flip coin
|
|
[] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1);
|
|
// write tails -1 (reset coin to add regularity)
|
|
[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
|
|
// write heads +1 (reset coin to add regularity)
|
|
[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
|
|
// check
|
|
// decide tails
|
|
[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
|
|
// decide heads
|
|
[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
|
|
// flip again
|
|
[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
|
|
// loop (all loop together when done)
|
|
[done] (pc1=3) -> (pc1'=3);
|
|
|
|
endmodule
|
|
|
|
module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule
|
|
module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule
|
|
module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule
|
|
|
|
label "finished" = pc1=3 &pc2=3 &pc3=3 &pc4=3;
|
|
label "all_coins_equal_1" = coin1=1 &coin2=1 &coin3=1 &coin4=1 ;
|
|
rewards "steps"
|
|
true : 1;
|
|
endrewards
|
|
|
|
|
|
|