From 2e756788f00e9d6a29ec17a5c38d59ee2cc5ed94 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 26 Nov 2016 12:40:22 +0100 Subject: [PATCH] refinement logic now fully in refiner object --- src/storm/abstraction/MenuGameAbstractor.h | 10 ++- src/storm/abstraction/MenuGameRefiner.cpp | 74 +++++++++---------- src/storm/abstraction/MenuGameRefiner.h | 13 +++- .../abstraction/prism/AbstractCommand.cpp | 10 +++ src/storm/abstraction/prism/AbstractCommand.h | 11 +++ .../abstraction/prism/AbstractModule.cpp | 10 +++ src/storm/abstraction/prism/AbstractModule.h | 14 ++++ .../abstraction/prism/AbstractProgram.cpp | 10 +++ src/storm/abstraction/prism/AbstractProgram.h | 14 ++++ .../prism/PrismMenuGameAbstractor.cpp | 20 ++--- .../prism/PrismMenuGameAbstractor.h | 6 +- 11 files changed, 138 insertions(+), 54 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 8fa79491b..9cc820d30 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -1,12 +1,19 @@ #pragma once +#include + #include "storm/storage/dd/DdType.h" #include "storm/abstraction/MenuGame.h" +#include "storm/storage/expressions/Expression.h" + namespace storm { namespace abstraction { + template + class AbstractionInformation; + template class MenuGameAbstractor { public: @@ -15,10 +22,11 @@ namespace storm { /// Retrieves information about the abstraction. virtual AbstractionInformation const& getAbstractionInformation() const = 0; + virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const = 0; + virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0; /// Methods to refine the abstraction. virtual void refine(std::vector const& predicates) = 0; - virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) = 0; /// Exports a representation of the current abstraction state in the dot format. virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const = 0; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index c2d7cd07d..3f809fb2b 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -1,14 +1,18 @@ #include "storm/abstraction/MenuGameRefiner.h" +#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/MenuGameAbstractor.h" #include "storm/utility/dd.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/AbstractionSettings.h" + namespace storm { namespace abstraction { template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitter(), equivalenceChecker(std::move(smtSolver)) { // Intentionally left empty. } @@ -47,14 +51,14 @@ namespace storm { return pivotState; } - template - void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { - AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + template + void MenuGameRefiner::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); // Decode the index of the command chosen by player 1. - storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); + storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); auto pl1It = player1ChoiceAsAdd.begin(); - uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); + uint_fast64_t player1Index = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); #ifdef LOCAL_DEBUG std::cout << "command index " << commandIndex << std::endl; std::cout << program.get() << std::endl; @@ -73,8 +77,8 @@ namespace storm { std::cout << "pivot is " << stateName.str() << std::endl; } #endif - storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; - storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); + // storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + // storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); #ifdef LOCAL_DEBUG player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); std::cout << concreteCommand << std::endl; @@ -84,19 +88,15 @@ namespace storm { // Check whether there are bottom states in the game and whether one of the choices actually picks the // bottom state as the successor. - bool buttomStateSuccessor = false; - if (!currentGame->getBottomStates().isZero()) { - buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); - } + bool buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate // command (that is the player 1 choice). if (buttomStateSuccessor) { STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); - abstractCommand.notifyGuardIsPredicate(); - storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); + storm::expressions::Expression newPredicate = abstractor.get().getGuard(player1Index); STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - this->refine({std::make_pair(newPredicate, true)}); + this->performRefinement({newPredicate}); } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); @@ -109,11 +109,11 @@ namespace storm { #ifdef LOCAL_DEBUG std::cout << "lower" << std::endl; #endif - std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); + std::map lowerChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(lowerChoice); #ifdef LOCAL_DEBUG std::cout << "upper" << std::endl; #endif - std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); + std::map upperChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(upperChoice); STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); #ifdef LOCAL_DEBUG @@ -145,8 +145,7 @@ namespace storm { // Now we know the point of the deviation (command, update, predicate). std::cout << "ref" << std::endl; std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl; - std::cout << concreteCommand.getUpdate(updateIndex) << std::endl; - newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify(); + newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(abstractor.get().getVariableUpdates(player1Index, updateIndex)).simplify(); break; } } @@ -155,8 +154,7 @@ namespace storm { STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - - this->refine({std::make_pair(newPredicate, true)}); + this->performRefinement({newPredicate}); } STORM_LOG_TRACE("Current set of predicates:"); @@ -166,7 +164,7 @@ namespace storm { } template - bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) { + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) const { STORM_LOG_TRACE("Trying refinement after qualitative check."); // Get all relevant strategies. storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); @@ -224,7 +222,7 @@ namespace storm { STORM_LOG_TRACE("Refining based on lower choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.get().refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + this->refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return true; @@ -237,7 +235,7 @@ namespace storm { if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.get().refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + this->refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return true; @@ -249,7 +247,7 @@ namespace storm { } template - bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) { + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const { STORM_LOG_TRACE("Refining after quantitative check."); // Get all relevant strategies. storm::dd::Bdd minPlayer1Strategy = quantitativeResult.min.player1Strategy; @@ -298,7 +296,7 @@ namespace storm { if (lowerChoicesDifferent) { STORM_LOG_TRACE("Refining based on lower choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.get().refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + this->refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); } else { @@ -310,7 +308,7 @@ namespace storm { if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.get().refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + this->refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); } else { @@ -322,12 +320,12 @@ namespace storm { template bool MenuGameRefiner::performRefinement(std::vector const& predicates) const { - for (auto const& predicate : predicates) { - storm::expressions::Expression const& predicate = predicateAllowSplitPair.first; - bool allowSplit = predicateAllowSplitPair.second; - STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); - - if (allowSplit && splitPredicates) { + if (splitPredicates) { + std::vector cleanedAtoms; + + for (auto const& predicate : predicates) { + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + // Split the predicates. std::vector atoms = splitter.split(predicate); @@ -342,14 +340,14 @@ namespace storm { } if (addAtom) { - uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom); - newPredicateIndices.push_back(newPredicateIndex); + cleanedAtoms.push_back(atom); } } - } else { - uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); - newPredicateIndices.push_back(newPredicateIndex); } + + abstractor.get().refine(cleanedAtoms); + } else { + abstractor.get().refine(predicates); } } diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 32e16e5e7..5e866f860 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -18,10 +18,10 @@ namespace storm { namespace abstraction { - template + template class MenuGameAbstractor; - template + template class MenuGame; template @@ -52,6 +52,8 @@ namespace storm { bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const; private: + void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; + /*! * Takes the given predicates, preprocesses them and then refines the abstractor. */ @@ -60,11 +62,14 @@ namespace storm { /// The underlying abstractor to refine. std::reference_wrapper> abstractor; + /// A flag indicating whether predicates shall be split before using them for refinement. + bool splitPredicates; + /// An object that can be used for splitting predicates. - storm::expressions::PredicateSplitter splitter; + mutable storm::expressions::PredicateSplitter splitter; /// An object that can be used to determine whether predicates are equivalent. - storm::expressions::EquivalenceChecker equivalenceChecker; + mutable storm::expressions::EquivalenceChecker equivalenceChecker; }; } diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/AbstractCommand.cpp index dd9b51efc..f41eb3e0f 100644 --- a/src/storm/abstraction/prism/AbstractCommand.cpp +++ b/src/storm/abstraction/prism/AbstractCommand.cpp @@ -71,6 +71,16 @@ namespace storm { bottomStateAbstractor.refine(predicates); } + template + storm::expressions::Expression const& AbstractCommand::getGuard() const { + return command.get().getGuardExpression(); + } + + template + std::map AbstractCommand::getVariableUpdates(uint64_t auxiliaryChoice) const { + return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); + } + template void AbstractCommand::recomputeCachedBdd() { STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h index 600693bbf..7cf45bee0 100644 --- a/src/storm/abstraction/prism/AbstractCommand.h +++ b/src/storm/abstraction/prism/AbstractCommand.h @@ -68,6 +68,17 @@ namespace storm { */ void refine(std::vector const& predicates); + /*! + * Retrieves the guard of this command. + */ + storm::expressions::Expression const& getGuard() const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given + * auxiliary choice. + */ + std::map getVariableUpdates(uint64_t auxiliaryChoice) const; + /*! * Computes the abstraction of the command wrt. to the current set of predicates. * diff --git a/src/storm/abstraction/prism/AbstractModule.cpp b/src/storm/abstraction/prism/AbstractModule.cpp index 24de6ba15..2c50b1401 100644 --- a/src/storm/abstraction/prism/AbstractModule.cpp +++ b/src/storm/abstraction/prism/AbstractModule.cpp @@ -36,6 +36,16 @@ namespace storm { } } + template + storm::expressions::Expression const& AbstractModule::getGuard(uint64_t player1Choice) const { + return commands[player1Choice].getGuard(); + } + + template + std::map AbstractModule::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + return commands[player1Choice].getVariableUpdates(auxiliaryChoice); + } + template GameBddResult AbstractModule::getAbstractBdd() { // First, we retrieve the abstractions of all commands. diff --git a/src/storm/abstraction/prism/AbstractModule.h b/src/storm/abstraction/prism/AbstractModule.h index b51be372e..82fb73f9f 100644 --- a/src/storm/abstraction/prism/AbstractModule.h +++ b/src/storm/abstraction/prism/AbstractModule.h @@ -50,6 +50,20 @@ namespace storm { */ void refine(std::vector const& predicates); + /*! + * Retrieves the guard of the given player 1 choice. + * + * @param player1Choice The choice of player 1. + * @return The guard of the player 1 choice. + */ + storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player + * 1 choice and auxiliary choice. + */ + std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const; + /*! * Computes the abstraction of the module wrt. to the current set of predicates. * diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp index da7ae8f56..a68c730cf 100644 --- a/src/storm/abstraction/prism/AbstractProgram.cpp +++ b/src/storm/abstraction/prism/AbstractProgram.cpp @@ -118,6 +118,16 @@ namespace storm { return abstractionInformation; } + template + storm::expressions::Expression const& AbstractProgram::getGuard(uint64_t player1Choice) const { + return modules.front().getGuard(player1Choice); + } + + template + std::map AbstractProgram::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice); + } + template storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h index b30d1eb39..fca4ab6c0 100644 --- a/src/storm/abstraction/prism/AbstractProgram.h +++ b/src/storm/abstraction/prism/AbstractProgram.h @@ -64,6 +64,20 @@ namespace storm { */ AbstractionInformation const& getAbstractionInformation() const; + /*! + * Retrieves the guard predicate of the given player 1 choice. + * + * @param player1Choice The choice for which to retrieve the guard. + * @return The guard of the player 1 choice. + */ + storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player + * 1 choice and auxiliary choice. + */ + std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const; + /*! * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it * was either given as an initial predicate or used as a refining predicate later. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index d2ac18a63..a4a1eae47 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -10,7 +10,7 @@ namespace storm { namespace prism { template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet(), storm::settings::getModule().isSplitPredicatesSet()) { + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet()) { // Intentionally left empty. } @@ -19,22 +19,24 @@ namespace storm { return abstractProgram.getAbstractGame(); } + template AbstractionInformation const& PrismMenuGameAbstractor::getAbstractionInformation() const { return abstractProgram.getAbstractionInformation(); } template - void PrismMenuGameAbstractor::refine(std::vector const& predicates) { - std::vector> predicatesWithFlags; - for (auto const& predicate : predicates) { - predicatesWithFlags.emplace_back(predicate, true); - } - abstractProgram.refine(predicatesWithFlags); + storm::expressions::Expression const& PrismMenuGameAbstractor::getGuard(uint64_t player1Choice) const { + return abstractProgram.getGuard(player1Choice); + } + + template + std::map PrismMenuGameAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + return abstractProgram.getVariableUpdates(player1Choice, auxiliaryChoice); } template - void PrismMenuGameAbstractor::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { - abstractProgram.refine(pivotState, player1Choice, lowerChoice, upperChoice); + void PrismMenuGameAbstractor::refine(std::vector const& predicates) { + abstractProgram.refine(predicates); } template diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index ff59beb8a..9b856ba3d 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -14,10 +14,12 @@ namespace storm { PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); virtual storm::abstraction::MenuGame abstract() override; + virtual AbstractionInformation const& getAbstractionInformation() const override; - + virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override; + virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override; + virtual void refine(std::vector const& predicates) override; - virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) override; void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override;