From 836b5cebc6d83e282ececbdf12282c17689e919e Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 13 May 2015 22:04:33 +0200 Subject: [PATCH] implemented some auxilarry functions for parameterregions Former-commit-id: 590a0f216c2741b36863f45eb806ea8e7ce811e3 --- .../SparseDtmcRegionModelChecker.cpp | 125 +++++++++------ .../SparseDtmcRegionModelChecker.h | 48 ++++-- src/utility/cli.h | 21 +-- src/utility/regions.cpp | 142 ++++++++++++++++++ src/utility/regions.h | 90 +++++++++++ 5 files changed, 354 insertions(+), 72 deletions(-) create mode 100644 src/utility/regions.cpp create mode 100644 src/utility/regions.h diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 3ac5a0ce9..945f83fd0 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -22,11 +22,74 @@ #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" -#include "exceptions/UnexpectedException.h" +#include "src/exceptions/UnexpectedException.h" + namespace storm { namespace modelchecker { + + template + SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds) { + // Intentionally left empty. + //todo: check whether both mappings map the same variables + } + + template + std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const{ + std::set result; + for(auto const& variableWithBound : lowerBounds) { + result.insert(variableWithBound.first); + } + return result; + } + + template + typename SparseDtmcRegionModelChecker::BoundType const& SparseDtmcRegionModelChecker::ParameterRegion::getLowerBound(VariableType const& variable) const{ + auto const& result = lowerBounds.find(variable); + STORM_LOG_THROW(result!=lowerBounds.end(), storm::exceptions::IllegalArgumentException, "tried to find a lower bound of a variable that is not specified by this region"); + return (*result).second; + } + + template + typename SparseDtmcRegionModelChecker::BoundType const& SparseDtmcRegionModelChecker::ParameterRegion::getUpperBound(VariableType const& variable) const{ + auto const& result = upperBounds.find(variable); + STORM_LOG_THROW(result!=upperBounds.end(), storm::exceptions::IllegalArgumentException, "tried to find an upper bound of a variable that is not specified by this region"); + return (*result).second; + } + + template + std::vector::VariableType, typename SparseDtmcRegionModelChecker::BoundType>> SparseDtmcRegionModelChecker::ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const{ + std::size_t const numOfVariables=consideredVariables.size(); + std::size_t const numOfVertices=std::pow(2,numOfVariables); + std::vector> resultingVector(numOfVertices,std::map()); + if(numOfVertices==1){ + //no variables are given, the returned vector will still contain an empty map + return resultingVector; + } + + for(uint_fast64_t vertexId=0; vertexId>variableIndex)%2==0 ){ + resultingVector[vertexId].insert(std::pair(variable, getLowerBound(variable))); + } + else{ + resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); + } + ++variableIndex; + } + } + return resultingVector; + } + + + + + template SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), eliminationModelChecker(model) { // Intentionally left empty. @@ -275,14 +338,14 @@ namespace storm { } template<> - void SparseDtmcRegionModelChecker::restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, std::vector const& regions, storm::logic::ComparisonType const& compType){ + void SparseDtmcRegionModelChecker::restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, ParameterRegion const& region, storm::logic::ComparisonType const& compType){ //We are going to build a new (non parametric) MDP which has an action for the lower bound and an action for the upper bound of every parameter //todo invent something better to obtain the substitutions. //this only works as long as there is only one parameter per state, // also: check whether the terms are linear/monotone(?) - STORM_LOG_WARN("the probability restriction is experimental.. only works on linear terms with one parameter per state"); + STORM_LOG_WARN("the probability restriction only works on linear terms which is not checked"); storm::storage::sparse::state_type const numOfStates=subsystem.getNumberOfSetBits() + 2; //subsystem + target state + sink state storm::models::sparse::StateLabeling stateLabeling(numOfStates); stateLabeling.addLabel("init", storm::storage::BitVector(numOfStates, true)); @@ -293,19 +356,7 @@ namespace storm { sinkLabel.set(numOfStates-1, true); stateLabeling.addLabel("sink", std::move(sinkLabel)); - std::map substitutionLB; - for(auto const& parRegion : regions){ - substitutionLB.insert(std::pair(parRegion.variable, parRegion.lowerBound)); - } - std::map substitutionUB; - for(auto const& parRegion : regions){ - substitutionUB.insert(std::pair(parRegion.variable, parRegion.upperBound)); - } - std::vector> substitutions; - substitutions.push_back(substitutionLB); - substitutions.push_back(substitutionUB); - - std::pair,std::vector>> instantiation = instantiateFlexibleMatrix(flexibleMatrix, substitutions, subsystem, true, oneStepProbabilities, true); + std::pair,std::vector>> instantiation = instantiateFlexibleMatrix(flexibleMatrix, region.getVerticesOfRegion(region.getVariables()), subsystem, true, oneStepProbabilities, true); boost::optional> noStateRewards; boost::optional> noTransitionRewards; storm::models::sparse::Mdp mdp(instantiation.first, std::move(stateLabeling),noStateRewards,noTransitionRewards,instantiation.second); @@ -339,23 +390,7 @@ namespace storm { storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); storm::modelchecker::SparseMdpPrctlModelChecker modelChecker(mdp); std::unique_ptr resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType); - std::vector resultVector = resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); - - //todo this is experimental.. - if (true){ - std::cout << "the matrix has " << mdp.getTransitionMatrix().getRowGroupCount() << "row groups, " << mdp.getTransitionMatrix().getRowCount() << " rows, and " << mdp.getTransitionMatrix().getColumnCount() << "columns" << std::endl; - boost::container::flat_set< uint_fast64_t> lbChoiceLabel; - lbChoiceLabel.insert(1); - lbChoiceLabel.insert(2); - storm::models::sparse::Dtmc dtmc(mdp.restrictChoiceLabels(lbChoiceLabel).getTransitionMatrix(), std::move(stateLabeling)); - //modelchecking on dtmc - storm::modelchecker::SparseDtmcPrctlModelChecker dtmcModelChecker(dtmc); - std::unique_ptr resultPtrDtmc = dtmcModelChecker.computeEventuallyProbabilities(eventuallyFormula); - std::vector resultVectorDtmc = resultPtrDtmc->asExplicitQuantitativeCheckResult().getValueVector(); - std::cout << "dtmc result with lower bounds:" << resultVectorDtmc[0]; - std::cout << "mdp result:" << resultVector[0]; - } - + std::vector resultVector = resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); //formulate constraints for the solver uint_fast64_t boundDenominator = 1.0/storm::settings::generalSettings().getPrecision(); //we need to approx. the obtained bounds as rational numbers @@ -371,12 +406,12 @@ namespace storm { } template - void SparseDtmcRegionModelChecker::restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, std::vector const& regions, storm::logic::ComparisonType const& compType){ + void SparseDtmcRegionModelChecker::restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, ParameterRegion const& region, storm::logic::ComparisonType const& compType){ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "restricting Probability Variables is not supported for this type"); } template<> - bool SparseDtmcRegionModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ + bool SparseDtmcRegionModelChecker::checkRegion(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(); @@ -481,20 +516,22 @@ namespace storm { //the bounds for the parameters solver.push(); - for(auto param : parameterRegions){ - storm::RawPolynomial lB(param.variable); - lB -= param.lowerBound; + //STORM_LOG_THROW(parameterRegions.size()==1, storm::exceptions::NotImplementedException, "multiple regions not yet implemented"); + ParameterRegion region=parameterRegions[0]; + for(auto variable : region.getVariables()){ + storm::RawPolynomial lB(variable); + lB -= region.getLowerBound(variable); solver.add(carl::Constraint(lB,storm::CompareRelation::GEQ)); - storm::RawPolynomial uB(param.variable); - uB -= param.upperBound; + storm::RawPolynomial uB(variable); + uB -= region.getUpperBound(variable); solver.add(carl::Constraint(uB,storm::CompareRelation::LEQ)); } std::chrono::high_resolution_clock::time_point timeSmtFormulationEnd = std::chrono::high_resolution_clock::now(); // find further restriction on probabilities - restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions, storm::logic::ComparisonType::Less); //probOpForm.getComparisonType()); - restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions, storm::logic::ComparisonType::Greater); + restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions[0], storm::logic::ComparisonType::Less); //probOpForm.getComparisonType()); + restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions[0], storm::logic::ComparisonType::Greater); std::chrono::high_resolution_clock::time_point timeRestrictingEnd = std::chrono::high_resolution_clock::now(); @@ -544,7 +581,7 @@ namespace storm { } template - bool SparseDtmcRegionModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ + bool SparseDtmcRegionModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions){ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type"); } @@ -553,5 +590,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseDtmcRegionModelChecker; #endif + //note: for other template instantiations, add a rule for the typedefs of VariableType and BoundType + } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 96f6385b2..18a9eb1b4 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -1,14 +1,13 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ -//TODO remove useless includes +#include #include "src/storage/sparse/StateType.h" #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Mdp.h" -//#include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/constants.h" -//#include "src/solver/SmtSolver.h" +#include "utility/regions.h" #include "src/solver/Smt2SmtSolver.h" #include "SparseDtmcEliminationModelChecker.h" @@ -18,24 +17,45 @@ namespace storm { template class SparseDtmcRegionModelChecker { public: - explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model); - virtual bool canHandle(storm::logic::Formula const& formula) const; - -#ifdef STORM_HAVE_CARL - struct ParameterRegion{ - storm::Variable variable; - storm::RationalFunction::CoeffType lowerBound; - storm::RationalFunction::CoeffType upperBound; + //The type of variables and bounds depends on the template arguments + typedef typename std::conditional<(std::is_same::value), storm::Variable,std::nullptr_t>::type VariableType; + typedef typename std::conditional<(std::is_same::value), storm::RationalFunction::CoeffType,std::nullptr_t>::type BoundType; + + class ParameterRegion{ + public: + + ParameterRegion(std::map lowerBounds, std::map upperBounds); + + std::set getVariables() const; + BoundType const& getLowerBound(VariableType const& variable) const; + BoundType const& getUpperBound(VariableType const& variable) const; + + /* + * Returns a vector of all possible combinations of lower and upper bounds of the given variables. + * The first entry of the returned vector will map every variable to its lower bound + * The second entry will map every variable to its lower bound, except the first one (i.e. *consVariables.begin()) + * ... + * The last entry will map every variable to its upper bound + */ + std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; + + private: + + std::map const lowerBounds; + std::map const upperBounds; + }; - + explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model); + + virtual bool canHandle(storm::logic::Formula const& formula) const; + /*! * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals) */ bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); -#endif private: typedef typename storm::modelchecker::SparseDtmcEliminationModelChecker::FlexibleSparseMatrix FlexibleMatrix; @@ -67,7 +87,7 @@ namespace storm { void formulateModelWithSMT(storm::solver::Smt2SmtSolver& solver, std::vector& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities); - void restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, std::vector const& regions, storm::logic::ComparisonType const& compTypeOfProperty); + void restrictProbabilityVariables(storm::solver::Smt2SmtSolver& solver, std::vector const& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities, ParameterRegion const& region, storm::logic::ComparisonType const& compTypeOfProperty); #endif diff --git a/src/utility/cli.h b/src/utility/cli.h index 59d20e7eb..4dd080c98 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -7,6 +7,7 @@ #include #include #include +#include #include "storm-config.h" // Includes for the linked libraries and versions header. @@ -17,7 +18,7 @@ # include "glpk.h" #endif #ifdef STORM_HAVE_GUROBI -# include "gurobi_c.h" +#include "gurobi_c.h" #endif #ifdef STORM_HAVE_Z3 # include "z3.h" @@ -66,6 +67,7 @@ log4cplus::Logger printer; #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcRegionModelChecker.h" +#include "src/utility/regions.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" @@ -476,20 +478,9 @@ namespace storm { if(settings.isParametricRegionSet()){ std::cout << std::endl; //experimental implementation! check some hardcoded region - std::vector::ParameterRegion> regions; - storm::RationalFunction::CoeffType zeroPointOne(1); - zeroPointOne = zeroPointOne/10; - storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion param1; - param1.lowerBound= zeroPointOne*zeroPointOne*78; - param1.upperBound= zeroPointOne*zeroPointOne*82; - param1.variable=carl::VariablePool::getInstance().findVariableWithName("pL"); - regions.push_back(param1); - storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion param2; - param2.lowerBound= zeroPointOne*zeroPointOne*78; - param2.upperBound= zeroPointOne*zeroPointOne*82;; - param2.variable=carl::VariablePool::getInstance().findVariableWithName("pK"); - regions.push_back(param2); - + + std::vector::ParameterRegion> regions=storm::utility::regions::RegionParser::parseMultipleRegions("0.78<=pL<=0.82,0.78<=pK<=0.82; 0.3<=pL<=0.5,0.1<=pK<=0.7;0.6<=pL<=0.7,0.8<=pK<=0.9"); + storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); bool result = modelchecker.checkRegion(*formula.get(), regions); std::cout << "... done." << std::endl; diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp new file mode 100644 index 000000000..de8277c35 --- /dev/null +++ b/src/utility/regions.cpp @@ -0,0 +1,142 @@ +/* + * File: Regions.cpp + * Author: Tim Quatmann + * + * Created on May 13, 2015, 12:54 PM + */ + +#include + +#include "src/utility/regions.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "adapters/CarlAdapter.h" + +namespace storm { + namespace utility{ + namespace regions { + + template + void RegionParser::parseParameterBounds( + std::map& lowerBounds, + std::map& upperBounds, + std::string const& parameterBoundsString, + double const precision){ + double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); + + std::string::size_type positionOfFirstRelation = parameterBoundsString.find("<="); + STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the first number"); + std::string::size_type positionOfSecondRelation = parameterBoundsString.find("<=", positionOfFirstRelation+2); + STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the parameter"); + + std::string parameter=parameterBoundsString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); + //removes all whitespaces from the parameter string: + parameter.erase(std::remove_if(parameter.begin(), parameter.end(), isspace), parameter.end()); + STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a parameter"); + double lowerBound, upperBound; + try{ + lowerBound=std::stod(parameterBoundsString.substr(0,positionOfFirstRelation)); + upperBound=std::stod(parameterBoundsString.substr(positionOfSecondRelation+2)); + } + catch (std::exception const& exception) { + STORM_LOG_ERROR("Failed to parse the region: " << parameterBoundsString << ". The correct format for regions is lowerBound<=parameter<=upperbound"); + throw exception; + } + + VariableType var = getVariableFromString(parameter); + BoundType lb = convertNumber(lowerBound, true, actualPrecision); + BoundType ub = convertNumber(upperBound, false, actualPrecision); + lowerBounds.emplace(std::make_pair(var, lb)); + upperBounds.emplace(std::make_pair(var, ub)); + std::cout << "parsed bounds " << parameterBoundsString << ": lb=" << lowerBound << " ub=" << upperBound << " param='" << parameter << "' precision=" << actualPrecision << std::endl; + } + + template + typename RegionParser::ParameterRegion RegionParser::parseRegion(std::string const& regionString, double precision){ + double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); + std::map lowerBounds; + std::map upperBounds; + std::vector parameterBounds; + boost::split(parameterBounds, regionString, boost::is_any_of(",")); + for(auto const& parameterBound : parameterBounds){ + std::cout << "parsing a parameter bound" << std::endl; + RegionParser::parseParameterBounds(lowerBounds, upperBounds, parameterBound, actualPrecision); + std::cout << "created a parameter bound. lower bound has size" << lowerBounds.size() << std::endl; + std::cout << "parsing a param bound is done" << std::endl; + } + return ParameterRegion(lowerBounds, upperBounds); + } + + template + std::vector::ParameterRegion> RegionParser::parseMultipleRegions(std::string const& regionsString, double precision){ + double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); + std::vector result; + std::vector regionsStrVec; + boost::split(regionsStrVec, regionsString, boost::is_any_of(";")); + for(auto const& regionStr : regionsStrVec){ + std::cout << "parsing a region" << std::endl; + result.emplace_back(RegionParser::parseRegion(regionStr, actualPrecision)); + std::cout << "parsing a region is done" << std::endl; + } + return result; + } + + template<> + storm::RationalFunction::CoeffType convertNumber(double const& number, bool const& roundDown, double const& precision){ + double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision); + uint_fast64_t denominator = 1.0/actualPrecision; + uint_fast64_t numerator; + if(roundDown){ + numerator= number*denominator; //this will always round down if necessary + } else{ + numerator = number*denominator*10; //*10 to look whether we have to round up + if(numerator%10>0){ + numerator+=10; + } + numerator/=10; + } + storm::RationalFunction::CoeffType result=numerator; + result = result/denominator; + return result; + } + + template<> + storm::RationalFunction convertNumber(double const& number, bool const& roundDown, double const& precision){ + return storm::RationalFunction(convertNumber(number, roundDown, precision)); + } + + template<> + double convertNumber(cln::cl_RA const& number, bool const& roundDown, double const& precision){ + return cln::double_approx(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<> + storm::Variable getVariableFromString(std::string variableString){ + storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString); + 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"); + } + + //explicit instantiations +#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 storm::Variable getVariableFromString(std::string variableString); +#endif + } + } +} diff --git a/src/utility/regions.h b/src/utility/regions.h new file mode 100644 index 000000000..f17bdf93e --- /dev/null +++ b/src/utility/regions.h @@ -0,0 +1,90 @@ +/* + * File: Regions.h + * Author: Tim Quatmann + * + * Created on May 13, 2015, 12:54 PM + */ + +#include "src/modelchecker/reachability/SparseDtmcRegionModelChecker.h" //to get the ParameterRegion type + +#ifndef STORM_UTILITY_REGIONS_H +#define STORM_UTILITY_REGIONS_H + +// Forward-declare region modelchecker class. + namespace storm { + namespace modelchecker{ + template + class SparseDtmcRegionModelChecker; + } + } + +namespace storm { + namespace utility{ + namespace regions { + template + class RegionParser{ + public: + typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion ParameterRegion; + typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::VariableType VariableType; + typedef typename storm::modelchecker::SparseDtmcRegionModelChecker::BoundType BoundType; + + /* + * Can be used to parse a single parameter with its bounds from a string of the form "0.3<=p<=0.5". + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. + * If no precision is given, the one from the settings is used. + * The results will be inserted in the given maps + * + */ + static void parseParameterBounds( + std::map& lowerBounds, + std::map& upperBounds, + std::string const& parameterBoundsString, + double const precision=0.0 + ); + + /* + * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7". + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. + * If no precision is given, the one from the settings is used. + * + */ + static ParameterRegion parseRegion( + std::string const& regionString, + double precision=0.0); + + /* + * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4". + * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype. + * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up. + * If no precision is given, the one from the settings is used. + * + */ + static std::vector parseMultipleRegions( + std::string const& regionsString, + double precision=0.0); + + }; + + + /* + * Converts a number from one type to a number from the other. + * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings. + */ + template + TargetType convertNumber(SourceType const& number, bool const& roundDown=true, double const& precision=0.0); + + /* + * retrieves the variable object from the given string + * Throws an exception if variable not found + */ + template + VariableType getVariableFromString(std::string variableString); + } + } +} + + +#endif /* STORM_UTILITY_REGIONS_H */ +