diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 084f0c987..7c08140f5 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -28,9 +28,40 @@ namespace storm { template SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { - // Intentionally left empty. //todo: check whether both mappings map the same variables } + + template + void SparseDtmcRegionModelChecker::ParameterRegion::setUnSatPoint(std::map const& unSatPoint) { + this->unSatPoint = unSatPoint; + } + + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getUnSatPoint() const { + return unSatPoint; + } + + template + void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { + this->satPoint = satPoint; + } + + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::BoundType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { + return satPoint; + } + + template + void SparseDtmcRegionModelChecker::ParameterRegion::setCheckResult(RegionCheckResult checkResult) { + this->checkResult = checkResult; + } + + template + typename SparseDtmcRegionModelChecker::RegionCheckResult SparseDtmcRegionModelChecker::ParameterRegion::getCheckResult() const { + return checkResult; + } + + template std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const{ @@ -84,7 +115,7 @@ namespace storm { } template - std::string SparseDtmcRegionModelChecker::ParameterRegion::getCheckResultAsString() const { + std::string SparseDtmcRegionModelChecker::ParameterRegion::checkResultToString() const { switch (this->checkResult) { case RegionCheckResult::UNKNOWN: return "unknown"; @@ -100,7 +131,7 @@ namespace storm { } template - std::string SparseDtmcRegionModelChecker::ParameterRegion::getRegionAsString() const { + std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { std::stringstream regionstringstream; for(auto var : this->getVariables()){ regionstringstream << storm::utility::regions::convertNumber::BoundType,double>(this->getLowerBound(var)); @@ -197,14 +228,14 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeInitialStateEliminationStart = std::chrono::high_resolution_clock::now(); // eliminate all states with only constant outgoing transitions //TODO: maybe also states with constant incoming tranistions. THEN the ordering of the eliminated states does matter. - eliminateStatesConstSucc(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->oneStepProbabilities, this->initialState); + eliminateStatesConstSucc(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->oneStepProbabilities, this->hasOnlyLinearFunctions, this->initialState); 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; //eliminate the remaining states to get the reachability probability function this->sparseTransitions = flexibleTransitions.getSparseMatrix(); this->sparseBackwardTransitions = this->sparseTransitions.transpose(); this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState); - std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl; + // 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(); //some information for statistics... @@ -220,20 +251,27 @@ namespace storm { FlexibleMatrix& flexTransitions, FlexibleMatrix& flexBackwardTransitions, std::vector& oneStepProbs, + bool& allFunctionsAreLinear, storm::storage::sparse::state_type const& initialState) { //temporarily unselect the initial state to skip it. subsys.set(initialState, false); + allFunctionsAreLinear=true; + boost::optional> missingStateRewards; for (auto const& state : subsys) { bool onlyConstantOutgoingTransitions=true; - for(auto const& entry : flexTransitions.getRow(state)){ + for(auto& entry : flexTransitions.getRow(state)){ if(!this->parametricTypeComparator.isConstant(entry.getValue())){ onlyConstantOutgoingTransitions=false; - break; + allFunctionsAreLinear &= storm::utility::regions::functionIsLinear(entry.getValue()); } } + if(!this->parametricTypeComparator.isConstant(oneStepProbs[state])){ + onlyConstantOutgoingTransitions=false; + allFunctionsAreLinear &= storm::utility::regions::functionIsLinear(oneStepProbs[state]); + } if(onlyConstantOutgoingTransitions){ this->eliminationModelChecker.eliminateState(flexTransitions, oneStepProbs, state, flexBackwardTransitions, missingStateRewards); subsys.set(state,false); @@ -301,9 +339,131 @@ namespace storm { return workingCopyOneStepProbs[initState]; } + + + + + template + void SparseDtmcRegionModelChecker::checkRegion(ParameterRegion& region) { + 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_DEBUG("Analyzing the region " << region.toString()); + + //switches for the different steps. + bool doSampling=true; + bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions + bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions + bool doFullSmt=false; //true; + + std::chrono::high_resolution_clock::time_point timeSamplingStart = std::chrono::high_resolution_clock::now(); + if(doSampling){ + STORM_LOG_DEBUG("Testing Sample points..."); + if(testSamplePoints(region)){ + ++this->numOfRegionsSolvedThroughSampling; + STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through sampling."); + doApproximation=false; + doSubsystemSmt=false; + doFullSmt=false; + } + } + std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now(); + if(doApproximation){ + STORM_LOG_WARN("Approximation approach not yet implemented"); + } + std::chrono::high_resolution_clock::time_point timeApproximationEnd = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point timeSubsystemSmtStart = std::chrono::high_resolution_clock::now(); + if(doSubsystemSmt){ + STORM_LOG_WARN("SubsystemSmt approach not yet implemented"); + } + std::chrono::high_resolution_clock::time_point timeSubsystemSmtEnd = std::chrono::high_resolution_clock::now(); - + std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now(); + if(doFullSmt){ + STORM_LOG_WARN("FullSmt approach not yet implemented"); + } + 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; + this->timeSampling = timeSamplingEnd - timeSamplingStart; + this->timeApproximation = timeApproximationEnd - timeApproximationStart; + this->timeSubsystemSmt = timeSubsystemSmtEnd - timeSubsystemSmtStart; + this->timeFullSmt = timeFullSmtEnd - timeFullSmtStart; + } + + template + void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { + for(auto& region : regions){ + this->checkRegion(region); + } + } + + template + bool SparseDtmcRegionModelChecker::testSamplePoints(ParameterRegion& region) { + + auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //only test the 4 corner points (for now) + + bool regionHasSatPoint = !region.getSatPoint().empty(); + bool regionHasUnSatPoint = !region.getUnSatPoint().empty(); + 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 (!regionHasSatPoint){ + region.setSatPoint(point); + regionHasSatPoint=true; + if(regionHasUnSatPoint){ + region.setCheckResult(RegionCheckResult::INCONCLUSIVE); + return true; + } + } + } + else{ + if (!regionHasUnSatPoint){ + region.setUnSatPoint(point); + regionHasUnSatPoint=true; + if(regionHasSatPoint){ + region.setCheckResult(RegionCheckResult::INCONCLUSIVE); + return true; + } + } + } + } + return false; + } + + + + + + + + + + + + + + + + + + + + + + + + + template<> std::pair,std::vector>> SparseDtmcRegionModelChecker::instantiateFlexibleMatrix(FlexibleMatrix const& matrix, std::vector> const& substitutions, storm::storage::BitVector const& filter, bool addSinkState, std::vector const& oneStepProbabilities, bool addSelfLoops) const { @@ -584,7 +744,7 @@ namespace storm { } template<> - bool SparseDtmcRegionModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions){ + bool SparseDtmcRegionModelChecker::checkRegionOld(storm::logic::Formula const& formula, std::vector parameterRegions){ //Note: this is an 'experimental' implementation std::chrono::high_resolution_clock::time_point timeStart = std::chrono::high_resolution_clock::now(); @@ -754,13 +914,14 @@ namespace storm { } template - bool SparseDtmcRegionModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions){ + bool SparseDtmcRegionModelChecker::checkRegionOld(storm::logic::Formula const& formula, std::vector parameterRegions){ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type"); } 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."); double valueAsDouble = storm::utility::regions::convertNumber(value); switch (this->probabilityOperatorFormula->getComparisonType()) { case storm::logic::ComparisonType::Greater: @@ -779,17 +940,30 @@ namespace storm { template void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { + if(this->probabilityOperatorFormula==nullptr){ + outstream << "Statistic Region Model Checker Statistics Error: No formula specified." << std::endl; + return; + } + std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(this->timePreprocessing); std::chrono::milliseconds timeInitialStateEliminationInMilliseconds = std::chrono::duration_cast(this->timeInitialStateElimination); std::chrono::high_resolution_clock::duration timeOverall = timePreprocessing; // + ... std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(timeOverall); - outstream << std::endl << "Statistics Region Model Checker:" << std::endl; + std::size_t subsystemTransitions = this->sparseTransitions.getNonzeroEntryCount(); + for(auto const& transition : this->oneStepProbabilities){ + if(!this->parametricTypeComparator.isZero(transition)){ + ++subsystemTransitions; + } + } + + outstream << std::endl << "Statistics Region Model Checker Statistics:" << std::endl; outstream << "-----------------------------------------------" << std::endl; outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; - outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << this->sparseTransitions.getEntryCount() << "transitions" << std::endl; + outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << "transitions" << std::endl; outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl; + outstream << "All occuring functions in the model are " << (this->hasOnlyLinearFunctions ? "" : "not") << " linear" << std::endl; outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; outstream << "Running times:" << std::endl; outstream << " " << timeOverallInMilliseconds.count() << "ms overall" << std::endl; diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 29b2700ed..014935da1 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -37,13 +37,6 @@ namespace storm { ParameterRegion(std::map lowerBounds, std::map upperBounds); - void setCheckResult(RegionCheckResult checkResult) { - this->checkResult = checkResult; - } - - RegionCheckResult getCheckResult() const { - return checkResult; - } std::set getVariables() const; @@ -59,14 +52,46 @@ namespace storm { */ std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; - std::string getCheckResultAsString() const; - std::string getRegionAsString() const; + //returns the currently set check result as a string + std::string checkResultToString() const; + + //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5; + std::string toString() const; + + void setCheckResult(RegionCheckResult checkResult); + RegionCheckResult getCheckResult() const; + + /*! + * Sets a point in the region for which the considered property is not satisfied. + */ + void setUnSatPoint(std::map const& unSatPoint); + + /*! + * 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; + + + /*! + * Sets a point in the region for which the considered property is satisfied. + */ + void setSatPoint(std::map const& satPoint); + + /*! + * Retrieves a point in the region for which is considered property is satisfied. + * If such a point is not known, the returned map is empty. + */ + std::map getSatPoint() const; private: std::map const lowerBounds; std::map const upperBounds; RegionCheckResult checkResult; + std::map satPoint; + std::map unSatPoint; + }; @@ -87,11 +112,32 @@ namespace storm { */ void specifyFormula(storm::logic::Formula const& formula); + /*! + * 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. + * + * @note A formula has to be specified first. + * + * @param region The considered region + * + */ + void checkRegion(ParameterRegion& region); + + /*! + * 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. + * + * @note A formula has to be specified first. + * + * @param region The considered region + */ + void checkRegions(std::vector& regions); + /*! * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions * ParameterRegions should contain all parameters. */ - bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); + bool checkRegionOld(storm::logic::Formula const& formula, std::vector parameterRegions); /*! * Prints statistical information (mostly running times) to the given stream. @@ -142,12 +188,16 @@ namespace storm { template bool valueIsInBoundOfFormula(ValueType value); - //eliminates all states for which the outgoing transitions are constant. + /*! + * eliminates all states for which the outgoing transitions are constant. + * Also checks whether the non constant functions are linear + */ void eliminateStatesConstSucc( storm::storage::BitVector& subsys, FlexibleMatrix& flexTransitions, FlexibleMatrix& flexBackwardTransitions, std::vector& oneStepProbs, + bool& allFunctionsAreLinear, storm::storage::sparse::state_type const& initState ); @@ -163,6 +213,14 @@ namespace storm { ); + /*! + * 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 + * may also change the regioncheckresult of the region + * + * @return true if an unsat point as well as a sat point has been found during the process + */ + bool testSamplePoints(ParameterRegion& region); @@ -195,6 +253,8 @@ namespace storm { storm::storage::sparse::state_type initialState; // the set of states that have not been eliminated storm::storage::BitVector subsystem; + // a flag that is true if there are only linear functions at transitions of the model + bool hasOnlyLinearFunctions; // The function for the reachability probability in the initial state ParametricType reachProbFunction; @@ -202,8 +262,18 @@ namespace storm { // runtimes and other information for statistics. uint_fast64_t numOfCheckedRegions; + uint_fast64_t numOfRegionsSolvedThroughSampling; + uint_fast64_t numOfRegionsSolvedThroughApproximation; + uint_fast64_t numOfRegionsSolvedThroughSubsystemSmt; + uint_fast64_t numOfRegionsSolvedThroughFullSmt; + std::chrono::high_resolution_clock::duration timePreprocessing; std::chrono::high_resolution_clock::duration timeInitialStateElimination; + std::chrono::high_resolution_clock::duration timeCheckRegion; + std::chrono::high_resolution_clock::duration timeSampling; + std::chrono::high_resolution_clock::duration timeApproximation; + std::chrono::high_resolution_clock::duration timeSubsystemSmt; + std::chrono::high_resolution_clock::duration timeFullSmt; }; } // namespace modelchecker diff --git a/src/utility/cli.h b/src/utility/cli.h index 1b730de51..9966f8bc8 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -480,18 +480,14 @@ namespace storm { storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { modelchecker.specifyFormula(*formula.get()); + modelchecker.checkRegions(regions); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric region check engine currently does not support this property."); } - - auto result = modelchecker.checkRegion(*formula.get(), regions); std::cout << "... done." << std::endl; - if (!result){ - std::cout << "The result of one or more regions is still unknown." << std::endl; - } for(auto const& reg : regions){ - std::cout << reg.getRegionAsString() << " Result: " << reg.getCheckResultAsString() << std::endl; + std::cout << reg.toString() << " Result: " << reg.checkResultToString() << std::endl; } modelchecker.printStatisticsToStream(std::cout); diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index 84ada2e41..8b27122cf 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -131,11 +131,11 @@ namespace storm { return number; } - template - TargetType convertNumber(SourceType const& number, bool const& roundDown, double const& precision){ - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "number conversion between the given types not implemented"); + template<> + cln::cl_RA convertNumber(cln::cl_RA const& number, bool const& roundDown, double const& precision){ + return number; } - + template<> storm::Variable getVariableFromString(std::string variableString){ @@ -143,33 +143,46 @@ namespace storm { STORM_LOG_THROW(var!=carl::Variable::NO_VARIABLE, storm::exceptions::InvalidArgumentException, "Variable '" + variableString + "' could not be found."); return var; } - - template - VariableType getVariableFromString(std::string variableString){ - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Variable from String not implemented for this type"); - } - + template<> std::string getVariableName(storm::Variable variable){ return carl::VariablePool::getInstance().getName(variable); } + + template<> + typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType evaluateFunction( + storm::RationalFunction const& function, + std::map::VariableType, + typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType> const& point){ + return function.evaluate(point); + } - template - std::string getVariableName(VariableType variable){ - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "VariableName from Variable not implemented for this type"); + template<> + bool functionIsLinear(storm::RationalFunction const& function){ + // Note: At this moment there is no function in carl for rationalFunctions. + // We therefore check whether the numerator is linear and the denominator constant. + // We simplify the function to (hopefully) avoid wrong answers for situations like x^2/x + storm::utility::simplify(function); + bool result=(function.nominator().isLinear() && function.denominator().isConstant()); + STORM_LOG_WARN_COND(result, "The function " << function << "is not considered as linear."); + return result; } //explicit instantiations + template double convertNumber(double const& number, bool const& roundDown, double const& precision); + #ifdef STORM_HAVE_CARL template class RegionParser; template storm::RationalFunction convertNumber(double const& number, bool const& roundDown, double const& precision); template storm::RationalFunction::CoeffType convertNumber(double const& number, bool const& roundDown, double const& precision); template double convertNumber(storm::RationalFunction::CoeffType const& number, bool const& roundDown, double const& precision); - template double convertNumber(double const& number, bool const& roundDown, double const& precision); + template cln::cl_RA convertNumber(cln::cl_RA const& number, bool const& roundDown, double const& precision); template storm::Variable getVariableFromString(std::string variableString); template std::string getVariableName(storm::Variable variable); + + template bool functionIsLinear(storm::RationalFunction const& function); #endif } } diff --git a/src/utility/regions.h b/src/utility/regions.h index f32ce62b3..d4ade330e 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -97,6 +97,16 @@ namespace storm { */ template std::string getVariableName(VariableType variable); + + template + typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType evaluateFunction(ParametricType const& function, std::map::VariableType, typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType> const& point); + + /*! + * Returns true if the function is rational. Note that the function might be simplified. + */ + template + bool functionIsLinear(ParametricType const& function); + } } }