diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
index 9ba2ab69a..4ffff8722 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
@@ -1007,7 +1007,7 @@ cuddAddMinAbstractRepresentativeRecur(
return one;
}
if (cuddIsConstant(f)) {
- res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
+ res = cuddAddMinAbstractRepresentativeRecur(manager, f, cuddT(cube));
if (res == NULL) {
return(NULL);
}
@@ -1193,7 +1193,7 @@ cuddAddMaxAbstractRepresentativeRecur(
return one;
}
if (cuddIsConstant(f)) {
- res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
+ res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cuddT(cube));
if (res == NULL) {
return(NULL);
}
diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
index 1b26c6987..f8830d64c 100644
--- a/resources/3rdparty/include_cudd.cmake
+++ b/resources/3rdparty/include_cudd.cmake
@@ -28,4 +28,4 @@ add_dependencies(resources cudd3)
message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}")
#message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}")
-include_directories(${CUDD_INCLUDE_DIR})
\ No newline at end of file
+include_directories(${CUDD_INCLUDE_DIR})
diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp
index 77337751d..92c763e5c 100644
--- a/src/abstraction/StateSetAbstractor.cpp
+++ b/src/abstraction/StateSetAbstractor.cpp
@@ -65,7 +65,6 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
- STORM_LOG_TRACE("Building source state BDD.");
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
for (auto const& variableIndexPair : relevantPredicatesAndVariables) {
if (model.getBooleanValue(variableIndexPair.first)) {
@@ -81,8 +80,6 @@ namespace storm {
void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() {
// Now check whether we need to recompute the cached BDD.
std::set<uint_fast64_t> newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables);
- STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor.");
-
// Since the number of relevant predicates is monotonic, we can simply check for the size here.
STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates.");
bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size();
diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp
index cb46308a4..0f1dc3932 100644
--- a/src/abstraction/prism/AbstractCommand.cpp
+++ b/src/abstraction/prism/AbstractCommand.cpp
@@ -21,7 +21,7 @@ namespace storm {
namespace abstraction {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
- AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0, 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
+ AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
// Make the second component of relevant predicates have the right size.
relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -109,8 +109,9 @@ namespace storm {
STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
+ // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice.
+ uint_fast64_t distributionIndex = 1;
storm::dd::Bdd<DdType> allDistributions = this->getAbstractionInformation().getDdManager().getBddZero();
- uint_fast64_t distributionIndex = 0;
for (auto const& distribution : sourceDistributionsPair.second) {
allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded);
++distributionIndex;
@@ -126,7 +127,7 @@ namespace storm {
STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
// Cache the result.
- cachedDd = GameBddResult<DdType>(resultBdd, numberOfVariablesNeeded, maximalNumberOfChoices);
+ cachedDd = GameBddResult<DdType>(resultBdd, numberOfVariablesNeeded);
}
template <storm::dd::DdType DdType, typename ValueType>
@@ -215,7 +216,6 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
- STORM_LOG_TRACE("Building source state BDD.");
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
if (model.getBooleanValue(variableIndexPair.first)) {
@@ -231,7 +231,6 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
- STORM_LOG_TRACE("Building distribution BDD.");
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
@@ -330,7 +329,7 @@ namespace storm {
result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false);
// Add the command encoding and the next free player 2 encoding.
- result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount());
+ result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount());
return result;
}
diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp
index 79c144c9d..b9b001bd7 100644
--- a/src/abstraction/prism/AbstractModule.cpp
+++ b/src/abstraction/prism/AbstractModule.cpp
@@ -41,11 +41,9 @@ namespace storm {
// First, we retrieve the abstractions of all commands.
std::vector<GameBddResult<DdType>> commandDdsAndUsedOptionVariableCounts;
uint_fast64_t maximalNumberOfUsedOptionVariables = 0;
- uint_fast64_t nextFreePlayer2Index = 0;
for (auto& command : commands) {
commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd());
maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables);
- nextFreePlayer2Index = std::max(nextFreePlayer2Index, commandDdsAndUsedOptionVariableCounts.back().nextFreePlayer2Index);
}
// Then, we build the module BDD by adding the single command DDs. We need to make sure that all command
@@ -54,7 +52,7 @@ namespace storm {
for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) {
result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
}
- return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index);
+ return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables);
}
template <storm::dd::DdType DdType, typename ValueType>
diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp
index a175b62ad..ec146d67e 100644
--- a/src/abstraction/prism/AbstractProgram.cpp
+++ b/src/abstraction/prism/AbstractProgram.cpp
@@ -180,7 +180,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).
- newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap());
+ newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
break;
}
}
diff --git a/src/abstraction/prism/GameBddResult.cpp b/src/abstraction/prism/GameBddResult.cpp
index df22713d7..2e7df1f5e 100644
--- a/src/abstraction/prism/GameBddResult.cpp
+++ b/src/abstraction/prism/GameBddResult.cpp
@@ -5,12 +5,12 @@ namespace storm {
namespace prism {
template <storm::dd::DdType DdType>
- GameBddResult<DdType>::GameBddResult() : bdd(), numberOfPlayer2Variables(0), nextFreePlayer2Index(0) {
+ GameBddResult<DdType>::GameBddResult() : bdd(), numberOfPlayer2Variables(0) {
// Intentionally left empty.
}
template <storm::dd::DdType DdType>
- GameBddResult<DdType>::GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) {
+ GameBddResult<DdType>::GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) {
// Intentionally left empty.
}
diff --git a/src/abstraction/prism/GameBddResult.h b/src/abstraction/prism/GameBddResult.h
index c04309e98..02ad2f724 100644
--- a/src/abstraction/prism/GameBddResult.h
+++ b/src/abstraction/prism/GameBddResult.h
@@ -9,11 +9,10 @@ namespace storm {
template <storm::dd::DdType DdType>
struct GameBddResult {
GameBddResult();
- GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index);
+ GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables);
storm::dd::Bdd<DdType> bdd;
uint_fast64_t numberOfPlayer2Variables;
- uint_fast64_t nextFreePlayer2Index;
};
}
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 2357770af..18451494c 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -195,18 +195,19 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
- storm::dd::Bdd<Type> transitionsInIntersection = (transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables());
-
- // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the
- // state space *under both* strategy pairs.
- storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables());
-
- // Then constrain this set by requiring that the two stratey pairs resolve the nondeterminism differently.
- pivotStates &= (prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy()).exclusiveOr(prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables());
+ // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies.
+ storm::dd::Bdd<Type> reachableTransitions = prob01.min.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy();
+ reachableTransitions = (prob01.min.first.getPlayer1Strategy() && reachableTransitions) || (prob01.max.second.getPlayer1Strategy() && reachableTransitions);
+ reachableTransitions &= transitionMatrixBdd;
+ reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
+ storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
+
+ // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different.
+ pivotStates &= ((prob01.min.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy()) && (prob01.min.first.getPlayer2Strategy().exclusiveOr(prob01.max.second.getPlayer2Strategy()))).existsAbstract(game.getNondeterminismVariables());
STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates.");
// Now that we have the pivot state candidates, we need to pick one.
- storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables(), pivotStates);
+ storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
// Compute the lower and the upper choice for the pivot state.
std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
@@ -235,7 +236,22 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<storm::dd::Add<Type, ValueType>> startVector = boost::none) {
+ struct MaybeStateResult {
+ MaybeStateResult() = default;
+
+ MaybeStateResult(storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+ // Intentionally left empty.
+ }
+
+ storm::dd::Add<Type, ValueType> values;
+ storm::dd::Bdd<Type> player1Strategy;
+ storm::dd::Bdd<Type> player2Strategy;
+ };
+
+ template<storm::dd::DdType Type, typename ValueType>
+ MaybeStateResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<MaybeStateResult<Type, ValueType>> startInfo = boost::none) {
+
+ STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
// Compute the ingredients of the equation system.
storm::dd::Add<Type, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -248,14 +264,28 @@ namespace storm {
submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs());
// Cut the starting vector to the maybe states of this query.
- if (startVector) {
- startVector.get() *= maybeStatesAdd;
+ storm::dd::Add<Type, ValueType> startVector;
+ if (startInfo) {
+ startVector = startInfo.get().values * maybeStatesAdd;
+ } else {
+ startVector = game.getManager().template getAddZero<ValueType>();
}
// Create the solver and solve the equation system.
storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
- return solver->solveGame(player1Direction, player2Direction, startVector ? startVector.get() : game.getManager().template getAddZero<ValueType>(), subvector);
+ solver->setGeneratePlayersStrategies(true);
+ auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector);
+ storm::dd::Bdd<Type> player1Strategy = solver->getPlayer1Strategy();
+ storm::dd::Bdd<Type> player2Strategy = solver->getPlayer2Strategy();
+
+ // If we were given a starting point, we fix the strategies now. That is, we only deviate from the
+ if (startInfo) {
+ player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy);
+ player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy);
+ }
+
+ return MaybeStateResult<Type, ValueType>(values, player1Strategy, player2Strategy);
}
template<storm::dd::DdType Type, typename ValueType>
@@ -285,9 +315,8 @@ namespace storm {
}
storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
-
for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
- STORM_LOG_TRACE("Starting iteration " << iterations);
+ STORM_LOG_TRACE("Starting iteration " << iterations << ".");
abstractor.exportToDot("game" + std::to_string(iterations) + ".dot");
// 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
@@ -351,13 +380,16 @@ namespace storm {
storm::dd::Add<Type, ValueType> initialStatesAdd = game.getInitialStates().template toAdd<ValueType>();
ValueType minValue = (prob01.min.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+ MaybeStateResult<Type, ValueType> minMaybeStateResult;
if (!maybeMin.isZero()) {
- minResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states);
+ minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states);
+ minResult += minMaybeStateResult.values;
storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult;
- STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() == 1, "Wrong number of results for initial states.");
+ // Here we can only require a non-zero count of *at most* one, because the result may actually be 0.
+ STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states.");
minValue = initialStateMin.getMax();
}
- STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue);
+ STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << ".");
// Check whether we can abort the computation because of the lower value.
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minValue);
@@ -366,13 +398,18 @@ namespace storm {
}
ValueType maxValue = (prob01.max.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+ MaybeStateResult<Type, ValueType> maxMaybeStateResult;
if (!maybeMax.isZero()) {
- maxResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional<storm::dd::Add<Type, ValueType>>(minResult));
+ // FIXME: fix strategy: only change if improved.
+ maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional<MaybeStateResult<Type, ValueType>>(minMaybeStateResult));
+ maxResult += maxMaybeStateResult.values;
storm::dd::Add<Type, ValueType> initialStateMax = (initialStatesAdd * maxResult);
+ // Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in
+ // fact 0, the result would be 0, which would have been detected earlier by the graph algorithms.
STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states.");
maxValue = initialStateMax.getMax();
}
- STORM_LOG_TRACE("Obtained quantitative upper bound " << minValue);
+ STORM_LOG_TRACE("Obtained quantitative upper bound " << minValue << ".");
// Check whether we can abort the computation because of the upper value.
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxValue);
@@ -386,6 +423,9 @@ namespace storm {
if (result) {
return result;
}
+
+ // If we arrived at this point, it means that we have all qualitative and quantitative information
+ // about the game, but we could not yet answer the query. In this case, we need to refine.
STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)");
}
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index 97abf9581..ad1dadc6c 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -57,6 +57,11 @@ namespace storm {
return *manager;
}
+ template<storm::dd::DdType Type, typename ValueType>
+ std::shared_ptr<storm::dd::DdManager<Type>> const& Model<Type, ValueType>::getManagerAsSharedPointer() const {
+ return manager;
+ }
+
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> const& Model<Type, ValueType>::getReachableStates() const {
return reachableStates;
diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h
index 359ae8255..4483a2a6c 100644
--- a/src/models/symbolic/Model.h
+++ b/src/models/symbolic/Model.h
@@ -109,6 +109,13 @@ namespace storm {
* @return The manager responsible for the DDs that represent this model.
*/
storm::dd::DdManager<Type>& getManager();
+
+ /*!
+ * Retrieves the manager responsible for the DDs that represent this model.
+ *
+ * @return The manager responsible for the DDs that represent this model.
+ */
+ std::shared_ptr<storm::dd::DdManager<Type>> const& getManagerAsSharedPointer() const;
/*!
* Retrieves the reachable states of the model.
diff --git a/src/solver/OptimizationDirection.cpp b/src/solver/OptimizationDirection.cpp
index cd88657b9..7c4691f69 100644
--- a/src/solver/OptimizationDirection.cpp
+++ b/src/solver/OptimizationDirection.cpp
@@ -31,7 +31,7 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& out, OptimizationDirection d) {
- return d == OptimizationDirection::Minimize ? out << "Minimize" : out << "Maximize";
+ return d == OptimizationDirection::Minimize ? out << "minimize" : out << "maximize";
}
}
}
diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp
index b6f73e6df..8788ce122 100644
--- a/src/solver/SymbolicGameSolver.cpp
+++ b/src/solver/SymbolicGameSolver.cpp
@@ -20,17 +20,27 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd<ValueType>()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd<ValueType>()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
+ SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
// Intentionally left empty.
}
template<storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b) const {
+ storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b) {
// Set up the environment.
storm::dd::Add<Type, ValueType> xCopy = x;
uint_fast64_t iterations = 0;
bool converged = false;
-
+
+ // Prepare some data storage in case we need to generate strategies.
+ if (generatePlayer1Strategy) {
+ player1Strategy = A.getDdManager().getBddZero();
+ }
+ boost::optional<storm::dd::Add<Type, ValueType>> previousPlayer2Values;
+ if (generatePlayer2Strategy) {
+ previousPlayer2Values = A.getDdManager().template getAddZero<ValueType>();
+ player2Strategy = A.getDdManager().getBddZero();
+ }
+
do {
// Compute tmp = A * x + b.
storm::dd::Add<Type, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
@@ -39,15 +49,50 @@ namespace storm {
// Now abstract from player 2 and player 1 variables.
if (player2Goal == storm::OptimizationDirection::Maximize) {
- tmp = tmp.maxAbstract(this->player2Variables);
+ storm::dd::Add<Type, ValueType> newValues = tmp.maxAbstract(this->player2Variables);
+
+ if (generatePlayer2Strategy) {
+ // Update only the choices that strictly improved the value.
+ storm::dd::Bdd<Type> maxChoices = tmp.maxAbstractRepresentative(this->player2Variables);
+ player2Strategy = newValues.greater(previousPlayer2Values.get()).ite(maxChoices, player2Strategy.get());
+ previousPlayer2Values = newValues;
+ }
+
+ tmp = newValues;
} else {
- tmp = (tmp + illegalPlayer2Mask).minAbstract(this->player2Variables);
+ tmp = (tmp + illegalPlayer2Mask);
+ storm::dd::Add<Type, ValueType> newValues = tmp.minAbstract(this->player2Variables);
+
+ if (generatePlayer2Strategy) {
+ player2Strategy = tmp.minAbstractRepresentative(this->player2Variables);
+ }
+
+ tmp = newValues;
}
if (player1Goal == storm::OptimizationDirection::Maximize) {
- tmp = tmp.maxAbstract(this->player1Variables);
+ tmp.exportToDot("pl1_val_" + std::to_string(iterations) + ".dot");
+ storm::dd::Add<Type, ValueType> newValues = tmp.maxAbstract(this->player1Variables);
+
+ newValues.exportToDot("pl1_valabs_" + std::to_string(iterations) + ".dot");
+ if (generatePlayer1Strategy) {
+ // Update only the choices that strictly improved the value.
+ storm::dd::Bdd<Type> maxChoices = tmp.maxAbstractRepresentative(this->player1Variables);
+ maxChoices.template toAdd<ValueType>().exportToDot("pl1_choices_" + std::to_string(iterations) + ".dot");
+ player1Strategy = newValues.greater(xCopy).ite(maxChoices, player1Strategy.get());
+ player1Strategy.get().template toAdd<ValueType>().exportToDot("pl1_" + std::to_string(iterations) + ".dot");
+ }
+
+ tmp = newValues;
} else {
- tmp = (tmp + illegalPlayer1Mask).minAbstract(this->player1Variables);
+ tmp = (tmp + illegalPlayer1Mask);
+ storm::dd::Add<Type, ValueType> newValues = tmp.minAbstract(this->player1Variables);
+
+ if (generatePlayer1Strategy) {
+ player1Strategy = tmp.minAbstractRepresentative(this->player1Variables);
+ }
+
+ tmp = newValues;
}
// Now check if the process already converged within our precision.
@@ -75,7 +120,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- void SymbolicGameSolver<Type, ValueType>::setGeneratePlayerStrategies(bool value) {
+ void SymbolicGameSolver<Type, ValueType>::setGeneratePlayersStrategies(bool value) {
setGeneratePlayer1Strategy(value);
setGeneratePlayer2Strategy(value);
}
diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h
index a6ac3c007..6ebe5d052 100644
--- a/src/solver/SymbolicGameSolver.h
+++ b/src/solver/SymbolicGameSolver.h
@@ -66,12 +66,12 @@ namespace storm {
* @param b The vector to add after matrix-vector multiplication.
* @return The solution vector.
*/
- virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b) const;
+ virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b);
// Setters that enable the generation of the players' strategies.
void setGeneratePlayer1Strategy(bool value);
void setGeneratePlayer2Strategy(bool value);
- void setGeneratePlayerStrategies(bool value);
+ void setGeneratePlayersStrategies(bool value);
// Getters to retrieve the players' strategies. Only legal if they were generated.
storm::dd::Bdd<Type> const& getPlayer1Strategy() const;
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index 6162ef7c5..db4323c6a 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -149,8 +149,7 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative");
- //return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
+ return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>
@@ -165,8 +164,7 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstractRepresentative");
- //return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
+ return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MaxAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>