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();