From 5b49307eaff109645d8cd91a8d6bb4b500813717 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 7 Mar 2013 15:28:38 +0100 Subject: [PATCH] Added PRISM files for all of our examples. Added missing reward models. Added result files that indicate the results of PRISM on our examples. --- examples/dtmc/crowds/crowds.pctl | 3 + examples/dtmc/crowds/crowds.res | 19 +++ examples/dtmc/crowds/crowds10_5.pm | 80 +++++++++++++ examples/dtmc/crowds/crowds15_5.pm | 95 +++++++++++++++ examples/dtmc/crowds/crowds20_5.pm | 110 ++++++++++++++++++ examples/dtmc/crowds/crowds5_5.pm | 65 +++++++++++ examples/dtmc/die/die.pctl | 4 + examples/dtmc/die/die.pm | 31 +++++ examples/dtmc/die/die.res | 4 + examples/dtmc/synchronous_leader/leader.pctl | 3 + examples/dtmc/synchronous_leader/leader.res | 14 +++ examples/dtmc/synchronous_leader/leader3_5.pm | 85 ++++++++++++++ examples/dtmc/synchronous_leader/leader4_8.pm | 89 ++++++++++++++ examples/dtmc/synchronous_leader/leader5_8.pm | 90 ++++++++++++++ examples/dtmc/synchronous_leader/leader6_8.pm | 91 +++++++++++++++ examples/mdp/asynchronous_leader/leader.pctl | 8 ++ examples/mdp/asynchronous_leader/leader.res | 49 ++++++++ examples/mdp/asynchronous_leader/leader3.nm | 96 +++++++++++++++ examples/mdp/asynchronous_leader/leader4.nm | 97 +++++++++++++++ examples/mdp/asynchronous_leader/leader5.nm | 98 ++++++++++++++++ examples/mdp/asynchronous_leader/leader6.nm | 99 ++++++++++++++++ examples/mdp/asynchronous_leader/leader7.nm | 100 ++++++++++++++++ examples/mdp/two_dice/two_dice.pctl | 13 +++ examples/mdp/two_dice/two_dice.res | 13 +++ 24 files changed, 1356 insertions(+) create mode 100644 examples/dtmc/crowds/crowds.pctl create mode 100644 examples/dtmc/crowds/crowds.res create mode 100644 examples/dtmc/crowds/crowds10_5.pm create mode 100644 examples/dtmc/crowds/crowds15_5.pm create mode 100644 examples/dtmc/crowds/crowds20_5.pm create mode 100644 examples/dtmc/crowds/crowds5_5.pm create mode 100644 examples/dtmc/die/die.pctl create mode 100644 examples/dtmc/die/die.pm create mode 100644 examples/dtmc/die/die.res create mode 100644 examples/dtmc/synchronous_leader/leader.pctl create mode 100644 examples/dtmc/synchronous_leader/leader.res create mode 100644 examples/dtmc/synchronous_leader/leader3_5.pm create mode 100644 examples/dtmc/synchronous_leader/leader4_8.pm create mode 100644 examples/dtmc/synchronous_leader/leader5_8.pm create mode 100644 examples/dtmc/synchronous_leader/leader6_8.pm create mode 100644 examples/mdp/asynchronous_leader/leader.pctl create mode 100644 examples/mdp/asynchronous_leader/leader.res create mode 100644 examples/mdp/asynchronous_leader/leader3.nm create mode 100644 examples/mdp/asynchronous_leader/leader4.nm create mode 100644 examples/mdp/asynchronous_leader/leader5.nm create mode 100644 examples/mdp/asynchronous_leader/leader6.nm create mode 100644 examples/mdp/asynchronous_leader/leader7.nm create mode 100644 examples/mdp/two_dice/two_dice.pctl create mode 100644 examples/mdp/two_dice/two_dice.res diff --git a/examples/dtmc/crowds/crowds.pctl b/examples/dtmc/crowds/crowds.pctl new file mode 100644 index 000000000..a7c83e667 --- /dev/null +++ b/examples/dtmc/crowds/crowds.pctl @@ -0,0 +1,3 @@ +P=? [ F "observe0Greater1" ] +P=? [ F "observeIGreater1" ] +P=? [ F "observeOnlyTrueSender" ] diff --git a/examples/dtmc/crowds/crowds.res b/examples/dtmc/crowds/crowds.res new file mode 100644 index 000000000..8e41056f7 --- /dev/null +++ b/examples/dtmc/crowds/crowds.res @@ -0,0 +1,19 @@ +// 5/5 +P=? [ F "observe0Greater1" ] // 0.3328777473921436 +P=? [ F "observeIGreater1" ] // 0.15221847380560186 +P=? [ F "observeOnlyTrueSender" ] // 0.3215351607995943 + +// 10/5 +P=? [ F "observe0Greater1" ] // 0.26345583706046355 +P=? [ F "observeIGreater1" ] // 0.09236405558901994 +P=? [ F "observeOnlyTrueSender" ] // 0.25849872034453947 + +// 15/5 +P=? [ F "observe0Greater1" ] // 0.2408422942249347 +P=? [ F "observeIGreater1" ] // 0.0655686905854717 +P=? [ F "observeOnlyTrueSender" ] // 0.2377298605519743 + +// 20/5 +P=? [ F "observe0Greater1" ] // 0.22967858575985317 +P=? [ F "observeIGreater1" ] // 0.05073192927314383 +P=? [ F "observeOnlyTrueSender" ] // 0.22742031678667812 diff --git a/examples/dtmc/crowds/crowds10_5.pm b/examples/dtmc/crowds/crowds10_5.pm new file mode 100644 index 000000000..752b3f9bb --- /dev/null +++ b/examples/dtmc/crowds/crowds10_5.pm @@ -0,0 +1,80 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 10; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + observe5: [0..TotalRuns] init 0; + + observe6: [0..TotalRuns] init 0; + + observe7: [0..TotalRuns] init 0; + + observe8: [0..TotalRuns] init 0; + + observe9: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/10 : (lastSeen'=0) & (phase'=3) + 1/10 : (lastSeen'=1) & (phase'=3) + 1/10 : (lastSeen'=2) & (phase'=3) + 1/10 : (lastSeen'=3) & (phase'=3) + 1/10 : (lastSeen'=4) & (phase'=3) + 1/10 : (lastSeen'=5) & (phase'=3) + 1/10 : (lastSeen'=6) & (phase'=3) + 1/10 : (lastSeen'=7) & (phase'=3) + 1/10 : (lastSeen'=8) & (phase'=3) + 1/10 : (lastSeen'=9) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> (phase'=0); + +endmodule + +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1; \ No newline at end of file diff --git a/examples/dtmc/crowds/crowds15_5.pm b/examples/dtmc/crowds/crowds15_5.pm new file mode 100644 index 000000000..aa4921cbf --- /dev/null +++ b/examples/dtmc/crowds/crowds15_5.pm @@ -0,0 +1,95 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 15; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + observe5: [0..TotalRuns] init 0; + + observe6: [0..TotalRuns] init 0; + + observe7: [0..TotalRuns] init 0; + + observe8: [0..TotalRuns] init 0; + + observe9: [0..TotalRuns] init 0; + + observe10: [0..TotalRuns] init 0; + + observe11: [0..TotalRuns] init 0; + + observe12: [0..TotalRuns] init 0; + + observe13: [0..TotalRuns] init 0; + + observe14: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4); + [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4); + [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4); + [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4); + [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4); + [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> (phase'=0); + +endmodule + +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; \ No newline at end of file diff --git a/examples/dtmc/crowds/crowds20_5.pm b/examples/dtmc/crowds/crowds20_5.pm new file mode 100644 index 000000000..cdbbb61f6 --- /dev/null +++ b/examples/dtmc/crowds/crowds20_5.pm @@ -0,0 +1,110 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 20; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + observe5: [0..TotalRuns] init 0; + + observe6: [0..TotalRuns] init 0; + + observe7: [0..TotalRuns] init 0; + + observe8: [0..TotalRuns] init 0; + + observe9: [0..TotalRuns] init 0; + + observe10: [0..TotalRuns] init 0; + + observe11: [0..TotalRuns] init 0; + + observe12: [0..TotalRuns] init 0; + + observe13: [0..TotalRuns] init 0; + + observe14: [0..TotalRuns] init 0; + + observe15: [0..TotalRuns] init 0; + + observe16: [0..TotalRuns] init 0; + + observe17: [0..TotalRuns] init 0; + + observe18: [0..TotalRuns] init 0; + + observe19: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/20 : (lastSeen'=0) & (phase'=3) + 1/20 : (lastSeen'=1) & (phase'=3) + 1/20 : (lastSeen'=2) & (phase'=3) + 1/20 : (lastSeen'=3) & (phase'=3) + 1/20 : (lastSeen'=4) & (phase'=3) + 1/20 : (lastSeen'=5) & (phase'=3) + 1/20 : (lastSeen'=6) & (phase'=3) + 1/20 : (lastSeen'=7) & (phase'=3) + 1/20 : (lastSeen'=8) & (phase'=3) + 1/20 : (lastSeen'=9) & (phase'=3) + 1/20 : (lastSeen'=10) & (phase'=3) + 1/20 : (lastSeen'=11) & (phase'=3) + 1/20 : (lastSeen'=12) & (phase'=3) + 1/20 : (lastSeen'=13) & (phase'=3) + 1/20 : (lastSeen'=14) & (phase'=3) + 1/20 : (lastSeen'=15) & (phase'=3) + 1/20 : (lastSeen'=16) & (phase'=3) + 1/20 : (lastSeen'=17) & (phase'=3) + 1/20 : (lastSeen'=18) & (phase'=3) + 1/20 : (lastSeen'=19) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4); + [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4); + [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4); + [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4); + [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4); + [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+1) & (phase'=4); + [] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> (observe15'=observe15+1) & (phase'=4); + [] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> (observe16'=observe16+1) & (phase'=4); + [] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> (observe17'=observe17+1) & (phase'=4); + [] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> (observe18'=observe18+1) & (phase'=4); + [] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> (observe19'=observe19+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> (phase'=0); + +endmodule + +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1; \ No newline at end of file diff --git a/examples/dtmc/crowds/crowds5_5.pm b/examples/dtmc/crowds/crowds5_5.pm new file mode 100644 index 000000000..e1146b586 --- /dev/null +++ b/examples/dtmc/crowds/crowds5_5.pm @@ -0,0 +1,65 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 5; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> (phase'=0); + +endmodule + +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1; \ No newline at end of file diff --git a/examples/dtmc/die/die.pctl b/examples/dtmc/die/die.pctl new file mode 100644 index 000000000..b0eb88dcd --- /dev/null +++ b/examples/dtmc/die/die.pctl @@ -0,0 +1,4 @@ +P=? [ F "one" ] +P=? [ F "two" ] +P=? [ F "three" ] +R=? [ F "done" ] diff --git a/examples/dtmc/die/die.pm b/examples/dtmc/die/die.pm new file mode 100644 index 000000000..f32a1c04b --- /dev/null +++ b/examples/dtmc/die/die.pm @@ -0,0 +1,31 @@ +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the die + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards + +label "one" = s=7&d=1; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "four" = s=7&d=4; +label "five" = s=7&d=5; +label "six" = s=7&d=6; +label "done" = s=7; \ No newline at end of file diff --git a/examples/dtmc/die/die.res b/examples/dtmc/die/die.res new file mode 100644 index 000000000..003af5dbd --- /dev/null +++ b/examples/dtmc/die/die.res @@ -0,0 +1,4 @@ +P=? [ F "one" ] // 0.16666650772094727 +P=? [ F "two" ] // 0.16666650772094727 +P=? [ F "three" ] // 0.16666650772094727 +R=? [ F "done" ] // 3.6666650772094727 diff --git a/examples/dtmc/synchronous_leader/leader.pctl b/examples/dtmc/synchronous_leader/leader.pctl new file mode 100644 index 000000000..e8b1899e6 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader.pctl @@ -0,0 +1,3 @@ +P=? [ F "elected" ] +P=? [ F<=(4*(N+1)) "elected" ] +R=? [ F "elected" ] diff --git a/examples/dtmc/synchronous_leader/leader.res b/examples/dtmc/synchronous_leader/leader.res new file mode 100644 index 000000000..26451a894 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader.res @@ -0,0 +1,14 @@ +// 3/5 +P=? [ F "elected" ] // 1.0 +P=? [ F<=(4*(N+1)) "elected" ] // 0.999997440000001 +R=? [ F "elected" ] // 1.0416666623999995 + +// 4/8 +P=? [ F "elected" ] // 1.0 +P=? [ F<=(4*(N+1)) "elected" ] // 0.9999965911265463 +R=? [ F "elected" ] // 1.0448979526072435 + +// 5/8 +P=? [ F "elected" ] // 1.0 +P=? [ F<=(4*(N+1)) "elected" ] // 0.9999999097195733 +R=? [ F "elected" ] // 1.0176397499602707 \ No newline at end of file diff --git a/examples/dtmc/synchronous_leader/leader3_5.pm b/examples/dtmc/synchronous_leader/leader3_5.pm new file mode 100644 index 000000000..0a45ad217 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader3_5.pm @@ -0,0 +1,85 @@ +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const N = 3; // number of processes +const K = 5; // range of probabilistic choice + +// counter module used to count the number of processes that have been read +// and to know when a process has decided +module counter + + // counter (c=i means process j reading process (i-1)+j next) + c : [1..N-1]; + + // reading + [read] c (c'=c+1); + // finished reading + [read] c=N-1 -> (c'=c); + //decide + [done] u1|u2|u3 -> (c'=c); + // pick again reset counter + [retry] !(u1|u2|u3) -> (c'=1); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (c'=c); + +endmodule + +// processes form a ring and suppose: +// process 1 reads process 2 +// process 2 reads process 3 +// process 3 reads process 1 +module process1 + + // local state + s1 : [0..3]; + // s1=0 make random choice + // s1=1 reading + // s1=2 deciding + // s1=3 finished + + // has a unique id so far (initially true) + u1 : bool; + + // value to be sent to next process in the ring (initially sets this to its own value) + v1 : [0..K-1]; + + // random choice + p1 : [0..K-1]; + + // pick value + [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) + + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) + + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); + // read + [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + // read and move to decide + [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + // deciding + // done + [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + //retry + [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (s1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule +module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule + +// expected number of rounds +rewards "num_rounds" + [pick] true : 1; +endrewards + +// labels +label "elected" = s1=3&s2=3&s3=3; + diff --git a/examples/dtmc/synchronous_leader/leader4_8.pm b/examples/dtmc/synchronous_leader/leader4_8.pm new file mode 100644 index 000000000..fc8f167a0 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader4_8.pm @@ -0,0 +1,89 @@ +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const N = 4; // number of processes +const K = 8; // range of probabilistic choice + +// counter module used to count the number of processes that have been read +// and to know when a process has decided +module counter + + // counter (c=i means process j reading process (i-1)+j next) + c : [1..N-1]; + + // reading + [read] c (c'=c+1); + // finished reading + [read] c=N-1 -> (c'=c); + //decide + [done] u1|u2|u3|u4 -> (c'=c); + // pick again reset counter + [retry] !(u1|u2|u3|u4) -> (c'=1); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (c'=c); + +endmodule + +// processes form a ring and suppose: +// process 1 reads process 2 +// process 2 reads process 3 +// process 3 reads process 1 +module process1 + + // local state + s1 : [0..3]; + // s1=0 make random choice + // s1=1 reading + // s1=2 deciding + // s1=3 finished + + // has a unique id so far (initially true) + u1 : bool; + + // value to be sent to next process in the ring (initially sets this to its own value) + v1 : [0..K-1]; + + // random choice + p1 : [0..K-1]; + + // pick value + [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) + + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) + + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true) + + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) + + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) + + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); + // read + [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + // read and move to decide + [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + // deciding + // done + [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + //retry + [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (s1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule +module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule +module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v1 ] endmodule + +// expected number of rounds +rewards "num_rounds" + [pick] true : 1; +endrewards + +// labels +label "elected" = s1=3&s2=3&s3=3&s4=3; + diff --git a/examples/dtmc/synchronous_leader/leader5_8.pm b/examples/dtmc/synchronous_leader/leader5_8.pm new file mode 100644 index 000000000..72139fda9 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader5_8.pm @@ -0,0 +1,90 @@ +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const N = 5; // number of processes +const K = 8; // range of probabilistic choice + +// counter module used to count the number of processes that have been read +// and to know when a process has decided +module counter + + // counter (c=i means process j reading process (i-1)+j next) + c : [1..N-1]; + + // reading + [read] c (c'=c+1); + // finished reading + [read] c=N-1 -> (c'=c); + //decide + [done] u1|u2|u3|u4|u5 -> (c'=c); + // pick again reset counter + [retry] !(u1|u2|u3|u4|u5) -> (c'=1); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (c'=c); + +endmodule + +// processes form a ring and suppose: +// process 1 reads process 2 +// process 2 reads process 3 +// process 3 reads process 1 +module process1 + + // local state + s1 : [0..3]; + // s1=0 make random choice + // s1=1 reading + // s1=2 deciding + // s1=3 finished + + // has a unique id so far (initially true) + u1 : bool; + + // value to be sent to next process in the ring (initially sets this to its own value) + v1 : [0..K-1]; + + // random choice + p1 : [0..K-1]; + + // pick value + [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) + + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) + + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true) + + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) + + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) + + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); + // read + [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + // read and move to decide + [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + // deciding + // done + [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + //retry + [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (s1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule +module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule +module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule +module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule + +// expected number of rounds +rewards "num_rounds" + [pick] true : 1; +endrewards + +// labels +label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; + diff --git a/examples/dtmc/synchronous_leader/leader6_8.pm b/examples/dtmc/synchronous_leader/leader6_8.pm new file mode 100644 index 000000000..283042ad5 --- /dev/null +++ b/examples/dtmc/synchronous_leader/leader6_8.pm @@ -0,0 +1,91 @@ +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const N = 6; // number of processes +const K = 8; // range of probabilistic choice + +// counter module used to count the number of processes that have been read +// and to know when a process has decided +module counter + + // counter (c=i means process j reading process (i-1)+j next) + c : [1..N-1]; + + // reading + [read] c (c'=c+1); + // finished reading + [read] c=N-1 -> (c'=c); + //decide + [done] u1|u2|u3|u4|u5|u6 -> (c'=c); + // pick again reset counter + [retry] !(u1|u2|u3|u4|u5|u6) -> (c'=1); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (c'=c); + +endmodule + +// processes form a ring and suppose: +// process 1 reads process 2 +// process 2 reads process 3 +// process 3 reads process 1 +module process1 + + // local state + s1 : [0..3]; + // s1=0 make random choice + // s1=1 reading + // s1=2 deciding + // s1=3 finished + + // has a unique id so far (initially true) + u1 : bool; + + // value to be sent to next process in the ring (initially sets this to its own value) + v1 : [0..K-1]; + + // random choice + p1 : [0..K-1]; + + // pick value + [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) + + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) + + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true) + + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) + + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) + + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); + // read + [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + // read and move to decide + [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + // deciding + // done + [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + //retry + [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> (s1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule +module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule +module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule +module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v6 ] endmodule +module process6 = process1 [ s1=s6,p1=p6,v1=v6,u1=u6,v2=v1 ] endmodule + +// expected number of rounds +rewards "num_rounds" + [pick] true : 1; +endrewards + +// labels +label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3&s6=3; + diff --git a/examples/mdp/asynchronous_leader/leader.pctl b/examples/mdp/asynchronous_leader/leader.pctl new file mode 100644 index 000000000..49e4dbeaa --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader.pctl @@ -0,0 +1,8 @@ +Pmin=? [ F "elected" ] + +const int K = 25; +Pmin=? [ F<=K "elected" ] +Pmax=? [ F<=K "elected" ] + +Rmin=? [ F "elected" ] +Rmax=? [ F "elected" ] diff --git a/examples/mdp/asynchronous_leader/leader.res b/examples/mdp/asynchronous_leader/leader.res new file mode 100644 index 000000000..447403e11 --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader.res @@ -0,0 +1,49 @@ +// 3 +Pmin=? [ F "elected" ] // 1.0 + +const int K = 25; +Pmin=? [ F<=K "elected" ] // 0.5625 +Pmax=? [ F<=K "elected" ] // 0.5625 + +Rmin=? [ F "elected" ] // 3.3333212586585432 +Rmax=? [ F "elected" ] // 3.3333206579554826 + +// 4 +Pmin=? [ F "elected" ] // 1.0 + +const int K = 25; +Pmin=? [ F<=K "elected" ] // 0.0625 +Pmax=? [ F<=K "elected" ] // 0.0625 + +Rmin=? [ F "elected" ] // 4.2856896106114934 +Rmax=? [ F "elected" ] // 4.28569043544414 + +// 5 +Pmin=? [ F "elected" ] // 1.0 + +const int K = 25; +Pmin=? [ F<=K "elected" ] // 0.0 +Pmax=? [ F<=K "elected" ] // 0.0 + +Rmin=? [ F "elected" ] // 5.034886386278894 +Rmax=? [ F "elected" ] // 5.034881859133309 + +// 6 +Pmin=? [ F "elected" ] // 1.0 + +const int K = 25; +Pmin=? [ F<=K "elected" ] // 0.0 +Pmax=? [ F<=K "elected" ] // 0.0 + +Rmin=? [ F "elected" ] // 5.649720120334257 +Rmax=? [ F "elected" ] // 5.649719114527437 + +// 7 +Pmin=? [ F "elected" ] // 1.0 + +const int K = 25; +Pmin=? [ F<=K "elected" ] // 0.0 +Pmax=? [ F<=K "elected" ] // 0.0 + +Rmin=? [ F "elected" ] // 6.172433512043686 +Rmax=? [ F "elected" ] // 6.172434400085756 \ No newline at end of file diff --git a/examples/mdp/asynchronous_leader/leader3.nm b/examples/mdp/asynchronous_leader/leader3.nm new file mode 100644 index 000000000..25a3ec89d --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader3.nm @@ -0,0 +1,96 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const N= 3; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..3-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c31] (s1=2) & (receive1=1) & (sent1=2) & (c3 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1); + // receive counter + [c31] (s1=3) & (receive1=1) & (c3 (c1'=c3+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); +label "elected" = s1=4|s2=4|s3=4; + diff --git a/examples/mdp/asynchronous_leader/leader4.nm b/examples/mdp/asynchronous_leader/leader4.nm new file mode 100644 index 000000000..81ade2ea7 --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader4.nm @@ -0,0 +1,97 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const N= 4; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..4-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p41] (s1=1) & (receive1=0) & !( (p1=0) & (p4=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p41] (s1=1) & (receive1=0) & (p1=0) & (p4=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c41] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c41] (s1=2) & (receive1=1) & (sent1=2) & (c4=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c41] (s1=2) & (receive1=1) & (sent1=2) & (c4 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p41] (s1=3) & (receive1=0) -> (p1'=p4) & (receive1'=1); + // receive counter + [c41] (s1=3) & (receive1=1) & (c4 (c1'=c4+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p41=p12,c12=c23,c41=c12,p4=p1,c4=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p41=p23,c12=c34,c41=c23,p4=p2,c4=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p41,p41=p34,c12=c41,c41=c34,p4=p3,c4=c3] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4; + diff --git a/examples/mdp/asynchronous_leader/leader5.nm b/examples/mdp/asynchronous_leader/leader5.nm new file mode 100644 index 000000000..558bab560 --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader5.nm @@ -0,0 +1,98 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const N= 5; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..5-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p51] (s1=1) & (receive1=0) & (p1=0) & (p5=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); + // receive counter + [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule +module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; + diff --git a/examples/mdp/asynchronous_leader/leader6.nm b/examples/mdp/asynchronous_leader/leader6.nm new file mode 100644 index 000000000..84b3283ad --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader6.nm @@ -0,0 +1,99 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const N= 6; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..6-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p61] (s1=1) & (receive1=0) & !( (p1=0) & (p6=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p61] (s1=1) & (receive1=0) & (p1=0) & (p6=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c61] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c61] (s1=2) & (receive1=1) & (sent1=2) & (c6=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c61] (s1=2) & (receive1=1) & (sent1=2) & (c6 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p61] (s1=3) & (receive1=0) -> (p1'=p6) & (receive1'=1); + // receive counter + [c61] (s1=3) & (receive1=1) & (c6 (c1'=c6+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p61=p12,c12=c23,c61=c12,p6=p1,c6=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p61=p23,c12=c34,c61=c23,p6=p2,c6=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p61=p34,c12=c45,c61=c34,p6=p3,c6=c3] endmodule +module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p61=p45,c12=c56,c61=c45,p6=p4,c6=c4] endmodule +module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p61,p61=p56,c12=c61,c61=c56,p6=p5,c6=c5] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4; + diff --git a/examples/mdp/asynchronous_leader/leader7.nm b/examples/mdp/asynchronous_leader/leader7.nm new file mode 100644 index 000000000..fd1a84bed --- /dev/null +++ b/examples/mdp/asynchronous_leader/leader7.nm @@ -0,0 +1,100 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const N= 7; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..7-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p71] (s1=1) & (receive1=0) & !( (p1=0) & (p7=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p71] (s1=1) & (receive1=0) & (p1=0) & (p7=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c71] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c71] (s1=2) & (receive1=1) & (sent1=2) & (c7=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c71] (s1=2) & (receive1=1) & (sent1=2) & (c7 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p71] (s1=3) & (receive1=0) -> (p1'=p7) & (receive1'=1); + // receive counter + [c71] (s1=3) & (receive1=1) & (c7 (c1'=c7+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p71=p12,c12=c23,c71=c12,p7=p1,c7=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p71=p23,c12=c34,c71=c23,p7=p2,c7=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p71=p34,c12=c45,c71=c34,p7=p3,c7=c3] endmodule +module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p71=p45,c12=c56,c71=c45,p7=p4,c7=c4] endmodule +module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67,p71=p56,c12=c67,c71=c56,p7=p5,c7=c5] endmodule +module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p71,p71=p67,c12=c71,c71=c67,p7=p6,c7=c6] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4; + diff --git a/examples/mdp/two_dice/two_dice.pctl b/examples/mdp/two_dice/two_dice.pctl new file mode 100644 index 000000000..10cdff821 --- /dev/null +++ b/examples/mdp/two_dice/two_dice.pctl @@ -0,0 +1,13 @@ +Pmin=? [ F "two" ] +Pmax=? [ F "two" ] +Pmin=? [ F "three" ] +Pmax=? [ F "three" ] +Pmin=? [ F "four" ] +Pmax=? [ F "four" ] +Pmin=? [ F "five" ] +Pmax=? [ F "five" ] +Pmin=? [ F "six" ] +Pmax=? [ F "six" ] + +Rmin=? [ F "done" ] +Rmax=? [ F "done" ] diff --git a/examples/mdp/two_dice/two_dice.res b/examples/mdp/two_dice/two_dice.res new file mode 100644 index 000000000..9f38b8153 --- /dev/null +++ b/examples/mdp/two_dice/two_dice.res @@ -0,0 +1,13 @@ +Pmin=? [ F "two" ] // 0.027777761220932007 +Pmax=? [ F "two" ] // 0.027777761220932007 +Pmin=? [ F "three" ] // 0.055555522441864014 +Pmax=? [ F "three" ] // 0.055555522441864014 +Pmin=? [ F "four" ] // 0.08333328366279602 +Pmax=? [ F "four" ] // 0.08333328366279602 +Pmin=? [ F "five" ] // 0.11111104488372803 +Pmax=? [ F "five" ] // 0.11111104488372803 +Pmin=? [ F "six" ] // 0.13888880610466003 +Pmax=? [ F "six" ] // 0.13888880610466003 + +Rmin=? [ F "done" ] // 7.333329498767853 +Rmax=? [ F "done" ] // 7.333329498767853