diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index e115aa28d..4e4a88ee1 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -52,6 +52,7 @@ namespace storm { } std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); + // Since the number of relevant predicates is monotonic, we can simply check for the size here. STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); if (newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size()) { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a5f4be44a..0ebb77f7d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -564,7 +564,7 @@ namespace storm { auto abstractionStart = std::chrono::high_resolution_clock::now(); storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states, " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); + STORM_LOG_INFO("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); @@ -576,10 +576,10 @@ namespace storm { } // #ifdef LOCAL_DEBUG -// initialStates.template toAdd().exportToDot("init.dot"); -// targetStates.template toAdd().exportToDot("target.dot"); +// initialStates.template toAdd().exportToDot("init" + std::to_string(iterations) + ".dot"); +// targetStates.template toAdd().exportToDot("target" + std::to_string(iterations) + ".dot"); // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); -// game.getReachableStates().template toAdd().exportToDot("reach.dot"); +// game.getReachableStates().template toAdd().exportToDot("reach" + std::to_string(iterations) + ".dot"); // #endif std::unique_ptr result;