diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index a262d2ffe..25c4242ba 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -870,14 +870,11 @@ namespace storm { auto assertionStart = std::chrono::high_resolution_clock::now(); storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true)); uint64_t stepCounter = 0; - auto traceIt = trace.rbegin(); - auto traceIte = trace.rend(); - for (; traceIt != traceIte; ++traceIt) { - auto const& step = *traceIt; - interpolatingSolver.push(); + for (auto const& traceElement : trace) { + // interpolatingSolver.push(); interpolatingSolver.setInterpolationGroup(stepCounter); - for (auto const& predicate : step) { + for (auto const& predicate : traceElement) { interpolatingSolver.add(predicate); } @@ -898,6 +895,7 @@ namespace storm { storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager()); if (interpolant.isFalse()) { // If the interpolant is false, it means that the prefix has become unsatisfiable. + STORM_LOG_TRACE("Trace formula became unsatisfiable at position " << step << " of " << stepCounter << "."); break; } if (!interpolant.isTrue()) { @@ -1231,16 +1229,18 @@ namespace storm { } } - if (currentLower) { - performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); - } else { - performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); + // We only need to search further if the state has some value deviation. + if (!lowerValues || !upperValues || (*lowerValues)[currentState] < (*upperValues)[currentState]) { + if (currentLower) { + performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); + } else { + performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, false, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); + } } } if (foundPivotState) { - ExplicitPivotStateResult result; - return result; + return ExplicitPivotStateResult(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors)); } // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state, diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index ff9884720..4a22b976f 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -565,7 +565,8 @@ namespace storm { template storm::dd::Bdd CommandAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector> const& variablePredicates) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); - for (auto const& variableIndexPair : variablePredicates) { + for (auto variableIndexPairIt = variablePredicates.rbegin(), variableIndexPairIte = variablePredicates.rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) { + auto const& variableIndexPair = *variableIndexPairIt; if (model.getBooleanValue(variableIndexPair.first)) { result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { @@ -585,7 +586,8 @@ namespace storm { storm::dd::Bdd updateBdd = this->getAbstractionInformation().getDdManager().getBddOne(); // Translate block variables for this update into a successor block. - for (auto const& variableIndexPair : variablePredicates[updateIndex]) { + for (auto variableIndexPairIt = variablePredicates[updateIndex].rbegin(), variableIndexPairIte = variablePredicates[updateIndex].rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) { + auto const& variableIndexPair = *variableIndexPairIt; if (model.getBooleanValue(variableIndexPair.first)) { updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } else { @@ -613,17 +615,21 @@ namespace storm { for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { // Compute the identities that are missing for this update. - auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin(); - auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end(); + auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].rbegin(); + auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].rend(); storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); - for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { + for (uint_fast64_t predicateIndex = this->getAbstractionInformation().getNumberOfPredicates() - 1;; --predicateIndex) { if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) { updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); } else { ++updateRelevantIt; } + + if (predicateIndex == 0) { + break; + } } result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); @@ -631,25 +637,6 @@ namespace storm { return result; } -// template -// storm::dd::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { -// storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); -// -// auto relevantIt = relevantPredicatesAndVariables.first.begin(); -// auto relevantIte = relevantPredicatesAndVariables.first.end(); -// -// for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { -// if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { -// std::cout << "adding global identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(predicateIndex) << std::endl; -// result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); -// } else { -// ++relevantIt; -// } -// } -// -// return result; -// } - template GameBddResult CommandAbstractor::abstract() { if (forceRecomputation) { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ca01fca3b..f08785a6d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -91,6 +91,8 @@ namespace storm { reuseQualitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Qualitative; reuseQuantitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Quantitative; maximalNumberOfAbstractions = abstractionSettings.getMaximalAbstractionCount(); + fixPlayer1Strategy = abstractionSettings.isFixPlayer1StrategySet(); + fixPlayer2Strategy = abstractionSettings.isFixPlayer2StrategySet(); } template @@ -560,6 +562,8 @@ namespace storm { boost::optional> previousSymbolicQualitativeResult = boost::none; boost::optional> previousSymbolicMinQuantitativeResult = boost::none; boost::optional> previousExplicitResult = boost::none; + uint64_t peakPlayer1States = 0; + uint64_t peakTransitions = 0; for (iteration = 0; iteration < maximalNumberOfAbstractions; ++iteration) { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iteration << "."); @@ -569,7 +573,12 @@ namespace storm { storm::abstraction::MenuGame game = abstractor->abstract(); abstractionWatch.stop(); totalAbstractionWatch.add(abstractionWatch); - STORM_LOG_INFO("Abstraction in iteration " << iteration << " 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 " << abstractionWatch.getTimeInMilliseconds() << "ms)."); + + uint64_t numberOfPlayer1States = game.getNumberOfStates(); + peakPlayer1States = std::max(peakPlayer1States, numberOfPlayer1States); + uint64_t numberOfTransitions = game.getNumberOfTransitions(); + peakTransitions = std::max(peakTransitions, numberOfTransitions); + STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << numberOfPlayer1States << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << numberOfTransitions << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << abstractionWatch.getTimeInMilliseconds() << "ms)."); // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); @@ -596,7 +605,7 @@ namespace storm { if (result) { totalWatch.stop(); - printStatistics(*abstractor, game, iteration); + printStatistics(*abstractor, game, iteration, peakPlayer1States, peakTransitions); return result; } @@ -712,54 +721,169 @@ namespace storm { } template - void postProcessStrategies(abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, bool sanityCheck) { + void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) { + + if (!redirectPlayer1 && !redirectPlayer2) { + return; + } + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + bool isProb0Min = qualitativeResult.getProb0Min().getStates().get(state); + + bool hasMinPlayer1Choice = false; + uint64_t lowerPlayer1Choice = 0; + bool hasMaxPlayer1Choice = false; + uint64_t upperPlayer1Choice = 0; + + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + hasMinPlayer1Choice = true; + lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); + + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + if (lowerPlayer2Choice == upperPlayer2Choice) { + continue; + } + + bool redirect = true; + if (isProb0Min) { + for (auto const& entry : transitionMatrix.getRow(upperPlayer2Choice)) { + if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) { + redirect = false; + break; + } + } + } + + if (redirectPlayer2 && redirect) { + minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + } + } + } + + bool lowerChoiceUnderUpperIsProb0 = false; + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); + + if (lowerPlayer1Choice != upperPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + hasMaxPlayer1Choice = true; + + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + if (lowerPlayer2Choice == upperPlayer2Choice) { + continue; + } + + lowerChoiceUnderUpperIsProb0 = true; + for (auto const& entry : transitionMatrix.getRow(lowerPlayer2Choice)) { + if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) { + lowerChoiceUnderUpperIsProb0 = false; + break; + } + } + + bool redirect = true; + if (lowerChoiceUnderUpperIsProb0) { + for (auto const& entry : transitionMatrix.getRow(upperPlayer2Choice)) { + if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) { + redirect = false; + break; + } + } + } + + if (redirectPlayer2 && redirect) { + minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + } + } + } + + if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) { + if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) { + if (!isProb0Min || lowerChoiceUnderUpperIsProb0) { + minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice); + } + } + } + } + } + + template + void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) { + + if (!redirectPlayer1 && !redirectPlayer2) { + return; + } + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); + bool hasMinPlayer1Choice = false; + uint64_t lowerPlayer1Choice = 0; + ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero(); + bool hasMaxPlayer1Choice = false; + uint64_t upperPlayer1Choice = 0; + ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero(); + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); + hasMinPlayer1Choice = true; + lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); - STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ")."); + STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ")."); uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); - if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { + lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2; minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); - if (sanityCheck) { - STORM_LOG_TRACE("[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice); - } } } } } if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); + upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); - STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); - uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); - - if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + hasMaxPlayer1Choice = true; + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; + + STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); - if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); - STORM_LOG_TRACE("[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice); } } } } + + if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) { + if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) { + if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) { + minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice); + } + } + } } if (sanityCheck) { @@ -894,6 +1018,9 @@ namespace storm { STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + // Post-process strategies for better refinements. + postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, qualitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug); + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. storm::utility::Stopwatch refinementWatch(true); @@ -937,7 +1064,8 @@ namespace storm { return result; } - postProcessStrategies(minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->debug); + // Post-process strategies for better refinements. + postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug); // Make sure that all strategies are still valid strategies. STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << "."); @@ -1128,7 +1256,7 @@ namespace storm { } template - void GameBasedMdpModelChecker::printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements) const { + void GameBasedMdpModelChecker::printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const { if (storm::settings::getModule().isShowStatisticsSet()) { storm::abstraction::AbstractionInformation const& abstractionInformation = abstractor.getAbstractionInformation(); @@ -1137,10 +1265,11 @@ namespace storm { std::cout << std::endl; std::cout << "Statistics:" << std::endl; - std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states" << std::endl; + std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states, " << game.getTransitionMatrix().getNonZeroCount() << " transitions" << std::endl; + std::cout << " * peak size of game: " << peakPlayer1States << " player 1 states, " << peakTransitions << " transitions" << std::endl; std::cout << " * transitions (final game): " << game.getTransitionMatrix().getNonZeroCount() << std::endl; std::cout << " * refinements: " << refinements << std::endl; - std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl; + std::cout << " * predicates: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl; uint64_t totalAbstractionTimeMillis = totalAbstractionWatch.getTimeInMilliseconds(); uint64_t totalTranslationTimeMillis = totalTranslationWatch.getTimeInMilliseconds(); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index cf6d059aa..353be113a 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -115,7 +115,7 @@ namespace storm { ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair); - void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements) const; + void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const; /* * Retrieves the expression characterized by the formula. The formula needs to be propositional. @@ -150,6 +150,12 @@ namespace storm { /// The performed number of refinement iterations. uint64_t iteration; + /// A flag indicating whether to fix player 1 strategies. + bool fixPlayer1Strategy; + + /// A flag indicating whether to fix player 2 strategies. + bool fixPlayer2Strategy; + /// A flag that indicates whether debug mode is enabled. bool debug; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 0f73e2c4f..8153b8e2c 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -29,7 +29,9 @@ namespace storm { const std::string AbstractionSettings::constraintsOptionName = "constraints"; const std::string AbstractionSettings::useEagerRefinementOptionName = "eagerref"; const std::string AbstractionSettings::debugOptionName = "debug"; - const std::string AbstractionSettings::injectRefinementPredicatesOption = "injectref"; + const std::string AbstractionSettings::injectRefinementPredicatesOptionName = "injectref"; + const std::string AbstractionSettings::fixPlayer1StrategyOptionName = "fixpl1strat"; + const std::string AbstractionSettings::fixPlayer2StrategyOptionName = "fixpl2strat"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -106,10 +108,20 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build()) .build()); - this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOption, true, "Specifies predicates used by the refinement instead of the derived predicates.") + this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer2StrategyOptionName, true, "Sets whether to fix player 2 strategies.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, true, "Sets whether to enable debug mode.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("off").build()) @@ -225,11 +237,19 @@ namespace storm { } bool AbstractionSettings::isInjectRefinementPredicatesSet() const { - return this->getOption(injectRefinementPredicatesOption).getHasOptionBeenSet(); + return this->getOption(injectRefinementPredicatesOptionName).getHasOptionBeenSet(); } std::string AbstractionSettings::getInjectedRefinementPredicates() const { - return this->getOption(injectRefinementPredicatesOption).getArgumentByName("predicates").getValueAsString(); + return this->getOption(injectRefinementPredicatesOptionName).getArgumentByName("predicates").getValueAsString(); + } + + bool AbstractionSettings::isFixPlayer1StrategySet() const { + return this->getOption(fixPlayer1StrategyOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + + bool AbstractionSettings::isFixPlayer2StrategySet() const { + return this->getOption(fixPlayer2StrategyOptionName).getArgumentByName("value").getValueAsString() == "on"; } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index f6627129f..95f1e3e36 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -161,7 +161,17 @@ namespace storm { * Retrieves a string containing refinement predicates to inject (if there are any). */ std::string getInjectedRefinementPredicates() const; - + + /*! + * Retrieves whether player 1 strategies are to be fixed. + */ + bool isFixPlayer1StrategySet() const; + + /*! + * Retrieves whether player 2 strategies are to be fixed. + */ + bool isFixPlayer2StrategySet() const; + const static std::string moduleName; private: @@ -181,7 +191,9 @@ namespace storm { const static std::string constraintsOptionName; const static std::string useEagerRefinementOptionName; const static std::string debugOptionName; - const static std::string injectRefinementPredicatesOption; + const static std::string injectRefinementPredicatesOptionName; + const static std::string fixPlayer1StrategyOptionName; + const static std::string fixPlayer2StrategyOptionName; }; }