The variable pool of carl needs to be cleared after executing a test.

Sampling for mdps now uses the policy of the previous iteration as initial guess


Former-commit-id: 3b8b25f30f

src/modelchecker/region/ApproximationModel.cpp

@@ -70,6 +70,9 @@ namespace storm {
                 
                 this->solverData.result = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one<ConstantType>() : ConstantType(0.5));
                 this->solverData.initialStateIndex = newIndices[initialState];
+                this->solverData.lastMinimizingPolicy = Policy(this->matrixData.matrix.getRowGroupCount(), 0);
+                this->solverData.lastMaximizingPolicy = Policy(this->matrixData.matrix.getRowGroupCount(), 0);
+                this->solverData.lastPlayer1Policy = Policy(this->matrixData.matrix.getRowGroupCount(), 0);
             }                
 
             template<typename ParametricSparseModelType, typename ConstantType>
@@ -272,10 +275,6 @@ namespace storm {
                 instantiate(region, computeLowerBounds);
                 Policy& policy = computeLowerBounds ? this->solverData.lastMinimizingPolicy : this->solverData.lastMaximizingPolicy;
                 //TODO: at this point, set policy to the one stored in the region.
-                if(policy.empty()){
-                    //No guess available (yet)
-                    policy = Policy(this->matrixData.matrix.getRowGroupCount(), 0);
-                }
                 invokeSolver(computeLowerBounds, policy);
                 
                 //TODO: policy for games.

src/modelchecker/region/SamplingModel.cpp

@@ -26,7 +26,7 @@ namespace storm {
         namespace region {
         
             template<typename ParametricSparseModelType, typename ConstantType>
-            SamplingModel<ParametricSparseModelType, ConstantType>::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula> formula) : solveGoal(storm::logic::isLowerBound(formula->getComparisonType())){
+            SamplingModel<ParametricSparseModelType, ConstantType>::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula> formula){
                 //First some simple checks and initializations..
                 if(formula->isProbabilityOperatorFormula()){
                     this->computeRewards=false;
@@ -38,6 +38,7 @@ namespace storm {
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << formula << ". Sampling model only supports eventually or reachability reward formulae.");
                 }
+                this->solverData.solveGoal = storm::solver::SolveGoal(storm::logic::isLowerBound(formula->getComparisonType()));
                 STORM_LOG_THROW(parametricModel.hasLabel("target"), storm::exceptions::InvalidArgumentException, "The given Model has no \"target\"-statelabel.");
                 this->targetStates = parametricModel.getStateLabeling().getStates("target");
                 STORM_LOG_THROW(parametricModel.hasLabel("sink"), storm::exceptions::InvalidArgumentException, "The given Model has no \"sink\"-statelabel.");
@@ -63,8 +64,9 @@ namespace storm {
                 this->matrixData.assignment.shrink_to_fit();
                 this->vectorData.assignment.shrink_to_fit();
                 
-                this->eqSysResult = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one<ConstantType>() : ConstantType(0.5));
-                this->eqSysInitIndex = newIndices[initialState];
+                this->solverData.result = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one<ConstantType>() : ConstantType(0.5));
+                this->solverData.initialStateIndex = newIndices[initialState];
+                this->solverData.lastPolicy = Policy(this->matrixData.matrix.getRowGroupCount(), 0);
             }
             
             template<typename ParametricSparseModelType, typename ConstantType>
@@ -209,7 +211,7 @@ namespace storm {
                 instantiate(point);
                 invokeSolver();
                 std::vector<ConstantType> result(this->maybeStates.size());
-                storm::utility::vector::setVectorValues(result, this->maybeStates, this->eqSysResult);
+                storm::utility::vector::setVectorValues(result, this->maybeStates, this->solverData.result);
                 storm::utility::vector::setVectorValues(result, this->targetStates, this->computeRewards ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>());
                 storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>());
                 
@@ -220,7 +222,7 @@ namespace storm {
             ConstantType SamplingModel<ParametricSparseModelType, ConstantType>::computeInitialStateValue(std::map<VariableType, CoefficientType>const& point) {
                 instantiate(point);
                 invokeSolver();
-                return this->eqSysResult[this->eqSysInitIndex];
+                return this->solverData.result[this->solverData.initialStateIndex];
             }
             
             template<typename ParametricSparseModelType, typename ConstantType>
@@ -247,16 +249,14 @@ namespace storm {
             template<>
             void SamplingModel<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::invokeSolver(){
                 std::unique_ptr<storm::solver::LinearEquationSolver<double>> solver = storm::utility::solver::LinearEquationSolverFactory<double>().create(this->matrixData.matrix);
-                solver->solveEquationSystem(this->eqSysResult, this->vectorData.vector);
+                solver->solveEquationSystem(this->solverData.result, this->vectorData.vector);
             }
             template<>
             void SamplingModel<storm::models::sparse::Mdp<storm::RationalFunction>, double>::invokeSolver(){
-                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> solver = storm::solver::configureMinMaxLinearEquationSolver(this->solveGoal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
-                if(!this->solveGoal.minimize()){
-                    //The value iteration method is not correct if the value is maximized and the initial x-vector is not <= the actual probability/reward.
-                    this->eqSysResult.assign(this->eqSysResult.size(), storm::utility::zero<double>());
-                }
-                solver->solveEquationSystem(this->eqSysResult, this->vectorData.vector);
+                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> solver = storm::solver::configureMinMaxLinearEquationSolver(this->solverData.solveGoal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
+                solver->setPolicyTracking();
+                solver->solveEquationSystem(this->solverData.solveGoal.direction(), this->solverData.result, this->vectorData.vector, nullptr, nullptr, &this->solverData.lastPolicy);
+                this->solverData.lastPolicy = solver->getPolicy();
             }
             
             

src/modelchecker/region/SamplingModel.h

@@ -51,24 +51,28 @@ namespace storm {
                 ConstantType computeInitialStateValue(std::map<VariableType, CoefficientType>const& point);
 
             private:
-
                 typedef typename std::unordered_map<ParametricType, ConstantType>::value_type FunctionEntry;
+                typedef std::vector<storm::storage::sparse::state_type> Policy;
+                
                 void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector<std::size_t> const& newIndices);
                 void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector<std::size_t> const& newIndices);
                 void instantiate(std::map<VariableType, CoefficientType>const& point);
                 void invokeSolver();
                 
-                //Some designated states in the original model
-                storm::storage::BitVector targetStates, maybeStates;
-                //The last result of the solving the equation system. Also serves as first guess for the next call.
-                //Note: eqSysResult.size==maybeStates.numberOfSetBits
-                std::vector<ConstantType> eqSysResult;
-                //The index which represents the result for the initial state in the eqSysResult vector
-                std::size_t eqSysInitIndex;
                 //A flag that denotes whether we compute probabilities or rewards
                 bool computeRewards;
-                //The goal we want to accomplish when solving the eq sys.
-                storm::solver::SolveGoal solveGoal;
+                
+                //Some designated states in the original model
+                storm::storage::BitVector targetStates, maybeStates;
+                
+                struct SolverData{
+                    //The result from the previous instantiation. Serve as first guess for the next call.
+                    std::vector<ConstantType> result; //Note: result.size==maybeStates.numberOfSetBits
+                    std::size_t initialStateIndex; //The index which represents the result for the initial state in the result vector
+                    //The following is only relevant if we consider mdps:
+                    storm::solver::SolveGoal solveGoal = storm::solver::SolveGoal(true); //No default cunstructor for solve goal...
+                    Policy lastPolicy; //best policy from the previous instantiation. Serves as first guess for the next call.
+                } solverData;
                 
 
                 /* The data required for the equation system, i.e., a matrix and a vector.

test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

@@ -87,10 +87,10 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
     
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
-    
     std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm";
     std::string const& formulaAsString = "R>2.5 [F \"target\" ]";
     std::string const& constantsAsString = "pL=0.9,TOAck=0.5";
@@ -178,8 +178,8 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
     modelchecker.checkRegion(exBothHardRegionSmt);
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
     
-    
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
@@ -226,6 +226,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
     
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
@@ -289,6 +290,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
     
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
@@ -377,6 +379,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
     
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
@@ -442,6 +445,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
     
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
@@ -490,6 +494,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
 //smt    EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
 
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 #endif

test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp

@@ -66,6 +66,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
     EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
 
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
@@ -94,11 +95,11 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
     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.4<=p<=0.7,0.55<=q<=0.6");
 
-    EXPECT_NEAR(0.9512773402, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
+    EXPECT_NEAR(0.95127874851, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
     EXPECT_NEAR(0.26787251126, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()),  storm::settings::generalSettings().getPrecision());
-    EXPECT_NEAR(0.41879628383, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
+    EXPECT_NEAR(0.41880006098, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
     EXPECT_NEAR(0.01535089684, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()),  storm::settings::generalSettings().getPrecision());
-    EXPECT_NEAR(0.24952471590, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
+    EXPECT_NEAR(0.24952791523, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision());
     EXPECT_NEAR(0.01711494956, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()),  storm::settings::generalSettings().getPrecision());
    
     //test approximative method
@@ -114,6 +115,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
     EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
 
     storm::settings::mutableRegionSettings().resetModes();
+    carl::VariablePool::getInstance().clear();
 }
 
 #endif