From d26f38b9a26d506773910f8006f0268c109882f3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 13 Sep 2015 19:24:52 +0200 Subject: [PATCH] minor stuff, some more pmdp examples and an mdp test case Former-commit-id: f48e308e5f132672022916d0d1cca5be61442ffc --- examples/pmdp/consensus/coin2_1024.nm | 65 +++++++++++++++++ examples/pmdp/consensus/coin2_64.nm | 65 +++++++++++++++++ examples/pmdp/consensus/coin2_8.nm | 65 +++++++++++++++++ examples/pmdp/consensus/coin4_2.nm | 67 +++++++++++++++++ examples/pmdp/consensus/coin4_8.nm | 67 +++++++++++++++++ examples/pmdp/consensus/coin6_2.nm | 69 ++++++++++++++++++ examples/pmdp/consensus/coin6_8.nm | 70 ++++++++++++++++++ .../AbstractSparseRegionModelChecker.cpp | 2 +- .../region/SparseMdpRegionModelChecker.cpp | 24 ++++++- .../SparseDtmcRegionModelCheckerTest.cpp | 1 - .../SparseMdpRegionModelCheckerTest.cpp | 71 +++++++++++++++++++ 11 files changed, 563 insertions(+), 3 deletions(-) create mode 100644 examples/pmdp/consensus/coin2_1024.nm create mode 100644 examples/pmdp/consensus/coin2_64.nm create mode 100644 examples/pmdp/consensus/coin2_8.nm create mode 100644 examples/pmdp/consensus/coin4_2.nm create mode 100644 examples/pmdp/consensus/coin4_8.nm create mode 100644 examples/pmdp/consensus/coin6_2.nm create mode 100644 examples/pmdp/consensus/coin6_8.nm create mode 100644 test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp diff --git a/examples/pmdp/consensus/coin2_1024.nm b/examples/pmdp/consensus/coin2_1024.nm new file mode 100644 index 000000000..c45370e98 --- /dev/null +++ b/examples/pmdp/consensus/coin2_1024.nm @@ -0,0 +1,65 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K=1024; +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; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin2_64.nm b/examples/pmdp/consensus/coin2_64.nm new file mode 100644 index 000000000..c2fe236c1 --- /dev/null +++ b/examples/pmdp/consensus/coin2_64.nm @@ -0,0 +1,65 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K=64; +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; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin2_8.nm b/examples/pmdp/consensus/coin2_8.nm new file mode 100644 index 000000000..9bc7e590c --- /dev/null +++ b/examples/pmdp/consensus/coin2_8.nm @@ -0,0 +1,65 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K=8; +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; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin4_2.nm b/examples/pmdp/consensus/coin4_2.nm new file mode 100644 index 000000000..f0e534ee4 --- /dev/null +++ b/examples/pmdp/consensus/coin4_2.nm @@ -0,0 +1,67 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=4; +const int K=2; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin4_8.nm b/examples/pmdp/consensus/coin4_8.nm new file mode 100644 index 000000000..5acd2c6fa --- /dev/null +++ b/examples/pmdp/consensus/coin4_8.nm @@ -0,0 +1,67 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=4; +const int K=8; +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; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin6_2.nm b/examples/pmdp/consensus/coin6_2.nm new file mode 100644 index 000000000..b9f9c1467 --- /dev/null +++ b/examples/pmdp/consensus/coin6_2.nm @@ -0,0 +1,69 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=6; +const int K=2; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule +module process5 = process1[pc1=pc5,coin1=coin5] endmodule +module process6 = process1[pc1=pc6,coin1=coin6,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=4 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/coin6_8.nm b/examples/pmdp/consensus/coin6_8.nm new file mode 100644 index 000000000..15f429865 --- /dev/null +++ b/examples/pmdp/consensus/coin6_8.nm @@ -0,0 +1,70 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=6; +const int K=8; +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; + +//Coin Probabilities +const double p; +const double q; + +// 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) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule +module process3 = process1[pc1=pc3,coin1=coin3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule +module process5 = process1[pc1=pc5,coin1=coin5] endmodule +module process6 = process1[pc1=pc6,coin1=coin6,p=q] 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 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=4 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index a03506db1..f787207a0 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -87,7 +87,7 @@ namespace storm { template void AbstractSparseRegionModelChecker::specifyFormula(std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Specifying the formula " << formula); + STORM_LOG_DEBUG("Specifying the formula " << *formula.get()); STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled."); //Initialize the context for this formula if (formula->isProbabilityOperatorFormula()) { diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index d0c2da693..8ae59ce99 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -76,7 +76,29 @@ namespace storm { STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); storm::storage::BitVector maybeStates, targetStates; preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult); - //TODO: Actually get a more simple model. This makes a deep copy of the model... + + //lets count the number of states without nondet choices and with constant outgoing transitions + //TODO: Remove this + storm::storage::SparseMatrixconst& matrix=this->getModel().getTransitionMatrix(); + uint_fast64_t stateCounter=0; + for (uint_fast64_t state=0; stategetModel().getNumberOfStates();++state){ + if(matrix.getRowGroupSize(state)==1){ + bool hasConstTransitions=true; + for(auto const& entry : matrix.getRowGroup(state)){ + if(!storm::utility::isConstant(entry.getValue())){ + hasConstTransitions = false; + } + } + if(hasConstTransitions){ + ++stateCounter; + } + } + } + std::cout << "Found that " << stateCounter << " of " << this->getModel().getNumberOfStates() << " states could be eliminated" << std::endl; + + + + //TODO: Actually eliminate the states... STORM_LOG_WARN("No simplification of the original model (like elimination of constant transitions) is happening. Will just use a copy of the original model"); simpleModel = std::make_shared(this->getModel()); //Note: an actual copy is technically not necessary.. but we will do it here.. simpleFormula = this->getSpecifiedFormula(); diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index e5f3a213a..b36eb24f8 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -489,7 +489,6 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { modelchecker.checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - std::cout << "End" << std::endl; storm::settings::mutableRegionSettings().resetModes(); } diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp new file mode 100644 index 000000000..19a8ba486 --- /dev/null +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -0,0 +1,71 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_CARL + +#include "src/adapters/CarlAdapter.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/RegionSettings.h" + +#include "src/models/sparse/Dtmc.h" +#include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/models/ModelBase.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "builder/ExplicitPrismModelBuilder.h" +#include "modelchecker/region/SparseMdpRegionModelChecker.h" +#include "modelchecker/region/ParameterRegion.h" + +TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pmdp/consensus/coin2_2.nm"; + std::string const& formulaAsString = "P>0.25 [F \"finish_with_1\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + //Build model, formula, region model checker + boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); + program->checkValidity(); + storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); + std::vector> formulas = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); + ASSERT_EQ(storm::models::ModelType::Mdp, model->getType()); + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::region::SparseMdpRegionModelChecker, double> modelchecker(*mdp); + ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); + modelchecker.specifyFormula(formulas[0]); + + //start testing + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=p<=0.4,0.2<=q<=0.4"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p<=0.65,0.5<=q<=0.7"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=p<=0.75,0.7<=q<=0.72"); + + EXPECT_NEAR(0.9512773402, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7455934939, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.4187982158, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.01535089684, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.01711494956, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.004422535374, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + + //test approximative method + storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); + ASSERT_TRUE(storm::settings::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(allSatRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + +#endif \ No newline at end of file