sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

working towards predicate synthesis from explicit (qualitative) result for game-based abstraction

main
dehnert 7 years ago
parent
c6a5d5a74d
commit
c2e646b887
10 changed files with 225 additions and 76 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 19
      src/storm/abstraction/ExplicitGameStrategy.cpp
  2. 5
      src/storm/abstraction/ExplicitGameStrategy.h
  3. 6
      src/storm/abstraction/ExplicitGameStrategyPair.cpp
  4. 3
      src/storm/abstraction/ExplicitGameStrategyPair.h
  5. 189
      src/storm/abstraction/MenuGameRefiner.cpp
  6. 26
      src/storm/abstraction/MenuGameRefiner.h
  7. 12
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  8. 22
      src/storm/storage/dd/Odd.cpp
  9. 13
      src/storm/storage/dd/Odd.h
  10. 6
      src/storm/utility/graph.cpp

19
src/storm/abstraction/ExplicitGameStrategy.cpp
View File

@ -35,5 +35,24 @@ namespace storm {
}
}
std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy) {
std::vector<uint64_t> undefinedStates;
for (uint64_t state = 0; state < strategy.getNumberOfStates(); ++state) {
uint64_t choice = strategy.getChoice(state);
if (choice == ExplicitGameStrategy::UNDEFINED) {
undefinedStates.emplace_back(state);
} else {
out << state << " -> " << choice << std::endl;
}
}
out << "undefined states: ";
for (auto state : undefinedStates) {
out << state << ", ";
}
out << std::endl;
return out;
}
}
}

5
src/storm/abstraction/ExplicitGameStrategy.h
View File

@ -2,6 +2,7 @@
#include <cstdint>
#include <vector>
#include <ostream>
namespace storm {
namespace abstraction {
@ -18,10 +19,12 @@ namespace storm {
void setChoice(uint64_t state, uint64_t choice);
bool hasDefinedChoice(uint64_t state) const;
void undefineAll();
private:
std::vector<uint64_t> choices;
};
std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy);
}
}

6
src/storm/abstraction/ExplicitGameStrategyPair.cpp
View File

@ -27,5 +27,11 @@ namespace storm {
return player2Strategy;
}
std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& strategyPair) {
out << "player 1 strategy: " << std::endl << strategyPair.getPlayer1Strategy() << std::endl;
out << "player 2 strategy: " << std::endl << strategyPair.getPlayer2Strategy() << std::endl;
return out;
}
}
}

3
src/storm/abstraction/ExplicitGameStrategyPair.h
View File

@ -1,6 +1,7 @@
#pragma once
#include <cstdint>
#include <ostream>
#include "storm/abstraction/ExplicitGameStrategy.h"
@ -22,5 +23,7 @@ namespace storm {
ExplicitGameStrategy player2Strategy;
};
std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& strategyPair);
}
}

189
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -394,9 +394,12 @@ namespace storm {
// Derive predicates from lower choice.
storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
lowerChoice1.template toAdd<ValueType>().exportToDot("lower1.dot");
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
lowerChoice2.template toAdd<ValueType>().exportToDot("lower2.dot");
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero();
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Deriving predicate based on lower choice.");
@ -523,30 +526,12 @@ namespace storm {
predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution));
return std::make_pair(predicates, stepVariableToCopiedVariableMap);
}
template<storm::dd::DdType Type, typename ValueType>
boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, SymbolicPivotStateResult<Type, ValueType> const& symbolicPivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
// Compute the most probable path from any initial state to the pivot state.
SymbolicMostProbablePathsResult<Type, ValueType> symbolicMostProbablePathsResult;
if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) {
symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
} else {
symbolicMostProbablePathsResult = symbolicPivotStateResult.symbolicMostProbablePathsResult.get();
}
// Create a new expression manager that we can use for the interpolation.
std::shared_ptr<storm::expressions::ExpressionManager> interpolationManager = abstractionInformation.getExpressionManager().clone();
// Build the trace of the most probable path in terms of which predicates hold in each step.
std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState);
auto const& trace = traceAndVariableSubstitution.first;
auto const& variableSubstitution = traceAndVariableSubstitution.second;
template<storm::dd::DdType Type>
boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation<Type> const& abstractionInformation, std::vector<std::vector<storm::expressions::Expression>> const& trace, std::map<storm::expressions::Variable, storm::expressions::Expression> const& variableSubstitution) {
// Create solver and interpolation groups.
storm::solver::MathsatSmtSolver interpolatingSolver(*interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true));
storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true));
uint64_t stepCounter = 0;
auto traceIt = trace.rbegin();
auto traceIte = trace.rend();
@ -559,7 +544,7 @@ namespace storm {
interpolatingSolver.add(predicate);
}
++stepCounter;
storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check();
// If the result already became unsatisfiable
if (result == storm::solver::SmtSolver::CheckResult::Unsat) {
@ -591,6 +576,33 @@ namespace storm {
return boost::none;
}
template<storm::dd::DdType Type, typename ValueType>
boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, SymbolicPivotStateResult<Type, ValueType> const& symbolicPivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
// Compute the most probable path from any initial state to the pivot state.
SymbolicMostProbablePathsResult<Type, ValueType> symbolicMostProbablePathsResult;
if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) {
symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
} else {
symbolicMostProbablePathsResult = symbolicPivotStateResult.symbolicMostProbablePathsResult.get();
}
// Create a new expression manager that we can use for the interpolation.
std::shared_ptr<storm::expressions::ExpressionManager> interpolationManager = abstractionInformation.getExpressionManager().clone();
// Build the trace of the most probable path in terms of which predicates hold in each step.
std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState);
return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second);
}
template<storm::dd::DdType Type, typename ValueType>
boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const {
// TODO.
}
template<storm::dd::DdType Type, typename ValueType>
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax<Type> const& qualitativeResult) const {
STORM_LOG_TRACE("Trying refinement after qualitative check.");
@ -613,6 +625,7 @@ namespace storm {
// 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 (pivotStateCandidatesResult.pivotStates.isZero()) {
STORM_LOG_TRACE("Did not find pivot state in qualitative fragment.");
return false;
}
STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates.");
@ -680,35 +693,25 @@ namespace storm {
}
template<typename ValueType>
ExplicitMostProbablePathsResult<ValueType>::ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector<std::pair<uint64_t, uint64_t>>&& predecessors) : maxProbability(maxProbability), predecessors(std::move(predecessors)) {
// Intentionally left empty.
}
template<typename ValueType>
ExplicitPivotStateResult<ValueType>::ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional<ExplicitMostProbablePathsResult<ValueType>>&& explicitMostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), explicitMostProbablePathsResult(std::move(explicitMostProbablePathsResult)) {
// Intentionally left empty.
}
template<typename ValueType>
ExplicitPivotStateResult<ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) {
boost::optional<ExplicitPivotStateResult<ValueType>> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) {
// Perform Dijkstra search that stays within the relevant states and searches for a state in which the
// strategies for the (commonly chosen) player 1 action leads to a player 2 state in which the choices differ.
ExplicitPivotStateResult<ValueType> explicitPivotStateResult;
explicitPivotStateResult.explicitMostProbablePathsResult = ExplicitMostProbablePathsResult<ValueType>();
auto& explicitMostProbablePathsResult = explicitPivotStateResult.explicitMostProbablePathsResult.get();
ExplicitPivotStateResult<ValueType> result;
bool probabilityDistances = pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MostProbablePath;
uint64_t numberOfStates = initialStates.size();
ValueType inftyDistance = probabilityDistances ? storm::utility::zero<ValueType>() : storm::utility::infinity<ValueType>();
ValueType zeroDistance = probabilityDistances ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
std::vector<ValueType> distances(numberOfStates, inftyDistance);
explicitMostProbablePathsResult.predecessors.resize(numberOfStates, std::make_pair(0, 0));
if (generatePredecessors) {
result.predecessors.resize(numberOfStates, std::make_pair(0, 0));
}
// Use set as priority queue with unique membership; default comparison on pair works fine if distance is
// the first entry.
std::set<std::pair<ValueType, uint64_t>, std::greater<std::pair<ValueType, uint64_t>>> dijkstraQueue;
for (auto initialState : initialStates) {
if (!relevantStates.get(initialState)) {
continue;
@ -718,28 +721,44 @@ namespace storm {
dijkstraQueue.emplace(zeroDistance, initialState);
}
// For some heuristics, we need to potentially find more than just one pivot.
bool foundPivotState = false;
ValueType maximalDeviation = storm::utility::zero<ValueType>();
while (!dijkstraQueue.empty()) {
uint64_t currentState = (*dijkstraQueue.begin()).second;
auto distanceStatePair = *dijkstraQueue.begin();
uint64_t currentState = distanceStatePair.second;
ValueType currentDistance = distanceStatePair.first;
dijkstraQueue.erase(dijkstraQueue.begin());
if (foundPivotState && currentDistance > result.distance) {
return result;
}
// Determine whether the current state is a pivot state.
bool isPivotState = false;
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) {
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) {
isPivotState = true;
}
} else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) {
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) {
isPivotState = true;
}
}
// If it is indeed a pivot state, we can abort the search here.
if (isPivotState) {
explicitPivotStateResult.pivotState = currentState;
return explicitPivotStateResult;
if (foundPivotState && haveQuantitativeResults && deviationOfCurrentState > currentPivotState) {
result.pivotState = currentState;
maximalDeviation = deviationForCurrentState;
} else if (!foundPivotState) {
result.pivotState = currentState;
result.distance = distances[currentState];
foundPivotState = true;
}
}
// Otherwise, we explore all its relevant successors.
@ -753,10 +772,12 @@ namespace storm {
continue;
}
ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one<ValueType>();
ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
distances[player1Successor] = alternateDistance;
explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor);
if (generatePredecessors) {
result.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor);
}
dijkstraQueue.emplace(alternateDistance, player1Successor);
}
}
@ -771,10 +792,12 @@ namespace storm {
continue;
}
ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one<ValueType>();
ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
distances[player1Successor] = alternateDistance;
explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor);
if (generatePredecessors) {
result.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor);
}
dijkstraQueue.emplace(alternateDistance, player1Successor);
}
}
@ -783,24 +806,76 @@ namespace storm {
// If we arrived at this point, we have explored all relevant states, but none of them was a pivot state,
// which can happen when trying to refine using the qualitative result only.
return explicitPivotStateResult;
return boost::none;
}
template<storm::dd::DdType Type, typename ValueType>
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> 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 {
STORM_LOG_THROW(heuristic != AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation, storm::exceptions::NotImplementedException, "The pivot selection heuristic 'maximal weighted deviation' is not supported by the sparse solution strategy.");
// 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());
ExplicitPivotStateResult<ValueType> pivotStateResult = pickPivotState(pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
// If there was no pivot state, continue the search.
if (!pivotStateResult.pivotState) {
if (!optionalPivotStateResult) {
STORM_LOG_TRACE("Did not find pivot state in qualitative fragment.");
return false;
}
// Otherwise, we can refine.
storm::dd::Bdd<Type> pivotState = storm::dd::Bdd<Type>::getEncoding(game.getManager(), pivotStateResult.pivotState.get(), odd, game.getRowVariables());
auto const& pivotStateResult = optionalPivotStateResult.get();
STORM_LOG_TRACE("Found pivot state " << pivotStateResult.pivotState << " with distance " << pivotStateResult.distance << ".");
// Translate the explicit states/choices to the symbolic ones, so we can reuse the predicate derivation techniques.
auto const& abstractionInformation = abstractor.get().getAbstractionInformation();
uint64_t pivotState = pivotStateResult.pivotState;
storm::dd::Bdd<Type> symbolicPivotState = storm::dd::Bdd<Type>::getEncoding(game.getManager(), pivotState, odd, game.getRowVariables());
storm::dd::Bdd<Type> minPlayer1Strategy = game.getManager().getBddZero();
storm::dd::Bdd<Type> maxPlayer1Strategy = game.getManager().getBddZero();
storm::dd::Bdd<Type> minPlayer2Strategy = game.getManager().getBddZero();
storm::dd::Bdd<Type> maxPlayer2Strategy = game.getManager().getBddZero();
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) {
uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(pivotState);
minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[player2State]], abstractionInformation.getPlayer1VariableCount());
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State);
minPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
}
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State);
maxPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
}
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) {
uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(pivotState);
maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[player2State]], abstractionInformation.getPlayer1VariableCount());
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State);
minPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
}
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State);
maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
}
}
boost::optional<RefinementPredicates> predicates;
if (useInterpolation) {
predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd);
}
if (!predicates) {
predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
}
STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");
std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates(predicates.get().getPredicates(), predicates.get().getSource());
performRefinement(createGlobalRefinement(preparedPredicates));
return true;
}
template<storm::dd::DdType Type, typename ValueType>
@ -818,16 +893,16 @@ namespace storm {
STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to refine without pivot state candidates.");
// Now that we have the pivot state candidates, we need to pick one.
SymbolicPivotStateResult<Type, ValueType> SymbolicPivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult);
SymbolicPivotStateResult<Type, ValueType> symbolicPivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult);
boost::optional<RefinementPredicates> predicates;
if (useInterpolation) {
predicates = derivePredicatesFromInterpolation(game, SymbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
predicates = derivePredicatesFromInterpolation(game, symbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
}
if (predicates) {
STORM_LOG_TRACE("Obtained predicates by interpolation.");
} else {
predicates = derivePredicatesFromPivotState(game, SymbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
predicates = derivePredicatesFromPivotState(game, symbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
}
STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");

26
src/storm/abstraction/MenuGameRefiner.h
View File

@ -73,26 +73,17 @@ namespace storm {
boost::optional<SymbolicMostProbablePathsResult<Type, ValueType>> symbolicMostProbablePathsResult;
};
template<typename ValueType>
struct ExplicitMostProbablePathsResult {
ExplicitMostProbablePathsResult() = default;
ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector<std::pair<uint64_t, uint64_t>>&& predecessors);
/// The maximal probability with which the state in question is reached.
ValueType maxProbability;
/// The predecessors for the states to obtain this probability.
std::vector<std::pair<uint64_t, uint64_t>> predecessors;
};
template<typename ValueType>
struct ExplicitPivotStateResult {
ExplicitPivotStateResult() = default;
ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional<ExplicitMostProbablePathsResult<ValueType>>&& explicitMostProbablePathsResult = boost::none);
boost::optional<uint64_t> pivotState;
storm::OptimizationDirection fromDirection;
boost::optional<ExplicitMostProbablePathsResult<ValueType>> explicitMostProbablePathsResult;
uint64_t pivotState;
/// The distance with which the state in question is reached.
ValueType distance;
/// The predecessors for the states to obtain the given distance.
std::vector<std::pair<uint64_t, uint64_t>> predecessors;
};
class ExplicitQualitativeGameResultMinMax;
@ -155,7 +146,8 @@ namespace storm {
boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, SymbolicPivotStateResult<Type, ValueType> const& symbolicPivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const;
boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const;
void performRefinement(std::vector<RefinementCommand> const& refinementCommands) const;
/// The underlying abstractor to refine.

12
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -157,6 +157,12 @@ namespace storm {
}
}
}
} else {
if (player2Direction == storm::OptimizationDirection::Minimize && (prob1 && initialStates) == initialStates) {
result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::one<ValueType>());
} else if (player2Direction == storm::OptimizationDirection::Maximize && (prob0 && initialStates) == initialStates) {
result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::zero<ValueType>());
}
}
return result;
@ -204,6 +210,12 @@ namespace storm {
}
}
}
} else {
if (player2Direction == storm::OptimizationDirection::Minimize && initialStates.isSubsetOf(prob1)) {
result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::one<ValueType>());
} else if (player2Direction == storm::OptimizationDirection::Maximize && initialStates.isSubsetOf(prob0)) {
result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::zero<ValueType>());
}
}
return result;

22
src/storm/storage/dd/Odd.cpp
View File

@ -4,6 +4,8 @@
#include <fstream>
#include <boost/algorithm/string/join.hpp>
#include "storm/storage/BitVector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/file.h"
@ -130,6 +132,26 @@ namespace storm {
storm::utility::closeFile(dotFile);
}
void getEncodingRec(Odd const& odd, uint64_t index, uint64_t offset, storm::storage::BitVector& result) {
if (odd.isTerminalNode()) {
return;
}
bool thenPath = false;
if (odd.getElseOffset() <= offset) {
thenPath = true;
offset -= odd.getElseOffset();
result.set(index);
}
getEncodingRec(thenPath ? odd.getThenSuccessor() : odd.getElseSuccessor(), index + 1, offset, result);
}
storm::storage::BitVector Odd::getEncoding(uint64_t offset, uint64_t variableCount) const {
storm::storage::BitVector result(variableCount > 0 ? variableCount : this->getHeight());
getEncodingRec(*this, 0, offset, result);
return result;
}
void Odd::addToLevelToOddNodesMap(std::map<uint_fast64_t, std::unordered_set<storm::dd::Odd const*>>& levelToOddNodesMap, uint_fast64_t level) const {
levelToOddNodesMap[level].emplace(this);
if (!this->isTerminalNode()) {

13
src/storm/storage/dd/Odd.h
View File

@ -7,6 +7,10 @@
#include <unordered_set>
namespace storm {
namespace storage {
class BitVector;
}
namespace dd {
class Odd {
public:
@ -119,6 +123,15 @@ namespace storm {
*/
void exportToDot(std::string const& filename) const;
/*!
* Retrieves the encoding for the given offset.
*
* @param offset The target offset.
* @param variableCount If not null, this indicates how many variables are contained in the encoding. If 0,
* this number is automatically determined.
*/
storm::storage::BitVector getEncoding(uint64_t offset, uint64_t variableCount = 0) const;
private:
/*!
* Adds all nodes below the current one to the given mapping.

6
src/storm/utility/graph.cpp
View File

@ -1315,7 +1315,7 @@ namespace storm {
while (!stack.empty()) {
currentState = stack.back();
stack.pop_back();
for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) {
uint64_t player2Predecessor = player2PredecessorEntry.getColumn();
if (!player2Solution.get(player2PredecessorEntry.getColumn())) {
@ -1392,6 +1392,10 @@ namespace storm {
if (result.player1States == player1Solution) {
maybeStatesDone = true;
result.player2States = player2Solution;
// If we were asked to produce strategies, we propagate that by triggering another iteration.
// We only do this if at least one strategy will be produced.
produceStrategiesInIteration = !produceStrategiesInIteration && ((player1Strategy && player1Direction == OptimizationDirection::Maximize) || (player2Strategy && player2Direction == OptimizationDirection::Maximize));
} else {
result.player1States = player1Solution;
result.player2States = player2Solution;

Write Preview
Loading…
Cancel
Save