diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index d350c8fba..46751ca6b 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -72,11 +72,11 @@ namespace storm { STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled."); this->hasOnlyLinearFunctions=false; - this->isReachProbFunctionComputed=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. @@ -87,28 +87,24 @@ namespace storm { // 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 - std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelStart = std::chrono::high_resolution_clock::now(); computeSimplifiedModel(targetStates); - std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelEnd = std::chrono::high_resolution_clock::now(); //now create the model used for Approximation - std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); if(storm::settings::regionSettings().doApprox()){ - this->approximationModel=std::make_shared(*this->simplifiedModel); + initializeApproximationModel(*this->simplifiedModel); } - std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now(); //now create the model used for Sampling - std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now(); if(storm::settings::regionSettings().doSample() || (storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ - this->samplingModel=std::make_shared(*this->simplifiedModel); + initializeSamplingModel(*this->simplifiedModel); } - std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now(); - + //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); + } + //some information for statistics... std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart; - this->timeComputeSimplifiedModel = timeComputeSimplifiedModelEnd - timeComputeSimplifiedModelStart; - this->timeInitSamplingModel = timeInitSamplingModelEnd - timeInitSamplingModelStart; - this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart; this->numOfCheckedRegions=0; this->numOfRegionsSolvedThroughSampling=0; this->numOfRegionsSolvedThroughApproximation=0; @@ -125,7 +121,7 @@ namespace storm { template void SparseDtmcRegionModelChecker::computeSimplifiedModel(storm::storage::BitVector const& targetStates){ - + std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelStart = std::chrono::high_resolution_clock::now(); //Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model, storm::storage::BitVector(this->model.getNumberOfStates(),true), targetStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; @@ -134,8 +130,7 @@ namespace storm { // 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)) { STORM_LOG_WARN("The probability of the initial state is constant (0 or 1)"); - this->reachProbFunction = statesWithProbability0.get(*(this->model.getInitialStates().begin())) ? storm::utility::zero() : storm::utility::one(); - this->isReachProbFunctionComputed=true; + this->reachProbFunction = std::make_shared(statesWithProbability0.get(*(this->model.getInitialStates().begin())) ? storm::utility::zero() : storm::utility::one()); this->isResultConstant=true; this->hasOnlyLinearFunctions=true; } @@ -183,7 +178,6 @@ namespace storm { } subsystem.set(initialState, true); STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl); - std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl; if(allReachableFunctionsAreConstant){ //Check if this is also the case for the initial state @@ -248,6 +242,58 @@ namespace storm { boost::optional>> noChoiceLabeling; // the final model this->simplifiedModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(noStateRewards), std::move(noTransitionRewards), std::move(noChoiceLabeling)); + std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelEnd = std::chrono::high_resolution_clock::now(); + this->timeComputeSimplifiedModel = timeComputeSimplifiedModelEnd - timeComputeSimplifiedModelStart; + } + + 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); + std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now(); + this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart; + STORM_LOG_DEBUG("Initialized Approximation Model"); + } + + 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); + 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(); + //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()); + std::vector oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero()); + for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){ + if(entry.getColumn() forwardTransitions=simpleModel.getTransitionMatrix().getSubmatrix(false,maybeStates,maybeStates); + //now compute the functions using methods from elimination model checker + storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates; + storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true); + 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)); + /* 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; } template @@ -268,8 +314,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(*getReachProbFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); + if(valueIsInBoundOfFormula(storm::utility::regions::getConstantPart(*getReachProbFunction()))){ region.setCheckResult(RegionCheckResult::ALLSAT); } else{ @@ -356,8 +402,7 @@ namespace storm { bool SparseDtmcRegionModelChecker::checkApproximativeProbabilities(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(); - STORM_LOG_THROW(this->approximationModel!=nullptr, storm::exceptions::UnexpectedException, "Approximation model not initialized"); - this->approximationModel->instantiate(region); + getApproximationModel()->instantiate(region); std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now(); this->timeMDPBuild += timeMDPBuildEnd-timeMDPBuildStart; @@ -404,15 +449,15 @@ namespace storm { bool formulaSatisfied; if((formulaHasUpperBound && proveAllSat) || (!formulaHasUpperBound && !proveAllSat)){ //these are the cases in which we need to compute upper bounds - upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); + upperBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); lowerBounds = std::vector(); - formulaSatisfied = valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()]); + formulaSatisfied = valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ //for the remaining cases we compute lower bounds - lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); + lowerBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); upperBounds = std::vector(); - formulaSatisfied = valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()]); + formulaSatisfied = valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } //check if approximation was conclusive @@ -430,12 +475,12 @@ namespace storm { proveAllSat=!proveAllSat; if(lowerBounds.empty()){ - lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); - formulaSatisfied=valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()]); + lowerBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); + formulaSatisfied=valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ - upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); - formulaSatisfied=valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()]); + upperBounds = getApproximationModel()->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); + formulaSatisfied=valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); } //check if approximation was conclusive @@ -452,6 +497,15 @@ namespace storm { return false; } + template + std::shared_ptr::ApproximationModel> const& SparseDtmcRegionModelChecker::getApproximationModel() { + if(this->approximationModel==nullptr){ + STORM_LOG_WARN("Approximation model requested but it has not been initialized when specifying the formula. Will initialize it now."); + initializeApproximationModel(*this->simplifiedModel); + } + return this->approximationModel; + } + template bool SparseDtmcRegionModelChecker::checkSamplePoints(ParameterRegion& region) { auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points @@ -468,12 +522,11 @@ namespace storm { 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)); + valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(*getReachProbFunction(), point)); } else{ - STORM_LOG_THROW(this->samplingModel!=nullptr, storm::exceptions::UnexpectedException, "Sampling model not initialized"); - this->samplingModel->instantiate(point); - valueInBoundOfFormula=this->valueIsInBoundOfFormula(this->samplingModel->computeReachabilityProbabilities()[*this->samplingModel->getModel()->getInitialStates().begin()]); + getSamplingModel()->instantiate(point); + valueInBoundOfFormula=this->valueIsInBoundOfFormula(getSamplingModel()->computeReachabilityProbabilities()[*getSamplingModel()->getModel()->getInitialStates().begin()]); } if(valueInBoundOfFormula){ @@ -500,36 +553,19 @@ namespace storm { } template - ParametricType SparseDtmcRegionModelChecker::getReachProbFunction() { - if(!this->isReachProbFunctionComputed){ - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = 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(this->simplifiedModel->getBackwardTransitions()); - std::vector oneStepProbabilities(this->simplifiedModel->getNumberOfStates()-2, storm::utility::zero()); - for(auto const& entry : backwardTransitions.getRow(*(this->simplifiedModel->getStates("target").begin()))){ - if(entry.getColumn()simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink")); - backwardTransitions=backwardTransitions.getSubmatrix(false,maybeStates,maybeStates); - storm::storage::SparseMatrix forwardTransitions=this->simplifiedModel->getTransitionMatrix().getSubmatrix(false,maybeStates,maybeStates); - //now compute the functions using methods from elimination model checker - storm::storage::BitVector newInitialStates = this->simplifiedModel->getInitialStates() % maybeStates; - storm::storage::BitVector phiStates(this->simplifiedModel->getNumberOfStates(), true); - boost::optional> noStateRewards; - std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); - this->reachProbFunction=this->eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, this->simplifiedModel->getStates("target"), noStateRewards, statePriorities); - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now(); - /* 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"); - this->isReachProbFunctionComputed=true; - this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart; + std::shared_ptr::SamplingModel> const& SparseDtmcRegionModelChecker::getSamplingModel() { + if(this->samplingModel==nullptr){ + STORM_LOG_WARN("Sampling model requested but it has not been initialized when specifying the formula. Will initialize it now."); + initializeSamplingModel(*this->simplifiedModel); + } + return this->samplingModel; + } + + 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); } return this->reachProbFunction; } @@ -543,7 +579,7 @@ namespace storm { } if(this->smtSolver==nullptr){ - initializeSMTSolver(this->smtSolver, getReachProbFunction(),*this->probabilityOperatorFormula); + initializeSMTSolver(this->smtSolver, *getReachProbFunction(),*this->probabilityOperatorFormula); } this->smtSolver->push(); @@ -624,7 +660,7 @@ 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(this->smtSolver,*getReachProbFunction(), *this->probabilityOperatorFormula); } return false; } @@ -741,17 +777,17 @@ namespace storm { outstream << " " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl; outstream << std::endl; outstream << "Running times:" << std::endl; - outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing)" << std::endl; + outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing, bisimulation (if applied))" << std::endl; outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl; 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 << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; - outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; outstream << " " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl; + outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; outstream << " " << timeFullSmtInMilliseconds.count() << "ms Smt solving" << std::endl; - outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function (already included in one of the above)" << std::endl; outstream << "-----------------------------------------------" << std::endl; } diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index c976e7afe..2735d3996 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -1,6 +1,8 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ +#include + #include "src/storage/sparse/StateType.h" #include "src/models/sparse/Dtmc.h" #include "src/utility/constants.h" @@ -94,6 +96,21 @@ namespace storm { */ void computeSimplifiedModel(storm::storage::BitVector const& targetStates); + /*! + * initializes the Approximation Model + */ + void initializeApproximationModel(storm::models::sparse::Dtmc const& simpleModel); + + /*! + * initializes the Sampling Model + */ + void initializeSamplingModel(storm::models::sparse::Dtmc const& simpleModel); + + /*! + * Computes the reachability probability function via state elimination + */ + void computeReachProbFunction(storm::models::sparse::Dtmc const& simpleModel); + /*! * Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability. * If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED). @@ -105,6 +122,12 @@ namespace storm { */ bool checkApproximativeProbabilities(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds); + /*! + * Returns the approximation model. + * If it is not yet available, it is computed. + */ + std::shared_ptr const& getApproximationModel(); + /*! * 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 @@ -128,12 +151,17 @@ namespace storm { */ bool checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction=false); + /*! + * Returns the sampling model. + * If it is not yet available, it is computed. + */ + std::shared_ptr const& getSamplingModel(); + /*! * Returns the reachability probability function. - * If it is not yet available, it is computed via state elimination. - * After that, the function is available and for the next call of this method it will not be computed again. + * If it is not yet available, it is computed. */ - ParametricType getReachProbFunction(); + std::shared_ptr const& getReachProbFunction(); /*! * Starts the SMTSolver to get the result. @@ -174,11 +202,9 @@ namespace storm { // 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 - ParametricType reachProbFunction; + std::shared_ptr reachProbFunction; // 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 reachability probability function has been computed - bool isReachProbFunctionComputed; // a flag that is true iff the resulting reachability probability is constant bool isResultConstant; // the smt solver that is used to prove properties with the help of the reachProbFunction