reimplemented region model check via smt solving

Former-commit-id: 38a75413a5

src/adapters/Smt2ExpressionAdapter.h

@@ -68,6 +68,19 @@ namespace storm {
              */
             std::string translateExpression(carl::Constraint<storm::RawPolynomial> const& constraint) {
                                 
+                return  "(" + carl::toString(constraint.rel()) + " " +
+                            constraint.lhs().toString(false, useReadableVarNames) + " " +
+                            "0 " +
+                        ")";
+            }
+            /*!
+             * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
+			 
+             * @param constraint
+             * @return An equivalent expression for Smt2.
+             */
+            std::string translateExpression(carl::Constraint<storm::Polynomial> const& constraint) {
+                                
                 return  "(" + carl::toString(constraint.rel()) + " " +
                             constraint.lhs().toString(false, useReadableVarNames) + " " +
                             "0 " +

src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp

@@ -32,13 +32,13 @@ namespace storm {
         }
 
         template<typename ParametricType, typename ConstantType>        
-        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setUnSatPoint(std::map<VariableType, BoundType> const& unSatPoint) {
-            this->unSatPoint = unSatPoint;
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setViolatedPoint(std::map<VariableType, BoundType> const& violatedPoint) {
+            this->violatedPoint = violatedPoint;
         }
         
         template<typename ParametricType, typename ConstantType>
-        std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getUnSatPoint() const {
-            return unSatPoint;
+        std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getViolatedPoint() const {
+            return violatedPoint;
         }
         
         template<typename ParametricType, typename ConstantType>
@@ -55,14 +55,14 @@ namespace storm {
         void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setCheckResult(RegionCheckResult checkResult) {
             //a few sanity checks
             STORM_LOG_THROW((this->checkResult==RegionCheckResult::UNKNOWN || checkResult!=RegionCheckResult::UNKNOWN),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from something known to UNKNOWN ");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSSAT || checkResult!=RegionCheckResult::EXISTSUNSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSUNSAT");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSSAT || checkResult!=RegionCheckResult::ALLUNSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to ALLUNSAT");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSUNSAT || checkResult!=RegionCheckResult::EXISTSSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSUNSAT to EXISTSSAT");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSUNSAT || checkResult!=RegionCheckResult::ALLSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSUNSAT to ALLSAT");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSSAT || checkResult!=RegionCheckResult::EXISTSVIOLATED),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSVIOLATED");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSSAT || checkResult!=RegionCheckResult::ALLVIOLATED),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to ALLVIOLATED");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSVIOLATED || checkResult!=RegionCheckResult::EXISTSSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to EXISTSSAT");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSVIOLATED || checkResult!=RegionCheckResult::ALLSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to ALLSAT");
             STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSBOTH || checkResult!=RegionCheckResult::ALLSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLSAT");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSBOTH || checkResult!=RegionCheckResult::ALLUNSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLUNSAT");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::EXISTSBOTH || checkResult!=RegionCheckResult::ALLVIOLATED),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLVIOLATED");
             STORM_LOG_THROW((this->checkResult!=RegionCheckResult::ALLSAT || checkResult==RegionCheckResult::ALLSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLSAT to something else");
-            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::ALLUNSAT || checkResult==RegionCheckResult::ALLUNSAT),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLUNSAT to something else");
+            STORM_LOG_THROW((this->checkResult!=RegionCheckResult::ALLVIOLATED || checkResult==RegionCheckResult::ALLVIOLATED),storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLVIOLATED to something else");
             this->checkResult = checkResult;
         }
 
@@ -96,6 +96,16 @@ namespace storm {
             return (*result).second;
         }
 
+        template<typename ParametricType, typename ConstantType>
+        const std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getUpperBounds() const {
+            return upperBounds;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        const std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getLowerBounds() const {
+            return lowerBounds;
+        }
+        
         template<typename ParametricType, typename ConstantType>
         std::vector<std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType>> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const{
             std::size_t const numOfVariables=consideredVariables.size();
@@ -131,14 +141,14 @@ namespace storm {
                     return "unknown";
                 case RegionCheckResult::EXISTSSAT:
                     return "ExistsSat";
-                case RegionCheckResult::EXISTSUNSAT:
-                    return "ExistsUnsat";
+                case RegionCheckResult::EXISTSVIOLATED:
+                    return "ExistsViolated";
                 case RegionCheckResult::EXISTSBOTH:
                     return "ExistsBoth";
                 case RegionCheckResult::ALLSAT:
                     return "allSat";
-                case RegionCheckResult::ALLUNSAT:
-                    return "allUnsat";
+                case RegionCheckResult::ALLVIOLATED:
+                    return "allViolated";
             }
             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not identify check result")
             return "ERROR";
@@ -164,7 +174,7 @@ namespace storm {
         
         
         template<typename ParametricType, typename ConstantType>
-        SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) : model(model), eliminationModelChecker(model), probabilityOperatorFormula(nullptr) {
+        SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) : model(model), eliminationModelChecker(model), smtSolver(nullptr), probabilityOperatorFormula(nullptr) {
             // Intentionally left empty.
         }
         
@@ -254,6 +264,8 @@ namespace storm {
       //      std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl;
             std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now();
             
+            initializeSMTSolver(this->smtSolver, this->reachProbFunction,*this->probabilityOperatorFormula);
+            
             //some information for statistics...
             std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
             this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart;
@@ -367,6 +379,56 @@ namespace storm {
             return workingCopyOneStepProbs[initState];
         }
 
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeSMTSolver(std::shared_ptr<storm::solver::Smt2SmtSolver>& solver, const ParametricType& reachProbFunction, const storm::logic::ProbabilityOperatorFormula& formula) {
+                    
+            storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
+            solver = std::shared_ptr<storm::solver::Smt2SmtSolver>(new storm::solver::Smt2SmtSolver(manager, true));
+            
+            ParametricType bound= storm::utility::regions::convertNumber<double, ParametricType>(this->probabilityOperatorFormula->getBound());
+            std::cout << "bound is " << bound << std::endl;
+            
+            // To prove that the property is satisfied in the initial state for all parameters,
+            // we ask the solver whether the negation of the property is satisfiable and invert the answer.
+            // In this case, assert that this variable is true:
+            VariableType proveAllSatVar=storm::utility::regions::getNewVariable<VariableType>("proveAllSat", storm::utility::regions::VariableSort::VS_BOOL);
+            
+            //Example:
+            //Property:    P<=p [ F 'target' ] holds iff...
+            // f(x)         <= p
+            // Hence: If  f(x) > p is unsat, the property is satisfied for all parameters.
+            
+            storm::logic::ComparisonType proveAllSatRel; //the relation from the property needs to be inverted
+            switch (this->probabilityOperatorFormula->getComparisonType()) {
+                case storm::logic::ComparisonType::Greater:
+                    proveAllSatRel=storm::logic::ComparisonType::LessEqual;
+                    break;
+                case storm::logic::ComparisonType::GreaterEqual:
+                    proveAllSatRel=storm::logic::ComparisonType::Less;
+                    break;
+                case storm::logic::ComparisonType::Less:
+                    proveAllSatRel=storm::logic::ComparisonType::GreaterEqual;
+                    break;
+                case storm::logic::ComparisonType::LessEqual:
+                    proveAllSatRel=storm::logic::ComparisonType::Greater;
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+            }
+            storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, this->reachProbFunction, proveAllSatRel, bound);
+            
+            // To prove that the property is violated in the initial state for all parameters,
+            // we ask the solver whether the the property is satisfiable and invert the answer.
+            // In this case, assert that this variable is true:
+            VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable<VariableType>("proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL);        
+            
+            //Example:
+            //Property:    P<=p [ F 'target' ] holds iff...
+            // f(x)         <= p
+            // Hence: If f(x)  <= p is unsat, the property is violated for all parameters. 
+            storm::logic::ComparisonType proveAllViolatedRel = this->probabilityOperatorFormula->getComparisonType();
+            storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllViolatedVar, this->reachProbFunction, proveAllViolatedRel, bound);          
+        }
 
 
 
@@ -396,7 +458,7 @@ namespace storm {
                     STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through approximation.");
                     doSampling=false;
                     doSubsystemSmt=false;
-                    doFullSmt=false;
+                    doFullSmt=true; //TODO set this back to false.. this is just for testing
                 }
             }
             std::chrono::high_resolution_clock::time_point timeApproximationEnd = std::chrono::high_resolution_clock::now();
@@ -410,7 +472,7 @@ namespace storm {
                     STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through sampling.");
                     doApproximation=false;
                     doSubsystemSmt=false;
-                    doFullSmt=false;
+                    doFullSmt=true;//TODO set this back to false.. this is just for testing
                 }
             }
             std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now();
@@ -423,12 +485,19 @@ namespace storm {
             
             std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now();
             if(doFullSmt){
-                STORM_LOG_WARN("FullSmt approach not yet implemented");
+                STORM_LOG_DEBUG("Checking with Smt Solving...");
+                std::cout << "  Checking with Smt Solving..." << std::endl;
+                if(checkFullSmt(region)){
+                    ++this->numOfRegionsSolvedThroughFullSmt;
+                    STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through Smt Solving.");
+                    doApproximation=false;
+                    doSampling=false;
+                    doSubsystemSmt=false;
+                }
             }
             std::chrono::high_resolution_clock::time_point timeFullSmtEnd = std::chrono::high_resolution_clock::now();
             
             
-            
             //some information for statistics...
             std::chrono::high_resolution_clock::time_point timeCheckRegionEnd = std::chrono::high_resolution_clock::now();
             this->timeCheckRegion += timeCheckRegionEnd-timeCheckRegionStart;
@@ -449,14 +518,31 @@ namespace storm {
         template<typename ParametricType, typename ConstantType>
         bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkSamplePoints(ParameterRegion& region) {
             
-            auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //only test the 4 corner points (for now)
-            
+            auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points
             for (auto const& point : samplingPoints){
+                if(checkPoint(region, point, true)){
+                    return true;
+                }            
+            }
+            return false;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, BoundType>const& point, bool viaReachProbFunction) {
+            
             // check whether the property is satisfied or not at the given point
-                if(this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(this->reachProbFunction, point))){
+            bool valueInBoundOfFormula;
+            if(viaReachProbFunction){
+                valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(this->reachProbFunction, point));
+            }
+            else{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "sample point check with model instantiation not yet implemented");
+            }
+                
+            if(valueInBoundOfFormula){
                 if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){
                     region.setSatPoint(point);
-                        if(region.getCheckResult()==RegionCheckResult::EXISTSUNSAT){
+                    if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){
                         region.setCheckResult(RegionCheckResult::EXISTSBOTH);
                         return true;
                     }
@@ -464,14 +550,13 @@ namespace storm {
                 }
             }
             else{
-                    if (region.getCheckResult()!=RegionCheckResult::EXISTSUNSAT){
-                        region.setUnSatPoint(point);
+                if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){
+                    region.setViolatedPoint(point);
                     if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){
                         region.setCheckResult(RegionCheckResult::EXISTSBOTH);
                         return true;
                     }
-                        region.setCheckResult(RegionCheckResult::EXISTSUNSAT);
-                    }
+                    region.setCheckResult(RegionCheckResult::EXISTSVIOLATED);
                 }
             }
             return false;
@@ -500,11 +585,11 @@ namespace storm {
                         case RegionCheckResult::UNKNOWN: 
                             firstOpType=storm::logic::OptimalityType::Minimize;
                             break;
-                        case RegionCheckResult::EXISTSUNSAT:
+                        case RegionCheckResult::EXISTSVIOLATED:
                             firstOpType=storm::logic::OptimalityType::Maximize;
                             break;
                         default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSUNSAT or UNKNOWN");
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN");
                     }
                     break;
                 case storm::logic::ComparisonType::Less:
@@ -514,11 +599,11 @@ namespace storm {
                         case RegionCheckResult::UNKNOWN: 
                             firstOpType=storm::logic::OptimalityType::Maximize;
                             break;
-                        case RegionCheckResult::EXISTSUNSAT:
+                        case RegionCheckResult::EXISTSVIOLATED:
                             firstOpType=storm::logic::OptimalityType::Minimize;
                             break;
                         default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSUNSAT or UNKNOWN");
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN");
                     }
                     break;
                 default:
@@ -544,7 +629,7 @@ namespace storm {
                     else{
                         if((this->probabilityOperatorFormula->getComparisonType()== storm::logic::ComparisonType::Greater) || 
                                 (this->probabilityOperatorFormula->getComparisonType()== storm::logic::ComparisonType::GreaterEqual)){
-                            region.setCheckResult(RegionCheckResult::ALLUNSAT);
+                            region.setCheckResult(RegionCheckResult::ALLVIOLATED);
                             return true;
                         }
                     }
@@ -564,7 +649,7 @@ namespace storm {
                     else{
                         if((this->probabilityOperatorFormula->getComparisonType()== storm::logic::ComparisonType::Less) || 
                                 (this->probabilityOperatorFormula->getComparisonType()== storm::logic::ComparisonType::LessEqual)){
-                            region.setCheckResult(RegionCheckResult::ALLUNSAT);
+                            region.setCheckResult(RegionCheckResult::ALLVIOLATED);
                             return true;
                         }
                     }                
@@ -697,15 +782,93 @@ namespace storm {
 
         
         
+        template<typename ParametricType, typename ConstantType>
+        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkFullSmt(ParameterRegion& region) {
+            if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
+                //Sampling needs to be done (on a single point)
+                checkPoint(region,region.getLowerBounds(), true);
+            }
             
+            this->smtSolver->push();
             
+            //add constraints for the region
+            for(auto const& variable : region.getVariables()) {
+                storm::utility::regions::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBound(variable));
+                storm::utility::regions::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBound(variable));
+            }
             
+            //add constraint that states what we want to prove            
+            VariableType proveAllSatVar=storm::utility::regions::getVariableFromString<VariableType>("proveAllSat");     
+            VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString<VariableType>("proveAllViolated");     
+            switch(region.getCheckResult()){
+                case RegionCheckResult::EXISTSBOTH:
+                    STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkFullSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now...");
+                case RegionCheckResult::ALLSAT:
+                    STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLSAT), "checkFullSmt invoked although the result is already clear (ALLSAT). Will validate this now...");
+                case RegionCheckResult::EXISTSSAT:
+                    storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, true);
+                    storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, false);
+                    break;
+                case RegionCheckResult::ALLVIOLATED:
+                    STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLVIOLATED), "checkFullSmt invoked although the result is already clear (ALLVIOLATED). Will validate this now...");
+                case RegionCheckResult::EXISTSVIOLATED:
+                    storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, false);
+                    storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, true);
+                    break;
+                default:
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not handle the current region CheckResult: " << region.checkResultToString());
+            }
             
+            storm::solver::SmtSolver::CheckResult solverResult= this->smtSolver->check();
+            this->smtSolver->pop();
             
-        
-        
-        
-        
+            switch(solverResult){
+                case storm::solver::SmtSolver::CheckResult::Sat:
+                    switch(region.getCheckResult()){
+                        case RegionCheckResult::EXISTSSAT:
+                            region.setCheckResult(RegionCheckResult::EXISTSBOTH);
+                            //There is also a violated point
+                            STORM_LOG_WARN("Extracting a violated point from the smt solver is not yet implemented!");
+                            break;
+                        case RegionCheckResult::EXISTSVIOLATED:
+                            region.setCheckResult(RegionCheckResult::EXISTSBOTH);
+                            //There is also a sat point
+                            STORM_LOG_WARN("Extracting a sat point from the smt solver is not yet implemented!");
+                            break;
+                        case RegionCheckResult::EXISTSBOTH:
+                            //That was expected
+                            STORM_LOG_WARN("result EXISTSBOTH Validated!");
+                            break;
+                        default:
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (sat)");
+                    }
+                    return true;
+                case storm::solver::SmtSolver::CheckResult::Unsat:
+                    switch(region.getCheckResult()){
+                        case RegionCheckResult::EXISTSSAT:
+                            region.setCheckResult(RegionCheckResult::ALLSAT);
+                            break;
+                        case RegionCheckResult::EXISTSVIOLATED:
+                            region.setCheckResult(RegionCheckResult::ALLVIOLATED);
+                            break;
+                        case RegionCheckResult::ALLSAT:
+                            //That was expected...
+                            STORM_LOG_WARN("result ALLSAT Validated!");
+                            break;
+                        case RegionCheckResult::ALLVIOLATED:
+                            //That was expected...
+                            STORM_LOG_WARN("result ALLVIOLATED Validated!");
+                            break;
+                        default:
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (unsat)");
+                    }
+                    return true;
+                case storm::solver::SmtSolver::CheckResult::Unknown:
+                default:
+                    STORM_LOG_WARN("The SMT solver was not able to compute a result for this region");
+                    return false;
+            }
+        }
 
         
 
@@ -1204,6 +1367,7 @@ namespace storm {
             std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSampling);
             std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeApproximation);
             std::chrono::milliseconds timeMDPBuildInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeMDPBuild);
+            std::chrono::milliseconds timeFullSmtInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeFullSmt);
             
             std::chrono::high_resolution_clock::duration timeOverall = timePreprocessing + timeCheckRegion; // + ...
             std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(timeOverall);
@@ -1222,7 +1386,7 @@ namespace storm {
             outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl;
             outstream << (this->hasOnlyLinearFunctions ? "A" : "Not a") << "ll occuring functions in the model are linear" << std::endl;
             outstream << "Number of checked regions: " << this->numOfCheckedRegions << " with..." << std::endl;
-            outstream << "  " << this->numOfRegionsSolvedThroughSampling << " regions solved through sampling" << std::endl;
+            outstream << "  " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
             outstream << "  " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl;
             outstream << "  " << this->numOfRegionsSolvedThroughSubsystemSmt << " regions solved through SubsystemSmt" << std::endl;
             outstream << "  " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl;
@@ -1235,7 +1399,7 @@ namespace storm {
             outstream << "    " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
             outstream << "    " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl;
             outstream << "      " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl;
-            //outstream << "  " << timeInMilliseconds.count() << "ms " << std::endl;
+            outstream << "    " << timeFullSmtInMilliseconds.count() << "ms Full Smt solving" << std::endl;
             outstream << "-----------------------------------------------" << std::endl;
             
         }

src/modelchecker/reachability/SparseDtmcRegionModelChecker.h

@@ -28,10 +28,10 @@ namespace storm {
             enum class RegionCheckResult { 
                 UNKNOWN, /*!< the result is unknown */
                 EXISTSSAT, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
-                EXISTSUNSAT, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
+                EXISTSVIOLATED, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
                 EXISTSBOTH, /*!< the formula is satisfied for some parameters but also violated for others */
                 ALLSAT, /*!< the formula is satisfied for all parameters in the given region */
-                ALLUNSAT /*!< the formula is violated for all parameters in the given region */
+                ALLVIOLATED /*!< the formula is violated for all parameters in the given region */
             };
             
             class ParameterRegion{
@@ -44,6 +44,8 @@ namespace storm {
                 std::set<VariableType> getVariables() const;
                 BoundType const& getLowerBound(VariableType const& variable) const;
                 BoundType const& getUpperBound(VariableType const& variable) const;
+                const std::map<VariableType, BoundType> getUpperBounds() const;
+                const std::map<VariableType, BoundType> getLowerBounds() const;
                 
                 /*
                  * Returns a vector of all possible combinations of lower and upper bounds of the given variables.
@@ -68,13 +70,13 @@ namespace storm {
                 /*!
                  * Sets a point in the region for which the considered property is not satisfied. 
                  */
-                void setUnSatPoint(std::map<VariableType, BoundType> const& unSatPoint);
+                void setViolatedPoint(std::map<VariableType, BoundType> const& violatedPoint);
                 
                 /*!
                  * Retrieves a point in the region for which is considered property is not satisfied.
                  * If such a point is not known, the returned map is empty.
                  */
-                std::map<VariableType, BoundType> getUnSatPoint() const;
+                std::map<VariableType, BoundType> getViolatedPoint() const;
                 
                 
                 /*!
@@ -94,7 +96,7 @@ namespace storm {
                 std::map<VariableType, BoundType> const upperBounds;
                 RegionCheckResult checkResult;
                 std::map<VariableType, BoundType> satPoint;
-                std::map<VariableType, BoundType> unSatPoint;
+                std::map<VariableType, BoundType> violatedPoint;
                 
                 
             };
@@ -118,7 +120,7 @@ namespace storm {
 
             /*!
              * Checks whether the given formula holds for all parameters that lie in the given region.
-             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.unSatPoint will be set.
+             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set.
              * 
              * @note A formula has to be specified first.
              * 
@@ -129,7 +131,7 @@ namespace storm {
             
             /*!
              * Checks for every given region whether the specified formula holds for all parameters that lie in that region.
-             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.unSatPoint will be set.
+             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set.
              * 
              * @note A formula has to be specified first.
              * 
@@ -216,16 +218,30 @@ namespace storm {
                 storm::storage::sparse::state_type const& initState
             );
             
+            //initializes the given solver which can later be used to give an exact result regarding the whole model.
+            void initializeSMTSolver(std::shared_ptr<storm::solver::Smt2SmtSolver>& solver, ParametricType const& reachProbFunction, storm::logic::ProbabilityOperatorFormula const& formula);
             
             /*!
-             * Checks the value of the function at some sampling points within the given region
-             * may set the satPoint and unSatPoint of the regions if they are not yet specified and such points are found
-             * Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSUNSAT, or EXISTSBOTH
+             * Checks the value of the function at some sampling points within the given region.
+             * May set the satPoint and violatedPoint of the regions if they are not yet specified and such points are found
+             * Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
              * 
-             * @return true if an unsat point as well as a sat point has been found during the process
+             * @return true if an violated point as well as a sat point has been found during the process
              */
             bool checkSamplePoints(ParameterRegion& region);
             
+            /*!
+             * Checks the value of the function at the given sampling point.
+             * May set the satPoint and violatedPoint of the regions if thy are not yet specified and such point is given.
+             * Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
+             * 
+             * @param viaReachProbFunction if set, the sampling will be done via the reachProbFunction.
+             *                             Otherwise, the model will be instantiated and checked
+             * 
+             * @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH
+             */
+            bool checkPoint(ParameterRegion& region, std::map<VariableType, BoundType>const& point, bool viaReachProbFunction=false);
+            
             /*!
              * Builds an MDP that is used to compute bounds on the maximal/minimal reachability probability,
              * If this approximation already yields that the property is satisfied/violated in the whole region,
@@ -242,6 +258,15 @@ namespace storm {
              */
             storm::models::sparse::Mdp<ConstantType> buildMdpForApproximation(ParameterRegion const& region);
             
+            /*!
+             * Starts the SMTSolver to get the result.
+             * The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
+             * Otherwise, a sampingPoint will be computed.
+             * True is returned iff the solver was successful (i.e., it returned sat or unsat)
+             * A Sat- or Violated point is set, if the solver has found one.
+             * The region checkResult of the given region is changed accordingly.
+             */
+            bool checkFullSmt(ParameterRegion& region); 
             
             
             // The model this model checker is supposed to analyze.
@@ -255,6 +280,9 @@ namespace storm {
             storm::utility::ConstantsComparator<ConstantType> constantTypeComparator;
             
             
+            std::shared_ptr<storm::solver::Smt2SmtSolver> smtSolver;
+            
+
             //the following members depend on the currently specified formula:
             
             //the currently specified formula

src/solver/Smt2SmtSolver.cpp

@@ -36,7 +36,7 @@ namespace storm {
 #ifndef WINDOWS
             processIdOfSolver=0;
 #endif
-            expressionAdapter = std::unique_ptr<storm::adapters::Smt2ExpressionAdapter>(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true));
+            this->expressionAdapter = std::unique_ptr<storm::adapters::Smt2ExpressionAdapter>(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), this->useReadableVarNames));
             init();
         }
 
@@ -90,12 +90,10 @@ namespace storm {
             writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
         }
         
-        template<>
         void Smt2SmtSolver::add(carl::Constraint<storm::RationalFunction> const& constraint) {
             add(constraint.lhs(), constraint.rel());
         }
         
-        template<>
         void Smt2SmtSolver::add(carl::Constraint<storm::RawPolynomial> const& constraint) {
             //if some of the occurring variables are not declared yet, we will have to.
             std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
@@ -106,6 +104,35 @@ namespace storm {
             writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true);
         }
         
+        void Smt2SmtSolver::add(storm::Variable const& guard, typename carl::Constraint<storm::Polynomial> const& constraint){
+            STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool.");
+            //if some of the occurring variables are not declared yet, we will have to (including the guard!).
+            std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
+            variables.insert(guard);
+            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
+            for (auto declaration : varDeclarations){
+                writeCommand(declaration, true);
+            }
+            std::string guardName= carl::VariablePool::getInstance().getName(guard, this->useReadableVarNames);
+            writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true);
+        }
+        
+        void Smt2SmtSolver::add(const storm::Variable& variable, bool value){
+            STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable.");
+            std::set<storm::Variable> variableSet;
+            variableSet.insert(variable);
+            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet);
+            for (auto declaration : varDeclarations){
+                writeCommand(declaration, true);
+            }
+            std::string varName= carl::VariablePool::getInstance().getName(variable, this->useReadableVarNames);
+            if(value){
+                writeCommand("( assert " + varName + " )", true);
+            }
+            else{
+                writeCommand("( assert (not " + varName + ") )", true);
+            }
+        }
         
 #endif
 

src/solver/Smt2SmtSolver.h

@@ -60,8 +60,14 @@ namespace storm {
             virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0));
             
             //adds the given carl constraint
-            template<typename FunctionType>
-            void add(typename carl::Constraint<FunctionType> const& constraint);
+            void add(typename carl::Constraint<storm::RationalFunction> const& constraint);
+            void add(typename carl::Constraint<storm::RawPolynomial> const& constraint);
+            
+            // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool'
+            void add(storm::Variable const& guard, typename carl::Constraint<storm::Polynomial> const& constraint);
+            
+            // asserts that the given variable has the given value. The variable should have type 'bool'
+            void add(storm::Variable const& variable, bool value);
 #endif
 
             virtual CheckResult check() override;
@@ -145,6 +151,9 @@ namespace storm {
             // A flag that states whether we want to use carl expressions.
             bool useCarlExpressions;
 
+            // A flag that states whether to use readable variable names
+            bool useReadableVarNames=true;
+            
         };
     }
 }

src/utility/regions.cpp

@@ -144,6 +144,28 @@ namespace storm {
                 return var;
             }
             
+            template<>
+            storm::Variable getNewVariable<storm::Variable>(std::string variableName, VariableSort sort){
+                storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName);
+                STORM_LOG_THROW(var==carl::Variable::NO_VARIABLE, storm::exceptions::InvalidArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use.");
+                
+                carl::VariableType carlVarType;
+                switch(sort){
+                    case VariableSort::VS_BOOL:
+                        carlVarType = carl::VariableType::VT_BOOL;
+                        break;
+                    case VariableSort::VS_REAL:
+                        carlVarType = carl::VariableType::VT_REAL;
+                        break;
+                    case VariableSort::VS_INT:
+                        carlVarType = carl::VariableType::VT_INT;
+                        break;
+                    default:
+                        STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given variable sort is not implemented");
+                }
+                return carl::VariablePool::getInstance().getFreshVariable(variableName, carlVarType);
+            }
+                      
             template<>
             std::string getVariableName<storm::Variable>(storm::Variable variable){
                 return carl::VariablePool::getInstance().getName(variable);
@@ -173,6 +195,61 @@ namespace storm {
                 function.gatherVariables(variableSet);
             }
             
+            template<>
+            void addGuardedConstraintToSmtSolver<storm::solver::Smt2SmtSolver, storm::RationalFunction, storm::Variable>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver,storm::Variable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){
+                STORM_LOG_THROW(guard.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver whose guard is not of type bool");
+                storm::CompareRelation compRel;
+                switch (relation){
+                    case storm::logic::ComparisonType::Greater:
+                        compRel=storm::CompareRelation::GT;
+                        break;
+                    case storm::logic::ComparisonType::GreaterEqual:
+                        compRel=storm::CompareRelation::GEQ;
+                        break;
+                    case storm::logic::ComparisonType::Less:
+                        compRel=storm::CompareRelation::LT;
+                        break;
+                    case storm::logic::ComparisonType::LessEqual:
+                        compRel=storm::CompareRelation::LEQ;
+                        break;
+                    default:
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+                }        
+               //Note: this only works if numerators and denominators are positive...
+                carl::Constraint<storm::Polynomial> constraint((leftHandSide.nominator() * rightHandSide.denominator()) - (rightHandSide.nominator() * leftHandSide.denominator()), compRel);
+                solver->add(guard,constraint);
+            }
+            
+            template<>
+            void addParameterBoundsToSmtSolver<storm::solver::Smt2SmtSolver, storm::Variable, cln::cl_RA>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver, storm::Variable const& variable, storm::logic::ComparisonType relation, cln::cl_RA const& bound){
+                storm::CompareRelation compRel;
+                switch (relation){
+                    case storm::logic::ComparisonType::Greater:
+                        compRel=storm::CompareRelation::GT;
+                        break;
+                    case storm::logic::ComparisonType::GreaterEqual:
+                        compRel=storm::CompareRelation::GEQ;
+                        break;
+                    case storm::logic::ComparisonType::Less:
+                        compRel=storm::CompareRelation::LT;
+                        break;
+                    case storm::logic::ComparisonType::LessEqual:
+                        compRel=storm::CompareRelation::LEQ;
+                        break;
+                    default:
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+                }
+                storm::RawPolynomial leftHandSide(variable);
+                leftHandSide -= bound;
+                solver->add(carl::Constraint<storm::RawPolynomial>(leftHandSide,compRel));
+            }
+            
+            template<>
+            void addBoolVariableToSmtSolver<storm::solver::Smt2SmtSolver, storm::Variable>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver,storm::Variable const& variable, bool value){
+                STORM_LOG_THROW(variable.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver that is a non boolean variable. Only boolean variables are allowed");
+                solver->add(variable, value);
+            }
+            
             //explicit instantiations
        template double convertNumber<double, double>(double const& number, bool const& roundDown, double const& precision);
        
@@ -191,6 +268,10 @@ namespace storm {
        
        template void gatherOccurringVariables<storm::RationalFunction, storm::Variable>(storm::RationalFunction const& function, std::set<storm::Variable>& variableSet);
        
+       template void addGuardedConstraintToSmtSolver<storm::solver::Smt2SmtSolver, storm::RationalFunction, storm::Variable>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver,storm::Variable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide);
+       template void addParameterBoundsToSmtSolver<storm::solver::Smt2SmtSolver, storm::Variable, cln::cl_RA>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver, storm::Variable const& variable, storm::logic::ComparisonType relation, cln::cl_RA const& bound);
+       template void addBoolVariableToSmtSolver<storm::solver::Smt2SmtSolver, storm::Variable>(std::shared_ptr<storm::solver::Smt2SmtSolver> solver, storm::Variable const& variable, bool value);
+       
 #endif 
         }
     }

src/utility/regions.h

@@ -3,13 +3,18 @@
  * Author: Tim Quatmann
  *
  * Created on May 13, 2015, 12:54 PM
+ * 
+ * This file provides some auxiliary functions for the Region Model Checker.
+ * The purpose of many of this functions is to deal with the different types (e.g., carl expressions)
  */
 
-#include "src/modelchecker/reachability/SparseDtmcRegionModelChecker.h" //to get the ParameterRegion type
 
 #ifndef STORM_UTILITY_REGIONS_H
 #define	STORM_UTILITY_REGIONS_H
 
+#include "src/modelchecker/reachability/SparseDtmcRegionModelChecker.h"
+#include "src/logic/ComparisonType.h"
+
 // Forward-declare region modelchecker  class.
     namespace storm {
         namespace modelchecker{
@@ -92,6 +97,16 @@ namespace storm {
             template<typename VariableType>
             VariableType getVariableFromString(std::string variableString);
             
+            
+            enum class VariableSort {VS_BOOL, VS_REAL, VS_INT};
+            
+            /*
+             * Creates a new variable with the given name and the given sort
+             * Throws an exception if there is already a variable with that name.
+             */
+            template<typename VariableType>
+            VariableType getNewVariable(std::string variableName, VariableSort sort);
+            
             /*
              * retrieves the variable name  from the given variable
              */
@@ -113,6 +128,32 @@ namespace storm {
             template<typename ParametricType, typename VariableType>
             void gatherOccurringVariables(ParametricType const& function, std::set<VariableType>& variableSet);
             
+            
+            /*!
+             * Adds the given constraint to the given Smt solver
+             * The constraint is of the form 'guard implies leftHandSide relation rightHandSide'
+             * @attention the numerators and denominators of the left and right hand side should be positive!
+             * 
+             * @param guard variable of type bool
+             * @param leftHandSide left hand side of the constraint
+             * @param relation relation of the constraint
+             * @param rightHandSide right hand side of the constraint
+             */
+            template<typename SolverType, typename ParametricType, typename VariableType>
+            void addGuardedConstraintToSmtSolver(std::shared_ptr<SolverType> solver, VariableType const& guard, ParametricType const& leftHandSide, storm::logic::ComparisonType relation, ParametricType const& rightHandSide);
+            
+            /*!
+             * Adds the given constraint to the given Smt solver
+             * The constraint is of the form 'variable relation bound'
+             */
+            template<typename SolverType, typename VariableType, typename BoundType>
+            void addParameterBoundsToSmtSolver(std::shared_ptr<SolverType> solver, VariableType const& variable, storm::logic::ComparisonType relation, BoundType const& bound);
+            
+            /*!
+             * Adds the given (boolean) variable to the solver. Can be used to assert that guards are true/false
+             */
+            template<typename SolverType, typename VariableType>
+            void addBoolVariableToSmtSolver(std::shared_ptr<SolverType> solver, VariableType const& variable, bool value);
         }
     }
 }