minor stuff, some more pmdp examples and an mdp test case

Former-commit-id: f48e308e5f

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<range) -> 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<right) -> 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
+

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<range) -> 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<right) -> 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
+

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<range) -> 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<right) -> 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
+

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<range) -> 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<right) -> 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
+

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<range) -> 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<right) -> 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
+

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<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,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
+

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<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,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
+

src/modelchecker/region/AbstractSparseRegionModelChecker.cpp

@@ -87,7 +87,7 @@ namespace storm {
             template<typename ParametricSparseModelType, typename ConstantType>
             void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifyFormula(std::shared_ptr<storm::logic::Formula> 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()) {

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::SparseMatrix<ParametricType>const& matrix=this->getModel().getTransitionMatrix();
+                uint_fast64_t stateCounter=0;
+                for (uint_fast64_t state=0; state<this->getModel().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<ParametricSparseModelType>(this->getModel()); //Note: an actual copy is technically not necessary.. but we will do it here..
                 simpleFormula = this->getSpecifiedFormula();

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();
 }
 

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<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
+    program->checkValidity();
+    storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
+    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = formulaParser.parseFromString(formulaAsString);
+    typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+    options.addConstantDefinitionsFromString(program.get(), constantsAsString); 
+    options.preserveFormula(*formulas[0]);
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
+    ASSERT_EQ(storm::models::ModelType::Mdp, model->getType());
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = model->template as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> modelchecker(*mdp);
+    ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
+    modelchecker.specifyFormula(formulas[0]);
+    
+    //start testing
+    auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p<=0.4,0.2<=q<=0.4");
+    auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p<=0.65,0.5<=q<=0.7");
+    auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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