dehnert
12 years ago
1 changed files with 20 additions and 85 deletions
-
105test.input
@ -1,89 +1,24 @@ |
|||
// Knuth's model of a fair die using only fair coins |
|||
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<TotalRuns -> 1: (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 -> 1: (observe0'=observe0+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (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 -> 1: (phase'=0); |
|||
|
|||
module die |
|||
|
|||
// local state |
|||
s : [0..7] init 0; |
|||
// value of the dice |
|||
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 -> 1: (s'=7); |
|||
|
|||
endmodule |
|||
|
|||
label "observe0Greater1" = observe0>1; |
|||
label "observe1Greater1" = observe1>1; |
|||
label "observe2Greater1" = observe2>1; |
|||
label "observe3Greater1" = observe3>1; |
|||
label "observe4Greater1" = observe4>1; |
|||
label "observe5Greater1" = observe5>1; |
|||
label "observe6Greater1" = observe6>1; |
|||
label "observe7Greater1" = observe7>1; |
|||
label "observe8Greater1" = observe8>1; |
|||
label "observe9Greater1" = observe9>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; |
|||
rewards "coin_flips" |
|||
[] s<7 : 1; |
|||
endrewards |
Write
Preview
Loading…
Cancel
Save
Reference in new issue