From 77179c02ac8fcfaa553093eeecc9ed369d1f809a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 18 May 2018 15:01:29 +0200 Subject: [PATCH] added option to feed additional constraints to abstraction --- .../abstraction/AbstractionInformation.cpp | 30 ++++++++++++++++++- src/storm/abstraction/StateSetAbstractor.cpp | 4 +++ .../abstraction/GameBasedMdpModelChecker.cpp | 6 ++-- src/storm/parser/ExpressionCreator.cpp | 11 ++++--- src/storm/parser/ExpressionCreator.h | 6 +--- src/storm/parser/ExpressionParser.cpp | 6 +++- src/storm/parser/ExpressionParser.h | 4 ++- .../settings/modules/AbstractionSettings.cpp | 14 +++++++++ .../settings/modules/AbstractionSettings.h | 15 ++++++++++ src/storm/settings/modules/IOSettings.h | 4 +-- .../storage/SymbolicModelDescription.cpp | 24 +++++++++++++++ src/storm/storage/SymbolicModelDescription.h | 2 ++ 12 files changed, 110 insertions(+), 16 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 5c5737f89..e9cb479a6 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -1,9 +1,16 @@ #include "storm/abstraction/AbstractionInformation.h" +#include + #include "storm/storage/BitVector.h" #include "storm/storage/dd/DdManager.h" +#include "storm/settings/modules/AbstractionSettings.h" +#include "storm/settings/SettingsManager.h" + +#include "storm/parser/ExpressionParser.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -15,7 +22,28 @@ namespace storm { template AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), allLocationIdentities(ddManager->getBddOne()), expressionToBddMap() { - // Intentionally left empty. + + // Obtain additional constraints from the settings. + auto const& settings = storm::settings::getModule(); + if (settings.isConstraintsSet()) { + std::string constraintsString = settings.getConstraintString(); + + std::vector constraintsAsStrings; + boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(",")); + + storm::parser::ExpressionParser expressionParser(expressionManager); + std::unordered_map variableMapping; + for (auto const& variableTypePair : expressionManager) { + variableMapping[variableTypePair.first.getName()] = variableTypePair.first; + } + expressionParser.setIdentifierMapping(variableMapping); + + for (auto const& constraintString : constraintsAsStrings) { + storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString); + STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << "."); + constraints.emplace_back(constraint); + } + } } template diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index 86a3b8412..e115aa28d 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -16,6 +16,10 @@ namespace storm { template StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::vector const& statePredicates, std::shared_ptr const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), relevantPredicatesAndVariables(), concretePredicateVariables(), forceRecomputation(true), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) { + for (auto const& constraint : abstractionInformation.getConstraints()) { + smtSolver->add(constraint); + } + // Assert all state predicates. for (auto const& predicate : statePredicates) { smtSolver->add(predicate); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index e6eab03dc..7c626b093 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -58,7 +58,9 @@ namespace storm { template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { - model.requireNoUndefinedConstants(); + + STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants."); + if (model.isPrismProgram()) { storm::prism::Program const& originalProgram = model.asPrismProgram(); STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); @@ -566,7 +568,7 @@ namespace storm { // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); - STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states."); +// STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states."); storm::dd::Bdd constraintStates = globalConstraintStates && game.getReachableStates(); storm::dd::Bdd targetStates = globalTargetStates && game.getReachableStates(); if (player1Direction == storm::OptimizationDirection::Minimize) { diff --git a/src/storm/parser/ExpressionCreator.cpp b/src/storm/parser/ExpressionCreator.cpp index b96dd5080..682342e29 100644 --- a/src/storm/parser/ExpressionCreator.cpp +++ b/src/storm/parser/ExpressionCreator.cpp @@ -16,6 +16,12 @@ namespace storm { // Intenetionally left empty. } + ExpressionCreator::~ExpressionCreator() { + if (deleteIdentifierMapping) { + delete this->identifiers; + } + } + storm::expressions::Expression ExpressionCreator::createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const { if (this->createExpressions) { try { @@ -241,7 +247,7 @@ namespace storm { void ExpressionCreator::setIdentifierMapping(std::unordered_map const& identifierMapping) { unsetIdentifierMapping(); - createExpressions =true; + createExpressions = true; identifiers = new qi::symbols(); for (auto const& identifierExpressionPair : identifierMapping) { identifiers->add(identifierExpressionPair.first, identifierExpressionPair.second); @@ -257,9 +263,6 @@ namespace storm { } this->identifiers = nullptr; } - - - } } diff --git a/src/storm/parser/ExpressionCreator.h b/src/storm/parser/ExpressionCreator.h index 20bcc5854..cdf36c1fc 100644 --- a/src/storm/parser/ExpressionCreator.h +++ b/src/storm/parser/ExpressionCreator.h @@ -19,11 +19,7 @@ namespace storm { public: ExpressionCreator(storm::expressions::ExpressionManager const& manager); - virtual ~ExpressionCreator() { - if (deleteIdentifierMapping) { - delete this->identifiers; - } - } + ~ExpressionCreator(); /*! * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp index 5d824d82d..eec7e8349 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm/parser/ExpressionParser.cpp @@ -38,7 +38,7 @@ namespace storm { namespace parser { ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerModuloOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerModuloOperator_(), invalidIdentifiers_(invalidIdentifiers_) { - expressionCreator = new ExpressionCreator(manager); + expressionCreator = std::make_unique(manager); identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); @@ -176,6 +176,10 @@ namespace storm { } } + ExpressionParser::~ExpressionParser() { + // Needed, because auto-generated destructor requires ExpressionCreator to be a complete type in the header. + } + void ExpressionParser::setIdentifierMapping(qi::symbols const* identifiers_) { expressionCreator->setIdentifierMapping(identifiers_); } diff --git a/src/storm/parser/ExpressionParser.h b/src/storm/parser/ExpressionParser.h index cb415c53e..d92de1e74 100644 --- a/src/storm/parser/ExpressionParser.h +++ b/src/storm/parser/ExpressionParser.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include "storm/parser/SpiritParserDefinitions.h" #include "storm/parser/SpiritErrorHandler.h" @@ -46,6 +47,7 @@ namespace storm { * also parses boolean conjuncts that are erroneously consumed by the expression parser. */ ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_ = qi::symbols(), bool enableErrorHandling = true, bool allowBacktracking = false); + ~ExpressionParser(); ExpressionParser(ExpressionParser const& other) = default; ExpressionParser& operator=(ExpressionParser const& other) = default; @@ -207,7 +209,7 @@ namespace storm { prefixPowerModuloOperatorStruct prefixPowerModuloOperator_; - ExpressionCreator* expressionCreator; + std::unique_ptr expressionCreator; // The symbol table of invalid identifiers. diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 404298782..fccd65722 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -25,6 +25,7 @@ namespace storm { const std::string AbstractionSettings::solveModeOptionName = "solve"; const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs"; const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred"; + const std::string AbstractionSettings::constraintsOptionName = "constraints"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -86,6 +87,11 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("off").build()) .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build()) + .build()); + } AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { @@ -176,6 +182,14 @@ namespace storm { return this->getOption(rankRefinementPredicatesOptionName).getArgumentByName("value").getValueAsString() == "on"; } + bool AbstractionSettings::isConstraintsSet() const { + return this->getOption(constraintsOptionName).getHasOptionBeenSet(); + } + + std::string AbstractionSettings::getConstraintString() const { + return this->getOption(constraintsOptionName).getArgumentByName("constraints").getValueAsString(); + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 7fe212fbd..7cd950042 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -123,6 +123,20 @@ namespace storm { */ bool isRankRefinementPredicatesSet() const; + /*! + * Retrieves whether the constraints option was set. + * + * @return True if the constraints option was set. + */ + bool isConstraintsSet() const; + + /*! + * Retrieves the string that specifies additional constraints. + * + * @return The string that defines the constraints. + */ + std::string getConstraintString() const; + const static std::string moduleName; private: @@ -138,6 +152,7 @@ namespace storm { const static std::string solveModeOptionName; const static std::string maximalAbstractionOptionName; const static std::string rankRefinementPredicatesOptionName; + const static std::string constraintsOptionName; }; } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index cc41176bf..7371cda76 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -214,9 +214,9 @@ namespace storm { std::string getChoiceLabelingFilename() const; /*! - * Retrieves whether the export-to-dot option was set. + * Retrieves whether the constants option was set. * - * @return True if the export-to-dot option was set. + * @return True if the constants option was set. */ bool isConstantsSet() const; diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index b08166125..d5387d73e 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -179,6 +179,30 @@ namespace storm { } } + bool SymbolicModelDescription::hasUndefinedConstants() const { + if (this->isPrismProgram()) { + return this->asPrismProgram().hasUndefinedConstants(); + } else { + return this->asJaniModel().hasUndefinedConstants(); + } + } + + std::vector SymbolicModelDescription::getUndefinedConstants() const { + std::vector result; + if (this->isPrismProgram()) { + std::vector> constants = this->asPrismProgram().getUndefinedConstants(); + for (auto const& constant : constants) { + result.emplace_back(constant.get().getExpressionVariable()); + } + } else { + std::vector> constants = this->asJaniModel().getUndefinedConstants(); + for (auto const& constant : constants) { + result.emplace_back(constant.get().getExpressionVariable()); + } + } + return result; + } + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) { if (model.isPrismProgram()) { out << model.asPrismProgram(); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index 137f1a7d4..c83f36358 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -47,6 +47,8 @@ namespace storm { std::map parseConstantDefinitions(std::string const& constantDefinitionString) const; void requireNoUndefinedConstants() const; + bool hasUndefinedConstants() const; + std::vector getUndefinedConstants() const; private: boost::optional> modelDescription;