From 726324a37a5ff90d449e63e4b28af11fc4c48d05 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 12 Mar 2013 23:07:52 +0100 Subject: [PATCH] Added missing model files for consensus example. --- examples/mdp/consensus/coin2.nm | 60 +++++++++++++++++++++++++++++++ examples/mdp/consensus/coin4.nm | 62 ++++++++++++++++++++++++++++++++ examples/mdp/consensus/coin6.nm | 64 +++++++++++++++++++++++++++++++++ 3 files changed, 186 insertions(+) create mode 100644 examples/mdp/consensus/coin2.nm create mode 100644 examples/mdp/consensus/coin4.nm create mode 100644 examples/mdp/consensus/coin6.nm diff --git a/examples/mdp/consensus/coin2.nm b/examples/mdp/consensus/coin2.nm new file mode 100644 index 000000000..07ec59e17 --- /dev/null +++ b/examples/mdp/consensus/coin2.nm @@ -0,0 +1,60 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K; +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) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (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 (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 (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 ; +label "agree" = coin1=coin2 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/mdp/consensus/coin4.nm b/examples/mdp/consensus/coin4.nm new file mode 100644 index 000000000..8639b867b --- /dev/null +++ b/examples/mdp/consensus/coin4.nm @@ -0,0 +1,62 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=4; +const int K; +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) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (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 (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 (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; +label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/mdp/consensus/coin6.nm b/examples/mdp/consensus/coin6.nm new file mode 100644 index 000000000..b373c40d5 --- /dev/null +++ b/examples/mdp/consensus/coin6.nm @@ -0,0 +1,64 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=6; +const int K; +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) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (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 (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 (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4] endmodule +module process5 = process1[pc1=pc5,coin1=coin5] endmodule +module process6 = process1[pc1=pc6,coin1=coin6] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ; +label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ; + +// rewards +rewards "steps" + true : 1; +endrewards +