diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/AbstractCommand.cpp index 40c910cd0..63a889472 100644 --- a/src/storm/abstraction/prism/AbstractCommand.cpp +++ b/src/storm/abstraction/prism/AbstractCommand.cpp @@ -1,5 +1,7 @@ #include "storm/abstraction/prism/AbstractCommand.h" +#include + #include #include "storm/abstraction/AbstractionInformation.h" @@ -40,11 +42,11 @@ namespace storm { for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) { allPredicateIndices[index] = index; } - this->refine(allPredicateIndices); + this->refine(allPredicateIndices, true); } template - void AbstractCommand::refine(std::vector const& predicates) { + void AbstractCommand::refine(std::vector const& predicates, bool forceRecomputation) { // Add all predicates to the variable partition. for (auto predicateIndex : predicates) { localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex); @@ -57,7 +59,7 @@ namespace storm { std::pair, std::vector>> newRelevantPredicates = this->computeRelevantPredicates(); // If the DD does not need recomputation, we can return the cached result. - bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates); + bool recomputeDd = forceRecomputation || this->relevantPredicatesChanged(newRelevantPredicates); if (!recomputeDd) { // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities. cachedDd.bdd &= computeMissingGlobalIdentities(); @@ -76,11 +78,14 @@ namespace storm { template void AbstractCommand::recomputeCachedBdd() { STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); + auto start = std::chrono::high_resolution_clock::now(); // Create a mapping from source state DDs to their distributions. std::unordered_map, std::vector>> sourceToDistributionsMap; - smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { + uint64_t numberOfSolutions = 0; + smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); + ++numberOfSolutions; return true; }); @@ -127,6 +132,9 @@ namespace storm { // Cache the result. cachedDd = GameBddResult(resultBdd, numberOfVariablesNeeded); + auto end = std::chrono::high_resolution_clock::now(); + + STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); } template @@ -309,6 +317,7 @@ namespace storm { template BottomStateResult AbstractCommand::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get()); 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. diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h index 7446333e9..2e7b65689 100644 --- a/src/storm/abstraction/prism/AbstractCommand.h +++ b/src/storm/abstraction/prism/AbstractCommand.h @@ -65,8 +65,9 @@ namespace storm { * Refines the abstract command with the given predicates. * * @param predicates The new predicates. + * @param forceRecomputation If set, the BDD is recomputed even if the relevant predicates have not changed. */ - void refine(std::vector const& predicates); + void refine(std::vector const& predicates, bool forceRecomputation = false); /*! * Computes the abstraction of the command wrt. to the current set of predicates. diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp index 849285757..1088a703f 100644 --- a/src/storm/abstraction/prism/AbstractProgram.cpp +++ b/src/storm/abstraction/prism/AbstractProgram.cpp @@ -20,8 +20,6 @@ #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" -//#define LOCAL_DEBUG - namespace storm { namespace abstraction { namespace prism { @@ -30,8 +28,8 @@ namespace storm { AbstractProgram::AbstractProgram(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory, - bool addAllGuards) - : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr) { + bool addAllGuards, bool splitPredicates) + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. @@ -66,42 +64,62 @@ namespace storm { // odds are that it's impossible to treat such models in any event. abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); - // Now that we have created all other DD variables, we create the DD variables for the predicates. - std::vector allPredicateIndices; - if (addAllGuards) { - for (auto const& guard : allGuards) { - allPredicateIndices.push_back(abstractionInformation.addPredicate(guard)); - } - } - for (auto const& predicate : initialPredicates) { - allPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); - } - // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, addAllGuards); } - // Refine the initial state abstractors using the initial predicates. - initialStateAbstractor.refine(allPredicateIndices); - // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); - // Finally, we build the game the first time. - currentGame = buildGame(); + // Now that we have created all other DD variables, we create the DD variables for the predicates. + std::vector> allPredicates; + for (auto const& predicate : initialPredicates) { + allPredicates.push_back(std::make_pair(predicate, false)); + } + if (addAllGuards) { + for (auto const& guard : allGuards) { + allPredicates.push_back(std::make_pair(guard, true)); + } + } + // Finally, refine using the all predicates and build game as a by-product. + this->refine(allPredicates); } template - void AbstractProgram::refine(std::vector const& predicates) { + void AbstractProgram::refine(std::vector> const& predicates) { STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); // Add the predicates to the global list of predicates. std::vector newPredicateIndices; - for (auto const& predicate : predicates) { + for (auto const& predicateAllowSplitPair : predicates) { + storm::expressions::Expression const& predicate = predicateAllowSplitPair.first; + bool allowSplit = predicateAllowSplitPair.second; STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); - uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); - newPredicateIndices.push_back(newPredicateIndex); + + if (allowSplit && splitPredicates) { + // Split the predicates. + std::vector atoms = splitter.split(predicate); + + // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have. + for (auto const& atom : atoms) { + bool addAtom = true; + for (auto const& oldPredicate : abstractionInformation.getPredicates()) { + if (equivalenceChecker.areEquivalent(atom, oldPredicate)) { + addAtom = false; + break; + } + } + + if (addAtom) { + uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom); + newPredicateIndices.push_back(newPredicateIndex); + } + } + } else { + uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); + newPredicateIndices.push_back(newPredicateIndex); + } } // Refine all abstract modules. @@ -183,8 +201,8 @@ namespace storm { STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); abstractCommand.notifyGuardIsPredicate(); storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); - STORM_LOG_TRACE("Derived new predicate: " << newPredicate); - this->refine({newPredicate}); + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + this->refine({std::make_pair(newPredicate, true)}); } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); @@ -231,6 +249,7 @@ namespace storm { for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) { // Now we know the point of the deviation (command, update, predicate). + std::cout << "pred: " << abstractionInformation.getPredicateByIndex(predicateIndex) << " and update " << concreteCommand.getUpdate(updateIndex) << std::endl; newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify(); break; } @@ -239,9 +258,9 @@ namespace storm { } STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); - STORM_LOG_TRACE("Derived new predicate: " << newPredicate); + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - this->refine({newPredicate}); + this->refine({std::make_pair(newPredicate, true)}); } STORM_LOG_TRACE("Current set of predicates:"); @@ -299,7 +318,9 @@ namespace storm { } // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); + transitionMatrix *= commandUpdateProbabilitiesAdd; + transitionMatrix += deadlockTransitions; // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h index f37c28327..5cfca0f41 100644 --- a/src/storm/abstraction/prism/AbstractProgram.h +++ b/src/storm/abstraction/prism/AbstractProgram.h @@ -9,6 +9,8 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/PredicateSplitter.h" +#include "storm/storage/expressions/EquivalenceChecker.h" namespace storm { namespace utility { @@ -43,8 +45,9 @@ namespace storm { * @param initialPredicates The initial set of predicates. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates. + * @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added. */ - AbstractProgram(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false); + AbstractProgram(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false, bool splitPredicates = false); AbstractProgram(AbstractProgram const&) = default; AbstractProgram& operator=(AbstractProgram const&) = default; @@ -72,7 +75,7 @@ namespace storm { * * @param predicates The new predicates. */ - void refine(std::vector const& predicates); + void refine(std::vector> const& predicates); /*! * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that @@ -125,6 +128,15 @@ namespace storm { // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; + // A flag indicating whether predicates are to be split into atoms or not. + bool splitPredicates; + + // An object that can be used for splitting predicates. + storm::expressions::PredicateSplitter splitter; + + // An object that can be used to determine whether predicates are equivalent. + storm::expressions::EquivalenceChecker equivalenceChecker; + // A flag that stores whether all guards were added (which is relevant for determining the bottom states). bool addedAllGuards; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index b1c5eee1e..e6ce56eca 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -10,7 +10,7 @@ namespace storm { namespace prism { template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet()) { + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet(), storm::settings::getModule().isSplitPredicatesSet()) { // Intentionally left empty. } @@ -21,7 +21,11 @@ namespace storm { template void PrismMenuGameAbstractor::refine(std::vector const& predicates) { - abstractProgram.refine(predicates); + std::vector> predicatesWithFlags; + for (auto const& predicate : predicates) { + predicatesWithFlags.emplace_back(predicate, true); + } + abstractProgram.refine(predicatesWithFlags); } template diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 05a24ebe9..789a1c07c 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -263,7 +263,10 @@ namespace storm { bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Refining based on lower choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return true; } else { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; @@ -273,7 +276,10 @@ namespace storm { bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return true; } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); @@ -309,11 +315,6 @@ namespace storm { // Start with constructing the player 2 states that have a (min) and a (max) strategy. // TODO: necessary? storm::dd::Bdd constraint = minStrategyPair.second.existsAbstract(game.getPlayer2Variables()) && maxStrategyPair.second.existsAbstract(game.getPlayer2Variables()); - -// (minStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); -// (maxStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); -// (minStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); -// (maxStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); // Now construct all player 2 choices that actually exist and differ in the min and max case. constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); @@ -326,55 +327,20 @@ namespace storm { // 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::Add pivotStateLower = pivotState.template toAdd() * minResult; -// storm::dd::Add pivotStateUpper = pivotState.template toAdd() * maxResult; -// storm::dd::Bdd pivotStateIsMinProb0 = pivotState && prob01.min.first.getPlayer1States(); -// storm::dd::Bdd pivotStateIsMaxProb0 = pivotState && prob01.max.first.getPlayer1States(); -// storm::dd::Bdd pivotStateLowerStrategies = pivotState && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy(); -// storm::dd::Bdd pivotStateUpperStrategies = pivotState && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy(); -// storm::dd::Bdd pivotStateLowerPl1Strategy = pivotState && prob01.min.first.getPlayer1Strategy(); -// storm::dd::Bdd pivotStateUpperPl1Strategy = pivotState && prob01.max.first.getPlayer1Strategy(); -// storm::dd::Bdd pivotStateLowerPl2Strategy = pivotState && prob01.min.first.getPlayer2Strategy(); -// storm::dd::Bdd pivotStateUpperPl2Strategy = pivotState && prob01.max.first.getPlayer2Strategy(); -// -// minResult.exportToDot("minresult.dot"); -// maxResult.exportToDot("maxresult.dot"); -// pivotState.template toAdd().exportToDot("pivot.dot"); -// pivotStateLower.exportToDot("pivot_lower.dot"); -// pivotStateUpper.exportToDot("pivot_upper.dot"); -// pivotStateIsMinProb0.template toAdd().exportToDot("pivot_is_minprob0.dot"); -// pivotStateIsMaxProb0.template toAdd().exportToDot("pivot_is_maxprob0.dot"); -// pivotStateLowerStrategies.template toAdd().exportToDot("pivot_lower_strats.dot"); -// pivotStateUpperStrategies.template toAdd().exportToDot("pivot_upper_strats.dot"); -// pivotStateLowerPl1Strategy.template toAdd().exportToDot("pivot_lower_pl1_strat.dot"); -// pivotStateUpperPl1Strategy.template toAdd().exportToDot("pivot_upper_pl1_strat.dot"); -// pivotStateLowerPl2Strategy.template toAdd().exportToDot("pivot_lower_pl2_strat.dot"); -// pivotStateUpperPl2Strategy.template toAdd().exportToDot("pivot_upper_pl2_strat.dot"); - // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; -// (pivotState && minStrategyPair.first).template toAdd().exportToDot("pl1_choice_in_pivot.dot"); -// (pivotState && minStrategyPair.first && maxStrategyPair.second).template toAdd().exportToDot("pl1and2_choice_in_pivot.dot"); -// (pivotState && maxStrategyPair.second).template toAdd().exportToDot("pl2_choice_in_pivot.dot"); storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); -// lowerChoice.template toAdd().exportToDot("lower.dot"); -// maxStrategyPair.second.template toAdd().exportToDot("max_strat.dot"); storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); -// lowerChoice2.template toAdd().exportToDot("tmp_lower.dot"); -// lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); -#ifdef LOCAL_DEBUG - lowerChoice.template toAdd().exportToDot("ref_lower.dot"); - lowerChoice1.template toAdd().exportToDot("ref_lower1.dot"); - lowerChoice2.template toAdd().exportToDot("ref_lower2.dot"); -#endif - bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Refining based on lower choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); } else { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); @@ -383,7 +349,10 @@ namespace storm { bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); } @@ -462,6 +431,7 @@ namespace storm { storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { + auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. @@ -479,10 +449,11 @@ namespace storm { targetStates |= game.getBottomStates(); } -#ifdef LOCAL_DEBUG - abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); -#endif - + // #ifdef LOCAL_DEBUG + // abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + // #endif + + auto qualitativeStart = std::chrono::high_resolution_clock::now(); prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); if (result) { @@ -517,15 +488,19 @@ namespace storm { } STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); - + // 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. qualitativeRefinement = refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); } + auto qualitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative step completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); + if (!qualitativeRefinement) { // At this point, we know that we cannot answer the query without further numeric computation. STORM_LOG_TRACE("Starting numerical solution step."); + auto quantitativeStart = std::chrono::high_resolution_clock::now(); // Prepare some storage that we use on-demand during the quantitative solving step. storm::dd::Add minResult = prob01.min.second.getPlayer1States().template toAdd(); @@ -539,6 +514,7 @@ namespace storm { // the result right away. ValueType minValue = storm::utility::zero(); MaybeStateResult minMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); + auto minStart = std::chrono::high_resolution_clock::now(); if (!maybeMin.isZero()) { minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); minMaybeStateResult.player1Strategy &= game.getReachableStates(); @@ -549,7 +525,8 @@ namespace storm { STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << "."); minValue = initialStateMin.getMax(); } - STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << "."); + auto minEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << " in " << std::chrono::duration_cast(minEnd - minStart).count() << "ms."); minMaybeStateResult.player1Strategy = combinedMinPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMinPlayer1QualitativeStrategies, minMaybeStateResult.player1Strategy); minMaybeStateResult.player2Strategy = combinedMinPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMinPlayer2QualitativeStrategies, minMaybeStateResult.player2Strategy); @@ -566,6 +543,7 @@ namespace storm { // Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have // given the result right awy. ValueType maxValue = storm::utility::one(); + auto maxStart = std::chrono::high_resolution_clock::now(); MaybeStateResult maxMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMax.isZero()) { maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult)); @@ -578,7 +556,8 @@ namespace storm { STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states. Expected 1, but got " << initialStateMax.getNonZeroCount() << "."); maxValue = initialStateMax.getMax(); } - STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << "."); + auto maxEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << " in " << std::chrono::duration_cast(maxEnd - maxStart).count() << "ms."); maxMaybeStateResult.player1Strategy = combinedMaxPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMaxPlayer1QualitativeStrategies, maxMaybeStateResult.player1Strategy); maxMaybeStateResult.player2Strategy = combinedMaxPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMaxPlayer2QualitativeStrategies, maxMaybeStateResult.player2Strategy); @@ -589,7 +568,8 @@ namespace storm { return result; } - STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states."); + auto quantitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); result = checkForResultAfterQuantitativeCheck(checkTask, minValue, maxValue); if (result) { @@ -608,19 +588,12 @@ namespace storm { // Check whether the strategies coincide over the reachable parts. storm::dd::Bdd tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy); storm::dd::Bdd commonReach = storm::utility::dd::computeReachableStates(game.getInitialStates(), tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables()); - //std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy)) << std::endl; - //std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl; STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide."); -#ifdef LOCAL_DEBUG - abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy); - abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy); - abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy); - abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy)); -#endif - refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } + auto iterationEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); } STORM_LOG_ASSERT(false, "This point must not be reached."); @@ -630,8 +603,6 @@ namespace storm { template std::pair, storm::utility::graph::GameProb01Result> GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { // Compute the states with probability 0/1. -// storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize); -// storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize); storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index ff573bdd9..0ba299dbf 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -9,14 +9,20 @@ namespace storm { const std::string AbstractionSettings::moduleName = "abstraction"; const std::string AbstractionSettings::addAllGuardsOptionName = "allguards"; + const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, splitPredicatesOptionName, true, "Sets whether the predicates are split into atoms before they are added.").build()); } bool AbstractionSettings::isAddAllGuardsSet() const { return this->getOption(addAllGuardsOptionName).getHasOptionBeenSet(); } + + bool AbstractionSettings::isSplitPredicatesSet() const { + return this->getOption(splitPredicatesOptionName).getHasOptionBeenSet(); + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index f09bf5694..144ca289a 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -22,11 +22,19 @@ namespace storm { * @return True iff the option was set. */ bool isAddAllGuardsSet() const; + + /*! + * Retrieves whether the option to split predicates to atoms was set. + * + * @return True iff the option was set. + */ + bool isSplitPredicatesSet() const; const static std::string moduleName; private: const static std::string addAllGuardsOptionName; + const static std::string splitPredicatesOptionName; }; } diff --git a/src/storm/storage/expressions/EquivalenceChecker.cpp b/src/storm/storage/expressions/EquivalenceChecker.cpp new file mode 100644 index 000000000..31ee34894 --- /dev/null +++ b/src/storm/storage/expressions/EquivalenceChecker.cpp @@ -0,0 +1,23 @@ +#include "storm/storage/expressions/EquivalenceChecker.h" + +#include "storm/solver/SmtSolver.h" + +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace expressions { + + EquivalenceChecker::EquivalenceChecker(std::unique_ptr&& smtSolver, storm::expressions::Expression const& constraint) : smtSolver(std::move(smtSolver)) { + this->smtSolver->add(constraint); + } + + bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) { + this->smtSolver->push(); + this->smtSolver->add((first && !second) || (!first && second)); + bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat; + this->smtSolver->pop(); + return equivalent; + } + + } +} diff --git a/src/storm/storage/expressions/EquivalenceChecker.h b/src/storm/storage/expressions/EquivalenceChecker.h new file mode 100644 index 000000000..eba773014 --- /dev/null +++ b/src/storm/storage/expressions/EquivalenceChecker.h @@ -0,0 +1,28 @@ +#pragma once + +#include + +#include "storm/solver/SmtSolver.h" + +namespace storm { + namespace expressions { + class Expression; + + class EquivalenceChecker { + public: + /*! + * Creates an equivalence checker with the given solver and constraint. + * + * @param smtSolver The solver to use. + * @param constraint An additional constraint. Must be satisfiable. + */ + EquivalenceChecker(std::unique_ptr&& smtSolver, storm::expressions::Expression const& constraint); + + bool areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second); + + private: + std::unique_ptr smtSolver; + }; + + } +} diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 784d7025a..9b6c27e8e 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -66,6 +66,13 @@ namespace storm { */ Expression(Variable const& variable); + /*! + * Creates an expression with the given underlying base expression. + * + * @param expressionPtr A pointer to the underlying base expression. + */ + Expression(std::shared_ptr const& expressionPtr); + // Instantiate constructors and assignments with their default implementations. Expression(Expression const& other) = default; Expression& operator=(Expression const& other) = default; @@ -332,13 +339,6 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: - /*! - * Creates an expression with the given underlying base expression. - * - * @param expressionPtr A pointer to the underlying base expression. - */ - Expression(std::shared_ptr const& expressionPtr); - // A pointer to the underlying base expression. std::shared_ptr expressionPtr; }; diff --git a/src/storm/storage/expressions/PredicateSplitter.cpp b/src/storm/storage/expressions/PredicateSplitter.cpp new file mode 100644 index 000000000..39ac62a6d --- /dev/null +++ b/src/storm/storage/expressions/PredicateSplitter.cpp @@ -0,0 +1,80 @@ +#include "storm/storage/expressions/PredicateSplitter.h" + +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/Expressions.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace expressions { + + std::vector PredicateSplitter::split(storm::expressions::Expression const& expression) { + STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type."); + + // Gather all atoms. + atomicExpressions.clear(); + expression.accept(*this, boost::none); + + // Remove all boolean literals from the atoms. + std::vector atomsToKeep; + for (auto const& atom : atomicExpressions) { + if (!atom.isTrue() && !atom.isFalse()) { + atomsToKeep.push_back(atom); + } + } + atomicExpressions = std::move(atomsToKeep); + + return atomicExpressions; + } + + boost::any PredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) { + atomicExpressions.push_back(expression.shared_from_this()); + return boost::any(); + } + + boost::any PredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + expression.getFirstOperand()->accept(*this, data); + expression.getSecondOperand()->accept(*this, data); + return boost::any(); + } + + boost::any PredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) { + return boost::any(); + } + + boost::any PredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) { + atomicExpressions.push_back(expression.shared_from_this()); + return boost::any(); + } + + boost::any PredicateSplitter::visit(VariableExpression const& expression, boost::any const&) { + if (expression.hasBooleanType()) { + atomicExpressions.push_back(expression.shared_from_this()); + } + return boost::any(); + } + + boost::any PredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + expression.getOperand()->accept(*this, data); + return boost::any(); + } + + boost::any PredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { + return boost::any(); + } + + boost::any PredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) { + return boost::any(); + } + + boost::any PredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) { + return boost::any(); + } + + boost::any PredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) { + return boost::any(); + } + + } +} diff --git a/src/storm/storage/expressions/PredicateSplitter.h b/src/storm/storage/expressions/PredicateSplitter.h new file mode 100644 index 000000000..5fe784a18 --- /dev/null +++ b/src/storm/storage/expressions/PredicateSplitter.h @@ -0,0 +1,31 @@ +#pragma once + +#include + +#include "storm/storage/expressions/ExpressionVisitor.h" + +namespace storm { + namespace expressions { + class Expression; + + class PredicateSplitter : public ExpressionVisitor { + public: + std::vector split(storm::expressions::Expression const& expression); + + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; + + private: + std::vector atomicExpressions; + }; + + } +} diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 46f449cfe..499817ce0 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -929,7 +929,7 @@ namespace storm { // The solution sets. storm::dd::Bdd player1States = psiStates; storm::dd::Bdd player2States = model.getManager().getBddZero(); - + bool done = false; uint_fast64_t iterations = 0; while (!done) { @@ -960,18 +960,14 @@ namespace storm { } // Since we have determined the complements of the desired sets, we need to complement it now. - player1States.template toAdd().exportToDot("not_pl1_prob0.dot"); - (!player1States).template toAdd().exportToDot("pl1_negated_prob0.dot"); player1States = !player1States && model.getReachableStates(); player2States = !player2States && model.getReachableStates(); // Determine all transitions between prob0 states. storm::dd::Bdd transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs())); - player1States.template toAdd().exportToDot("pl1_prob0.dot"); // Determine the distributions that have only successors that are prob0 states. storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); - onlyProb0Successors.template toAdd().exportToDot("only_prob0.dot"); boost::optional> player2StrategyBdd; if (producePlayer2Strategy) { diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp index 7e78d75ca..f306183e7 100644 --- a/src/test/abstraction/PrismMenuGameTest.cpp +++ b/src/test/abstraction/PrismMenuGameTest.cpp @@ -434,7 +434,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -456,7 +456,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_shared()); @@ -595,7 +595,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(1335, game.getNumberOfTransitions()); + EXPECT_EQ(1379, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } @@ -616,7 +616,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(1335, game.getNumberOfTransitions()); + EXPECT_EQ(1379, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } @@ -639,7 +639,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(2656, game.getNumberOfTransitions()); + EXPECT_EQ(2744, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); } @@ -662,7 +662,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(2656, game.getNumberOfTransitions()); + EXPECT_EQ(2744, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); }