diff --git a/src/adapters/Smt2ExpressionAdapter.h b/src/adapters/Smt2ExpressionAdapter.h index 1d42b103c..f0d9cea08 100644 --- a/src/adapters/Smt2ExpressionAdapter.h +++ b/src/adapters/Smt2ExpressionAdapter.h @@ -68,6 +68,19 @@ namespace storm { */ std::string translateExpression(carl::Constraint 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 const& constraint) { + return "(" + carl::toString(constraint.rel()) + " " + constraint.lhs().toString(false, useReadableVarNames) + " " + "0 " + diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 828bc3633..c7fed339c 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -32,13 +32,13 @@ namespace storm { } template - void SparseDtmcRegionModelChecker::ParameterRegion::setUnSatPoint(std::map const& unSatPoint) { - this->unSatPoint = unSatPoint; + void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { + this->violatedPoint = violatedPoint; } template - std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getUnSatPoint() const { - return unSatPoint; + std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { + return violatedPoint; } template @@ -55,14 +55,14 @@ namespace storm { void SparseDtmcRegionModelChecker::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; } @@ -95,6 +95,16 @@ namespace storm { STORM_LOG_THROW(result!=upperBounds.end(), storm::exceptions::IllegalArgumentException, "tried to find an upper bound of a variable that is not specified by this region"); return (*result).second; } + + template + const std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getUpperBounds() const { + return upperBounds; + } + + template + const std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getLowerBounds() const { + return lowerBounds; + } template std::vector::VariableType, typename SparseDtmcRegionModelChecker::BoundType>> SparseDtmcRegionModelChecker::ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const{ @@ -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 - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), eliminationModelChecker(model), probabilityOperatorFormula(nullptr) { + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc 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; @@ -366,7 +378,57 @@ namespace storm { return workingCopyOneStepProbs[initState]; } - + + template + void SparseDtmcRegionModelChecker::initializeSMTSolver(std::shared_ptr& 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(new storm::solver::Smt2SmtSolver(manager, true)); + + ParametricType bound= storm::utility::regions::convertNumber(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("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("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; @@ -448,30 +517,46 @@ namespace storm { template bool SparseDtmcRegionModelChecker::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){ - // check whether the property is satisfied or not at the given point - if(this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(this->reachProbFunction, point))){ - if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ - region.setSatPoint(point); - if(region.getCheckResult()==RegionCheckResult::EXISTSUNSAT){ - region.setCheckResult(RegionCheckResult::EXISTSBOTH); - return true; - } - region.setCheckResult(RegionCheckResult::EXISTSSAT); + if(checkPoint(region, point, true)){ + return true; + } + } + return false; + } + + template + bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { + + // check whether the property is satisfied or not at the given point + bool valueInBoundOfFormula; + if(viaReachProbFunction){ + valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(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::EXISTSVIOLATED){ + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + return true; } + region.setCheckResult(RegionCheckResult::EXISTSSAT); } - else{ - if (region.getCheckResult()!=RegionCheckResult::EXISTSUNSAT){ - region.setUnSatPoint(point); - if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ - region.setCheckResult(RegionCheckResult::EXISTSBOTH); - return true; - } - region.setCheckResult(RegionCheckResult::EXISTSUNSAT); + } + else{ + if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ + region.setViolatedPoint(point); + if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + return true; } + 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,23 +782,101 @@ namespace storm { + template + bool SparseDtmcRegionModelChecker::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("proveAllSat"); + VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString("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(this->timeSampling); std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); std::chrono::milliseconds timeMDPBuildInMilliseconds = std::chrono::duration_cast(this->timeMDPBuild); + std::chrono::milliseconds timeFullSmtInMilliseconds = std::chrono::duration_cast(this->timeFullSmt); std::chrono::high_resolution_clock::duration timeOverall = timePreprocessing + timeCheckRegion; // + ... std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(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; } diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index d0993cd67..09b2d6928 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/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 getVariables() const; BoundType const& getLowerBound(VariableType const& variable) const; BoundType const& getUpperBound(VariableType const& variable) const; + const std::map getUpperBounds() const; + const std::map 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 const& unSatPoint); + void setViolatedPoint(std::map 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 getUnSatPoint() const; + std::map getViolatedPoint() const; /*! @@ -94,7 +96,7 @@ namespace storm { std::map const upperBounds; RegionCheckResult checkResult; std::map satPoint; - std::map unSatPoint; + std::map 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& 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::mapconst& 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 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. @@ -254,6 +279,9 @@ namespace storm { storm::utility::ConstantsComparator parametricTypeComparator; storm::utility::ConstantsComparator constantTypeComparator; + + std::shared_ptr smtSolver; + //the following members depend on the currently specified formula: diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp index 577163d82..6f06f3a3a 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/Smt2SmtSolver.cpp @@ -36,7 +36,7 @@ namespace storm { #ifndef WINDOWS processIdOfSolver=0; #endif - expressionAdapter = std::unique_ptr(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true)); + this->expressionAdapter = std::unique_ptr(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 const& constraint) { add(constraint.lhs(), constraint.rel()); } - template<> void Smt2SmtSolver::add(carl::Constraint const& constraint) { //if some of the occurring variables are not declared yet, we will have to. std::set 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 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 variables = constraint.lhs().gatherVariables(); + variables.insert(guard); + std::vector 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 variableSet; + variableSet.insert(variable); + std::vector 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 diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/Smt2SmtSolver.h index 3ba191349..40710d562 100644 --- a/src/solver/Smt2SmtSolver.h +++ b/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 - void add(typename carl::Constraint const& constraint); + void add(typename carl::Constraint const& constraint); + void add(typename carl::Constraint 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 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; + }; } } diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index a24116eba..ed3f34c27 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -143,6 +143,28 @@ namespace storm { STORM_LOG_THROW(var!=carl::Variable::NO_VARIABLE, storm::exceptions::InvalidArgumentException, "Variable '" + variableString + "' could not be found."); return var; } + + template<> + storm::Variable getNewVariable(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 variable){ @@ -173,6 +195,61 @@ namespace storm { function.gatherVariables(variableSet); } + template<> + void addGuardedConstraintToSmtSolver(std::shared_ptr 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 constraint((leftHandSide.nominator() * rightHandSide.denominator()) - (rightHandSide.nominator() * leftHandSide.denominator()), compRel); + solver->add(guard,constraint); + } + + template<> + void addParameterBoundsToSmtSolver(std::shared_ptr 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(leftHandSide,compRel)); + } + + template<> + void addBoolVariableToSmtSolver(std::shared_ptr 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 const& number, bool const& roundDown, double const& precision); @@ -191,6 +268,10 @@ namespace storm { template void gatherOccurringVariables(storm::RationalFunction const& function, std::set& variableSet); + template void addGuardedConstraintToSmtSolver(std::shared_ptr solver,storm::Variable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide); + template void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::Variable const& variable, storm::logic::ComparisonType relation, cln::cl_RA const& bound); + template void addBoolVariableToSmtSolver(std::shared_ptr solver, storm::Variable const& variable, bool value); + #endif } } diff --git a/src/utility/regions.h b/src/utility/regions.h index e4f9f8be8..02975761a 100644 --- a/src/utility/regions.h +++ b/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 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 + VariableType getNewVariable(std::string variableName, VariableSort sort); + /* * retrieves the variable name from the given variable */ @@ -113,6 +128,32 @@ namespace storm { template void gatherOccurringVariables(ParametricType const& function, std::set& 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 + void addGuardedConstraintToSmtSolver(std::shared_ptr 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 + void addParameterBoundsToSmtSolver(std::shared_ptr 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 + void addBoolVariableToSmtSolver(std::shared_ptr solver, VariableType const& variable, bool value); } } }