From 3a70c68d45edaffb8bc11fc40f40a2ddde208c70 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 13 Jun 2020 18:10:44 -0700 Subject: [PATCH] dd-based reachability exploration reports number of iterations in return value --- src/storm/abstraction/MenuGameAbstractor.cpp | 2 +- src/storm/abstraction/MenuGameRefiner.cpp | 4 ++-- src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp | 2 +- src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp | 2 +- src/storm/builder/DdJaniModelBuilder.cpp | 2 +- src/storm/builder/DdPrismModelBuilder.cpp | 2 +- src/storm/utility/dd.cpp | 8 ++++---- src/storm/utility/dd.h | 2 +- 8 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index 2094568a2..d75a8ddb4 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -76,7 +76,7 @@ namespace storm { 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()); + storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame.getInitialStates(), filteredTransitionsBdd, currentGame.getRowVariables(), currentGame.getColumnVariables()).first; filteredTransitions *= filteredReachableStates.template toAdd(); // Determine all initial states so we can color them blue. diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 23f2f4f34..f5dbd141d 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -471,8 +471,8 @@ namespace storm { result.reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); // Start with all reachable states as potential pivot states. - result.pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || - storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()); + result.pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()).first || + storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()).first; // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and // that the difference is not because of a missing strategy in either case. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 991870ede..666a1c200 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -204,7 +204,7 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract); initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); - storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()).first; relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 9e018ce3e..e26ea3c99 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -196,7 +196,7 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract); initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); - storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()).first; relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 259ad60d9..ff5b3609a 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -2201,7 +2201,7 @@ namespace storm { if (preparedModel.getModelType() == storm::jani::ModelType::MDP || preparedModel.getModelType() == storm::jani::ModelType::LTS || preparedModel.getModelType() == storm::jani::ModelType::MA) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables); } - modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); + modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables).first; // Check that the reachable fragment does not overlap with the illegal fragment. storm::dd::Bdd reachableIllegalFragment = modelComponents.reachableStates && system.illegalFragment; diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 32de16b91..9e907a857 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1349,7 +1349,7 @@ namespace storm { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); } - storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables).first; storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); transitionMatrix *= reachableStatesAdd; if (system.stateActionDd) { diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 3ecbef7d6..0bb898927 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -13,7 +13,7 @@ namespace storm { namespace dd { template - storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + std::pair,uint64_t> computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { STORM_LOG_TRACE("Computing reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states)."); @@ -42,7 +42,7 @@ namespace storm { auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast(end - start).count() << "ms)."); - return reachableStates; + return {reachableStates, iteration}; } template @@ -82,8 +82,8 @@ namespace storm { return ddManager.getIdentity(rowColumnMetaVariablePairs, false); } - template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); - template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template std::pair,uint64_t> computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template std::pair, uint64_t> computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); template storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); template storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); diff --git a/src/storm/utility/dd.h b/src/storm/utility/dd.h index 679e1bd50..26e014aca 100644 --- a/src/storm/utility/dd.h +++ b/src/storm/utility/dd.h @@ -24,7 +24,7 @@ namespace storm { namespace dd { template - storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + std::pair, uint64_t> computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); template storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables);