From bf294882191f423662b8484d0dc01e60cd7b3f9e Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 20 Dec 2016 13:21:54 +0100 Subject: [PATCH] fix for decomposition --- .../abstraction/AbstractionInformation.cpp | 18 +-- .../abstraction/AbstractionInformation.h | 24 +-- src/storm/abstraction/MenuGameAbstractor.cpp | 140 ++++++++++++++++++ src/storm/abstraction/MenuGameAbstractor.h | 7 +- src/storm/abstraction/MenuGameRefiner.cpp | 2 + .../abstraction/jani/AutomatonAbstractor.cpp | 2 +- src/storm/abstraction/jani/EdgeAbstractor.cpp | 4 +- .../jani/JaniMenuGameAbstractor.cpp | 139 +---------------- .../abstraction/jani/JaniMenuGameAbstractor.h | 3 + .../abstraction/prism/ModuleAbstractor.cpp | 2 +- .../prism/PrismMenuGameAbstractor.cpp | 135 +---------------- .../prism/PrismMenuGameAbstractor.h | 7 +- .../abstraction/GameBasedMdpModelChecker.cpp | 2 +- src/storm/utility/graph.cpp | 3 +- 14 files changed, 186 insertions(+), 302 deletions(-) create mode 100644 src/storm/abstraction/MenuGameAbstractor.cpp diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 4cfd9ee3f..c74cb60cb 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -64,6 +64,7 @@ namespace storm { sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); sourcePredicateVariables.insert(newMetaVariable.first); + successorPredicateVariables.insert(newMetaVariable.second); orderedSourcePredicateVariables.push_back(newMetaVariable.first); orderedSuccessorPredicateVariables.push_back(newMetaVariable.second); ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; @@ -223,16 +224,6 @@ namespace storm { uint_fast64_t AbstractionInformation::decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const { return decodeChoice(valuation, start, end, auxVariables); } - - template - storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const { - storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t index = start; index < end; ++index) { - result &= !player2VariableBdds[index]; - } - STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); - return result; - } template std::vector const& AbstractionInformation::getPlayer1Variables() const { @@ -283,7 +274,12 @@ namespace storm { std::set const& AbstractionInformation::getSourcePredicateVariables() const { return sourcePredicateVariables; } - + + template + std::set const& AbstractionInformation::getSuccessorPredicateVariables() const { + return successorPredicateVariables; + } + template std::vector const& AbstractionInformation::getOrderedSourcePredicateVariables() const { return orderedSourcePredicateVariables; diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index c9bdb3e7a..093342993 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -241,16 +241,6 @@ namespace storm { * @return The decoded auxiliary index. */ uint_fast64_t decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const; - - /*! - * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). - * - * @param numberOfVariables The number of variables to use in total. The number of variables in the returned - * cube is the number of variables minus the offset. - * @param offset The first variable of the range to return. - * @return The cube of variables starting from the offset until the given number of variables is reached. - */ - storm::dd::Bdd getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const; /*! * Retrieves the meta variables associated with the player 1 choices. @@ -347,7 +337,14 @@ namespace storm { * @return All source predicate meta variables. */ std::set const& getSourcePredicateVariables() const; - + + /*! + * Retrieves the set of successor predicate meta variables. + * + * @return All successor predicate meta variables. + */ + std::set const& getSuccessorPredicateVariables() const; + /*! * Retrieves a BDD representing the identities of all predicates. * @@ -570,7 +567,10 @@ namespace storm { /// The set of all source predicate variables. std::set sourcePredicateVariables; - + + /// The set of all successor predicate variables. + std::set successorPredicateVariables; + /// An ordered collection of the source variables. std::vector orderedSourcePredicateVariables; diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp new file mode 100644 index 000000000..9b0a11cc0 --- /dev/null +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -0,0 +1,140 @@ +#include "storm/abstraction/MenuGameAbstractor.h" + +#include "storm/abstraction/AbstractionInformation.h" + +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/utility/dd.h" + +#include "storm-config.h" +#include "storm/adapters/CarlAdapter.h" + +namespace storm { + namespace abstraction { + + template + std::string getStateName(std::pair const& stateValue, std::set const& locationVariables, std::set const& predicateVariables, storm::expressions::Variable const& bottomVariable) { + std::stringstream stateName; + + if (!locationVariables.empty()) { + stateName << "loc"; + } + + for (auto const& variable : locationVariables) { + stateName << stateValue.first.getIntegerValue(variable); + } + + if (!locationVariables.empty() && !predicateVariables.empty()) { + stateName << "_"; + } + + for (auto const& variable : predicateVariables) { + if (stateValue.first.getBooleanValue(variable)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + + if (stateValue.first.getBooleanValue(bottomVariable)) { + stateName << "bot"; + } + return stateName.str(); + } + + template + void MenuGameAbstractor::exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { + + std::ofstream out(filename); + AbstractionInformation const& abstractionInformation = this->getAbstractionInformation(); + + storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame.getTransitionMatrix(); + storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame.getNondeterminismVariables()); + storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame.getInitialStates(), filteredTransitionsBdd, currentGame.getRowVariables(), currentGame.getColumnVariables()); + filteredTransitions *= filteredReachableStates.template toAdd(); + + // Determine all initial states so we can color them blue. + std::unordered_set initialStates; + storm::dd::Add initialStatesAsAdd = currentGame.getInitialStates().template toAdd(); + for (auto stateValue : initialStatesAsAdd) { + initialStates.insert(getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true))); + } + + // Determine all highlight states so we can color them red. + std::unordered_set highlightStates; + storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); + for (auto stateValue : highlightStatesAdd) { + highlightStates.insert(getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true))); + } + + out << "digraph game {" << std::endl; + + // Create the player 1 nodes. + storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); + for (auto stateValue : statesAsAdd) { + out << "\tpl1_"; + std::string stateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)); + out << stateName; + out << " [ label=\""; + if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { + out << "*\", margin=0, width=0, height=0, shape=\"none\""; + } else { + out << stateName << "\", margin=0, width=0, height=0, shape=\"oval\""; + } + bool isInitial = initialStates.find(stateName) != initialStates.end(); + bool isHighlight = highlightStates.find(stateName) != highlightStates.end(); + if (isInitial && isHighlight) { + out << ", style=\"filled\", fillcolor=\"yellow\""; + } else if (isInitial) { + out << ", style=\"filled\", fillcolor=\"blue\""; + } else if (isHighlight) { + out << ", style=\"filled\", fillcolor=\"red\""; + } + out << " ];" << std::endl; + } + + // Create the nodes of the second player. + storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame.getColumnVariables()).existsAbstract(currentGame.getPlayer2Variables()).template toAdd(); + for (auto stateValue : player2States) { + out << "\tpl2_"; + std::string stateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)); + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + out << stateName << "_" << index; + out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; + out << "\tpl1_" << stateName << " -> " << "pl2_" << stateName << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + // Create the nodes of the probabilistic player. + storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame.getColumnVariables()).template toAdd(); + for (auto stateValue : playerPStates) { + out << "\tplp_"; + std::stringstream stateNameStream; + stateNameStream << getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)); + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + stateNameStream << "_" << index; + std::string stateName = stateNameStream.str(); + index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame.getPlayer2Variables().size()); + out << stateName << "_" << index; + out << " [ shape=\"point\", label=\"\" ];" << std::endl; + out << "\tpl2_" << stateName << " -> " << "plp_" << stateName << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + for (auto stateValue : filteredTransitions) { + std::string sourceStateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)); + std::string successorStateName = getStateName(stateValue, abstractionInformation.getSuccessorLocationVariables(), abstractionInformation.getSuccessorPredicateVariables(), abstractionInformation.getBottomStateVariable(false)); + uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame.getPlayer2Variables().size()); + out << "\tplp_" << sourceStateName << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName << " [ label=\"" << stateValue.second << "\"];" << std::endl; + } + + out << "}" << std::endl; + } + + template class MenuGameAbstractor; + template class MenuGameAbstractor; + +#ifdef STORM_HAVE_CARL + template class MenuGameAbstractor; +#endif + } +} diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 099d27440..283559470 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -42,9 +42,12 @@ namespace storm { /// Methods to refine the abstraction. virtual void refine(RefinementCommand const& command) = 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; + virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const = 0; + + protected: + void exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const; }; } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 9531d2e04..ff84b0f9b 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -438,6 +438,7 @@ namespace storm { std::map oldToNewVariables; for (auto const& variable : oldVariables) { + std::cout << "got old variable " << variable.getName() << std::endl; oldToNewVariables[variable] = expressionManager.getVariable(variable.getName()); } std::map lastSubstitution; @@ -470,6 +471,7 @@ namespace storm { // Retrieve the variable updates that the predecessor needs to perform to get to the current state. auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor)); for (auto const& update : variableUpdates) { + std::cout << "looking up old variable " << update.first.getName() << std::endl; storm::expressions::Variable newVariable = oldToNewVariables.at(update.first); if (update.second.hasBooleanType()) { predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution))); diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 673bb3c79..f22760db8 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -69,7 +69,7 @@ namespace storm { // DDs use the same amount DD variable encoding the choices of player 2. storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& edgeDd : edgeDdsAndUsedOptionVariableCounts) { - result |= edgeDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); + result |= edgeDd.bdd && this->getAbstractionInformation().encodePlayer2Choice(1, edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } return GameBddResult(result, maximalNumberOfUsedOptionVariables); } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index b333739ef..e95690d8e 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -81,7 +81,7 @@ namespace storm { template void EdgeAbstractor::recomputeCachedBddWithDecomposition() { - STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard() << " using the decomposition."); + STORM_LOG_TRACE("Recomputing BDD for edge with id " << edgeId << " and guard " << edge.get().getGuard() << " using the decomposition."); auto start = std::chrono::high_resolution_clock::now(); // compute a decomposition of the command @@ -369,7 +369,7 @@ namespace storm { template void EdgeAbstractor::recomputeCachedBddWithoutDecomposition() { - STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard()); + STORM_LOG_TRACE("Recomputing BDD for edge with id " << edgeId << " and guard " << edge.get().getGuard()); auto start = std::chrono::high_resolution_clock::now(); // Create a mapping from source state DDs to their distributions. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index b35376b6b..04002c400 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -32,7 +32,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) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression({model.getAutomaton(0)})}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { // 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. @@ -125,7 +125,7 @@ namespace storm { template storm::expressions::Expression JaniMenuGameAbstractor::getInitialExpression() const { - return model.get().getInitialStatesExpression(); + return model.get().getInitialStatesExpression({model.get().getAutomaton(0)}); } template @@ -199,139 +199,8 @@ namespace storm { } template - void JaniMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { - std::ofstream out(filename); - - storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); - storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); - storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); - filteredTransitions *= filteredReachableStates.template toAdd(); - - // Determine all initial states so we can color them blue. - std::unordered_set initialStates; - storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); - for (auto stateValue : initialStatesAsAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - initialStates.insert(stateName.str()); - } - - // Determine all highlight states so we can color them red. - std::unordered_set highlightStates; - storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); - for (auto stateValue : highlightStatesAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - highlightStates.insert(stateName.str()); - } - - out << "digraph game {" << std::endl; - - // Create the player 1 nodes. - storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); - for (auto stateValue : statesAsAdd) { - out << "\tpl1_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - std::string stateNameAsString = stateName.str(); - out << stateNameAsString; - out << " [ label=\""; - if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { - out << "*\", margin=0, width=0, height=0, shape=\"none\""; - } else { - out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; - } - bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); - bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); - if (isInitial && isHighlight) { - out << ", style=\"filled\", fillcolor=\"yellow\""; - } else if (isInitial) { - out << ", style=\"filled\", fillcolor=\"blue\""; - } else if (isHighlight) { - out << ", style=\"filled\", fillcolor=\"red\""; - } - out << " ];" << std::endl; - } - - // Create the nodes of the second player. - storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); - for (auto stateValue : player2States) { - out << "\tpl2_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - out << stateName.str() << "_" << index; - out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; - out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - // Create the nodes of the probabilistic player. - storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); - for (auto stateValue : playerPStates) { - out << "\tplp_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - stateName << "_" << index; - index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << stateName.str() << "_" << index; - out << " [ shape=\"point\", label=\"\" ];" << std::endl; - out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - for (auto stateValue : filteredTransitions) { - std::stringstream sourceStateName; - std::stringstream successorStateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - sourceStateName << "1"; - } else { - sourceStateName << "0"; - } - } - for (auto const& var : currentGame->getColumnVariables()) { - if (stateValue.first.getBooleanValue(var)) { - successorStateName << "1"; - } else { - successorStateName << "0"; - } - } - uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; - } - - out << "}" << std::endl; + void JaniMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const { + this->exportToDot(*currentGame, filename, highlightStates, filter); } // Explicitly instantiate the class. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 445616c4a..3a478fcb0 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -109,6 +109,9 @@ namespace storm { */ void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + protected: + using MenuGameAbstractor::exportToDot; + private: /*! * Builds the stochastic game representing the abstraction of the program. diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index 27b23c7a1..5670499ea 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -64,7 +64,7 @@ namespace storm { // DDs use the same amount DD variable encoding the choices of player 2. storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { - result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); + result |= commandDd.bdd && this->getAbstractionInformation().encodePlayer2Choice(1, commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } return GameBddResult(result, maximalNumberOfUsedOptionVariables); } diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 49fb8c2bd..e196c1510 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -199,139 +199,8 @@ namespace storm { } template - void PrismMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { - std::ofstream out(filename); - - storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); - storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); - storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); - filteredTransitions *= filteredReachableStates.template toAdd(); - - // Determine all initial states so we can color them blue. - std::unordered_set initialStates; - storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); - for (auto stateValue : initialStatesAsAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - initialStates.insert(stateName.str()); - } - - // Determine all highlight states so we can color them red. - std::unordered_set highlightStates; - storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); - for (auto stateValue : highlightStatesAdd) { - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - highlightStates.insert(stateName.str()); - } - - out << "digraph game {" << std::endl; - - // Create the player 1 nodes. - storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); - for (auto stateValue : statesAsAdd) { - out << "\tpl1_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - std::string stateNameAsString = stateName.str(); - out << stateNameAsString; - out << " [ label=\""; - if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { - out << "*\", margin=0, width=0, height=0, shape=\"none\""; - } else { - out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; - } - bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); - bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); - if (isInitial && isHighlight) { - out << ", style=\"filled\", fillcolor=\"yellow\""; - } else if (isInitial) { - out << ", style=\"filled\", fillcolor=\"blue\""; - } else if (isHighlight) { - out << ", style=\"filled\", fillcolor=\"red\""; - } - out << " ];" << std::endl; - } - - // Create the nodes of the second player. - storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); - for (auto stateValue : player2States) { - out << "\tpl2_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - out << stateName.str() << "_" << index; - out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; - out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - // Create the nodes of the probabilistic player. - storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); - for (auto stateValue : playerPStates) { - out << "\tplp_"; - std::stringstream stateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - stateName << "_" << index; - index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << stateName.str() << "_" << index; - out << " [ shape=\"point\", label=\"\" ];" << std::endl; - out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; - } - - for (auto stateValue : filteredTransitions) { - std::stringstream sourceStateName; - std::stringstream successorStateName; - for (auto const& var : currentGame->getRowVariables()) { - if (stateValue.first.getBooleanValue(var)) { - sourceStateName << "1"; - } else { - sourceStateName << "0"; - } - } - for (auto const& var : currentGame->getColumnVariables()) { - if (stateValue.first.getBooleanValue(var)) { - successorStateName << "1"; - } else { - successorStateName << "0"; - } - } - uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); - uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); - out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; - } - - out << "}" << std::endl; + void PrismMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const { + this->exportToDot(*currentGame, filename, highlightStates, filter); } // Explicitly instantiate the class. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index df5e740ca..49dc8e9dc 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -107,9 +107,12 @@ namespace storm { * @param highlightStates A BDD characterizing states that will be highlighted. * @param filter A filter that is applied to select which part of the game to export. */ - void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + + protected: + using MenuGameAbstractor::exportToDot; - private: + private: /*! * Builds the stochastic game representing the abstraction of the program. * diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ae6a17ab4..4609c5853 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -368,7 +368,7 @@ namespace storm { } // #ifdef LOCAL_DEBUG - // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); // #endif // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index e2354da57..df59052c6 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1008,7 +1008,7 @@ namespace storm { boost::optional> consideredPlayer1States; boost::optional> player2StrategyBdd; boost::optional> consideredPlayer2States; - + bool maybeStatesDone = false; uint_fast64_t maybeStateIterations = 0; while (!maybeStatesDone || produceStrategiesInIteration) { @@ -1032,7 +1032,6 @@ namespace storm { while (!solutionStatesDone) { // Start by computing the transitions that have only maybe states as successors. Note that at // this point, there may be illegal transitions. - // FIXME: use getIllegalSuccessorMask instead of !transitionMatrix? storm::dd::Bdd distributionsStayingInMaybe = (!transitionMatrix || maybePlayer1States.swapVariables(model.getRowColumnMetaVariablePairs())).universalAbstract(model.getColumnVariables()); // Then, determine all distributions that have at least one successor in the states that have