From 66b0817a35fe78dca1d633cad7081491fa41aa6f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 25 Aug 2016 14:53:58 +0200
Subject: [PATCH] fixed bugs here and there
Former-commit-id: d10d85339db5c28ef0bd107727f454723544132d
---
src/abstraction/AbstractionInformation.cpp | 2 +-
src/abstraction/prism/AbstractCommand.cpp | 7 +++++-
src/abstraction/prism/AbstractModule.cpp | 6 ++++-
.../abstraction/GameBasedMdpModelChecker.cpp | 23 ++++++++-----------
src/utility/graph.cpp | 12 ++++++----
5 files changed, 30 insertions(+), 20 deletions(-)
diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp
index 8e0d44def..395e23d0d 100644
--- a/src/abstraction/AbstractionInformation.cpp
+++ b/src/abstraction/AbstractionInformation.cpp
@@ -202,7 +202,7 @@ namespace storm {
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const {
storm::dd::Bdd<DdType> result = ddManager->getBddOne();
for (uint_fast64_t index = start; index < end; ++index) {
- result &= player2VariableBdds[index];
+ result &= !player2VariableBdds[index];
}
STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero.");
return result;
diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp
index a600f1792..cb46308a4 100644
--- a/src/abstraction/prism/AbstractCommand.cpp
+++ b/src/abstraction/prism/AbstractCommand.cpp
@@ -313,6 +313,11 @@ namespace storm {
BottomStateResult<DdType> AbstractCommand<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
+ // If the guard of this command is a predicate, there are not bottom states/transitions.
+ if (guardIsPredicate) {
+ return result;
+ }
+
// Use the state abstractor to compute the set of abstract states that has this command enabled but
// still has a transition to a bottom state.
bottomStateAbstractor.constrain(reachableStates && abstractGuard);
@@ -325,7 +330,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, cachedDd.numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount());
+ 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());
return result;
}
diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp
index bd2d42d32..79c144c9d 100644
--- a/src/abstraction/prism/AbstractModule.cpp
+++ b/src/abstraction/prism/AbstractModule.cpp
@@ -12,6 +12,8 @@
#include "storm-config.h"
#include "src/adapters/CarlAdapter.h"
+#include "src/utility/macros.h"
+
namespace storm {
namespace abstraction {
namespace prism {
@@ -27,7 +29,9 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void AbstractModule<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
- for (auto& command : commands) {
+ for (uint_fast64_t index = 0; index < commands.size(); ++index) {
+ STORM_LOG_TRACE("Refining command with index " << index << ".");
+ AbstractCommand<DdType, ValueType>& command = commands[index];
command.refine(predicates);
}
}
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 890614ccb..2357770af 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -195,11 +195,11 @@ 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();
+ 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.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
+ 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());
@@ -214,17 +214,19 @@ namespace storm {
storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.min.first.getPlayer1Strategy();
storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
-
+
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) {
+ STORM_LOG_TRACE("Refining based on lower choice.");
abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
} else {
storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy();
storm::dd::Bdd<Type> upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
storm::dd::Bdd<Type> upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
-
+
bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
if (upperChoicesDifferent) {
+ STORM_LOG_TRACE("Refining based on upper choice.");
abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
} else {
STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
@@ -317,13 +319,8 @@ namespace storm {
storm::dd::Bdd<Type> maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates();
storm::dd::Bdd<Type> maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates();
- maybeMin.template toAdd<ValueType>().exportToDot("maybemin.dot");
- maybeMax.template toAdd<ValueType>().exportToDot("maybemax.dot");
- game.getInitialStates().template toAdd<ValueType>().exportToDot("init.dot");
-
// 4. if the initial states are not maybe states, then we can refine at this point.
storm::dd::Bdd<Type> initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax);
- initialMaybeStates.template toAdd<ValueType>().exportToDot("initmaybe.dot");
if (initialMaybeStates.isZero()) {
// In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check.");
@@ -404,10 +401,10 @@ namespace storm {
storm::utility::graph::GameProb01Result<Type> prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize);
storm::utility::graph::GameProb01Result<Type> prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize);
- STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy.");
- STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy.");
- STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer1Strategy(), "Unable to proceed without strategy.");
- STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+ STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer1Strategy() && !prob0.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+ STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer2Strategy() && !prob0.getPlayer2Strategy().isZero()), "Unable to proceed without strategy.");
+ STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer1Strategy() && !prob1.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+ STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer2Strategy() && !prob1.getPlayer2Strategy().isZero()), "Unable to proceed without strategy.");
STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.states.getNonZeroCount() << " 'no' states, " << prob1.states.getNonZeroCount() << " 'yes' states.");
return std::make_pair(prob0, prob1);
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 5fd6b9682..9f3f9a002 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -1005,10 +1005,14 @@ namespace storm {
// If we are to produce strategies in this iteration, we prepare some storage.
if (produceStrategiesInIteration) {
- player1StrategyBdd = model.getManager().getBddZero();
- consideredPlayer1States = model.getManager().getBddZero();
- player2StrategyBdd = model.getManager().getBddZero();
- consideredPlayer2States = model.getManager().getBddZero();
+ if (player1Strategy == storm::OptimizationDirection::Maximize) {
+ player1StrategyBdd = model.getManager().getBddZero();
+ consideredPlayer1States = model.getManager().getBddZero();
+ }
+ if (player2Strategy == storm::OptimizationDirection::Maximize) {
+ player2StrategyBdd = model.getManager().getBddZero();
+ consideredPlayer2States = model.getManager().getBddZero();
+ }
}
storm::dd::Bdd<Type> solution = psiStates;