From d492d5c62fb7309203360c7ea3fa02af5f1d3484 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Aug 2016 22:44:27 +0200 Subject: [PATCH] fixed bug in ADD iterator and started on exporting menu games to dot file Former-commit-id: 9467aa70947298188e7156fc7679b72623080f7f --- src/abstraction/prism/AbstractProgram.cpp | 90 +++++++++++++++++++ src/abstraction/prism/AbstractProgram.h | 7 ++ .../prism/PrismMenuGameAbstractor.cpp | 5 ++ .../prism/PrismMenuGameAbstractor.h | 2 + .../abstraction/GameBasedMdpModelChecker.cpp | 2 +- src/storage/dd/cudd/CuddAddIterator.cpp | 9 +- 6 files changed, 110 insertions(+), 5 deletions(-) diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 07b3078c8..a0854e54a 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -202,6 +202,96 @@ namespace storm { return reachableStates; } + template + void AbstractProgram::exportToDot(std::string const& filename) const { + std::ofstream out(filename); + out << "digraph game {" << std::endl; + + // Create the player 1 nodes. + storm::dd::Add statesAsAdd = currentGame->getReachableStates().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"; + } + } + out << stateName.str(); + out << " [ label=\""; + if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { + out << "*"; + } else { + out << stateName.str(); + } + out << "\" ];" << std::endl; + } + + // Create the nodes of the second player. + storm::dd::Add player2States = currentGame->getTransitionMatrix().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 = 0; + for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { + index |= 1; + } + } + out << stateName.str() << "_" << index; + out << " [ shape=\"square\", label=\"\" ];" << 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 = currentGame->getTransitionMatrix().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 = 0; + for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { + index |= 1; + } + } + stateName << "_" << index; + index = 0; + for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) { + index |= 1; + } } + out << stateName.str() << "_" << index; + out << " [ shape=\"diamond\", label=\"\" ];" << std::endl; + out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + +// for (auto stateValue : currentGame->getTransitionMatrix()) { +// std::stringstream stateName; +// +// } + + out << "}" << std::endl; + } + // Explicitly instantiate the class. template class AbstractProgram; template class AbstractProgram; diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 77eb91c07..ec33b3135 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -74,6 +74,13 @@ namespace storm { */ void refine(std::vector const& predicates); + /*! + * Exports the current state of the abstraction in the dot format to the given file. + * + * @param filename The name of the file to which to write the dot output. + */ + void exportToDot(std::string const& filename) const; + private: /*! * Computes the reachable states of the transition relation. diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp index 535357f25..16421829a 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -23,6 +23,11 @@ namespace storm { void PrismMenuGameAbstractor::refine(std::vector const& predicates) { abstractProgram.refine(predicates); } + + template + void PrismMenuGameAbstractor::exportToDot(std::string const& filename) const { + abstractProgram.exportToDot(filename); + } template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h index 655e1a422..b46a4f497 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/abstraction/prism/PrismMenuGameAbstractor.h @@ -16,6 +16,8 @@ namespace storm { virtual storm::abstraction::MenuGame abstract() override; virtual void refine(std::vector const& predicates) override; + void exportToDot(std::string const& filename) const; + private: /// The abstract program that performs the actual abstraction. AbstractProgram abstractProgram; diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index d8da42d0a..f48c6fe9e 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -70,9 +70,9 @@ namespace storm { storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); - // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. storm::abstraction::MenuGame game = abstractor.abstract(); + abstractor.exportToDot("game.dot"); STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds. diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index 379a0ff22..a1432f901 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -117,7 +117,7 @@ namespace storm { // valuations later. for (auto const& metaVariable : *this->metaVariables) { bool metaVariableAppearsInCube = false; - std::vector> localRelenvantDontCareDdVariables; + std::vector> localRelevantDontCareDdVariables; auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); if (ddMetaVariable.getType() == MetaVariableType::Bool) { if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) { @@ -127,7 +127,8 @@ namespace storm { metaVariableAppearsInCube = true; currentValuation.setBooleanValue(metaVariable, true); } else { - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); + currentValuation.setBooleanValue(metaVariable, false); + localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); } } else { int_fast64_t intValue = 0; @@ -141,7 +142,7 @@ namespace storm { } else { // Temporarily leave bit unset so we can iterate trough the other option later. // Add the bit to the relevant don't care bits. - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); + localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); } } if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { @@ -152,7 +153,7 @@ namespace storm { // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the // missing bits to later enumerate all possible valuations. if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { - relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end()); + relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelevantDontCareDdVariables.begin(), localRelevantDontCareDdVariables.end()); } }