From d0f7e5f6da147ddcd3789bcfb85d8836f80c3a82 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 30 Aug 2015 17:32:37 +0200 Subject: [PATCH] First steps towards working with rewards Former-commit-id: 1230bb896fb8047df1f4376cb341afc144ea63b2 --- .../region/ApproximationModel.cpp | 23 +- src/modelchecker/region/ApproximationModel.h | 6 +- src/modelchecker/region/SamplingModel.cpp | 21 +- src/modelchecker/region/SamplingModel.h | 8 +- .../region/SparseDtmcRegionModelChecker.cpp | 228 ++++++++++-------- .../region/SparseDtmcRegionModelChecker.h | 40 +-- src/utility/cli.h | 2 +- 7 files changed, 191 insertions(+), 137 deletions(-) diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 2902c2647..658043c63 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -16,7 +16,7 @@ namespace storm { template - SparseDtmcRegionModelChecker::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc const& parametricModel) : mapping(), evaluationTable(), substitutions() { + SparseDtmcRegionModelChecker::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards) : mapping(), evaluationTable(), substitutions(), computeRewards(computeRewards){ // Run through the rows of the original model and obtain // (1) the different substitutions (this->substitutions) and the substitution used for every row std::vector rowSubstitutions; @@ -157,18 +157,25 @@ namespace storm { } template - std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeReachabilityProbabilities(storm::logic::OptimalityType const& optimalityType) { - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); - storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); - storm::modelchecker::SparseMdpPrctlModelChecker modelChecker(*this->model); + std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeValues(storm::logic::OptimalityType const& optimalityType) { - //perform model checking on the mdp - std::unique_ptr resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula, false, optimalityType); + storm::modelchecker::SparseMdpPrctlModelChecker modelChecker(*this->model); + std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); + std::unique_ptr resultPtr; + if(this->computeRewards){ + storm::logic::ReachabilityRewardFormula reachRewFormula(targetFormulaPtr); + //perform model checking on the mdp + resultPtr = modelChecker.computeReachabilityRewards(reachRewFormula, false, optimalityType); + } + else { + storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); + //perform model checking on the mdp + resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula, false, optimalityType); + } return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); } - #ifdef STORM_HAVE_CARL template class SparseDtmcRegionModelChecker::ApproximationModel; #endif diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index 06bc06155..d9ceb09f8 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -26,7 +26,7 @@ namespace storm { typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - ApproximationModel(storm::models::sparse::Dtmc const& parametricModel); + ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards); virtual ~ApproximationModel(); /*! @@ -44,7 +44,7 @@ namespace storm { * Undefined behavior if model has not been instantiated first! * @param optimalityType Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds */ - std::vector const& computeReachabilityProbabilities(storm::logic::OptimalityType const& optimalityType); + std::vector const& computeValues(storm::logic::OptimalityType const& optimalityType); private: @@ -70,6 +70,8 @@ namespace storm { //The Model with which we work std::shared_ptr> model; + bool computeRewards; + // comparators that can be used to compare constants. storm::utility::ConstantsComparator parametricTypeComparator; storm::utility::ConstantsComparator constantTypeComparator; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 7d71c7be8..08f09620f 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -15,7 +15,7 @@ namespace storm { template - SparseDtmcRegionModelChecker::SamplingModel::SamplingModel(storm::models::sparse::Dtmc const& parametricModel) : mapping(), evaluationTable(){ + SparseDtmcRegionModelChecker::SamplingModel::SamplingModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards) : mapping(), evaluationTable(), computeRewards(computeRewards){ // Run through the rows of the original model and obtain the set of distinct functions as well as a matrix with dummy entries std::set functionSet; storm::storage::SparseMatrixBuilder matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount()); @@ -86,13 +86,20 @@ namespace storm { } template - std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeReachabilityProbabilities() { - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); - storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); + std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeValues() { storm::modelchecker::SparseDtmcPrctlModelChecker modelChecker(*this->model); - - //perform model checking on the dtmc - std::unique_ptr resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula); + std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); + std::unique_ptr resultPtr; + if(this->computeRewards){ + storm::logic::ReachabilityRewardFormula reachRewFormula(targetFormulaPtr); + //perform model checking on the dtmc + resultPtr = modelChecker.computeReachabilityRewards(reachRewFormula); + } + else { + storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); + //perform model checking on the dtmc + resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula); + } return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); } diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 0f5aabf22..768e82d70 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -25,7 +25,7 @@ namespace storm { typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - SamplingModel(storm::models::sparse::Dtmc const& parametricModel); + SamplingModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards); virtual ~SamplingModel(); /*! @@ -41,10 +41,8 @@ namespace storm { /*! * Returns the reachability probabilities for every state according to the current instantiation. * Undefined behavior if model has not been instantiated first! - * - * @param optimalityType Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds */ - std::vector const& computeReachabilityProbabilities(); + std::vector const& computeValues(); private: @@ -62,6 +60,8 @@ namespace storm { //The model with which we work std::shared_ptr> model; + bool computeRewards; + // comparators that can be used to compare constants. storm::utility::ConstantsComparator parametricTypeComparator; storm::utility::ConstantsComparator constantTypeComparator; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 46751ca6b..b6305a43a 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -30,8 +30,9 @@ namespace storm { template SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), - eliminationModelChecker(model){ - //intentionally left empty + eliminationModelChecker(model), + specifiedFormula(nullptr){ + STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); } template @@ -41,67 +42,86 @@ namespace storm { template bool SparseDtmcRegionModelChecker::canHandle(storm::logic::Formula const& formula) const { - //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) - if(!formula.isStateFormula()){ - STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected a stateFormula"); - return false; - } - if(!formula.asStateFormula().isProbabilityOperatorFormula()){ - STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected a probabilityOperatorFormula"); - return false; - } - storm::logic::ProbabilityOperatorFormula const& probOpForm=formula.asStateFormula().asProbabilityOperatorFormula(); - if(!probOpForm.hasBound()){ - STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: The formula has no bound"); - return false; - } - if(!probOpForm.getSubformula().asPathFormula().isEventuallyFormula()){ - STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected an eventually subformula"); - return false; - } - if(model.getInitialStates().getNumberOfSetBits() != 1){ - STORM_LOG_DEBUG("Input model is required to have exactly one initial state."); - return false; + //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) and reachability reward formulas + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + return probabilityOperatorFormula.hasBound() && this->canHandle(probabilityOperatorFormula.getSubformula()); + } else if (formula.isRewardOperatorFormula()) { + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); + return rewardOperatorFormula.hasBound() && this->canHandle(rewardOperatorFormula.getSubformula()); + } else if (formula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); + if (eventuallyFormula.getSubformula().isPropositionalFormula()) { + return true; + } + } else if (formula.isReachabilityRewardFormula()) { + storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); + if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { + return true; + } + } else if (formula.isConditionalPathFormula()) { + storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula(); + if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { + return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); + } } - return true; + STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); + return false; } template - void SparseDtmcRegionModelChecker::specifyFormula(storm::logic::Formula const& formula) { + void SparseDtmcRegionModelChecker::specifyFormula(std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled."); + STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled."); this->hasOnlyLinearFunctions=false; this->isResultConstant=false; this->smtSolver=nullptr; this->approximationModel=nullptr; this->samplingModel=nullptr; - this->reachProbFunction=nullptr; - - //Get subformula, target states - //Note: canHandle already ensures that the formula has the right shape and that the model has a single initial state. - this->probabilityOperatorFormula = std::unique_ptr(new storm::logic::ProbabilityOperatorFormula(formula.asStateFormula().asProbabilityOperatorFormula())); - storm::logic::EventuallyFormula const& eventuallyFormula = this->probabilityOperatorFormula->getSubformula().asPathFormula().asEventuallyFormula(); - std::unique_ptr targetStatesResultPtr = this->eliminationModelChecker.check(eventuallyFormula.getSubformula()); + this->reachabilityFunction=nullptr; + + //Get bounds, comparison type, target states, .. + //Note: canHandle already ensures that the formula has the right shape. + this->specifiedFormula = formula; + std::unique_ptr targetStatesResultPtr; + if (this->specifiedFormula->isProbabilityOperatorFormula()) { + this->computeRewards=false; + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = this->specifiedFormula->asProbabilityOperatorFormula(); + this->specifiedFormulaCompType=probabilityOperatorFormula.getComparisonType(); + this->specifiedFormulaBound=probabilityOperatorFormula.getBound(); + targetStatesResultPtr=this->eliminationModelChecker.check(probabilityOperatorFormula.getSubformula().asEventuallyFormula().getSubformula()); + } + else if (this->specifiedFormula->isRewardOperatorFormula()) { + this->computeRewards=true; + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = this->specifiedFormula->asRewardOperatorFormula(); + this->specifiedFormulaCompType=rewardOperatorFormula.getComparisonType(); + this->specifiedFormulaBound=rewardOperatorFormula.getBound(); + targetStatesResultPtr=this->eliminationModelChecker.check(rewardOperatorFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); + } + else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The specified property " << formula << "is not supported"); + } storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector(); // get a more simple model with a single target state, a single sink state and where states with constant outgoing transitions have been removed // Note: also checks for linear functions and a constant result computeSimplifiedModel(targetStates); - //now create the model used for Approximation - if(storm::settings::regionSettings().doApprox()){ - initializeApproximationModel(*this->simplifiedModel); - } - //now create the model used for Sampling - if(storm::settings::regionSettings().doSample() || (storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ - initializeSamplingModel(*this->simplifiedModel); - } - //Check if the reachability probability function needs to be computed - if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || - (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ - computeReachProbFunction(*this->simplifiedModel); + if(!this->isResultConstant){ + //now create the model used for Approximation + if(storm::settings::regionSettings().doApprox()){ + initializeApproximationModel(*this->simplifiedModel); + } + //now create the model used for Sampling + if(storm::settings::regionSettings().doSample() || (storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ + initializeSamplingModel(*this->simplifiedModel); + } + //Check if the reachability function needs to be computed + if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || + (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ + computeReachabilityFunction(*this->simplifiedModel); + } } - //some information for statistics... std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart; @@ -126,13 +146,22 @@ namespace storm { std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model, storm::storage::BitVector(this->model.getNumberOfStates(),true), targetStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; + //if the target states are not reached with probability 1, then the expected reward is defined as infinity + if (this->computeRewards && !this->model.getInitialStates().isSubsetOf(statesWithProbability1)){ + STORM_LOG_WARN("The expected reward of the initial state is constant (infinity)"); + this->reachabilityFunction = std::make_shared(storm::utility::infinity()); + this->isResultConstant=true; + this->hasOnlyLinearFunctions=true; + return; //nothing else to do... + } storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. - if (this->model.getInitialStates().isDisjointFrom(maybeStates)) { + if (!this->computeRewards && this->model.getInitialStates().isDisjointFrom(maybeStates)) { STORM_LOG_WARN("The probability of the initial state is constant (0 or 1)"); - this->reachProbFunction = std::make_shared(statesWithProbability0.get(*(this->model.getInitialStates().begin())) ? storm::utility::zero() : storm::utility::one()); + this->reachabilityFunction = std::make_shared(statesWithProbability0.get(*(this->model.getInitialStates().begin())) ? storm::utility::zero() : storm::utility::one()); this->isResultConstant=true; this->hasOnlyLinearFunctions=true; + return; //nothing else to do... } // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->model.getTransitionMatrix(), this->model.getInitialStates(), maybeStates, statesWithProbability1); @@ -249,7 +278,7 @@ namespace storm { template void SparseDtmcRegionModelChecker::initializeApproximationModel(storm::models::sparse::Dtmc const& simpleModel) { std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); - this->approximationModel=std::make_shared(simpleModel); + this->approximationModel=std::make_shared(simpleModel, this->computeRewards); std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now(); this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart; STORM_LOG_DEBUG("Initialized Approximation Model"); @@ -258,15 +287,15 @@ namespace storm { template void SparseDtmcRegionModelChecker::initializeSamplingModel(storm::models::sparse::Dtmc const& simpleModel) { std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now(); - this->samplingModel=std::make_shared(simpleModel); + this->samplingModel=std::make_shared(simpleModel, this->computeRewards); std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now(); this->timeInitSamplingModel = timeInitSamplingModelEnd - timeInitSamplingModelStart; STORM_LOG_DEBUG("Initialized Sampling Model"); } template - void SparseDtmcRegionModelChecker::computeReachProbFunction(storm::models::sparse::Dtmc const& simpleModel){ - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now(); + void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel){ + std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionStart = std::chrono::high_resolution_clock::now(); //get the one step probabilities and the transition matrix of the simplified model without target/sink state //TODO check if this takes long... we could also store the oneSteps while creating the simplified model. Or(?) we keep the matrix the way it is and give the target state one step probability 1. storm::storage::SparseMatrix backwardTransitions(simpleModel.getBackwardTransitions()); @@ -285,15 +314,15 @@ namespace storm { boost::optional> noStateRewards; std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); - this->reachProbFunction=std::make_shared(this->eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, simpleModel.getStates("target"), noStateRewards, statePriorities)); + this->reachabilityFunction=std::make_shared(this->eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, simpleModel.getStates("target"), noStateRewards, statePriorities)); /* std::string funcStr = " (/ " + this->reachProbFunction->nominator().toString(false, true) + " " + this->reachProbFunction->denominator().toString(false, true) + " )"; std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;*/ STORM_LOG_DEBUG("Computed reachProbFunction"); - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now(); - this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart; + std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now(); + this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; } template @@ -301,7 +330,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now(); ++this->numOfCheckedRegions; - STORM_LOG_THROW(this->probabilityOperatorFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" ); + STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" ); STORM_LOG_DEBUG("Analyzing the region " << region.toString()); //std::cout << "Analyzing the region " << region.toString() << std::endl; @@ -314,8 +343,8 @@ namespace storm { if(!done && this->isResultConstant){ STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); - STORM_LOG_THROW(this->parametricTypeComparator.isConstant(*getReachProbFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); - if(valueIsInBoundOfFormula(storm::utility::regions::getConstantPart(*getReachProbFunction()))){ + STORM_LOG_THROW(this->parametricTypeComparator.isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); + if(valueIsInBoundOfFormula(storm::utility::regions::getConstantPart(*getReachabilityFunction()))){ region.setCheckResult(RegionCheckResult::ALLSAT); } else{ @@ -328,8 +357,8 @@ namespace storm { std::vector lowerBounds; std::vector upperBounds; if(!done && doApproximation){ - STORM_LOG_DEBUG("Checking approximative probabilities..."); - if(checkApproximativeProbabilities(region, lowerBounds, upperBounds)){ + STORM_LOG_DEBUG("Checking approximative values..."); + if(checkApproximativeValues(region, lowerBounds, upperBounds)){ ++this->numOfRegionsSolvedThroughApproximation; STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through approximation."); done=true; @@ -399,7 +428,7 @@ namespace storm { } template - bool SparseDtmcRegionModelChecker::checkApproximativeProbabilities(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { + bool SparseDtmcRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions."); std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); getApproximationModel()->instantiate(region); @@ -407,8 +436,8 @@ namespace storm { this->timeMDPBuild += timeMDPBuildEnd-timeMDPBuildStart; // Decide whether the formula has an upper or a lower bond ({<, <=} or {>, >=}) and whether to prove allsat or allviolated. (Hence, there are 4 cases) - bool formulaHasUpperBound = this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Less || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::LessEqual; - STORM_LOG_THROW((formulaHasUpperBound != (this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Greater || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::GreaterEqual)), + bool formulaHasUpperBound = this->specifiedFormulaCompType==storm::logic::ComparisonType::Less || this->specifiedFormulaCompType==storm::logic::ComparisonType::LessEqual; + STORM_LOG_THROW((formulaHasUpperBound != (this->specifiedFormulaCompType==storm::logic::ComparisonType::Greater || this->specifiedFormulaCompType==storm::logic::ComparisonType::GreaterEqual)), storm::exceptions::UnexpectedException, "Unexpected comparison Type of formula"); bool proveAllSat; switch (region.getCheckResult()){ @@ -442,20 +471,20 @@ namespace storm { proveAllSat=false; break; default: - STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative probabilities"); + STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values"); proveAllSat=true; } bool formulaSatisfied; if((formulaHasUpperBound && proveAllSat) || (!formulaHasUpperBound && !proveAllSat)){ //these are the cases in which we need to compute upper bounds - upperBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); + upperBounds = getApproximationModel()->computeValues(storm::logic::OptimalityType::Maximize); lowerBounds = std::vector(); formulaSatisfied = valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ //for the remaining cases we compute lower bounds - lowerBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); + lowerBounds = getApproximationModel()->computeValues(storm::logic::OptimalityType::Minimize); upperBounds = std::vector(); formulaSatisfied = valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } @@ -475,11 +504,11 @@ namespace storm { proveAllSat=!proveAllSat; if(lowerBounds.empty()){ - lowerBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); + lowerBounds = getApproximationModel()->computeValues(storm::logic::OptimalityType::Minimize); formulaSatisfied=valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ - upperBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); + upperBounds = getApproximationModel()->computeValues(storm::logic::OptimalityType::Maximize); formulaSatisfied=valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } @@ -518,15 +547,15 @@ namespace storm { } template - bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { + bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { bool valueInBoundOfFormula; if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || - (!storm::settings::regionSettings().doSample() && viaReachProbFunction)){ - valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(*getReachProbFunction(), point)); + (!storm::settings::regionSettings().doSample() && favorViaFunction)){ + valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point)); } else{ getSamplingModel()->instantiate(point); - valueInBoundOfFormula=this->valueIsInBoundOfFormula(getSamplingModel()->computeReachabilityProbabilities()[*getSamplingModel()->getModel()->getInitialStates().begin()]); + valueInBoundOfFormula=this->valueIsInBoundOfFormula(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]); } if(valueInBoundOfFormula){ @@ -562,12 +591,12 @@ namespace storm { } template - std::shared_ptr const& SparseDtmcRegionModelChecker::getReachProbFunction() { - if(this->reachProbFunction==nullptr){ - STORM_LOG_WARN("Reachability Probability Function requested but it has not been computed when specifying the formula. Will compute it now."); - computeReachProbFunction(*this->simplifiedModel); + std::shared_ptr const& SparseDtmcRegionModelChecker::getReachabilityFunction() { + if(this->reachabilityFunction==nullptr){ + STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now."); + computeReachabilityFunction(*this->simplifiedModel); } - return this->reachProbFunction; + return this->reachabilityFunction; } template @@ -579,7 +608,7 @@ namespace storm { } if(this->smtSolver==nullptr){ - initializeSMTSolver(this->smtSolver, *getReachProbFunction(),*this->probabilityOperatorFormula); + initializeSMTSolver(); } this->smtSolver->push(); @@ -660,19 +689,19 @@ namespace storm { default: STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); if(this->smtSolver->isNeedsRestart()){ - initializeSMTSolver(this->smtSolver,*getReachProbFunction(), *this->probabilityOperatorFormula); + initializeSMTSolver(); } return false; } } template - void SparseDtmcRegionModelChecker::initializeSMTSolver(std::shared_ptr& solver, const ParametricType& reachProbFunc, const storm::logic::ProbabilityOperatorFormula& formula) { + void SparseDtmcRegionModelChecker::initializeSMTSolver() { 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)); + this->smtSolver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); - ParametricType bound= storm::utility::regions::convertNumber(this->probabilityOperatorFormula->getBound()); + ParametricType bound= storm::utility::regions::convertNumber(this->specifiedFormulaBound); // 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. @@ -685,7 +714,7 @@ namespace storm { // 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()) { + switch (this->specifiedFormulaCompType) { case storm::logic::ComparisonType::Greater: proveAllSatRel=storm::logic::ComparisonType::LessEqual; break; @@ -701,7 +730,7 @@ namespace storm { default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); } - storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, reachProbFunc, proveAllSatRel, bound); + storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllSatVar, *getReachabilityFunction(), 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. @@ -712,24 +741,24 @@ namespace storm { //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, reachProbFunc, proveAllViolatedRel, bound); + storm::logic::ComparisonType proveAllViolatedRel = this->specifiedFormulaCompType; + storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound); } template template bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType value){ - STORM_LOG_THROW(this->probabilityOperatorFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified."); + STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified."); double valueAsDouble = storm::utility::regions::convertNumber(value); - switch (this->probabilityOperatorFormula->getComparisonType()) { + switch (this->specifiedFormulaCompType) { case storm::logic::ComparisonType::Greater: - return (valueAsDouble > this->probabilityOperatorFormula->getBound()); + return (valueAsDouble > this->specifiedFormulaBound); case storm::logic::ComparisonType::GreaterEqual: - return (valueAsDouble >= this->probabilityOperatorFormula->getBound()); + return (valueAsDouble >= this->specifiedFormulaBound); case storm::logic::ComparisonType::Less: - return (valueAsDouble < this->probabilityOperatorFormula->getBound()); + return (valueAsDouble < this->specifiedFormulaBound); case storm::logic::ComparisonType::LessEqual: - return (valueAsDouble <= this->probabilityOperatorFormula->getBound()); + return (valueAsDouble <= this->specifiedFormulaBound); default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); } @@ -738,7 +767,7 @@ namespace storm { template void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { - if(this->probabilityOperatorFormula==nullptr){ + if(this->specifiedFormula==nullptr){ outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl; return; } @@ -747,7 +776,7 @@ namespace storm { std::chrono::milliseconds timeComputeSimplifiedModelInMilliseconds = std::chrono::duration_cast(this->timeComputeSimplifiedModel); std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast(this->timeInitSamplingModel); std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast(this->timeInitApproxModel); - std::chrono::milliseconds timeComputeReachProbFunctionInMilliseconds = std::chrono::duration_cast(this->timeComputeReachProbFunction); + std::chrono::milliseconds timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast(this->timeComputeReachabilityFunction); std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast(this->timeCheckRegion); std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast(this->timeSampling); std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); @@ -762,8 +791,13 @@ namespace storm { outstream << std::endl << "Region Model Checker Statistics:" << std::endl; outstream << "-----------------------------------------------" << std::endl; outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; - outstream << "Simplified model: " << this->simplifiedModel->getNumberOfStates() << " states, " << this->simplifiedModel->getNumberOfTransitions() << " transitions" << std::endl; - outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl; + if(this->isResultConstant){ + outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl; + } + else{ + outstream << "Simplified model: " << this->simplifiedModel->getNumberOfStates() << " states, " << this->simplifiedModel->getNumberOfTransitions() << " transitions" << std::endl; + } + outstream << "Formula: " << *this->specifiedFormula << 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 << std::endl; outstream << " Number of solved regions: " << numOfSolvedRegions << "(" << numOfSolvedRegions*100/this->numOfCheckedRegions << "%)" << std::endl; @@ -782,7 +816,7 @@ namespace storm { outstream << " " << timeComputeSimplifiedModelInMilliseconds.count() << "ms to obtain a simplified model (state elimination of const transitions)" << std::endl; outstream << " " << timeInitApproxModelInMilliseconds.count() << "ms to initialize the Approximation Model" << std::endl; outstream << " " << timeInitSamplingModelInMilliseconds.count() << "ms to initialize the Sampling Model" << std::endl; - outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl; + outstream << " " << timeComputeReachabilityFunctionInMilliseconds.count() << "ms to compute the reachability function" << std::endl; outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; outstream << " " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 2735d3996..d56336974 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -51,7 +51,7 @@ namespace storm { * * @param formula the formula to be considered. */ - void specifyFormula(storm::logic::Formula const& formula); + void specifyFormula(std::shared_ptr formula); /*! * Checks whether the given formula holds for all parameters that lie in the given region. @@ -107,12 +107,12 @@ namespace storm { void initializeSamplingModel(storm::models::sparse::Dtmc const& simpleModel); /*! - * Computes the reachability probability function via state elimination + * Computes the reachability function via state elimination */ - void computeReachProbFunction(storm::models::sparse::Dtmc const& simpleModel); + void computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel); /*! - * Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability. + * Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward). * If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED). * If this succeeded, then the region check result is changed accordingly. * If the current region result is UNKNOWN, then this function first tries to prove ALLSAT and if that failed, it tries to prove ALLVIOLATED. @@ -120,7 +120,7 @@ namespace storm { * However, if only the lowerBounds (or upperBounds) have been computed, the other vector is set to a vector of size 0. * True is returned iff either ALLSAT or ALLVIOLATED could be proved. */ - bool checkApproximativeProbabilities(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds); + bool checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds); /*! * Returns the approximation model. @@ -143,7 +143,7 @@ namespace storm { * Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH * * @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the - * reachProbFunction if this flag is true. If the flag is false, sampling will be + * reachabilityFunction if this flag is true. If the flag is false, sampling will be * done via instantiation of the samplingmodel. Note that this argument is ignored, * unless sampling has been turned of in the settings * @@ -158,10 +158,10 @@ namespace storm { std::shared_ptr const& getSamplingModel(); /*! - * Returns the reachability probability function. + * Returns the reachability function. * If it is not yet available, it is computed. */ - std::shared_ptr const& getReachProbFunction(); + std::shared_ptr const& getReachabilityFunction(); /*! * Starts the SMTSolver to get the result. @@ -173,8 +173,8 @@ namespace storm { */ bool checkFullSmt(ParameterRegion& region); - //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); + //initializes this->smtSolver which can later be used to give an exact result regarding the whole model. + void initializeSMTSolver(); /*! * Returns true iff the given value satisfies the bound given by the specified property @@ -193,21 +193,25 @@ namespace storm { storm::utility::ConstantsComparator constantTypeComparator; //the following members depend on the currently specified formula: - //the currently specified formula - std::unique_ptr probabilityOperatorFormula; + //the currently specified formula, the bound and the comparison type + std::shared_ptr specifiedFormula; + bool computeRewards; + storm::logic::ComparisonType specifiedFormulaCompType; + double specifiedFormulaBound; + // the original model after states with constant transitions have been eliminated std::shared_ptr> simplifiedModel; - // the model that is used to approximate the probability values + // the model that is used to approximate the reachability values std::shared_ptr approximationModel; // the model that can be instantiated to check the value at a certain point std::shared_ptr samplingModel; - // The function for the reachability probability in the initial state - std::shared_ptr reachProbFunction; + // The function for the reachability probability (or: reachability reward) in the initial state + std::shared_ptr reachabilityFunction; // a flag that is true if there are only linear functions at transitions of the model bool hasOnlyLinearFunctions; - // a flag that is true iff the resulting reachability probability is constant + // a flag that is true iff the resulting reachability function is constant bool isResultConstant; - // the smt solver that is used to prove properties with the help of the reachProbFunction + // the smt solver that is used to prove properties with the help of the reachabilityFunction std::shared_ptr smtSolver; // runtimes and other information for statistics. @@ -223,7 +227,7 @@ namespace storm { std::chrono::high_resolution_clock::duration timeComputeSimplifiedModel; std::chrono::high_resolution_clock::duration timeInitApproxModel; std::chrono::high_resolution_clock::duration timeInitSamplingModel; - std::chrono::high_resolution_clock::duration timeComputeReachProbFunction; + std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction; std::chrono::high_resolution_clock::duration timeCheckRegion; std::chrono::high_resolution_clock::duration timeSampling; std::chrono::high_resolution_clock::duration timeApproximation; diff --git a/src/utility/cli.h b/src/utility/cli.h index 9f0b207ee..577b65347 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -288,7 +288,7 @@ namespace storm { auto regions=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::getRegionsFromSettings(); storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { - modelchecker.specifyFormula(*formula.get()); + modelchecker.specifyFormula(formula); modelchecker.checkRegions(regions); } else {