Browse Source
Merge branch 'master' into PrctlParser
Merge branch 'master' into PrctlParser
Conflicts: examples/mdp/asynchronous_leader/leader3.tra examples/mdp/asynchronous_leader/leader4.tra examples/mdp/asynchronous_leader/leader5.tra examples/mdp/asynchronous_leader/leader6.tra examples/mdp/asynchronous_leader/leader7.tra examples/mdp/two_dice/two_dice.lab examples/mdp/two_dice/two_dice.tra src/formula/NoBoundOperator.h src/formula/PathBoundOperator.h src/formula/ProbabilisticNoBoundOperator.h src/formula/RewardNoBoundOperator.h src/modelchecker/AbstractModelChecker.h src/modelchecker/DtmcPrctlModelChecker.h src/modelchecker/EigenDtmcPrctlModelChecker.h src/modelchecker/GmmxxDtmcPrctlModelChecker.h src/modelchecker/GmmxxMdpPrctlModelChecker.h src/modelchecker/MdpPrctlModelChecker.h src/models/GraphTransitions.h src/parser/AutoParser.h src/parser/DeterministicSparseTransitionParser.cpp src/parser/NondeterministicModelParser.cpp src/parser/NondeterministicSparseTransitionParser.cpp src/parser/NondeterministicSparseTransitionParser.h src/storage/BitVector.h src/storage/SparseMatrix.h src/storm.cpp src/utility/GraphAnalyzer.h src/utility/Vector.hmain
74 changed files with 4944 additions and 1447 deletions
-
14.gitignore
-
58CMakeLists.txt
-
3examples/dtmc/crowds/crowds.pctl
-
19examples/dtmc/crowds/crowds.res
-
80examples/dtmc/crowds/crowds10_5.pm
-
95examples/dtmc/crowds/crowds15_5.pm
-
110examples/dtmc/crowds/crowds20_5.pm
-
65examples/dtmc/crowds/crowds5_5.pm
-
4examples/dtmc/die/die.pctl
-
31examples/dtmc/die/die.pm
-
4examples/dtmc/die/die.res
-
3examples/dtmc/synchronous_leader/leader.pctl
-
14examples/dtmc/synchronous_leader/leader.res
-
85examples/dtmc/synchronous_leader/leader3_5.pm
-
89examples/dtmc/synchronous_leader/leader4_8.pm
-
90examples/dtmc/synchronous_leader/leader5_8.pm
-
91examples/dtmc/synchronous_leader/leader6_8.pm
-
8examples/mdp/asynchronous_leader/leader.pctl
-
49examples/mdp/asynchronous_leader/leader.res
-
96examples/mdp/asynchronous_leader/leader3.nm
-
97examples/mdp/asynchronous_leader/leader4.nm
-
98examples/mdp/asynchronous_leader/leader5.nm
-
99examples/mdp/asynchronous_leader/leader6.nm
-
100examples/mdp/asynchronous_leader/leader7.nm
-
20examples/mdp/consensus/coin.pctl
-
60examples/mdp/consensus/coin2.nm
-
62examples/mdp/consensus/coin4.nm
-
64examples/mdp/consensus/coin6.nm
-
40examples/mdp/two_dice/two_dice.nm
-
13examples/mdp/two_dice/two_dice.pctl
-
13examples/mdp/two_dice/two_dice.res
-
6src/adapters/EigenAdapter.h
-
42src/adapters/GmmxxAdapter.h
-
220src/adapters/StormAdapter.h
-
3src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
56src/formula/OptimizingOperator.h
-
20src/formula/PathBoundOperator.h
-
11src/formula/ProbabilisticBoundOperator.h
-
6src/formula/RewardBoundOperator.h
-
89src/modelchecker/AbstractModelChecker.h
-
246src/modelchecker/DtmcPrctlModelChecker.h
-
244src/modelchecker/EigenDtmcPrctlModelChecker.h
-
432src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
349src/modelchecker/GmmxxMdpPrctlModelChecker.h
-
335src/modelchecker/MdpPrctlModelChecker.h
-
139src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
-
188src/models/GraphTransitions.h
-
4src/parser/DeterministicModelParser.cpp
-
106src/parser/DeterministicSparseTransitionParser.cpp
-
4src/parser/DeterministicSparseTransitionParser.h
-
6src/parser/NondeterministicModelParser.cpp
-
181src/parser/NondeterministicSparseTransitionParser.cpp
-
4src/parser/NondeterministicSparseTransitionParser.h
-
13src/parser/Parser.cpp
-
17src/parser/Parser.h
-
40src/storage/BitVector.h
-
5src/storage/JacobiDecomposition.h
-
409src/storage/SparseMatrix.h
-
253src/storm.cpp
-
3src/utility/ConstTemplates.h
-
64src/utility/ErrorHandling.h
-
220src/utility/GraphAnalyzer.h
-
1src/utility/Settings.cpp
-
17src/utility/Settings.h
-
79src/utility/Vector.h
-
164test/functional/EigenDtmcPrctModelCheckerTest.cpp
-
162test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
-
248test/functional/GmmxxMdpPrctModelCheckerTest.cpp
-
81test/parser/PrctlParserTest.cpp
-
33test/storage/SparseMatrixTest.cpp
-
0test/storage/adapters/EigenAdapterTest.cpp
-
111test/storage/adapters/GmmAdapterTest.cpp
-
104test/storage/adapters/StormAdapterTest.cpp
@ -0,0 +1,3 @@ |
|||
P=? [ F "observe0Greater1" ] |
|||
P=? [ F "observeIGreater1" ] |
|||
P=? [ F "observeOnlyTrueSender" ] |
@ -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 |
@ -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<TotalRuns -> (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; |
@ -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<TotalRuns -> (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; |
@ -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<TotalRuns -> (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; |
@ -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<TotalRuns -> (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; |
@ -0,0 +1,4 @@ |
|||
P=? [ F "one" ] |
|||
P=? [ F "two" ] |
|||
P=? [ F "three" ] |
|||
R=? [ F "done" ] |
@ -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; |
@ -0,0 +1,4 @@ |
|||
P=? [ F "one" ] // 0.16666650772094727 |
|||
P=? [ F "two" ] // 0.16666650772094727 |
|||
P=? [ F "three" ] // 0.16666650772094727 |
|||
R=? [ F "done" ] // 3.6666650772094727 |
@ -0,0 +1,3 @@ |
|||
P=? [ F "elected" ] |
|||
P=? [ F<=(4*(N+1)) "elected" ] |
|||
R=? [ F "elected" ] |
@ -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 |
@ -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<N-1 -> (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<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (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; |
|||
|
@ -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<N-1 -> (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<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (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; |
|||
|
@ -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<N-1 -> (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<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (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; |
|||
|
@ -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<N-1 -> (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<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (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; |
|||
|
@ -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" ] |
@ -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 |
@ -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<N-1) -> (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<N-1) -> (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; |
|||
|
@ -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<N-1) -> (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<N-1) -> (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; |
|||
|
@ -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<N-1) -> (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<N-1) -> (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; |
|||
|
@ -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<N-1) -> (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<N-1) -> (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; |
|||
|
@ -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<N-1) -> (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<N-1) -> (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; |
|||
|
@ -0,0 +1,20 @@ |
|||
// C1 (with probability 1, all N processes finish the protocol) |
|||
Pmin=? [ F "finished" ] |
|||
|
|||
// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2) |
|||
// Results are same for v=1 and v=2 by symmetry |
|||
// Analytic bound is (K-1)/(2*K) |
|||
Pmin=? [ F "finished"&"all_coins_equal_0" ] |
|||
Pmin=? [ F "finished"&"all_coins_equal_1" ] |
|||
|
|||
// Max probability of finishing protocol with coins not all equal |
|||
Pmax=? [ F "finished"&!"agree" ] |
|||
|
|||
// Min/max probability of finishing within k steps |
|||
Pmin=? [ F<=k "finished" ] |
|||
Pmax=? [ F<=k "finished" ] |
|||
|
|||
// Min/max expected steps to finish |
|||
Rmin=? [ F "finished" ] |
|||
Rmax=? [ F "finished" ] |
|||
|
@ -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<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 |
|||
|
|||
// 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 |
|||
|
@ -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<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 |
|||
|
|||
// 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 |
|||
|
@ -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<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 |
|||
|
|||
// 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 |
|||
|
@ -0,0 +1,40 @@ |
|||
// sum of two dice as the asynchronous parallel composition of |
|||
// two copies of Knuth's model of a fair die using only fair coins |
|||
|
|||
mdp |
|||
|
|||
module die1 |
|||
|
|||
// local state |
|||
s1 : [0..7] init 0; |
|||
// value of the dice |
|||
d1 : [0..6] init 0; |
|||
|
|||
[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2); |
|||
[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4); |
|||
[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6); |
|||
[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1); |
|||
[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); |
|||
[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); |
|||
[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); |
|||
[] s1=7 & s2=7 -> (s1'=7); |
|||
endmodule |
|||
|
|||
module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule |
|||
|
|||
rewards "coinflips" |
|||
[] s1<7 | s2<7 : 1; |
|||
endrewards |
|||
|
|||
label "done" = s1=7 & s2=7; |
|||
label "two" = s1=7 & s2=7 & d1+d2=2; |
|||
label "three" = s1=7 & s2=7 & d1+d2=3; |
|||
label "four" = s1=7 & s2=7 & d1+d2=4; |
|||
label "five" = s1=7 & s2=7 & d1+d2=5; |
|||
label "six" = s1=7 & s2=7 & d1+d2=6; |
|||
label "seven" = s1=7 & s2=7 & d1+d2=7; |
|||
label "eight" = s1=7 & s2=7 & d1+d2=8; |
|||
label "nine" = s1=7 & s2=7 & d1+d2=9; |
|||
label "ten" = s1=7 & s2=7 & d1+d2=10; |
|||
label "eleven" = s1=7 & s2=7 & d1+d2=11; |
|||
label "twelve" = s1=7 & s2=7 & d1+d2=12; |
@ -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" ] |
@ -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 |
@ -0,0 +1,220 @@ |
|||
/* |
|||
* StormAdapter.h |
|||
* |
|||
* Created on: 02.03.2013 |
|||
* Author: Philipp Berger |
|||
*/ |
|||
|
|||
#ifndef STORM_ADAPTERS_STORMADAPTER_H_ |
|||
#define STORM_ADAPTERS_STORMADAPTER_H_ |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace adapters { |
|||
|
|||
class StormAdapter { |
|||
public: |
|||
/*! |
|||
* Converts a sparse matrix into a sparse matrix in the storm format. |
|||
* @return A pointer to a row-major sparse matrix in storm format. |
|||
*/ |
|||
template<class T> |
|||
static storm::storage::SparseMatrix<T>* toStormSparseMatrix(gmm::csr_matrix<T> const& matrix) { |
|||
uint_fast64_t realNonZeros = gmm::nnz(matrix); |
|||
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm."); |
|||
|
|||
// Prepare the resulting matrix. |
|||
storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.nrows(), matrix.ncols()); |
|||
|
|||
// Set internal NonZero Counter |
|||
result->nonZeroEntryCount = realNonZeros; |
|||
result->setState(result->Initialized); |
|||
|
|||
if (!result->prepareInternalStorage(false)) { |
|||
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting GMM++ Matrix to Storm."); |
|||
delete result; |
|||
return nullptr; |
|||
} else { |
|||
|
|||
// Copy Row Indications |
|||
std::copy(matrix.jc.begin(), matrix.jc.end(), std::back_inserter(result->rowIndications)); |
|||
// Copy Columns Indications |
|||
std::copy(matrix.ir.begin(), matrix.ir.end(), std::back_inserter(result->columnIndications)); |
|||
// And do the same thing with the actual values. |
|||
std::copy(matrix.pr.begin(), matrix.pr.end(), std::back_inserter(result->valueStorage)); |
|||
|
|||
result->currentSize = realNonZeros; |
|||
result->lastRow = matrix.nrows() - 1; |
|||
} |
|||
|
|||
result->finalize(); |
|||
|
|||
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format."); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Helper function to determine whether the given Eigen matrix is in RowMajor |
|||
* format. Always returns true, but is overloaded, so the compiler will |
|||
* only call it in case the Eigen matrix is in RowMajor format. |
|||
* @return True. |
|||
*/ |
|||
template<typename _Scalar, typename _Index> |
|||
static bool isEigenRowMajor(Eigen::SparseMatrix<_Scalar, Eigen::RowMajor, _Index>) { |
|||
return true; |
|||
} |
|||
|
|||
/*! |
|||
* Helper function to determine whether the given Eigen matrix is in RowMajor |
|||
* format. Always returns false, but is overloaded, so the compiler will |
|||
* only call it in case the Eigen matrix is in ColMajor format. |
|||
* @return False. |
|||
*/ |
|||
template<typename _Scalar, typename _Index> |
|||
static bool isEigenRowMajor( |
|||
Eigen::SparseMatrix<_Scalar, Eigen::ColMajor, _Index>) { |
|||
return false; |
|||
} |
|||
|
|||
/*! |
|||
* Converts a sparse matrix in the eigen format to Storm Sparse Matrix format. |
|||
* @return A pointer to a row-major sparse matrix in our format. |
|||
*/ |
|||
template<class T, int _Options, typename _Index> |
|||
static storm::storage::SparseMatrix<T>* toStormSparseMatrix(Eigen::SparseMatrix<T, _Options, _Index> const& matrix) { |
|||
uint_fast64_t realNonZeros = matrix.nonZeros(); |
|||
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from Eigen3 format into Storm."); |
|||
|
|||
// Throw an error in case the matrix is not in compressed format. |
|||
if (!matrix.isCompressed()) { |
|||
LOG4CPLUS_ERROR(logger, "Trying to convert from an Eigen matrix that is not in compressed form."); |
|||
return nullptr; |
|||
} |
|||
|
|||
/* |
|||
* Try to prepare the internal storage and throw an error in case of |
|||
* failure. |
|||
*/ |
|||
|
|||
// Get necessary pointers to the contents of the Eigen matrix. |
|||
const T* valuePtr = matrix.valuePtr(); |
|||
const _Index* indexPtr = matrix.innerIndexPtr(); |
|||
const _Index* outerPtr = matrix.outerIndexPtr(); |
|||
|
|||
const uint_fast64_t outerSize = matrix.outerSize(); |
|||
|
|||
storm::storage::SparseMatrix<T>* result = nullptr; |
|||
|
|||
// If the given matrix is in RowMajor format, copying can simply |
|||
// be done by adding all values in order. |
|||
// Direct copying is, however, prevented because we have to |
|||
// separate the diagonal entries from others. |
|||
if (isEigenRowMajor(matrix)) { |
|||
/* Because of the RowMajor format outerSize evaluates to the |
|||
* number of rows. |
|||
* Prepare the resulting matrix. |
|||
*/ |
|||
result = new storm::storage::SparseMatrix<T>(matrix.outerSize(), matrix.innerSize()); |
|||
|
|||
// Set internal NonZero Counter |
|||
result->nonZeroEntryCount = realNonZeros; |
|||
result->setState(result->Initialized); |
|||
|
|||
if (!result->prepareInternalStorage(false)) { |
|||
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 RM Matrix to Storm."); |
|||
delete result; |
|||
return nullptr; |
|||
} else { |
|||
|
|||
// Copy Row Indications |
|||
std::copy(outerPtr, outerPtr + outerSize, std::back_inserter(result->rowIndications)); |
|||
// Copy Columns Indications |
|||
std::copy(indexPtr, indexPtr + realNonZeros, std::back_inserter(result->columnIndications)); |
|||
// And do the same thing with the actual values. |
|||
std::copy(valuePtr, valuePtr + realNonZeros, std::back_inserter(result->valueStorage)); |
|||
|
|||
// This is our Sentinel Element. |
|||
result->rowIndications.push_back(realNonZeros); |
|||
|
|||
result->currentSize = realNonZeros; |
|||
result->lastRow = outerSize - 1; |
|||
} |
|||
} else { |
|||
/* Because of the RowMajor format outerSize evaluates to the |
|||
* number of columns. |
|||
* Prepare the resulting matrix. |
|||
*/ |
|||
const uint_fast64_t colCount = matrix.outerSize(); |
|||
result = new storm::storage::SparseMatrix<T>(matrix.innerSize(), colCount); |
|||
|
|||
// Set internal NonZero Counter |
|||
result->nonZeroEntryCount = realNonZeros; |
|||
result->setState(result->Initialized); |
|||
if (!result->prepareInternalStorage()) { |
|||
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 CM Matrix to Storm."); |
|||
delete result; |
|||
return nullptr; |
|||
} else { |
|||
// Set internal NonZero Counter |
|||
result->nonZeroEntryCount = realNonZeros; |
|||
result->setState(result->Initialized); |
|||
|
|||
// Create an array to remember which elements have to still |
|||
// be searched in each column and initialize it with the starting |
|||
// index for every column. |
|||
_Index* positions = new _Index[colCount](); |
|||
for (_Index i = 0; i < colCount; ++i) { |
|||
positions[i] = outerPtr[i]; |
|||
} |
|||
|
|||
// Now copy the elements. As the matrix is in ColMajor format, |
|||
// we need to iterate over the columns to find the next non-zero |
|||
// entry. |
|||
uint_fast64_t i = 0; |
|||
int currentRow = 0; |
|||
int currentColumn = 0; |
|||
while (i < realNonZeros) { |
|||
// If the current element belongs the the current column, |
|||
// add it in case it is also in the current row. |
|||
if ((positions[currentColumn] < outerPtr[currentColumn + 1]) |
|||
&& (indexPtr[positions[currentColumn]] == currentRow)) { |
|||
result->addNextValue(currentRow, currentColumn, valuePtr[positions[currentColumn]]); |
|||
// Remember that we found one more non-zero element. |
|||
++i; |
|||
// Mark this position as "used". |
|||
++positions[currentColumn]; |
|||
} |
|||
|
|||
// Now we can advance to the next column and also row, |
|||
// in case we just iterated through the last column. |
|||
++currentColumn; |
|||
if (currentColumn == colCount) { |
|||
currentColumn = 0; |
|||
++currentRow; |
|||
} |
|||
} |
|||
delete[] positions; |
|||
} |
|||
} |
|||
result->setState(result->Initialized); |
|||
result->finalize(); |
|||
|
|||
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format."); |
|||
|
|||
return result; |
|||
} |
|||
}; |
|||
|
|||
} //namespace adapters |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_ADAPTERS_STORMADAPTER_H_ */ |
@ -0,0 +1,56 @@ |
|||
#ifndef STORM_FORMULA_OPTIMIZINGOPERATOR_H_ |
|||
#define STORM_FORMULA_OPTIMIZINGOPERATOR_H_ |
|||
|
|||
namespace storm { |
|||
|
|||
namespace formula { |
|||
|
|||
class OptimizingOperator { |
|||
public: |
|||
/*! |
|||
* Empty constructor |
|||
*/ |
|||
OptimizingOperator() : optimalityOperator(false), minimumOperator(false) { |
|||
} |
|||
|
|||
/*! |
|||
* Constructor |
|||
* |
|||
* @param minimumOperator A flag indicating whether this operator is a minimizing or a maximizing operator. |
|||
*/ |
|||
OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) { |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator. |
|||
* @returns True if the operator is an optimizing operator. |
|||
*/ |
|||
bool isOptimalityOperator() const { |
|||
return optimalityOperator; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether the operator is a minimizing operator given that it is an optimality |
|||
* operator. |
|||
* @returns True if the operator is an optimizing operator and it is a minimizing operator and |
|||
* false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator. |
|||
*/ |
|||
bool isMinimumOperator() const { |
|||
return optimalityOperator && minimumOperator; |
|||
} |
|||
|
|||
private: |
|||
// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator |
|||
// over a nondeterministic model. |
|||
bool optimalityOperator; |
|||
|
|||
// In the case this operator is an optimizing operator, this flag indicates whether it is |
|||
// looking for the minimum or the maximum value. |
|||
bool minimumOperator; |
|||
}; |
|||
|
|||
} /* namespace formula */ |
|||
|
|||
} /* namespace storm */ |
|||
|
|||
#endif /* STORM_FORMULA_OPTIMIZINGOPERATOR_H_ */ |
@ -0,0 +1,139 @@ |
|||
/* |
|||
* GmmxxDtmcPrctlModelChecker.h |
|||
* |
|||
* Created on: 06.12.2012 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ |
|||
|
|||
#include <cmath> |
|||
|
|||
#include "src/models/Mdp.h" |
|||
#include "src/modelchecker/MdpPrctlModelChecker.h" |
|||
#include "src/utility/GraphAnalyzer.h" |
|||
#include "src/utility/Vector.h" |
|||
#include "src/utility/ConstTemplates.h" |
|||
#include "src/utility/Settings.h" |
|||
#include "src/adapters/GmmxxAdapter.h" |
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/storage/JacobiDecomposition.h" |
|||
|
|||
#include "gmm/gmm_matrix.h" |
|||
#include "gmm/gmm_iter_solvers.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace modelChecker { |
|||
|
|||
/* |
|||
* A model checking engine that makes use of the gmm++ backend. |
|||
*/ |
|||
template <class Type> |
|||
class TopologicalValueIterationMdpPrctlModelChecker : public MdpPrctlModelChecker<Type> { |
|||
|
|||
public: |
|||
explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp<Type>& mdp) : MdpPrctlModelChecker<Type>(mdp) { } |
|||
|
|||
virtual ~TopologicalValueIterationMdpPrctlModelChecker() { } |
|||
|
|||
private: |
|||
/*! |
|||
* Solves the given equation system under the given parameters using the power method. |
|||
* |
|||
* @param A The matrix A specifying the coefficients of the equations. |
|||
* @param x The vector x for which to solve the equations. The initial value of the elements of |
|||
* this vector are used as the initial guess and might thus influence performance and convergence. |
|||
* @param b The vector b specifying the values on the right-hand-sides of the equations. |
|||
* @return The solution of the system of linear equations in form of the elements of the vector |
|||
* x. |
|||
*/ |
|||
void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const { |
|||
// Get the settings object to customize solving. |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
|
|||
// Get relevant user-defined settings for solving the equations. |
|||
double precision = s->get<double>("precision"); |
|||
unsigned maxIterations = s->get<unsigned>("maxiter"); |
|||
bool relative = s->get<bool>("relative"); |
|||
|
|||
std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents; |
|||
storm::models::GraphTransitions<Type> stronglyConnectedComponentsDependencyGraph; |
|||
storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); |
|||
|
|||
std::vector<uint_fast64_t> topologicalSort; |
|||
storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph, topologicalSort); |
|||
|
|||
// Set up the environment for the power method. |
|||
std::vector<Type> multiplyResult(matrix.getRowCount()); |
|||
std::vector<Type>* currentX = &x; |
|||
std::vector<Type>* newX = new std::vector<Type>(x.size()); |
|||
std::vector<Type>* swap = nullptr; |
|||
uint_fast64_t currentMaxLocalIterations = 0; |
|||
uint_fast64_t localIterations = 0; |
|||
uint_fast64_t globalIterations = 0; |
|||
bool converged = true; |
|||
|
|||
for (auto sccIndexIt = topologicalSort.begin(); sccIndexIt != topologicalSort.end() && converged; ++sccIndexIt) { |
|||
std::vector<uint_fast64_t> const& scc = stronglyConnectedComponents[*sccIndexIt]; |
|||
|
|||
localIterations = 0; |
|||
converged = false; |
|||
while (!converged && localIterations < maxIterations) { |
|||
// Compute x' = A*x + b. |
|||
matrix.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); |
|||
storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b); |
|||
|
|||
// Reduce the vector x' by applying min/max for all non-deterministic choices. |
|||
if (this->minimumOperatorStack.top()) { |
|||
storm::utility::reduceVectorMin(multiplyResult, newX, scc, nondeterministicChoiceIndices); |
|||
} else { |
|||
storm::utility::reduceVectorMax(multiplyResult, newX, scc, nondeterministicChoiceIndices); |
|||
} |
|||
|
|||
// Determine whether the method converged. |
|||
// converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative); |
|||
converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); |
|||
|
|||
// Update environment variables. |
|||
swap = currentX; |
|||
currentX = newX; |
|||
newX = swap; |
|||
++localIterations; |
|||
++globalIterations; |
|||
} |
|||
|
|||
std::cout << "converged locally for scc of size " << scc.size() << std::endl; |
|||
|
|||
if (localIterations > currentMaxLocalIterations) { |
|||
currentMaxLocalIterations = localIterations; |
|||
} |
|||
} |
|||
|
|||
if (globalIterations % 2 == 1) { |
|||
std::swap(x, *currentX); |
|||
delete currentX; |
|||
} else { |
|||
delete newX; |
|||
} |
|||
|
|||
// Check if the solver converged and issue a warning otherwise. |
|||
if (converged) { |
|||
LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations."); |
|||
} else { |
|||
LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); |
|||
} |
|||
} |
|||
}; |
|||
|
|||
} //namespace modelChecker |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ */ |
@ -0,0 +1,64 @@ |
|||
/* |
|||
* File: ErrorHandling.h |
|||
* Author: Gereon Kremer |
|||
* |
|||
* Created on March 15, 2013, 4:10 PM |
|||
*/ |
|||
|
|||
#ifndef ERRORHANDLING_H |
|||
#define ERRORHANDLING_H |
|||
|
|||
#include <signal.h> |
|||
#include <execinfo.h> |
|||
#include <cxxabi.h> |
|||
|
|||
std::string demangle(const char* symbol) { |
|||
int status; |
|||
// Attention: sscanf format strings rely on size being 128 |
|||
char temp[128]; |
|||
char* demangled; |
|||
// Check for C++ symbol |
|||
if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) { |
|||
if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) { |
|||
std::string result(demangled); |
|||
free(demangled); |
|||
return result; |
|||
} |
|||
} |
|||
// Check for C symbol |
|||
if (sscanf(symbol, "%127s", temp) == 1) { |
|||
return temp; |
|||
} |
|||
// Return plain symbol |
|||
return symbol; |
|||
} |
|||
|
|||
void signalHandler(int sig) { |
|||
#define SIZE 128 |
|||
LOG4CPLUS_FATAL(logger, "We recieved a segfault. To start with, here is a backtrace."); |
|||
|
|||
void *buffer[SIZE]; |
|||
char **strings; |
|||
int nptrs; |
|||
nptrs = backtrace(buffer, SIZE); |
|||
|
|||
strings = backtrace_symbols(buffer, nptrs); |
|||
if (strings == nullptr) { |
|||
std::cerr << "Obtaining the backtrace symbols failed. Well, shit." << std::endl; |
|||
exit(2); |
|||
} |
|||
// j = 2: skip the handler itself. |
|||
for (int j = 1; j < nptrs; j++) { |
|||
LOG4CPLUS_FATAL(logger, nptrs-j << ": " << demangle(strings[j])); |
|||
} |
|||
free(strings); |
|||
LOG4CPLUS_FATAL(logger, "That's all we can do. Bye."); |
|||
exit(2); |
|||
} |
|||
|
|||
void installSignalHandler() { |
|||
signal(SIGSEGV, signalHandler); |
|||
} |
|||
|
|||
#endif /* ERRORHANDLING_H */ |
|||
|
@ -0,0 +1,164 @@ |
|||
/*
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "src/utility/Settings.h"
|
|||
#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
TEST(EigenDtmcPrctModelCheckerTest, Die) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 14); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("two"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("three"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(EigenDtmcPrctModelCheckerTest, Crowds) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 8608); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("observeIGreater1"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 12401); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 1), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
*/ |
@ -0,0 +1,162 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "src/utility/Settings.h"
|
|||
#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
TEST(GmmxxDtmcPrctModelCheckerTest, Die) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 13); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 27); |
|||
|
|||
storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("two"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("three"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - ((double)11/3)), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 8607); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460); |
|||
|
|||
storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("observeIGreater1"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
s->set("fix-deadlocks"); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 12400); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894); |
|||
|
|||
storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
@ -0,0 +1,248 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "src/utility/Settings.h"
|
|||
#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
TEST(GmmxxMdpPrctModelCheckerTest, Dice) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::MDP); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436); |
|||
|
|||
storm::modelChecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("two"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("two"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("three"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("three"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("four"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("four"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", ""); |
|||
|
|||
ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>(); |
|||
|
|||
storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp); |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); |
|||
|
|||
result = rewardFormula->check(stateRewardModelChecker); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); |
|||
|
|||
result = rewardFormula->check(stateRewardModelChecker); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>(); |
|||
|
|||
storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); |
|||
|
|||
result = rewardFormula->check(stateAndTransitionRewardModelChecker); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("done"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); |
|||
|
|||
result = rewardFormula->check(stateAndTransitionRewardModelChecker); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::MDP); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 3172); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144); |
|||
|
|||
storm::modelChecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp); |
|||
|
|||
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
eventuallyFormula = new storm::formula::Eventually<double>(apFormula); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25); |
|||
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision")); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::formula::Ap<double>("elected"); |
|||
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula); |
|||
rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision")); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
@ -0,0 +1,111 @@ |
|||
#include "gtest/gtest.h"
|
|||
|
|||
#include "gmm/gmm_matrix.h"
|
|||
#include "src/adapters/GmmxxAdapter.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "boost/integer/integer_mask.hpp"
|
|||
|
|||
#define STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
|
|||
#define STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
|
|||
|
|||
double getValue(gmm::csr_matrix<double> const& gmmSparseMatrix, uint_fast64_t row, uint_fast64_t col) { |
|||
uint_fast64_t rowStart = gmmSparseMatrix.jc.at(row); |
|||
uint_fast64_t rowEnd = gmmSparseMatrix.jc.at(row + 1); |
|||
while (rowStart < rowEnd) { |
|||
if (gmmSparseMatrix.ir.at(rowStart) == col) { |
|||
return gmmSparseMatrix.pr.at(rowStart); |
|||
} |
|||
if (gmmSparseMatrix.ir.at(rowStart) > col) { |
|||
break; |
|||
} |
|||
++rowStart; |
|||
} |
|||
|
|||
return 0.0; |
|||
} |
|||
|
|||
TEST(GmmAdapterTest, SimpleDenseSquareCopy) { |
|||
// 5 rows
|
|||
storm::storage::SparseMatrix<double> sm(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
|
|||
double values[STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; |
|||
sm.initialize(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
|
|||
int row = 0; |
|||
int col = 0; |
|||
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { |
|||
values[i] = static_cast<double>(i + 1); |
|||
|
|||
sm.addNextValue(row, col, values[i]); |
|||
++col; |
|||
if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
sm.finalize(); |
|||
|
|||
auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm); |
|||
|
|||
ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(gmm::nnz(*gsm), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
row = 0; |
|||
col = 0; |
|||
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { |
|||
ASSERT_EQ(values[i], getValue(*gsm, row, col)); |
|||
++col; |
|||
if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
} |
|||
|
|||
TEST(GmmAdapterTest, SimpleSparseSquareCopy) { |
|||
// 5 rows
|
|||
storm::storage::SparseMatrix<double> sm(STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
|
|||
double values[STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; |
|||
sm.initialize((STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); |
|||
|
|||
int row = 0; |
|||
int col = 0; |
|||
|
|||
bool everySecondElement = true; |
|||
|
|||
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { |
|||
values[i] = static_cast<double>(i + 1); |
|||
if (everySecondElement) { |
|||
sm.addNextValue(row, col, values[i]); |
|||
} |
|||
everySecondElement = !everySecondElement; |
|||
++col; |
|||
if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
sm.finalize(); |
|||
|
|||
auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm); |
|||
|
|||
ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(gmm::nnz(*gsm), (STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); |
|||
|
|||
row = 0; |
|||
col = 0; |
|||
everySecondElement = true; |
|||
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { |
|||
if (everySecondElement) { |
|||
ASSERT_EQ(values[i], getValue(*gsm, row, col)); |
|||
} |
|||
everySecondElement = !everySecondElement; |
|||
++col; |
|||
if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
} |
@ -0,0 +1,104 @@ |
|||
#include "gtest/gtest.h"
|
|||
|
|||
#include "gmm/gmm_matrix.h"
|
|||
#include "src/adapters/StormAdapter.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "boost/integer/integer_mask.hpp"
|
|||
|
|||
#define STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
|
|||
#define STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
|
|||
|
|||
TEST(StormAdapterTest, SimpleDenseSquareCopy) { |
|||
// 5 rows
|
|||
gmm::csr_matrix<double> gmmSparseMatrix; |
|||
|
|||
/*
|
|||
* As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy. |
|||
*/ |
|||
gmm::row_matrix<gmm::wsvector<double>> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
|
|||
double values[STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; |
|||
|
|||
int row = 0; |
|||
int col = 0; |
|||
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { |
|||
values[i] = static_cast<double>(i + 1); |
|||
|
|||
gmmPreMatrix(row, col) = values[i]; |
|||
++col; |
|||
if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
gmm::copy(gmmPreMatrix, gmmSparseMatrix); |
|||
|
|||
auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix); |
|||
|
|||
ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); |
|||
row = 0; |
|||
col = 0; |
|||
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { |
|||
ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col)); |
|||
++col; |
|||
if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
} |
|||
|
|||
TEST(StormAdapterTest, SimpleSparseSquareCopy) { |
|||
// 5 rows
|
|||
gmm::csr_matrix<double> gmmSparseMatrix; |
|||
|
|||
/*
|
|||
* As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy. |
|||
*/ |
|||
gmm::row_matrix<gmm::wsvector<double>> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
|
|||
double values[STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; |
|||
|
|||
int row = 0; |
|||
int col = 0; |
|||
|
|||
bool everySecondElement = true; |
|||
|
|||
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { |
|||
values[i] = static_cast<double>(i + 1); |
|||
if (everySecondElement) { |
|||
gmmPreMatrix(row, col) = values[i]; |
|||
} |
|||
everySecondElement = !everySecondElement; |
|||
++col; |
|||
if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
gmm::copy(gmmPreMatrix, gmmSparseMatrix); |
|||
|
|||
auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix); |
|||
|
|||
ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); |
|||
ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), (STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); |
|||
|
|||
|
|||
row = 0; |
|||
col = 0; |
|||
everySecondElement = true; |
|||
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { |
|||
if (everySecondElement) { |
|||
ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col)); |
|||
} |
|||
everySecondElement = !everySecondElement; |
|||
++col; |
|||
if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { |
|||
++row; |
|||
col = 0; |
|||
} |
|||
} |
|||
} |
Write
Preview
Loading…
Cancel
Save
Reference in new issue