diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 945f83fd0..6f91ace69 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { template - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds) { + 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 } @@ -96,41 +96,31 @@ namespace storm { } template - //Todo adapt bool SparseDtmcRegionModelChecker::canHandle(storm::logic::Formula const& formula) const { - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - return this->canHandle(probabilityOperatorFormula.getSubformula()); - } else if (formula.isRewardOperatorFormula()) { - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); - return this->canHandle(rewardOperatorFormula.getSubformula()); - } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { - if (formula.isUntilFormula()) { - storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); - if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) { - return true; - } - } 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()); - } - } else if (formula.isPropositionalFormula()) { - return true; + //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; } - 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; + } + return true; } + + + + 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 { diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 18a9eb1b4..412709ab4 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -22,6 +22,8 @@ namespace storm { 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; + enum class RegionCheckResult { UNKNOWN, ALLSAT, ALLUNSAT, INCONCLUSIVE}; + class ParameterRegion{ public: @@ -44,6 +46,7 @@ namespace storm { std::map const lowerBounds; std::map const upperBounds; + RegionCheckResult checkResult; }; @@ -53,7 +56,7 @@ namespace storm { /*! * 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) + * ParameterRegions should contain all parameters. */ bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); private: diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h index 4273d1c55..64162fa1a 100644 --- a/src/parser/MappedFile.h +++ b/src/parser/MappedFile.h @@ -51,7 +51,7 @@ namespace storm { /*! * Tests whether the given file exists and is readable. - * + *qi * @param filename Path and name of the file to be tested. * @return True iff the file exists and is readable. */ diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 89db9eb0e..ef9727d29 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -30,6 +30,7 @@ namespace storm { this->addModule(std::unique_ptr(new modules::Smt2SmtSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::TopologicalValueIterationEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::ParametricSettings(*this))); + this->addModule(std::unique_ptr(new modules::RegionSettings(*this))); this->addModule(std::unique_ptr(new modules::SparseDtmcEliminationModelCheckerSettings(*this))); } @@ -523,6 +524,10 @@ namespace storm { storm::settings::modules::ParametricSettings const& parametricSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::ParametricSettings::moduleName)); } + + storm::settings::modules::RegionSettings const& regionSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::RegionSettings::moduleName)); + } storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName)); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 389d51f41..d8d82feda 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -30,6 +30,7 @@ #include "src/settings/modules/GurobiSettings.h" #include "src/settings/modules/Smt2SmtSolverSettings.h" #include "src/settings/modules/ParametricSettings.h" +#include "src/settings/modules/RegionSettings.h" #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" @@ -333,6 +334,13 @@ namespace storm { * @return An object that allows accessing the settings for parameteric model checking. */ storm::settings::modules::ParametricSettings const& parametricSettings(); + + /*! + * Retrieves the settings for parametric region model checking. + * + * @return An object that allows accessing the settings for parametric region model checking. + */ + storm::settings::modules::RegionSettings const& regionSettings(); /* Retrieves the settings of the elimination-based DTMC model checker. * diff --git a/src/settings/modules/RegionSettings.cpp b/src/settings/modules/RegionSettings.cpp new file mode 100644 index 000000000..a53ac8979 --- /dev/null +++ b/src/settings/modules/RegionSettings.cpp @@ -0,0 +1,50 @@ +#include "src/settings/modules/RegionSettings.h" + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string RegionSettings::moduleName = "region"; + const std::string RegionSettings::regionfileOptionName = "regionfile"; + const std::string RegionSettings::regionsOptionName = "regions"; + + RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. Format: '0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9'") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build()); + } + + + + bool RegionSettings::isRegionFileSet() const{ + return this->getOption(regionfileOptionName).getHasOptionBeenSet(); + } + + std::string RegionSettings::getRegionFilePath() const{ + return this->getOption(regionfileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool RegionSettings::isRegionsSet() const{ + return this->getOption(regionsOptionName).getHasOptionBeenSet(); + } + + std::string RegionSettings::getRegionsFromCmdLine() const{ + return this->getOption(regionsOptionName).getArgumentByName("regions").getValueAsString(); + } + + bool RegionSettings::check() const{ + if(isRegionsSet() && isRegionFileSet()){ + STORM_LOG_ERROR("Regions specified twice: via command line AND via file."); + return false; + } + return true; + } + + + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/RegionSettings.h b/src/settings/modules/RegionSettings.h new file mode 100644 index 000000000..4e11a1380 --- /dev/null +++ b/src/settings/modules/RegionSettings.h @@ -0,0 +1,64 @@ +#ifndef STORM_SETTINGS_MODULES_REGIONSETTINGS_H_ +#define STORM_SETTINGS_MODULES_REGIONSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for parametric region model checking. + */ + class RegionSettings : public ModuleSettings { + public: + /** + * A type for saving the Solving Strategy. + * + */ + //enum class SolvingStrategy { ... }; + + /*! + * Creates a new set of parametric region model checking settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + RegionSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the regions are specified in a file. + * @return True iff the regions are specified in a file. + */ + bool isRegionFileSet() const; + + /*! + * Returns the file in which the regions are specified. + */ + std::string getRegionFilePath() const; + + /*! + * Retrieves whether the regions are specified as cmd line parameter + * @return True iff the regions are specified as cmd line parameter + */ + bool isRegionsSet() const; + + /*! + * Returns the regions that are specified as cmd line parameter + */ + std::string getRegionsFromCmdLine() const; + + + bool check() const override; + + const static std::string moduleName; + + private: + const static std::string regionfileOptionName; + const static std::string regionsOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_REGIONSETTINGS_H_ */ \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 4dd080c98..eef20473c 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -473,16 +473,13 @@ namespace storm { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); std::shared_ptr> dtmc = model->template as>(); - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - //do we want to check for a parameter region? if(settings.isParametricRegionSet()){ - std::cout << std::endl; - //experimental implementation! check some hardcoded region + std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl; - 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"); + auto regions=storm::utility::regions::RegionParser::getRegionsFromSettings(); storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); - bool result = modelchecker.checkRegion(*formula.get(), regions); + auto result = modelchecker.checkRegion(*formula.get(), regions); std::cout << "... done." << std::endl; if (result){ std::cout << "the property holds for all parameters in the given region" << std::endl; @@ -490,9 +487,9 @@ namespace storm { std::cout << "the property does NOT hold for all parameters in the given region" << std::endl; } - }else{ - //just obtain the resulting rational function + // obtain the resulting rational function + std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index de8277c35..cfe5afa73 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -11,6 +11,8 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidArgumentException.h" #include "adapters/CarlAdapter.h" +#include "exceptions/InvalidSettingsException.h" +#include "parser/MappedFile.h" namespace storm { namespace utility{ @@ -45,7 +47,9 @@ namespace storm { VariableType var = getVariableFromString(parameter); BoundType lb = convertNumber(lowerBound, true, actualPrecision); + STORM_LOG_WARN_COND((lowerBound==convertNumber(lb, true, actualPrecision)), "The lower bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); BoundType ub = convertNumber(upperBound, false, actualPrecision); + STORM_LOG_WARN_COND((upperBound==convertNumber(ub, true, actualPrecision)), "The upper bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); 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; @@ -59,10 +63,7 @@ namespace storm { 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); } @@ -74,28 +75,43 @@ namespace storm { std::vector regionsStrVec; boost::split(regionsStrVec, regionsString, boost::is_any_of(";")); for(auto const& regionStr : regionsStrVec){ - std::cout << "parsing a region" << std::endl; + if(!std::all_of(regionStr.begin(),regionStr.end(),isspace)){ //skip this string if it only consists of space result.emplace_back(RegionParser::parseRegion(regionStr, actualPrecision)); - std::cout << "parsing a region is done" << std::endl; + } } return result; } + template + std::vector::ParameterRegion> RegionParser::getRegionsFromSettings(double precision){ + STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified."); + STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed."); + + std::string regionsString; + if(storm::settings::regionSettings().isRegionsSet()){ + regionsString = storm::settings::regionSettings().getRegionsFromCmdLine(); + } + else{ + //if we reach this point we can assume that the region is given as a file. + STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::regionSettings().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); + storm::parser::MappedFile mf(storm::settings::regionSettings().getRegionFilePath().c_str()); + regionsString = std::string(mf.getData(),mf.getDataSize()); + } + return RegionParser::parseMultipleRegions(regionsString,precision); + } + + 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 + numerator= number*denominator; //this will always round down } else{ - numerator = number*denominator*10; //*10 to look whether we have to round up - if(numerator%10>0){ - numerator+=10; - } - numerator/=10; + numerator = std::ceil(number*denominator); } - storm::RationalFunction::CoeffType result=numerator; + storm::RationalFunction::CoeffType result(numerator); result = result/denominator; return result; } diff --git a/src/utility/regions.h b/src/utility/regions.h index f17bdf93e..0ec0ab383 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -65,6 +65,16 @@ namespace storm { std::string const& regionsString, double precision=0.0); + + /* + * Retrieves the regions that are specified in the settings. + * 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 getRegionsFromSettings(double precision=0.0); + };