diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 6c9ff1bce..e9a682c32 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -22,33 +22,49 @@ namespace storm { } template - storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { + storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionsMin, storm::dd::Bdd const& transitionsMax, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { // Perform a BFS and pick the first pivot state we encounter. storm::dd::Bdd pivotState; - storm::dd::Bdd frontier = initialStates; - storm::dd::Bdd frontierPivotStates = frontier && pivotStates; + storm::dd::Bdd frontierMin = initialStates; + storm::dd::Bdd frontierMax = initialStates; + storm::dd::Bdd frontierMinPivotStates = frontierMin && pivotStates; + storm::dd::Bdd frontierMaxPivotStates = frontierMinPivotStates; uint64_t level = 0; - bool foundPivotState = !frontierPivotStates.isZero(); + bool foundPivotState = !frontierMinPivotStates.isZero(); if (foundPivotState) { - pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << frontierMinPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); } else { while (!foundPivotState) { - frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables); - frontierPivotStates = frontier && pivotStates; + frontierMin = frontierMin.relationalProduct(transitionsMin, rowVariables, columnVariables); + frontierMax = frontierMax.relationalProduct(transitionsMax, rowVariables, columnVariables); + frontierMinPivotStates = frontierMin && pivotStates; + frontierMaxPivotStates = frontierMax && pivotStates; - if (!frontierPivotStates.isZero()) { + if (!frontierMinPivotStates.isZero()) { if (quantitativeResult) { - storm::dd::Add frontierPivotStatesAdd = frontierPivotStates.template toAdd(); + storm::dd::Add frontierPivotStatesAdd = frontierMinPivotStates.template toAdd(); storm::dd::Add diff = frontierPivotStatesAdd * quantitativeResult.get().max.values - frontierPivotStatesAdd * quantitativeResult.get().min.values; pivotState = diff.maxAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); foundPivotState = true; } else { - pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + foundPivotState = true; + } + } else if (!frontierMaxPivotStates.isZero()) { + if (quantitativeResult) { + storm::dd::Add frontierPivotStatesAdd = frontierMaxPivotStates.template toAdd(); + storm::dd::Add diff = frontierPivotStatesAdd * quantitativeResult.get().max.values - frontierPivotStatesAdd * quantitativeResult.get().min.values; + pivotState = diff.maxAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + foundPivotState = true; + } else { + pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); foundPivotState = true; } } @@ -58,7 +74,7 @@ namespace storm { return pivotState; } - + template void MenuGameRefiner::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); @@ -131,15 +147,19 @@ namespace storm { // state that is also a prob 0 state. minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); - // Build the fragment of transitions that is reachable by both the min and the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy; + // Build the fragment of transitions that is reachable by either the min or the max strategies. + storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - - // Require the pivot state to be a [0, 1] state. - // TODO: is this restriction necessary or is it already implied? - // pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States(); + + storm::dd::Bdd reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + storm::dd::Bdd reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + // Start with all reachable states as potential pivot states. + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || + storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()); + + //storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + // 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. @@ -150,10 +170,11 @@ namespace storm { constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + // pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either - // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob0 max define + // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob1 max define // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state // is found. In this case, we abort the qualitative refinement here. if (pivotStates.isZero()) { @@ -163,7 +184,7 @@ namespace storm { STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitionsMin, reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStates); // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); @@ -215,7 +236,15 @@ namespace storm { // Build the fragment of transitions that is reachable by both the min and the max strategies. storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + + storm::dd::Bdd reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + storm::dd::Bdd reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + + // Start with all reachable states as potential pivot states. + // storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || + storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()); + // Require the pivot state to be a state with a lower bound strictly smaller than the upper bound. pivotStates &= quantitativeResult.min.values.less(quantitativeResult.max.values); @@ -233,12 +262,13 @@ namespace storm { constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + // pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates, quantitativeResult); + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitionsMin, reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStates, quantitativeResult); // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/AbstractCommand.cpp index f41eb3e0f..4430dccc3 100644 --- a/src/storm/abstraction/prism/AbstractCommand.cpp +++ b/src/storm/abstraction/prism/AbstractCommand.cpp @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -108,12 +108,12 @@ namespace storm { // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); - if (!guardIsPredicate) { + if (!skipBottomStates) { abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); } uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { - if (!guardIsPredicate) { + if (!skipBottomStates) { abstractGuard |= sourceDistributionsPair.first; } @@ -327,8 +327,8 @@ namespace storm { BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); // If the guard of this command is a predicate, there are not bottom states/transitions. - if (guardIsPredicate) { - STORM_LOG_TRACE("Guard is predicate, no bottom state transitions for this command."); + if (skipBottomStates) { + STORM_LOG_TRACE("Skipping bottom state computation for this command."); return result; } @@ -336,6 +336,11 @@ namespace storm { // still has a transition to a bottom state. bottomStateAbstractor.constrain(reachableStates && abstractGuard); result.states = bottomStateAbstractor.getAbstractStates(); + + // If the result is empty one time, we can skip the bottom state computation from now on. + if (result.states.isZero()) { + skipBottomStates = true; + } // Now equip all these states with an actual transition to a bottom state. result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); @@ -364,11 +369,6 @@ namespace storm { return command.get(); } - template - void AbstractCommand::notifyGuardIsPredicate() { - guardIsPredicate = true; - } - template AbstractionInformation const& AbstractCommand::getAbstractionInformation() const { return abstractionInformation.get(); diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h index 7cf45bee0..f62ae3838 100644 --- a/src/storm/abstraction/prism/AbstractCommand.h +++ b/src/storm/abstraction/prism/AbstractCommand.h @@ -110,12 +110,6 @@ namespace storm { */ storm::prism::Command const& getConcreteCommand() const; - /*! - * Notifies this abstract command that its guard is now a predicate. This affects the computation of the - * bottom states. - */ - void notifyGuardIsPredicate(); - private: /*! * Determines the relevant predicates for source as well as successor states wrt. to the given assignments @@ -235,7 +229,7 @@ namespace storm { // A flag indicating whether the guard of the command was added as a predicate. If this is true, there // is no need to compute bottom states. - bool guardIsPredicate; + bool skipBottomStates; // A flag remembering whether we need to force recomputation of the BDD. bool forceRecomputation;