diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 524d772be..aaca1ec04 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -553,12 +553,72 @@ namespace storm { } } + std::vector parseConstraints(storm::expressions::ExpressionManager const& expressionManager, std::string const& constraintsString) { + std::vector constraints; + + 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); + } + + return constraints; + } + + std::vector> parseInjectedRefinementPredicates(storm::expressions::ExpressionManager const& expressionManager, std::string const& refinementPredicatesString) { + std::vector> injectedRefinementPredicates; + + storm::parser::ExpressionParser expressionParser(expressionManager); + std::unordered_map variableMapping; + for (auto const& variableTypePair : expressionManager) { + variableMapping[variableTypePair.first.getName()] = variableTypePair.first; + } + expressionParser.setIdentifierMapping(variableMapping); + + std::vector predicateGroupsAsStrings; + boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";")); + + for (auto const& predicateGroupString : predicateGroupsAsStrings) { + std::vector predicatesAsStrings; + boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":")); + + injectedRefinementPredicates.emplace_back(); + for (auto const& predicateString : predicatesAsStrings) { + storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString); + STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); + injectedRefinementPredicates.back().emplace_back(predicate); + } + STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step."); + + // Finally reverse the list, because we take the predicates from the back. + std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end()); + } + + // Finally reverse the list, because we take the predicates from the back. + std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end()); + + return injectedRefinementPredicates; + } + template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - verifyProperties(input, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule(); + storm::api::AbstractionRefinementOptions options(parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()), parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates())); + + verifyProperties(input, [&input,&options] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); - return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); + return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true), options); }); } diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 7e3215b3b..23fb06985 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -1,16 +1,9 @@ #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-parsers/parser/ExpressionParser.h" - #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -21,29 +14,8 @@ namespace storm { namespace abstraction { 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() { - - // 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); - } - } + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, AbstractionInformationOptions const& options, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), constraints(options.constraints), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), allLocationIdentities(ddManager->getBddOne()), expressionToBddMap() { + // Intentionally left empty. } template diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index e47e7ab2b..a6eb1f9c5 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -27,6 +27,16 @@ namespace storm { namespace abstraction { + struct AbstractionInformationOptions { + AbstractionInformationOptions() = default; + + AbstractionInformationOptions(std::vector const& constraints) : constraints(constraints) { + // Intentionally left empty. + } + + std::vector constraints; + }; + template class AbstractionInformation { public: @@ -38,7 +48,7 @@ namespace storm { * @param smtSolver An SMT solver that is used to detect equivalent predicates. * @param ddManager The manager responsible for the DDs. */ - AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager = std::make_shared>()); + AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, AbstractionInformationOptions const& options = AbstractionInformationOptions(), std::shared_ptr> ddManager = std::make_shared>()); /*! * Adds the given variable. diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 1887d60ec..92b3cc97b 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -21,6 +21,15 @@ namespace storm { template class AbstractionInformation; + struct MenuGameAbstractorOptions { + MenuGameAbstractorOptions() = default; + MenuGameAbstractorOptions(std::vector&& constraints) : constraints(std::move(constraints)) { + // Intentionally left empty. + } + + std::vector constraints; + }; + template class MenuGameAbstractor { public: diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 292257965..23f2f4f34 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -66,7 +66,7 @@ namespace storm { } template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(false), splitPredicates(false), rankPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver, MenuGameRefinerOptions const& options) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(false), splitPredicates(false), rankPredicates(false), addedAllGuardsFlag(false), refinementPredicatesToInject(options.refinementPredicates), pivotSelectionHeuristic(), splitter(), equivalenceChecker(std::move(smtSolver)) { auto const& abstractionSettings = storm::settings::getModule(); @@ -97,39 +97,6 @@ namespace storm { storm::expressions::Expression initialExpression = this->abstractor.get().getInitialExpression(); performRefinement(createGlobalRefinement(preprocessPredicates({initialExpression}, RefinementPredicates::Source::InitialExpression))); } - - if (abstractionSettings.isInjectRefinementPredicatesSet()) { - auto const& expressionManager = abstractor.getAbstractionInformation().getExpressionManager(); - storm::parser::ExpressionParser expressionParser(expressionManager); - std::unordered_map variableMapping; - for (auto const& variableTypePair : expressionManager) { - variableMapping[variableTypePair.first.getName()] = variableTypePair.first; - } - expressionParser.setIdentifierMapping(variableMapping); - - std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates(); - std::vector predicateGroupsAsStrings; - boost::split(predicateGroupsAsStrings, predicatesString, boost::is_any_of(";")); - - for (auto const& predicateGroupString : predicateGroupsAsStrings) { - std::vector predicatesAsStrings; - boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":")); - - refinementPredicatesToInject.emplace_back(); - for (auto const& predicateString : predicatesAsStrings) { - storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString); - STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); - refinementPredicatesToInject.back().emplace_back(predicate); - } - STORM_LOG_THROW(!refinementPredicatesToInject.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step."); - - // Finally reverse the list, because we take the predicates from the back. - std::reverse(refinementPredicatesToInject.back().begin(), refinementPredicatesToInject.back().end()); - } - - // Finally reverse the list, because we take the predicates from the back. - std::reverse(refinementPredicatesToInject.begin(), refinementPredicatesToInject.end()); - } } template diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index cb6d48fd4..c8a384057 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -98,13 +98,23 @@ namespace storm { template class ExplicitQuantitativeResultMinMax; + struct MenuGameRefinerOptions { + MenuGameRefinerOptions() = default; + + MenuGameRefinerOptions(std::vector>&& refinementPredicates) : refinementPredicates(std::move(refinementPredicates)) { + // Intentionally left empty. + } + + std::vector> refinementPredicates; + }; + template class MenuGameRefiner { public: /*! * Creates a refiner for the provided abstractor. */ - MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver); + MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver, MenuGameRefinerOptions const& options = MenuGameRefinerOptions()); /*! * Refines the abstractor with the given predicates. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 493b70e4b..a71d78f04 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -35,7 +35,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager()), AbstractionInformationOptions(options.constraints)), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { // Check whether the model is linear as the abstraction requires this. STORM_LOG_WARN_COND(model.isLinear(), "The model appears to contain non-linear expressions, which may cause malfunctioning of the abstraction."); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 80c625072..d9f04f828 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -46,7 +46,7 @@ namespace storm { * @param model The concrete model for which to build the abstraction. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory); + JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options = MenuGameAbstractorOptions()); JaniMenuGameAbstractor(JaniMenuGameAbstractor const&) = default; JaniMenuGameAbstractor& operator=(JaniMenuGameAbstractor const&) = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 92b7e3bfb..19001708a 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -33,8 +33,8 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) - : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options) + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager()), AbstractionInformationOptions(options.constraints)), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index a9ef79413..91c4fd2c7 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -46,7 +46,7 @@ namespace storm { * @param program The concrete program for which to build the abstraction. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory); + PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options = MenuGameAbstractorOptions()); PrismMenuGameAbstractor(PrismMenuGameAbstractor const&) = default; PrismMenuGameAbstractor& operator=(PrismMenuGameAbstractor const&) = default; diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 2bec11dcf..27392b81e 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -24,6 +24,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/AbstractionSettings.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" @@ -37,19 +38,31 @@ namespace storm { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); } + struct AbstractionRefinementOptions { + AbstractionRefinementOptions() = default; + AbstractionRefinementOptions(std::vector&& constraints, std::vector>&& injectedRefinementPredicates) : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { + // Intentionally left empty. + } + + std::vector constraints; + std::vector> injectedRefinementPredicates; + }; + template - typename std::enable_if::value || std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { + typename std::enable_if::value || std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); std::unique_ptr result; + storm::modelchecker::GameBasedMdpModelCheckerOptions modelCheckerOptions(options.constraints, options.injectedRefinementPredicates); + if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } @@ -60,7 +73,7 @@ namespace storm { } template - typename std::enable_if::value && !std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { + typename std::enable_if::value && !std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&, AbstractionRefinementOptions const& = AbstractionRefinementOptions()) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); } diff --git a/src/storm/logic/RewardAccumulation.cpp b/src/storm/logic/RewardAccumulation.cpp index 32065268a..4a4ba4366 100644 --- a/src/storm/logic/RewardAccumulation.cpp +++ b/src/storm/logic/RewardAccumulation.cpp @@ -3,7 +3,7 @@ namespace storm { namespace logic { - RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : steps(steps), time(time), exit(exit){ + RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : time(time), steps(steps), exit(exit){ // Intentionally left empty } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index d1cb9190b..30a495706 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -60,7 +60,7 @@ namespace storm { using detail::PreviousExplicitResult; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision(), storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision(), storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { if (model.hasUndefinedConstants()) { auto undefinedConstants = model.getUndefinedConstants(); @@ -559,10 +559,11 @@ namespace storm { storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask); // Create the abstractor. + storm::abstraction::MenuGameAbstractorOptions abstractorOptions(std::move(options.constraints)); if (preprocessedModel.isPrismProgram()) { - abstractor = std::make_shared>(preprocessedModel.asPrismProgram(), smtSolverFactory); + abstractor = std::make_shared>(preprocessedModel.asPrismProgram(), smtSolverFactory, abstractorOptions); } else { - abstractor = std::make_shared>(preprocessedModel.asJaniModel(), smtSolverFactory); + abstractor = std::make_shared>(preprocessedModel.asJaniModel(), smtSolverFactory, abstractorOptions); } if (!constraintExpression.isTrue()) { abstractor->addTerminalStates(!constraintExpression); @@ -571,7 +572,8 @@ namespace storm { abstractor->setTargetStates(targetStateExpression); // Create a refiner that can be used to refine the abstraction when needed. - storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); + storm::abstraction::MenuGameRefinerOptions refinerOptions(std::move(options.injectedRefinementPredicates)); + storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()), refinerOptions); refiner.refine(initialPredicates, false); storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index c8af37073..513b688e4 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -3,6 +3,8 @@ #include "storm/modelchecker/AbstractModelChecker.h" +#include + #include "storm/storage/prism/Program.h" #include "storm/storage/dd/DdType.h" @@ -18,6 +20,11 @@ #include "storm/settings/modules/AbstractionSettings.h" +#include "storm-parsers/parser/ExpressionParser.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + #include "storm/utility/ConstantsComparator.h" #include "storm/utility/solver.h" #include "storm/utility/graph.h" @@ -72,6 +79,16 @@ namespace storm { }; } + struct GameBasedMdpModelCheckerOptions { + GameBasedMdpModelCheckerOptions() = default; + GameBasedMdpModelCheckerOptions(std::vector const& constraints, std::vector> const& injectedRefinementPredicates) : constraints(constraints), injectedRefinementPredicates(injectedRefinementPredicates) { + // Intentionally left empty. + } + + std::vector constraints; + std::vector> injectedRefinementPredicates; + }; + template class GameBasedMdpModelChecker : public AbstractModelChecker { public: @@ -82,9 +99,10 @@ namespace storm { * verification calls will be answererd with respect to this model. * * @param model The model description that (symbolically) specifies the model to check. + * @param options Additional options for the abstraction-refinement process. * @param smtSolverFactory A factory used to create SMT solver when necessary. */ - explicit GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory = std::make_shared()); + explicit GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options = GameBasedMdpModelCheckerOptions(), std::shared_ptr const& smtSolverFactory = std::make_shared()); /// Overridden methods from super class. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -125,6 +143,9 @@ namespace storm { */ storm::expressions::Expression getExpression(storm::logic::Formula const& formula); + /// The options customizing the abstraction-refinement process. + GameBasedMdpModelCheckerOptions options; + /// The preprocessed model that contains only one module/automaton and otherwhise corresponds to the semantics /// of the original model description. storm::storage::SymbolicModelDescription preprocessedModel;