From 241f23f7304c7fbe09f40a5b0048d7d543695c69 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Aug 2016 11:02:58 +0200 Subject: [PATCH 1/5] fixed bug in abstraction information object Former-commit-id: 1338ecfa4736c1f1a8c59f60f2adb172393fce59 --- src/abstraction/AbstractionInformation.cpp | 1 + src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 2 -- src/utility/graph.cpp | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index d033be86b..0ce9201ef 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -48,6 +48,7 @@ namespace storm { std::pair newMetaVariable = ddManager->addMetaVariable(stream.str()); predicateDdVariables.push_back(newMetaVariable); + extendedPredicateDdVariables.push_back(newMetaVariable); predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1)); predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1))); allPredicateIdentities &= predicateIdentities.back(); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9b079d111..6c408f386 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -95,8 +95,6 @@ namespace storm { void GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); - game.getTransitionMatrix().exportToDot("trans.dot"); - bottomStatesBdd.template toAdd().exportToDot("bottom.dot"); storm::dd::Bdd targetStates = game.getStates(targetStateExpression); if (player1Direction == storm::OptimizationDirection::Minimize) { diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 04139d129..55cb72cda 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -955,7 +955,7 @@ namespace storm { solution = tmp; ++iterations; } - + // Since we have determined the inverse of the desired set, we need to complement it now. solution = !solution && model.getReachableStates(); From 9878c1bdc399f0a29cda3fe320d271d9dbf3f7dc Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Aug 2016 17:00:49 +0200 Subject: [PATCH 2/5] fixed some tests that were failing because of (now) proper bottom state computation Former-commit-id: ecc8dfb06546df84614c95071114999c3edbe1c0 --- .../abstraction/GameBasedMdpModelChecker.cpp | 18 +++++++++-- src/utility/graph.h | 20 ++++++++++++ test/functional/utility/GraphTest.cpp | 32 +++++++++---------- 3 files changed, 52 insertions(+), 18 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 6c408f386..16d63f245 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -101,14 +101,28 @@ namespace storm { targetStates |= game.getBottomStates(); } + transitionMatrixBdd.template toAdd().exportToDot("transbdd.dot"); + // Start by computing the states with probability 0/1 when player 2 minimizes. storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); - storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false); // Now compute the states with probability 0/1 when player 2 maximizes. - storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false); storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); +// STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy."); + + STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy."); + +// prob0Min.getPlayer1Strategy().template toAdd().exportToDot("prob0_min_pl1_strat.dot"); + prob0Min.getPlayer2Strategy().template toAdd().exportToDot("prob0_min_pl2_strat.dot"); + + prob1Max.getPlayer1Strategy().template toAdd().exportToDot("prob1_max_pl1_strat.dot"); + prob1Max.getPlayer2Strategy().template toAdd().exportToDot("prob1_max_pl2_strat.dot"); + STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); diff --git a/src/utility/graph.h b/src/utility/graph.h index ce5f1cd2f..d57c8a731 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -528,6 +528,26 @@ namespace storm { // Intentionally left empty. } + bool hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + storm::dd::Bdd const& getPlayer1Strategy() { + return player1Strategy.get(); + } + + bool hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + storm::dd::Bdd const& getPlayer2Strategy() { + return player2Strategy.get(); + } + + storm::dd::Bdd const& getStates() const { + return states; + } + storm::dd::Bdd states; boost::optional> player1Strategy; boost::optional> player2Strategy; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 33c31ac5b..79e52c8d8 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -215,30 +215,30 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(2, result.states.getNonZeroCount()); + EXPECT_EQ(3, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -249,7 +249,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { targetStates = game.getStates(initialPredicates[0], true); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -259,32 +259,32 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables());; - EXPECT_EQ(0, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(0, stateDistributionCount.getMax()); + EXPECT_EQ(1, stateDistributionCount.getMax()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(3, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(3, result.states.getNonZeroCount()); + EXPECT_EQ(4, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(3, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(3, result.states.getNonZeroCount()); + EXPECT_EQ(4, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -294,7 +294,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(3, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(4, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); From 5bf666be4c08540a1ad01f1c9eed5807401d8466 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Aug 2016 18:00:38 +0200 Subject: [PATCH 3/5] fix in existsAbstractRepresentative Former-commit-id: c884deaf11dfef4509fc48ab9ccf712d6e14ff83 --- resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c | 3 ++- src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 2 +- test/functional/utility/GraphTest.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index a908ca8ad..d7aa33cb3 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -611,11 +611,12 @@ cuddBddExistAbstractRepresentativeRecur( if (res1 == NULL) { return(NULL); } + // FIXME if (res1 == one) { if (F->ref != 1) { cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); } - return(one); + return(cube); } cuddRef(res1); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 16d63f245..d8da42d0a 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -100,7 +100,7 @@ namespace storm { if (player1Direction == storm::OptimizationDirection::Minimize) { targetStates |= game.getBottomStates(); } - + transitionMatrixBdd.template toAdd().exportToDot("transbdd.dot"); // Start by computing the states with probability 0/1 when player 2 minimizes. diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 79e52c8d8..176129ed6 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -258,7 +258,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); // Proceed by checking whether they select exactly one action in each state. - storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables());; + storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). From d492d5c62fb7309203360c7ea3fa02af5f1d3484 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Aug 2016 22:44:27 +0200 Subject: [PATCH 4/5] 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()); } } From 033faa62f028e25b3dfee14b6fcb00ebd6b5624c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Aug 2016 23:15:21 +0200 Subject: [PATCH 5/5] changed node shapes a little Former-commit-id: 8c7fffaf65bd64b7598d2dfc6d10ce7c992dc066 --- src/abstraction/prism/AbstractProgram.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index a0854e54a..7a1b2255f 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -222,9 +222,9 @@ namespace storm { out << stateName.str(); out << " [ label=\""; if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { - out << "*"; + out << "*\", margin=0, width=0, height=0, shape=\"none"; } else { - out << stateName.str(); + out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval"; } out << "\" ];" << std::endl; } @@ -249,7 +249,7 @@ namespace storm { } } out << stateName.str() << "_" << index; - out << " [ shape=\"square\", label=\"\" ];" << std::endl; + 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; } @@ -280,7 +280,7 @@ namespace storm { index |= 1; } } out << stateName.str() << "_" << index; - out << " [ shape=\"diamond\", label=\"\" ];" << std::endl; + out << " [ shape=\"point\", label=\"\" ];" << std::endl; out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; }