From dfa8d6a8e5585569bf3dfcc09a19e0ea7ff61d93 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 19 Jan 2016 16:57:28 +0100 Subject: [PATCH] started working on games again Former-commit-id: a27d6a68389bed4d6ee33e535c538fe1164be732 --- src/parser/PrismParser.cpp | 2 +- src/storage/dd/DdManager.cpp | 6 ++ src/storage/dd/DdManager.h | 10 +++- .../prism/menu_games/AbstractCommand.cpp | 20 +++---- .../prism/menu_games/AbstractCommand.h | 4 +- .../prism/menu_games/AbstractModule.cpp | 2 +- src/storage/prism/menu_games/AbstractModule.h | 2 +- .../prism/menu_games/AbstractProgram.cpp | 29 +++++++--- .../prism/menu_games/AbstractProgram.h | 2 +- .../menu_games/AbstractionDdInformation.cpp | 2 +- .../AbstractionExpressionInformation.cpp | 32 +++++++++++ .../AbstractionExpressionInformation.h | 57 +++++++++++++++++++ .../prism/menu_games/StateSetAbstractor.cpp | 16 +++--- .../prism/menu_games/StateSetAbstractor.h | 4 +- .../prism/menu_games/VariablePartition.h | 2 +- 15 files changed, 152 insertions(+), 38 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b2349ebf7..9040f3cf4 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -142,7 +142,7 @@ namespace storm { assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); updateListDefinition %= +updateDefinition(qi::_r1) % "+"; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index d3eeead6f..a6b267ae8 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -95,6 +95,12 @@ namespace storm { return result; } + template + Bdd DdManager::getCube(storm::expressions::Variable const& variable) const { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + return metaVariable.getCube(); + } + template std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional> const& position) { // Check whether the variable name is legal. diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index c299336d6..64588b91c 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -102,7 +102,7 @@ namespace storm { /*! * Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal - * values of the range of the meta variable to themselves. + * values of the range of the meta variable to the values themselves. * * @param variable The expression variable associated with the meta variable. * @return The identity of the meta variable. @@ -110,6 +110,14 @@ namespace storm { template Add getIdentity(storm::expressions::Variable const& variable) const; + /*! + * Retrieves a BDD that is the cube of the variables representing the given meta variable. + * + * @param variable The expression variable associated with the meta variable. + * @return The cube of the meta variable. + */ + Bdd getCube(storm::expressions::Variable const& variable) const; + /*! * Adds an integer meta variable with the given range. * diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 10f03967d..1c050cbc5 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -18,13 +18,13 @@ namespace storm { namespace prism { namespace menu_games { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); // Assert all range expressions to enforce legal variable values. - for (auto const& rangeExpression : expressionInformation.rangeExpressions) { + for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) { smtSolver->add(rangeExpression); } @@ -32,8 +32,8 @@ namespace storm { smtSolver->add(command.getGuardExpression()); // Refine the command based on all initial predicates. - std::vector allPredicateIndices(expressionInformation.predicates.size()); - for (auto index = 0; index < expressionInformation.predicates.size(); ++index) { + std::vector allPredicateIndices(expressionInformation.getPredicates().size()); + for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); @@ -43,7 +43,7 @@ namespace storm { void AbstractCommand::refine(std::vector const& predicates) { // Add all predicates to the variable partition. for (auto predicateIndex : predicates) { - variablePartition.addExpression(expressionInformation.predicates[predicateIndex]); + variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]); } STORM_LOG_TRACE("Current variable partition is: " << variablePartition); @@ -173,9 +173,9 @@ namespace storm { template void AbstractCommand::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { // Determine and add new relevant source predicates. - std::vector> newSourceVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.first, newRelevantPredicates.first); + std::vector> newSourceVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { - smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second])); decisionVariables.push_back(element.first); } @@ -185,9 +185,9 @@ namespace storm { // Do the same for every update. for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { - std::vector> newSuccessorVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + std::vector> newSuccessorVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); for (auto const& element : newSuccessorVariables) { - smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); decisionVariables.push_back(element.first); } @@ -277,7 +277,7 @@ namespace storm { auto relevantIte = relevantPredicatesAndVariables.first.end(); storm::dd::Bdd result = ddInformation.manager->getBddOne(); - for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) { + for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.getPredicates().size(); ++predicateIndex) { if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { result &= ddInformation.predicateIdentities[predicateIndex]; } else { diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index c3396df6b..77db969fe 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -50,7 +50,7 @@ namespace storm { * @param ddInformation The DD-related information including the manager. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstract command with the given predicates. @@ -156,7 +156,7 @@ namespace storm { std::unique_ptr smtSolver; // The expression-related information. - AbstractionExpressionInformation const& expressionInformation; + AbstractionExpressionInformation& expressionInformation; // The DD-related information. AbstractionDdInformation const& ddInformation; diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index c13a64274..c9d597d02 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -13,7 +13,7 @@ namespace storm { namespace menu_games { template - AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) { + AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index 7013efaa0..473eb4913 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -31,7 +31,7 @@ namespace storm { * @param ddInformation The DD-related information including the manager. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstract module with the given predicates. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index ad1e7e7e0..fd2403a91 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -17,7 +17,7 @@ namespace storm { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { // 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. @@ -30,7 +30,8 @@ namespace storm { // If we were requested to add all guards to the set of predicates, we do so now. for (auto const& command : module.getCommands()) { if (addAllGuards) { - expressionInformation.predicates.push_back(command.getGuardExpression()); + expressionInformation.getPredicates().push_back(command.getGuardExpression()); + allGuards.push_back(command.getGuardExpression()); } maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); } @@ -39,18 +40,28 @@ namespace storm { } // Create DD variable for the command encoding. - ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; + ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; // Create DD variable for update encoding. - ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; + ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first; // Create DD variables encoding the nondeterministic choices of player 2. // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices. // If for some reason this should not be enough, we could grow this vector dynamically, but odds are // that it's impossible to treat such models in any event. for (uint_fast64_t index = 0; index < 100; ++index) { - storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index), std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; - ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->template getIdentity(newOptionVar).toBdd())); + storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first; + ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getEncoding(newOptionVar, 1))); + } + + // Now that we have created all other DD variables, we create the DD variables for the predicates. + if (addAllGuards) { + for (auto const& guard : allGuards) { + ddInformation.addPredicate(guard); + } + } + for (auto const& predicate : initialPredicates) { + ddInformation.addPredicate(predicate); } // For each module of the concrete program, we create an abstract counterpart. @@ -70,7 +81,7 @@ namespace storm { STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); // Add the predicates to the global list of predicates. - uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size(); + uint_fast64_t firstNewPredicateIndex = expressionInformation.getPredicates().size(); expressionInformation.addPredicates(predicates); // Create DD variables and some auxiliary data structures for the new predicates. @@ -81,7 +92,7 @@ namespace storm { // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors. std::vector newPredicateIndices; - for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.predicates.size(); ++index) { + for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.getPredicates().size(); ++index) { newPredicateIndices.push_back(index); } @@ -110,7 +121,7 @@ namespace storm { storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); uint_fast64_t index = 0; - for (auto const& knownPredicate : expressionInformation.predicates) { + for (auto const& knownPredicate : expressionInformation.getPredicates()) { if (knownPredicate.areSame(predicate)) { return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; } diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index ce30ec1cb..ceccb33fc 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -62,7 +62,7 @@ namespace storm { storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); /*! - * Refines the abstract module with the given predicates. + * Refines the abstract program with the given predicates. * * @param predicates The new predicates. */ diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 70eddd811..a60bdb80f 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -53,7 +53,7 @@ namespace storm { predicateDdVariables.push_back(newMetaVariable); predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1)); - predicateIdentities.push_back(manager->template getIdentity(newMetaVariable.first).equals(manager->template getIdentity(newMetaVariable.second))); + predicateIdentities.push_back(manager->getEncoding(newMetaVariable.first, 1).iff(manager->getEncoding(newMetaVariable.second, 1))); allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp index b3fd5a64a..621d59c01 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp @@ -20,6 +20,38 @@ namespace storm { this->addPredicate(predicate); } } + + storm::expressions::ExpressionManager& AbstractionExpressionInformation::getManager() { + return manager; + } + + storm::expressions::ExpressionManager const& AbstractionExpressionInformation::getManager() const { + return manager; + } + + std::vector& AbstractionExpressionInformation::getPredicates() { + return predicates; + } + + std::vector const& AbstractionExpressionInformation::getPredicates() const { + return predicates; + } + + std::set& AbstractionExpressionInformation::getVariables() { + return variables; + } + + std::set const& AbstractionExpressionInformation::getVariables() const { + return variables; + } + + std::vector& AbstractionExpressionInformation::getRangeExpressions() { + return rangeExpressions; + } + + std::vector const& AbstractionExpressionInformation::getRangeExpressions() const { + return rangeExpressions; + } } } diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h index 2037fa364..25c23cb30 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h @@ -40,6 +40,63 @@ namespace storm { */ void addPredicates(std::vector const& predicates); + /*! + * Retrieves the expression manager. + * + * @return The manager. + */ + storm::expressions::ExpressionManager& getManager(); + + /*! + * Retrieves the expression manager. + * + * @return The manager. + */ + storm::expressions::ExpressionManager const& getManager() const; + + /*! + * Retrieves all currently known predicates. + * + * @return The list of known predicates. + */ + std::vector& getPredicates(); + + /*! + * Retrieves all currently known predicates. + * + * @return The list of known predicates. + */ + std::vector const& getPredicates() const; + + /*! + * Retrieves all currently known variables. + * + * @return The set of known variables. + */ + std::set& getVariables(); + + /*! + * Retrieves all currently known variables. + * + * @return The set of known variables. + */ + std::set const& getVariables() const; + + /*! + * Retrieves a list of expressions that ensure the ranges of the variables. + * + * @return The range expressions. + */ + std::vector& getRangeExpressions(); + + /*! + * Retrieves a list of expressions that ensure the ranges of the variables. + * + * @return The range expressions. + */ + std::vector const& getRangeExpressions() const; + + private: // The manager responsible for the expressions of the program and the SMT solvers. storm::expressions::ExpressionManager& manager; diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp index 06ac2728e..db8dab01d 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.cpp +++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp @@ -13,10 +13,10 @@ namespace storm { namespace menu_games { template - StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) { + StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) { // Assert all range expressions to enforce legal variable values. - for (auto const& rangeExpression : expressionInformation.rangeExpressions) { + for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) { smtSolver->add(rangeExpression); } @@ -31,8 +31,8 @@ namespace storm { } // Refine the command based on all initial predicates. - std::vector allPredicateIndices(expressionInformation.predicates.size()); - for (auto index = 0; index < expressionInformation.predicates.size(); ++index) { + std::vector allPredicateIndices(expressionInformation.getPredicates().size()); + for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); @@ -40,10 +40,10 @@ namespace storm { template void StateSetAbstractor::addMissingPredicates(std::set const& newRelevantPredicateIndices) { - std::vector> newPredicateVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables, newRelevantPredicateIndices); + std::vector> newPredicateVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices); for (auto const& element : newPredicateVariables) { - smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second])); decisionVariables.push_back(element.first); } @@ -55,7 +55,7 @@ namespace storm { void StateSetAbstractor::refine(std::vector const& newPredicates) { // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction. for (auto const& predicateIndex : newPredicates) { - variablePartition.addExpression(expressionInformation.predicates[predicateIndex]); + variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]); } needsRecomputation = true; } @@ -135,7 +135,7 @@ namespace storm { smtSolver->push(); // Then add the constraint. - std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap); + std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap); for (auto const& expression : result.first) { smtSolver->add(expression); diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h index c722d695b..fef77eb29 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.h +++ b/src/storage/prism/menu_games/StateSetAbstractor.h @@ -58,7 +58,7 @@ namespace storm { * supposed to abstract. * @param smtSolverFactory A factory that can create new SMT solvers. */ - StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstractor by making the given predicates new abstract predicates. @@ -116,7 +116,7 @@ namespace storm { std::unique_ptr smtSolver; // The expression-related information. - AbstractionExpressionInformation const& expressionInformation; + AbstractionExpressionInformation& expressionInformation; // The DD-related information. AbstractionDdInformation const& ddInformation; diff --git a/src/storage/prism/menu_games/VariablePartition.h b/src/storage/prism/menu_games/VariablePartition.h index ae6637943..b9d87dad1 100644 --- a/src/storage/prism/menu_games/VariablePartition.h +++ b/src/storage/prism/menu_games/VariablePartition.h @@ -74,7 +74,7 @@ namespace storm { uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const; /*! - * Retrieves the number of blocks of the varible partition. + * Retrieves the number of blocks of the variable partition. * * @return The number of blocks in this partition. */