From 64cd0ae212c911d1f3ce534b8984a9067ff98695 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Apr 2018 13:09:46 +0200 Subject: [PATCH] optimizations to trace formula generation --- src/storm/abstraction/MenuGameAbstractor.h | 1 + src/storm/abstraction/MenuGameRefiner.cpp | 322 ++++++++++++++---- src/storm/abstraction/MenuGameRefiner.h | 8 +- .../abstraction/jani/AutomatonAbstractor.cpp | 5 + .../abstraction/jani/AutomatonAbstractor.h | 5 + src/storm/abstraction/jani/EdgeAbstractor.cpp | 12 + src/storm/abstraction/jani/EdgeAbstractor.h | 8 + .../jani/JaniMenuGameAbstractor.cpp | 7 +- .../abstraction/jani/JaniMenuGameAbstractor.h | 5 + .../abstraction/prism/CommandAbstractor.cpp | 12 + .../abstraction/prism/CommandAbstractor.h | 8 + .../abstraction/prism/ModuleAbstractor.cpp | 5 + .../abstraction/prism/ModuleAbstractor.h | 5 + .../prism/PrismMenuGameAbstractor.cpp | 5 + .../prism/PrismMenuGameAbstractor.h | 5 + 15 files changed, 341 insertions(+), 72 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index ee753bebc..7e957e406 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -37,6 +37,7 @@ namespace storm { virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const = 0; std::vector> getVariableUpdates(uint64_t player1Choice) const; virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0; + virtual std::set const& getAssignedVariables(uint64_t player1Choice) const = 0; virtual storm::expressions::Expression getInitialExpression() const = 0; /*! diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 91fbb17e0..a821dc8e5 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -12,6 +12,7 @@ #include "storm/storage/dd/Odd.h" #include "storm/utility/dd.h" #include "storm/utility/solver.h" +#include "storm/utility/shortestPaths.h" #include "storm/solver/MathsatSmtSolver.h" @@ -478,6 +479,10 @@ namespace storm { for (auto& predicate : predicates.back()) { predicate = predicate.changeManager(expressionManager); } + // Add ranges of variables. + for (auto const& pred : abstractionInformation.getConstraints()) { + predicates.back().push_back(pred.changeManager(expressionManager)); + } // Perform a backward search for an initial state. storm::dd::Bdd currentState = pivotState; @@ -526,7 +531,10 @@ namespace storm { for (auto& predicate : predicates.back()) { predicate = predicate.changeManager(expressionManager).substitute(substitution); } - + // Add ranges of variables. + for (auto const& pred : abstractionInformation.getConstraints()) { + predicates.back().push_back(pred.changeManager(expressionManager).substitute(substitution)); + } // Move backwards one step. lastSubstitution = std::move(substitution); currentState = predecessorTransition.existsAbstract(variablesToAbstract); @@ -540,13 +548,34 @@ namespace storm { const uint64_t ExplicitPivotStateResult::NO_PREDECESSOR = std::numeric_limits::max(); template - std::pair>, std::map> MenuGameRefiner::buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const { + std::pair, std::vector> MenuGameRefiner::buildReversedLabeledPath(ExplicitPivotStateResult const& pivotStateResult) const { - std::vector> predicates; + std::pair, std::vector> result; + result.first.emplace_back(pivotStateResult.pivotState); + + uint64_t currentState = pivotStateResult.predecessors[pivotStateResult.pivotState].first; + uint64_t currentAction = pivotStateResult.predecessors[pivotStateResult.pivotState].second; + while (currentState != ExplicitPivotStateResult::NO_PREDECESSOR) { + STORM_LOG_ASSERT(currentAction != ExplicitPivotStateResult::NO_PREDECESSOR, "Expected predecessor action."); + result.first.emplace_back(currentState); + result.second.emplace_back(currentAction); + currentAction = pivotStateResult.predecessors[currentState].second; + currentState = pivotStateResult.predecessors[currentState].first; + } + + STORM_LOG_ASSERT(result.first.size() == result.second.size() + 1, "Path size mismatch."); + return result; + } + + template + std::pair>, std::map> MenuGameRefiner::buildTraceFromReversedLabeledPath(storm::expressions::ExpressionManager& expressionManager, std::vector const& reversedPath, std::vector const& reversedLabels, storm::dd::Odd const& odd, std::vector const* stateToOffset) const { + STORM_LOG_ASSERT(reversedPath.size() == reversedLabels.size() + 1, "Path size mismatch."); + std::vector> predicates; + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); storm::expressions::Expression initialExpression = abstractor.get().getInitialExpression(); - + std::set oldVariables = initialExpression.getVariables(); for (auto const& predicate : abstractionInformation.getPredicates()) { std::set usedVariables = predicate.getVariables(); @@ -557,94 +586,128 @@ namespace storm { for (auto const& variable : oldVariables) { oldToNewVariables[variable] = expressionManager.getVariable(variable.getName()); } - std::map lastSubstitution; + std::map currentSubstitution; for (auto const& variable : oldToNewVariables) { - lastSubstitution[variable.second] = variable.second; + currentSubstitution[variable.second] = variable.second; } std::map stepVariableToCopiedVariableMap; - // The state valuation also includes the bottom state, so we need to reserve one more than the number of - // predicates here. - storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(pivotStateResult.pivotState, abstractionInformation.getNumberOfPredicates() + 1); + auto pathIt = reversedPath.rbegin(); + + // Decode initial state. The state valuation also includes the bottom state, so we need to reserve one more + // than the number of predicates here. + storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + 1); + ++pathIt; - // Decode pivot state. + // Add all predicates of initial block. predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation)); for (auto& predicate : predicates.back()) { predicate = predicate.changeManager(expressionManager); } - // Perform a backward traversal from the pivot state along the chosen predecessors until there is no more - // predecessors. - uint64_t currentState = pivotStateResult.predecessors[pivotStateResult.pivotState].first; - uint64_t currentAction = pivotStateResult.predecessors[pivotStateResult.pivotState].second; - while (currentState != ExplicitPivotStateResult::NO_PREDECESSOR) { - // Create a new copy of each variable to use for this step. - std::map substitution; - for (auto const& variablePair : oldToNewVariables) { - storm::expressions::Variable variableCopy = expressionManager.declareVariableCopy(variablePair.second); - substitution[variablePair.second] = variableCopy; - stepVariableToCopiedVariableMap[variableCopy] = variablePair.second; + // Add ranges of further constraints. + for (auto const& pred : abstractionInformation.getConstraints()) { + predicates.back().push_back(pred.changeManager(expressionManager)); + } + + // Add initial expression. + predicates.back().push_back(initialExpression.changeManager(expressionManager)); + + // Traverse the path and construct necessary formula parts. + auto actionIt = reversedLabels.rbegin(); + for (; pathIt != reversedPath.rend(); ++pathIt) { + + // Add new predicate frame. + predicates.emplace_back(); + + // Add guard of action. + predicates.back().emplace_back(abstractor.get().getGuard(*actionIt).changeManager(expressionManager).substitute(currentSubstitution)); + + // Determine which variables are affected by the updates of the player 1 choice. + std::set const& assignedVariables = abstractor.get().getAssignedVariables(*actionIt); + + // Create new instances of the affected variables. + std::map newVariableMaps; + for (auto const& variable : assignedVariables) { + storm::expressions::Variable variableCopy = expressionManager.declareVariableCopy(variable); + newVariableMaps[oldToNewVariables.at(variable)] = variableCopy; + stepVariableToCopiedVariableMap[variableCopy] = variable; } - // Retrieve the variable updates that the predecessor needs to perform to get to the current state. - auto variableUpdateVector = abstractor.get().getVariableUpdates(currentAction); + // Retrieves the possible updates to the variables. + auto variableUpdateVector = abstractor.get().getVariableUpdates(*actionIt); + + // Encode these updates. storm::expressions::Expression allVariableUpdateExpression; for (auto const& variableUpdates : variableUpdateVector) { storm::expressions::Expression variableUpdateExpression; - for (auto const& oldNewVariablePair : oldToNewVariables) { - storm::expressions::Variable const& newVariable = oldNewVariablePair.second; - - // If the variable was set, use its update expression. - auto updateIt = variableUpdates.find(oldNewVariablePair.first); - if (updateIt != variableUpdates.end()) { - auto const& update = *updateIt; - - if (update.second.hasBooleanType()) { - variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), update.second.changeManager(expressionManager).substitute(substitution)); - } else { - variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == update.second.changeManager(expressionManager).substitute(substitution); - } + for (auto const& update : variableUpdates) { + if (update.second.hasBooleanType()) { + variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(newVariableMaps.at(update.first), update.second.changeManager(expressionManager).substitute(currentSubstitution)); } else { - // Otherwise, make sure that the new variable maintains the old value. - if (newVariable.hasBooleanType()) { - variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), substitution.at(newVariable)); - } else { - variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == substitution.at(newVariable); - } + variableUpdateExpression = variableUpdateExpression && newVariableMaps.at(update.first) == update.second.changeManager(expressionManager).substitute(currentSubstitution); } } allVariableUpdateExpression = allVariableUpdateExpression || variableUpdateExpression; } - - // Add variable update expression. predicates.back().emplace_back(allVariableUpdateExpression); - - // Add the guard of the choice. - predicates.back().emplace_back(abstractor.get().getGuard(currentAction).changeManager(expressionManager).substitute(substitution)); - // Retrieve the predicate valuation in the predecessor. - extendedPredicateValuation = odd.getEncoding(currentState, abstractionInformation.getNumberOfPredicates() + 1); - predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation)); - for (auto& predicate : predicates.back()) { - predicate = predicate.changeManager(expressionManager).substitute(substitution); + // Incorporate the new variables in the current substitution. + for (auto const& variablePair : newVariableMaps) { + currentSubstitution[variablePair.first] = variablePair.second; } - // Move backwards one step. - lastSubstitution = std::move(substitution); - - std::pair predecessorPair = pivotStateResult.predecessors[currentState]; - currentState = predecessorPair.first; - currentAction = predecessorPair.second; + // Decode current state. + extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + 1); + + // Encode the predicates whose value might have changed. + // FIXME: could be optimized by precomputation. + for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.getNumberOfPredicates(); ++predicateIndex) { + auto const& predicate = abstractionInformation.getPredicateByIndex(predicateIndex); + std::set usedVariables = predicate.getVariables(); + + bool containsAssignedVariables = false; + for (auto usedIt = usedVariables.begin(), assignedIt = assignedVariables.begin();;) { + if (usedIt == usedVariables.end() || assignedIt == assignedVariables.end()) { + break; + } + + if (*usedIt == *assignedIt) { + containsAssignedVariables = true; + break; + } + + if (*usedIt < *assignedIt) { + ++usedIt; + } else { + ++assignedIt; + } + } + + if (containsAssignedVariables) { + auto transformedPredicate = predicate.changeManager(expressionManager).substitute(currentSubstitution); + predicates.back().emplace_back(extendedPredicateValuation.get(predicateIndex + 1) ? transformedPredicate : !transformedPredicate); + } + } + + // Enforce ranges of all assigned variables. +// for (auto const& variablePair : newVariableMaps) { +// for (auto const& ) +// } + + ++actionIt; } - predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution)); + std::reverse(predicates.begin(), predicates.end()); return std::make_pair(predicates, stepVariableToCopiedVariableMap); } - - template - boost::optional derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation const& abstractionInformation, std::vector> const& trace, std::map const& variableSubstitution) { + + template + boost::optional MenuGameRefiner::derivePredicatesFromInterpolationFromTrace(storm::expressions::ExpressionManager& interpolationManager, std::vector> const& trace, std::map const& variableSubstitution) const { + + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); auto start = std::chrono::high_resolution_clock::now(); boost::optional predicates; @@ -656,7 +719,6 @@ namespace storm { auto traceIt = trace.rbegin(); auto traceIte = trace.rend(); for (; traceIt != traceIte; ++traceIt) { - auto iterationStart = std::chrono::high_resolution_clock::now(); auto const& step = *traceIt; interpolatingSolver.push(); @@ -664,13 +726,11 @@ namespace storm { for (auto const& predicate : step) { interpolatingSolver.add(predicate); } - auto iterationEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Asserting step of trace formula took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); ++stepCounter; } auto assertionEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Asserting trace formula until unsatisfiability took " << std::chrono::duration_cast(assertionEnd - assertionStart).count() << "ms."); + STORM_LOG_TRACE("Asserting trace formula took " << std::chrono::duration_cast(assertionEnd - assertionStart).count() << "ms."); // Now encode the trace as an SMT problem. storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check(); @@ -682,11 +742,18 @@ namespace storm { for (uint64_t step = 0; step < stepCounter; ++step) { prefix.push_back(step); storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager()); - if (!interpolant.isTrue() && !interpolant.isFalse()) { + if (interpolant.isFalse()) { + // If the interpolant is false, it means that the prefix has become unsatisfiable. + break; + } + if (!interpolant.isTrue()) { STORM_LOG_DEBUG("Derived new predicate (based on interpolation at step " << step << " out of " << stepCounter << "): " << interpolant); interpolants.push_back(interpolant); } } + + STORM_LOG_ASSERT(!interpolants.empty(), "Expected to have non-empty set of interpolants."); + predicates = boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); } else { STORM_LOG_TRACE("Trace formula is satisfiable, not using interpolation."); @@ -723,7 +790,7 @@ namespace storm { auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Building the trace and variable substitution for interpolation from symbolic most-probable paths result took " << std::chrono::duration_cast(end - start).count() << "ms."); - return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); + return derivePredicatesFromInterpolationFromTrace(*interpolationManager, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); } template @@ -735,11 +802,18 @@ namespace storm { // Build the trace of the most probable path in terms of which predicates hold in each step. auto start = std::chrono::high_resolution_clock::now(); - std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, pivotStateResult, odd); + std::pair, std::vector> labeledReversedPath = buildReversedLabeledPath(pivotStateResult); + + // If the initial state is the pivot state, we can stop here. + if (labeledReversedPath.first.size() == 1) { + return boost::none; + } + + std::pair>, std::map> traceAndVariableSubstitution = buildTraceFromReversedLabeledPath(*interpolationManager, labeledReversedPath.first, labeledReversedPath.second, odd); auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Building the trace and variable substitution for interpolation from explicit most-probable paths result took " << std::chrono::duration_cast(end - start).count() << "ms."); - return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); + return derivePredicatesFromInterpolationFromTrace(*interpolationManager, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); } template @@ -980,9 +1054,112 @@ namespace storm { return boost::none; } + template + boost::optional MenuGameRefiner::derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd, storm::expressions::ExpressionManager& interpolationManager, std::vector const& reversedPath, std::vector const& stateToOffset, std::vector const& reversedLabels) const { + + // Build the trace of the most probable path in terms of which predicates hold in each step. + auto start = std::chrono::high_resolution_clock::now(); + std::pair>, std::map> traceAndVariableSubstitution = buildTraceFromReversedLabeledPath(interpolationManager, reversedPath, reversedLabels, odd, &stateToOffset); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Building the trace and variable substitution for interpolation from explicit most-probable paths result took " << std::chrono::duration_cast(end - start).count() << "ms."); + + return derivePredicatesFromInterpolationFromTrace(interpolationManager, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); + } + + template + boost::optional MenuGameRefiner::derivePredicatesFromInterpolationKShortestPaths(storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability, ExplicitGameStrategyPair const& maxStrategyPair) const { + + // Extract the underlying DTMC of the max strategy pair. + + // Start by determining which states are reachable. + storm::storage::BitVector reachableStatesInMaxFragment(initialStates); + std::vector stack(initialStates.begin(), initialStates.end()); + while (!stack.empty()) { + uint64_t currentState = stack.back(); + stack.pop_back(); + + uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor); + for (auto const& successorEntry : transitionMatrix.getRow(player2Choice)) { + if (!reachableStatesInMaxFragment.get(successorEntry.getColumn())) { + reachableStatesInMaxFragment.set(successorEntry.getColumn()); + if (!targetStates.get(successorEntry.getColumn())) { + stack.push_back(successorEntry.getColumn()); + } + } + } + } + + uint64_t numberOfReachableStates = reachableStatesInMaxFragment.getNumberOfSetBits(); + std::vector reachableStatesWithLowerIndex = reachableStatesInMaxFragment.getNumberOfSetBitsBeforeIndices(); + + // Now construct the matrix just for these entries. + storm::storage::SparseMatrixBuilder builder(numberOfReachableStates, numberOfReachableStates); + storm::storage::BitVector dtmcInitialStates(numberOfReachableStates); + typename storm::utility::ksp::ShortestPathsGenerator::StateProbMap targetProbabilities; + std::vector stateToOffset(numberOfReachableStates); + std::vector dtmcPlayer1Labels(numberOfReachableStates); + uint64_t currentRow = 0; + for (auto currentState : reachableStatesInMaxFragment) { + stateToOffset[currentRow] = currentState; + if (targetStates.get(currentState)) { + targetProbabilities[currentRow] = storm::utility::one(); + builder.addNextValue(currentRow, currentRow, storm::utility::one()); + } else { + uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); + dtmcPlayer1Labels[currentRow] = player1Labeling[player2Successor]; + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor); + + for (auto const& successorEntry : transitionMatrix.getRow(player2Choice)) { + builder.addNextValue(currentRow, reachableStatesWithLowerIndex[successorEntry.getColumn()], successorEntry.getValue()); + } + } + + if (initialStates.get(currentState)) { + dtmcInitialStates.set(currentRow); + } + ++currentRow; + } + storm::storage::SparseMatrix dtmcMatrix = builder.build(); + + // Create a new expression manager that we can use for the interpolation. + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); + + // Use a path generator to compute k-shortest-paths. + storm::utility::ksp::ShortestPathsGenerator pathGenerator(dtmcMatrix, targetProbabilities, dtmcInitialStates, storm::utility::ksp::MatrixFormat::straight); + uint64_t currentShortestPath = 1; + bool considerNextPath = true; + + boost::optional result; + + while (currentShortestPath < 100 && considerNextPath) { + auto reversedPath = pathGenerator.getPathAsList(currentShortestPath); + std::vector reversedLabels; + for (auto stateIt = reversedPath.rbegin(); stateIt != reversedPath.rend() - 1; ++stateIt) { + reversedLabels.push_back(player1Labeling[maxStrategyPair.getPlayer1Strategy().getChoice(stateToOffset[*stateIt])]); + } + + boost::optional pathPredicates = derivePredicatesFromInterpolationReversedPath(odd, *interpolationManager, reversedPath, stateToOffset, reversedLabels); + if (pathPredicates) { + if (!result) { + result = RefinementPredicates(RefinementPredicates::Source::Interpolation, pathPredicates.get().getPredicates()); + } else { + result.get().addPredicates(pathPredicates.get().getPredicates()); + } + } + ++currentShortestPath; + } + + exit(-1); + return result; + } + template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const { +// boost::optional kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix, player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, storm::utility::zero(), storm::utility::one(), maxStrategyPair); + // Compute the set of states whose result we have for the min and max case. storm::storage::BitVector relevantStates = (qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates()) & (qualitativeResult.getProb0Max().getStates() | qualitativeResult.getProb1Max().getStates()); @@ -1054,6 +1231,11 @@ namespace storm { template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const { + ValueType lower = quantitativeResult.getMin().getRange(initialStates).first; + ValueType upper = quantitativeResult.getMax().getRange(initialStates).second; + +// boost::optional kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix, player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, lower, upper, maxStrategyPair); + // Compute the set of states whose result we have for the min and max case. storm::storage::BitVector relevantStates(odd.getTotalOffset(), true); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 1db5ed8df..a3269ac91 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -157,12 +157,18 @@ namespace storm { */ std::vector createGlobalRefinement(std::vector const& predicates) const; + boost::optional derivePredicatesFromInterpolationFromTrace(storm::expressions::ExpressionManager& interpolationManager, std::vector> const& trace, std::map const& variableSubstitution) const; + boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, SymbolicPivotStateResult const& symbolicPivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; std::pair>, std::map> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& spanningTree, storm::dd::Bdd const& pivotState) const; - std::pair>, std::map> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const; + std::pair, std::vector> buildReversedLabeledPath(ExplicitPivotStateResult const& pivotStateResult) const; + std::pair>, std::map> buildTraceFromReversedLabeledPath(storm::expressions::ExpressionManager& expressionManager, std::vector const& reversedPath, std::vector const& reversedLabels, storm::dd::Odd const& odd, std::vector const* stateToOffset = nullptr) const; boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const; + boost::optional derivePredicatesFromInterpolationKShortestPaths(storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability, ExplicitGameStrategyPair const& maxStrategyPair) const; + boost::optional derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd, storm::expressions::ExpressionManager& interpolationManager, std::vector const& reversedPath, std::vector const& stateToOffset, std::vector const& player1Labels) const; + void performRefinement(std::vector const& refinementCommands) const; /// The underlying abstractor to refine. diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 5ab326657..f5c8030da 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -61,6 +61,11 @@ namespace storm { return edges[player1Choice].getVariableUpdates(auxiliaryChoice); } + template + std::set const& AutomatonAbstractor::getAssignedVariables(uint64_t player1Choice) const { + return edges[player1Choice].getAssignedVariables(); + } + template GameBddResult AutomatonAbstractor::abstract() { // First, we retrieve the abstractions of all commands. diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index e9ff1d76a..658d154f4 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -68,6 +68,11 @@ namespace storm { */ std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const; + /*! + * Retrieves the variables assigned by the given player 1 choice. + */ + std::set const& getAssignedVariables(uint64_t player1Choice) const; + /*! * Computes the abstraction of the module wrt. to the current set of predicates. * diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 8f0ab300e..a1fbe6fe9 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -36,6 +36,13 @@ namespace storm { // Assert the guard of the command. smtSolver->add(edge.getGuard()); + + // Construct assigned variables. + for (auto const& destination : edge.getDestinations()) { + for (auto const& assignment : destination.getOrderedAssignments()) { + assignedVariables.insert(assignment.getExpressionVariable()); + } + } } template @@ -75,6 +82,11 @@ namespace storm { return edge.get().getDestination(auxiliaryChoice).getAsVariableToExpressionMap(); } + template + std::set const& EdgeAbstractor::getAssignedVariables() const { + return assignedVariables; + } + template void EdgeAbstractor::recomputeCachedBdd() { if (useDecomposition) { diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index f3dfa531c..22cc7c40d 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -83,6 +83,11 @@ namespace storm { */ std::map getVariableUpdates(uint64_t auxiliaryChoice) const; + /*! + * Retrieves the assigned variables. + */ + std::set const& getAssignedVariables() const; + /*! * Computes the abstraction of the edge wrt. to the current set of predicates. * @@ -230,6 +235,9 @@ namespace storm { // The concrete edge this abstract command refers to. std::reference_wrapper edge; + // The variables to which this edge assigns expressions. + std::set assignedVariables; + // The local expression-related information. LocalExpressionInformation localExpressionInformation; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index a5bc90ed0..b41ccf418 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -129,6 +129,11 @@ namespace storm { return automata.front().getVariableUpdates(player1Choice, auxiliaryChoice); } + template + std::set const& JaniMenuGameAbstractor::getAssignedVariables(uint64_t player1Choice) const { + return automata.front().getAssignedVariables(player1Choice); + } + template std::pair JaniMenuGameAbstractor::getPlayer1ChoiceRange() const { return std::make_pair(0, automata.front().getNumberOfEdges()); @@ -219,7 +224,7 @@ namespace storm { bool hasBottomStates = !bottomStateResult.states.isZero(); // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); + storm::dd::Add transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= edgeDecoratorAdd; transitionMatrix += deadlockTransitions; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 0a366c625..3a02583b4 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -86,6 +86,11 @@ namespace storm { */ std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override; + /*! + * Retrieves the variables assigned by the given player 1 choice. + */ + virtual std::set const& getAssignedVariables(uint64_t player1Choice) const override; + /*! * Retrieves the range of player 1 choices. */ diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 15b68685e..1c632e4c9 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -36,6 +36,13 @@ namespace storm { // Assert the guard of the command. smtSolver->add(command.getGuardExpression()); + + // Construct assigned variables. + for (auto const& update : command.getUpdates()) { + for (auto const& assignment : update.getAssignments()) { + assignedVariables.insert(assignment.getVariable()); + } + } } template @@ -75,6 +82,11 @@ namespace storm { return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); } + template + std::set const& CommandAbstractor::getAssignedVariables() const { + return assignedVariables; + } + template void CommandAbstractor::recomputeCachedBdd() { if (useDecomposition) { diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index d5c725921..cb448bad8 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -81,6 +81,11 @@ namespace storm { */ std::map getVariableUpdates(uint64_t auxiliaryChoice) const; + /*! + * Retrieves the assigned variables. + */ + std::set const& getAssignedVariables() const; + /*! * Computes the abstraction of the command wrt. to the current set of predicates. * @@ -223,6 +228,9 @@ namespace storm { // The concrete command this abstract command refers to. std::reference_wrapper command; + // The variables to which this command assigns expressions. + std::set assignedVariables; + // The local expression-related information. LocalExpressionInformation localExpressionInformation; diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index b5180ecf4..84c6d9523 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -55,6 +55,11 @@ namespace storm { return commands[player1Choice].getVariableUpdates(auxiliaryChoice); } + template + std::set const& ModuleAbstractor::getAssignedVariables(uint64_t player1Choice) const { + return commands[player1Choice].getAssignedVariables(); + } + template GameBddResult ModuleAbstractor::abstract() { // First, we retrieve the abstractions of all commands. diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 8aef43562..a8d5c94cd 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -71,6 +71,11 @@ namespace storm { */ std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const; + /*! + * Retrieves the variables assigned by the given player 1 choice. + */ + std::set const& getAssignedVariables(uint64_t player1Choice) const; + /*! * Computes the abstraction of the module wrt. to the current set of predicates. * diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index e7bfe8522..7908a5a5e 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -125,6 +125,11 @@ namespace storm { return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice); } + template + std::set const& PrismMenuGameAbstractor::getAssignedVariables(uint64_t player1Choice) const { + return modules.front().getAssignedVariables(player1Choice); + } + template std::pair PrismMenuGameAbstractor::getPlayer1ChoiceRange() const { return std::make_pair(0, modules.front().getCommands().size()); diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index ce5f7ac42..21d64cd30 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -85,6 +85,11 @@ namespace storm { * 1 choice and auxiliary choice. */ std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override; + + /*! + * Retrieves the variables assigned by the given player 1 choice. + */ + virtual std::set const& getAssignedVariables(uint64_t player1Choice) const override; /*! * Retrieves the range of player 1 choices.