From edbe3b19525bb78d85806b5d9bfa6c5cf9ffe86a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 24 Mar 2018 22:10:38 +0100 Subject: [PATCH] more work on explicit game solving --- ... => ExplicitQualitativeGameResultMinMax.h} | 10 +- .../abstraction/ExplicitQualitativeResult.h | 25 ++ .../ExplicitQualitativeResultMinMax.cpp | 29 ++ .../ExplicitQualitativeResultMinMax.h | 28 ++ src/storm/abstraction/QualitativeGameResult.h | 24 -- src/storm/abstraction/QualitativeMdpResult.h | 25 -- .../abstraction/QualitativeMdpResultMinMax.h | 40 --- src/storm/abstraction/QualitativeResult.cpp | 33 +++ src/storm/abstraction/QualitativeResult.h | 25 +- .../abstraction/QualitativeResultMinMax.cpp | 6 +- .../abstraction/QualitativeResultMinMax.h | 3 +- .../abstraction/QuantitativeGameResult.h | 61 ----- .../QuantitativeGameResultMinMax.h | 22 -- .../SymbolicQualitativeGameResult.cpp | 19 ++ .../SymbolicQualitativeGameResult.h | 19 ++ .../SymbolicQualitativeGameResultMinMax.cpp | 29 ++ .../SymbolicQualitativeGameResultMinMax.h | 25 ++ .../SymbolicQualitativeMdpResult.cpp | 20 ++ .../SymbolicQualitativeMdpResult.h | 23 ++ .../SymbolicQualitativeMdpResultMinMax.cpp | 29 ++ .../SymbolicQualitativeMdpResultMinMax.h | 27 ++ .../abstraction/SymbolicQualitativeResult.h | 26 ++ .../SymbolicQualitativeResultMinMax.cpp | 8 +- .../SymbolicQualitativeResultMinMax.h | 14 +- .../SymbolicQuantitativeGameResult.cpp | 61 +++++ .../SymbolicQuantitativeGameResult.h | 41 +++ .../SymbolicQuantitativeGameResultMinMax.cpp | 12 + .../SymbolicQuantitativeGameResultMinMax.h | 20 ++ .../abstraction/GameBasedMdpModelChecker.cpp | 251 ++++++++++-------- .../abstraction/GameBasedMdpModelChecker.h | 12 + .../settings/modules/AbstractionSettings.cpp | 4 +- .../settings/modules/AbstractionSettings.h | 2 +- src/storm/storage/dd/Add.cpp | 6 +- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 27 +- src/storm/storage/dd/cudd/InternalCuddAdd.h | 22 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 29 +- .../storage/dd/sylvan/InternalSylvanAdd.h | 23 +- src/storm/utility/graph.cpp | 16 +- src/storm/utility/graph.h | 12 +- src/test/storm/utility/GraphTest.cpp | 6 +- 40 files changed, 749 insertions(+), 365 deletions(-) rename src/storm/abstraction/{QualitativeGameResultMinMax.h => ExplicitQualitativeGameResultMinMax.h} (85%) create mode 100644 src/storm/abstraction/ExplicitQualitativeResult.h create mode 100644 src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp create mode 100644 src/storm/abstraction/ExplicitQualitativeResultMinMax.h delete mode 100644 src/storm/abstraction/QualitativeGameResult.h delete mode 100644 src/storm/abstraction/QualitativeMdpResult.h delete mode 100644 src/storm/abstraction/QualitativeMdpResultMinMax.h delete mode 100644 src/storm/abstraction/QuantitativeGameResult.h delete mode 100644 src/storm/abstraction/QuantitativeGameResultMinMax.h create mode 100644 src/storm/abstraction/SymbolicQualitativeGameResult.cpp create mode 100644 src/storm/abstraction/SymbolicQualitativeGameResult.h create mode 100644 src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp create mode 100644 src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h create mode 100644 src/storm/abstraction/SymbolicQualitativeMdpResult.cpp create mode 100644 src/storm/abstraction/SymbolicQualitativeMdpResult.h create mode 100644 src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp create mode 100644 src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h create mode 100644 src/storm/abstraction/SymbolicQualitativeResult.h create mode 100644 src/storm/abstraction/SymbolicQuantitativeGameResult.cpp create mode 100644 src/storm/abstraction/SymbolicQuantitativeGameResult.h create mode 100644 src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp create mode 100644 src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h diff --git a/src/storm/abstraction/QualitativeGameResultMinMax.h b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h similarity index 85% rename from src/storm/abstraction/QualitativeGameResultMinMax.h rename to src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h index c40338185..7764c3383 100644 --- a/src/storm/abstraction/QualitativeGameResultMinMax.h +++ b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h @@ -7,11 +7,10 @@ namespace storm { namespace abstraction { - - template - class QualitativeGameResultMinMax : public SymbolicQualitativeResultMinMax { + + class ExplicitQualitativeGameResultMinMax : public QualitativeResultMinMax { public: - QualitativeGameResultMinMax() = default; + ExplicitQualitativeGameResultMinMax() = default; virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override { if (dir == storm::OptimizationDirection::Minimize) { @@ -34,6 +33,7 @@ namespace storm { QualitativeGameResult prob0Max; QualitativeGameResult prob1Max; }; - + } } + diff --git a/src/storm/abstraction/ExplicitQualitativeResult.h b/src/storm/abstraction/ExplicitQualitativeResult.h new file mode 100644 index 000000000..8f8e6a151 --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeResult.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/QualitativeResult.h" + +namespace storm { + namespace storage { + class BitVector; + } + + namespace abstraction { + + class ExplicitQualitativeResult : public QualitativeResult { + public: + virtual ~ExplicitQualitativeResult() = default; + + virtual storm::storage::BitVector const& getStates() const = 0; + }; + + } +} + + + diff --git a/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp b/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp new file mode 100644 index 000000000..8d3a630f2 --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp @@ -0,0 +1,29 @@ +#include "storm/abstraction/ExplicitQualitativeResultMinMax.h" + +#include "storm/abstraction/ExplicitQualitativeResult.h" + +namespace storm { + namespace abstraction { + + bool ExplicitQualitativeResultMinMax::isExplicit() const { + return true; + } + + ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb0Min() const { + return getProb0(storm::OptimizationDirection::Minimize); + } + + ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb1Min() const { + return getProb1(storm::OptimizationDirection::Minimize); + } + + ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb0Max() const { + return getProb0(storm::OptimizationDirection::Maximize); + } + + ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb1Max() const { + return getProb1(storm::OptimizationDirection::Maximize); + } + + } +} diff --git a/src/storm/abstraction/ExplicitQualitativeResultMinMax.h b/src/storm/abstraction/ExplicitQualitativeResultMinMax.h new file mode 100644 index 000000000..2eabe123b --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeResultMinMax.h @@ -0,0 +1,28 @@ +#pragma once + +#include "storm/solver/OptimizationDirection.h" + +#include "storm/abstraction/QualitativeResultMinMax.h" + +namespace storm { + namespace abstraction { + class ExplicitQualitativeResult; + + class ExplicitQualitativeResultMinMax : public QualitativeResultMinMax { + public: + ExplicitQualitativeResultMinMax() = default; + + virtual bool isExplicit() const override; + + ExplicitQualitativeResult const& getProb0Min() const; + ExplicitQualitativeResult const& getProb1Min() const; + ExplicitQualitativeResult const& getProb0Max() const; + ExplicitQualitativeResult const& getProb1Max() const; + + virtual ExplicitQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; + virtual ExplicitQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + }; + + } +} + diff --git a/src/storm/abstraction/QualitativeGameResult.h b/src/storm/abstraction/QualitativeGameResult.h deleted file mode 100644 index ff3c6e44c..000000000 --- a/src/storm/abstraction/QualitativeGameResult.h +++ /dev/null @@ -1,24 +0,0 @@ -#pragma once - -#include "storm/utility/graph.h" -#include "storm/abstraction/QualitativeResult.h" - -namespace storm { - namespace abstraction { - - template - struct QualitativeGameResult : public storm::utility::graph::GameProb01Result, public QualitativeResult { - QualitativeGameResult() = default; - - QualitativeGameResult(storm::utility::graph::GameProb01Result const& prob01Result) : storm::utility::graph::GameProb01Result(prob01Result) { - // Intentionally left empty. - } - - virtual storm::dd::Bdd const& getStates() const override { - return this->getPlayer1States(); - } - - }; - - } -} diff --git a/src/storm/abstraction/QualitativeMdpResult.h b/src/storm/abstraction/QualitativeMdpResult.h deleted file mode 100644 index 9fc1fcc0e..000000000 --- a/src/storm/abstraction/QualitativeMdpResult.h +++ /dev/null @@ -1,25 +0,0 @@ -#pragma once - -#include "storm/abstraction/QualitativeResult.h" - -namespace storm { - namespace abstraction { - - template - struct QualitativeMdpResult : public QualitativeResult { - QualitativeMdpResult() = default; - - QualitativeMdpResult(storm::dd::Bdd const& states) : states(states) { - // Intentionally left empty. - } - - virtual storm::dd::Bdd const& getStates() const override { - return states; - } - - storm::dd::Bdd states; - }; - - } -} - diff --git a/src/storm/abstraction/QualitativeMdpResultMinMax.h b/src/storm/abstraction/QualitativeMdpResultMinMax.h deleted file mode 100644 index 9f2a3c130..000000000 --- a/src/storm/abstraction/QualitativeMdpResultMinMax.h +++ /dev/null @@ -1,40 +0,0 @@ -#pragma once - -#include "storm/storage/dd/DdType.h" - -#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" -#include "storm/abstraction/QualitativeMdpResult.h" - -namespace storm { - namespace abstraction { - - template - class QualitativeMdpResultMinMax : public SymbolicQualitativeResultMinMax { - public: - QualitativeMdpResultMinMax() = default; - - virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override { - if (dir == storm::OptimizationDirection::Minimize) { - return prob0Min; - } else { - return prob0Max; - } - } - - virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override { - if (dir == storm::OptimizationDirection::Minimize) { - return prob1Min; - } else { - return prob1Max; - } - } - - QualitativeMdpResult prob0Min; - QualitativeMdpResult prob1Min; - QualitativeMdpResult prob0Max; - QualitativeMdpResult prob1Max; - }; - - } -} - diff --git a/src/storm/abstraction/QualitativeResult.cpp b/src/storm/abstraction/QualitativeResult.cpp index 68a50d1e5..968b34894 100644 --- a/src/storm/abstraction/QualitativeResult.cpp +++ b/src/storm/abstraction/QualitativeResult.cpp @@ -1,3 +1,36 @@ #include "storm/abstraction/QualitativeResult.h" +#include "storm/abstraction/SymbolicQualitativeResult.h" +#include "storm/abstraction/ExplicitQualitativeResult.h" +namespace storm { + namespace abstraction { + + bool QualitativeResult::isSymbolic() const { + return false; + } + + bool QualitativeResult::isExplicit() const { + return false; + } + + template + SymbolicQualitativeResult& QualitativeResult::asSymbolicQualitativeResult() { + return static_cast&>(*this); + } + + template + SymbolicQualitativeResult const& QualitativeResult::asSymbolicQualitativeResult() const { + return static_cast const&>(*this); + } + + ExplicitQualitativeResult& QualitativeResult::asExplicitQualitativeResult() { + return static_cast(*this); + } + + ExplicitQualitativeResult const& QualitativeResult::asExplicitQualitativeResult() const { + return static_cast(*this); + } + + } +} diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h index 0d027b3a7..c7eafdc01 100644 --- a/src/storm/abstraction/QualitativeResult.h +++ b/src/storm/abstraction/QualitativeResult.h @@ -3,22 +3,29 @@ #include "storm/storage/dd/DdType.h" namespace storm { - namespace dd { - template - class Bdd; - } - namespace abstraction { - template + template + class SymbolicQualitativeResult; + + class ExplicitQualitativeResult; + class QualitativeResult { public: virtual ~QualitativeResult() = default; + + virtual bool isSymbolic() const; + virtual bool isExplicit() const; + + template + SymbolicQualitativeResult& asSymbolicQualitativeResult(); + template + SymbolicQualitativeResult const& asSymbolicQualitativeResult() const; + + ExplicitQualitativeResult& asExplicitQualitativeResult(); + ExplicitQualitativeResult const& asExplicitQualitativeResult() const; - virtual storm::dd::Bdd const& getStates() const = 0; }; } } - - diff --git a/src/storm/abstraction/QualitativeResultMinMax.cpp b/src/storm/abstraction/QualitativeResultMinMax.cpp index 95465172c..28eee28b1 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.cpp +++ b/src/storm/abstraction/QualitativeResultMinMax.cpp @@ -8,7 +8,11 @@ namespace storm { bool QualitativeResultMinMax::isSymbolic() const { return false; } - + + bool QualitativeResultMinMax::isExplicit() const { + return false; + } + template SymbolicQualitativeResultMinMax const& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() const { return static_cast const&>(*this); diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeResultMinMax.h index b6aa96382..3f789eca7 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.h +++ b/src/storm/abstraction/QualitativeResultMinMax.h @@ -13,7 +13,8 @@ namespace storm { virtual ~QualitativeResultMinMax() = default; virtual bool isSymbolic() const; - + virtual bool isExplicit() const; + template SymbolicQualitativeResultMinMax const& asSymbolicQualitativeResultMinMax() const; diff --git a/src/storm/abstraction/QuantitativeGameResult.h b/src/storm/abstraction/QuantitativeGameResult.h deleted file mode 100644 index 2d76a8618..000000000 --- a/src/storm/abstraction/QuantitativeGameResult.h +++ /dev/null @@ -1,61 +0,0 @@ -#pragma once - -#include "storm/storage/dd/DdType.h" -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/Bdd.h" - -namespace storm { - namespace abstraction { - - template - struct QuantitativeGameResult { - QuantitativeGameResult() = default; - - QuantitativeGameResult(storm::dd::Add const& values) : values(values) { - // Intentionally left empty. - } - - QuantitativeGameResult(boost::optional> const& initialStatesRange, storm::dd::Add const& values, boost::optional> const& player1Strategy, boost::optional> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { - // Intentionally left empty. - } - - bool hasPlayer1Strategy() const { - return static_cast(player1Strategy); - } - - storm::dd::Bdd const& getPlayer1Strategy() const { - return player1Strategy.get(); - } - - storm::dd::Bdd& getPlayer1Strategy() { - return player1Strategy.get(); - } - - bool hasPlayer2Strategy() const { - return static_cast(player2Strategy); - } - - storm::dd::Bdd const& getPlayer2Strategy() const { - return player2Strategy.get(); - } - - storm::dd::Bdd& getPlayer2Strategy() { - return player2Strategy.get(); - } - - bool hasInitialStatesRange() const { - return static_cast(initialStatesRange); - } - - std::pair const& getInitialStatesRange() const { - return initialStatesRange.get(); - } - - boost::optional> initialStatesRange; - storm::dd::Add values; - boost::optional> player1Strategy; - boost::optional> player2Strategy; - }; - - } -} diff --git a/src/storm/abstraction/QuantitativeGameResultMinMax.h b/src/storm/abstraction/QuantitativeGameResultMinMax.h deleted file mode 100644 index c88c014f3..000000000 --- a/src/storm/abstraction/QuantitativeGameResultMinMax.h +++ /dev/null @@ -1,22 +0,0 @@ -#pragma once - -#include "storm/abstraction/QuantitativeGameResult.h" - -namespace storm { - namespace abstraction { - - template - class QuantitativeGameResultMinMax { - public: - QuantitativeGameResultMinMax() = default; - - QuantitativeGameResultMinMax(QuantitativeGameResult const& min, QuantitativeGameResult const& max) : min(min), max(max) { - // Intentionally left empty. - } - - QuantitativeGameResult min; - QuantitativeGameResult max; - }; - - } -} diff --git a/src/storm/abstraction/SymbolicQualitativeGameResult.cpp b/src/storm/abstraction/SymbolicQualitativeGameResult.cpp new file mode 100644 index 000000000..0dfae3145 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeGameResult.cpp @@ -0,0 +1,19 @@ +#include "storm/abstraction/SymbolicQualitativeGameResult.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQualitativeGameResult::SymbolicQualitativeGameResult(storm::utility::graph::SymbolicGameProb01Result const& prob01Result) : storm::utility::graph::SymbolicGameProb01Result(prob01Result) { + // Intentionally left empty. + } + + template + storm::dd::Bdd const& SymbolicQualitativeGameResult::getStates() const { + return this->getPlayer1States(); + } + + template class SymbolicQualitativeGameResult; + template class SymbolicQualitativeGameResult; + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeGameResult.h b/src/storm/abstraction/SymbolicQualitativeGameResult.h new file mode 100644 index 000000000..2daea6ae6 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeGameResult.h @@ -0,0 +1,19 @@ +#pragma once + +#include "storm/utility/graph.h" +#include "storm/abstraction/SymbolicQualitativeResult.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQualitativeGameResult : public storm::utility::graph::SymbolicGameProb01Result, public SymbolicQualitativeResult { + SymbolicQualitativeGameResult() = default; + + SymbolicQualitativeGameResult(storm::utility::graph::SymbolicGameProb01Result const& prob01Result); + + virtual storm::dd::Bdd const& getStates() const override; + }; + + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp new file mode 100644 index 000000000..5a9d34ab5 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp @@ -0,0 +1,29 @@ +#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQualitativeResult const& SymbolicQualitativeGameResultMinMax::getProb0(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + template + SymbolicQualitativeResult const& SymbolicQualitativeGameResultMinMax::getProb1(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } + + template class SymbolicQualitativeResultMinMax; + template class SymbolicQualitativeResultMinMax; + + } +} + diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h new file mode 100644 index 000000000..beeadd0b0 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQualitativeGameResultMinMax : public SymbolicQualitativeResultMinMax { + public: + SymbolicQualitativeGameResultMinMax() = default; + + virtual SymbolicQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override; + virtual SymbolicQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override; + + SymbolicQualitativeResult prob0Min; + SymbolicQualitativeResult prob1Min; + SymbolicQualitativeResult prob0Max; + SymbolicQualitativeResult prob1Max; + }; + + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResult.cpp b/src/storm/abstraction/SymbolicQualitativeMdpResult.cpp new file mode 100644 index 000000000..418047333 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeMdpResult.cpp @@ -0,0 +1,20 @@ +#include "storm/abstraction/SymbolicQualitativeMdpResult.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQualitativeMdpResult::SymbolicQualitativeMdpResult(storm::dd::Bdd const& states) : states(states) { + // Intentionally left empty. + } + + template + storm::dd::Bdd const& SymbolicQualitativeMdpResult::getStates() const { + return states; + } + + template class SymbolicQualitativeMdpResult; + template class SymbolicQualitativeMdpResult; + + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResult.h b/src/storm/abstraction/SymbolicQualitativeMdpResult.h new file mode 100644 index 000000000..ee44a942e --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeMdpResult.h @@ -0,0 +1,23 @@ +#pragma once + +#include "storm/abstraction/SymbolicQualitativeResult.h" + +#include "storm/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQualitativeMdpResult : public SymbolicQualitativeResult { + SymbolicQualitativeMdpResult() = default; + + SymbolicQualitativeMdpResult(storm::dd::Bdd const& states); + + virtual storm::dd::Bdd const& getStates() const override; + + storm::dd::Bdd states; + }; + + } +} + diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp new file mode 100644 index 000000000..87b6f504f --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp @@ -0,0 +1,29 @@ +#include "storm/abstraction/SymbolicQualitativeMdpResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQualitativeResult const& SymbolicQualitativeMdpResultMinMax::getProb0(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + template + SymbolicQualitativeResult const& SymbolicQualitativeMdpResultMinMax::getProb1(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } + + template class SymbolicQualitativeMdpResultMinMax; + template class SymbolicQualitativeMdpResultMinMax; + + } +} + diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h new file mode 100644 index 000000000..554e0bd3d --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h @@ -0,0 +1,27 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeMdpResult.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQualitativeMdpResultMinMax : public SymbolicQualitativeResultMinMax { + public: + SymbolicQualitativeMdpResultMinMax() = default; + + virtual SymbolicQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override; + virtual SymbolicQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override; + + SymbolicQualitativeMdpResult prob0Min; + SymbolicQualitativeMdpResult prob1Min; + SymbolicQualitativeMdpResult prob0Max; + SymbolicQualitativeMdpResult prob1Max; + }; + + } +} + diff --git a/src/storm/abstraction/SymbolicQualitativeResult.h b/src/storm/abstraction/SymbolicQualitativeResult.h new file mode 100644 index 000000000..7703a1033 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeResult.h @@ -0,0 +1,26 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/QualitativeResult.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace abstraction { + + template + class SymbolicQualitativeResult : public QualitativeResult { + public: + virtual ~SymbolicQualitativeResult() = default; + + virtual storm::dd::Bdd const& getStates() const = 0; + }; + + } +} + + diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp index 772ee645d..51dff167a 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp @@ -11,22 +11,22 @@ namespace storm { } template - QualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Min() const { + SymbolicQualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Min() const { return getProb0(storm::OptimizationDirection::Minimize); } template - QualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Min() const { + SymbolicQualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Min() const { return getProb1(storm::OptimizationDirection::Minimize); } template - QualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Max() const { + SymbolicQualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Max() const { return getProb0(storm::OptimizationDirection::Maximize); } template - QualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Max() const { + SymbolicQualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Max() const { return getProb1(storm::OptimizationDirection::Maximize); } diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h index 8b9be7e23..fe4d21bf2 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h @@ -14,7 +14,7 @@ namespace storm { namespace abstraction { template - class QualitativeResult; + class SymbolicQualitativeResult; template class SymbolicQualitativeResultMinMax : public QualitativeResultMinMax { @@ -23,13 +23,13 @@ namespace storm { virtual bool isSymbolic() const override; - QualitativeResult const& getProb0Min() const; - QualitativeResult const& getProb1Min() const; - QualitativeResult const& getProb0Max() const; - QualitativeResult const& getProb1Max() const; + SymbolicQualitativeResult const& getProb0Min() const; + SymbolicQualitativeResult const& getProb1Min() const; + SymbolicQualitativeResult const& getProb0Max() const; + SymbolicQualitativeResult const& getProb1Max() const; - virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; - virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + virtual SymbolicQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; + virtual SymbolicQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; }; } } diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp b/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp new file mode 100644 index 000000000..9c91b1b97 --- /dev/null +++ b/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp @@ -0,0 +1,61 @@ +#include "storm/abstraction/SymbolicQuantitativeGameResult.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQuantitativeGameResult::SymbolicQuantitativeGameResult(storm::dd::Add const& values) : values(values) { + // Intentionally left empty. + } + + template + SymbolicQuantitativeGameResult::SymbolicQuantitativeGameResult(boost::optional> const& initialStatesRange, storm::dd::Add const& values, boost::optional> const& player1Strategy, boost::optional> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + // Intentionally left empty. + } + + template + bool SymbolicQuantitativeGameResult::hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + template + storm::dd::Bdd const& SymbolicQuantitativeGameResult::getPlayer1Strategy() const { + return player1Strategy.get(); + } + + template + storm::dd::Bdd& SymbolicQuantitativeGameResult::getPlayer1Strategy() { + return player1Strategy.get(); + } + + template + bool SymbolicQuantitativeGameResult::hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + template + storm::dd::Bdd const& SymbolicQuantitativeGameResult::getPlayer2Strategy() const { + return player2Strategy.get(); + } + + template + storm::dd::Bdd& SymbolicQuantitativeGameResult::getPlayer2Strategy() { + return player2Strategy.get(); + } + + template + bool SymbolicQuantitativeGameResult::hasInitialStatesRange() const { + return static_cast(initialStatesRange); + } + + template + std::pair const& SymbolicQuantitativeGameResult::getInitialStatesRange() const { + return initialStatesRange.get(); + } + + template class SymbolicQuantitativeGameResult; + template class SymbolicQuantitativeGameResult; + + } +} + diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResult.h b/src/storm/abstraction/SymbolicQuantitativeGameResult.h new file mode 100644 index 000000000..b9dc7eaa2 --- /dev/null +++ b/src/storm/abstraction/SymbolicQuantitativeGameResult.h @@ -0,0 +1,41 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQuantitativeGameResult { + public: + SymbolicQuantitativeGameResult() = default; + + SymbolicQuantitativeGameResult(storm::dd::Add const& values); + SymbolicQuantitativeGameResult(boost::optional> const& initialStatesRange, storm::dd::Add const& values, boost::optional> const& player1Strategy, boost::optional> const& player2Strategy); + + bool hasPlayer1Strategy() const; + + storm::dd::Bdd const& getPlayer1Strategy() const; + + storm::dd::Bdd& getPlayer1Strategy(); + + bool hasPlayer2Strategy() const; + + storm::dd::Bdd const& getPlayer2Strategy() const; + + storm::dd::Bdd& getPlayer2Strategy(); + + bool hasInitialStatesRange() const; + + std::pair const& getInitialStatesRange() const; + + boost::optional> initialStatesRange; + storm::dd::Add values; + boost::optional> player1Strategy; + boost::optional> player2Strategy; + }; + + } +} diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp new file mode 100644 index 000000000..08be6fad6 --- /dev/null +++ b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp @@ -0,0 +1,12 @@ +#include "storm/abstraction/SymbolicQuantitativeGameResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + SymbolicQuantitativeGameResultMinMax::SymbolicQuantitativeGameResultMinMax(SymbolicQuantitativeGameResult const& min, SymbolicQuantitativeGameResult const& max) : min(min), max(max) { + // Intentionally left empty. + } + + } +} diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h new file mode 100644 index 000000000..32ec71ce3 --- /dev/null +++ b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h @@ -0,0 +1,20 @@ +#pragma once + +#include "storm/abstraction/SymbolicQuantitativeGameResult.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicQuantitativeGameResultMinMax { + public: + SymbolicQuantitativeGameResultMinMax() = default; + + SymbolicQuantitativeGameResultMinMax(SymbolicQuantitativeGameResult const& min, SymbolicQuantitativeGameResult const& max); + + SymbolicQuantitativeGameResult min; + SymbolicQuantitativeGameResult max; + }; + + } +} diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ac3250f19..6ba963c63 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -367,8 +367,7 @@ namespace storm { auto abstractionEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); - // (2) Prepare transition matrix BDD and target state BDD for later use. - storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states."); storm::dd::Bdd constraintStates = globalConstraintStates && game.getReachableStates(); @@ -383,117 +382,18 @@ namespace storm { // game.getReachableStates().template toAdd().exportToDot("reach.dot"); // #endif - // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). - auto qualitativeStart = std::chrono::high_resolution_clock::now(); - QualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); + std::unique_ptr result; + if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) { + result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousQualitativeResult, previousMinQuantitativeResult); + } else { + result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner); + } + if (result) { printStatistics(*abstractor, game); return result; } - previousQualitativeResult = qualitativeResult; - auto qualitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); - // (4) compute the states for which we have to determine quantitative information. - storm::dd::Bdd maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates(); - storm::dd::Bdd maybeMax = !(qualitativeResult.prob0Max.getPlayer1States() || qualitativeResult.prob1Max.getPlayer1States()) && game.getReachableStates(); - - // (5) if the initial states are not maybe states, then we can refine at this point. - storm::dd::Bdd initialMaybeStates = (initialStates && maybeMin) || (initialStates && maybeMax); - bool qualitativeRefinement = false; - 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."); - - STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); - - // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) - // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); - qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); - auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); - } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) { - // If all initial states are 'maybe' states and the property we needed to check is a qualitative one, - // we can return the result here. - return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); - } - - // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. - if (!qualitativeRefinement) { - // At this point, we know that we cannot answer the query without further numeric computation. - STORM_LOG_TRACE("Starting numerical solution step."); - - // Solve abstraction using the selected mode. - if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) { - STORM_LOG_TRACE("Using dd-based solving."); - storm::dd::Add initialStatesAdd = initialStates.template toAdd(); - - auto quantitativeStart = std::chrono::high_resolution_clock::now(); - - QuantitativeGameResultMinMax quantitativeResult; - - // (7) Solve the min values and check whether we can give the answer already. - quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); - previousMinQuantitativeResult = quantitativeResult.min; - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); - if (result) { - printStatistics(*abstractor, game); - return result; - } - - // (8) Solve the max values and check whether we can give the answer already. - quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); - if (result) { - printStatistics(*abstractor, game); - return result; - } - - auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); - - // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. - result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); - if (result) { - printStatistics(*abstractor, game); - return result; - } - - // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); - - auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); - // (10) 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. - refiner.refine(game, transitionMatrixBdd, quantitativeResult); - auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); - } else { - STORM_LOG_TRACE("Using hybrid solving."); - - auto relevantStates = maybeMin || maybeMax || targetStates; - auto relevantStatesAdd = relevantStates.template toAdd(); - storm::dd::Odd odd = relevantStates.createOdd(); - - auto relevantStatesTransitionMatrix = game.getTransitionMatrix() * relevantStatesAdd * relevantStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); - std::pair, std::vector> transitionMatrixLabeling = relevantStatesTransitionMatrix.toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true); - auto const& transitionMatrix = transitionMatrixLabeling.first; - auto const& labeling = transitionMatrixLabeling.second; - - std::cout << transitionMatrix << std::endl; - for (auto const& e : labeling) { - std::cout << e << std::endl; - } - - exit(-1); - } - - } auto iterationEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); } @@ -502,6 +402,141 @@ namespace storm { return nullptr; } + template + std::unique_ptr GameBasedMdpModelChecker::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult) { + + STORM_LOG_TRACE("Using dd-based solving."); + + // Prepare transition matrix BDD. + storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + + // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). + auto qualitativeStart = std::chrono::high_resolution_clock::now(); + QualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); + if (result) { + return result; + } + previousQualitativeResult = qualitativeResult; + auto qualitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); + + // (2) compute the states for which we have to determine quantitative information. + storm::dd::Bdd maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates(); + storm::dd::Bdd maybeMax = !(qualitativeResult.prob0Max.getPlayer1States() || qualitativeResult.prob1Max.getPlayer1States()) && game.getReachableStates(); + + // (3) if the initial states are not maybe states, then we can refine at this point. + storm::dd::Bdd initialMaybeStates = (initialStates && maybeMin) || (initialStates && maybeMax); + bool qualitativeRefinement = false; + 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."); + + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) + // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); + qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); + auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); + } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) { + // If all initial states are 'maybe' states and the property we needed to check is a qualitative one, + // we can return the result here. + return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + } + + // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. + if (!qualitativeRefinement) { + // At this point, we know that we cannot answer the query without further numeric computation. + STORM_LOG_TRACE("Starting numerical solution step."); + + STORM_LOG_TRACE("Using dd-based solving."); + storm::dd::Add initialStatesAdd = initialStates.template toAdd(); + + auto quantitativeStart = std::chrono::high_resolution_clock::now(); + + QuantitativeGameResultMinMax quantitativeResult; + + // (7) Solve the min values and check whether we can give the answer already. + quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); + previousMinQuantitativeResult = quantitativeResult.min; + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); + if (result) { + return result; + } + + // (8) Solve the max values and check whether we can give the answer already. + quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); + if (result) { + return result; + } + + auto quantitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + + // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. + result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); + if (result) { + return result; + } + + // Make sure that all strategies are still valid strategies. + STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + + auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); + + // (10) 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. + refiner.refine(game, transitionMatrixBdd, quantitativeResult); + auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + } + + // Return null to indicate no result has been found yet. + return nullptr; + } + + template + std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner) { + STORM_LOG_TRACE("Using hybrid solving."); + + // (0) Start by transforming the necessary symbolic elements to explicit ones. + storm::dd::Odd odd = game.getReachableStates().createOdd(); + + std::pair, std::vector> transitionMatrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true); + auto const& transitionMatrix = transitionMatrixAndLabeling.first; + auto const& labeling = transitionMatrixAndLabeling.second; + + storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); + storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd); + storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd); + + // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). + auto qualitativeStart = std::chrono::high_resolution_clock::now(); + ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(game, player1Direction, transitionMatrix, constraintStates, targetStates); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); + if (result) { + return result; + } + auto qualitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); + + + + std::cout << transitionMatrix << std::endl; + std::cout << labeling.size() << std::endl; + std::cout << initialStates << std::endl; + std::cout << constraintStates << std::endl; + std::cout << targetStates << std::endl; + + exit(-1); + } + template std::vector GameBasedMdpModelChecker::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { std::vector initialPredicates; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index dd6c7cb2f..8556edc71 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -27,6 +27,15 @@ namespace storm { template class MenuGameAbstractor; + + template + class MenuGameRefiner; + + template + class QualitativeGameResultMinMax; + + template + struct QuantitativeGameResult; } namespace modelchecker { @@ -59,6 +68,9 @@ namespace storm { */ std::unique_ptr performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); + std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner); + /*! * Retrieves the initial predicates for the abstraction. */ diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 947b7b7ca..455cb7da8 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -44,7 +44,7 @@ namespace storm { .setDefaultValueString("all").build()) .build()); - std::vector solveModes = {"dd", "hybrid"}; + std::vector solveModes = {"dd", "sparse"}; this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(solveModes)) .setDefaultValueString("dd").build()) @@ -110,7 +110,7 @@ namespace storm { if (solveModeAsString == "dd") { return SolveMode::Dd; } - return SolveMode::Hybrid; + return SolveMode::Sparse; } bool AbstractionSettings::isAddAllGuardsSet() const { diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 2b361b273..f8b2e5c93 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -28,7 +28,7 @@ namespace storm { }; enum class SolveMode { - Dd, Hybrid + Dd, Sparse }; /*! diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 80b707639..75552108e 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -810,13 +810,11 @@ namespace storm { } statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd(); - statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); - if (buildLabeling) { uint64_t currentLabel = groupLabels[i]; - std::cout << "current label is " << currentLabel << std::endl; - // statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; }); + statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &labeling] (uint64_t const& offset, uint_fast64_t const& value) { labeling[rowGroupIndices[offset]] = currentLabel; }); } + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } // Since we modified the rowGroupIndices, we need to restore the correct values. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 6e5a57e4a..9ed21a92a 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -494,16 +494,24 @@ namespace storm { template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector] (uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); }); + } + + template + void InternalAdd::forEach(Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const { + forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function); } template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(this->getCuddDdNode(), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector, &offsets] (uint64_t const& offset, ValueType const& value) { + ValueType& targetValue = targetVector[offsets[offset]]; + targetValue = function(targetValue, value); + }); } template - void InternalAdd::composeWithExplicitVectorRec(DdNode const* dd, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + void InternalAdd::forEachRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { return; @@ -511,24 +519,22 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentLevel == maxLevel) { - ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset]; - targetValue = function(targetValue, storm::utility::convertNumber(Cudd_V(dd))); + function(currentOffset, storm::utility::convertNumber(Cudd_V(dd))); } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. - composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function); + forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. - composeWithExplicitVectorRec(Cudd_E_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(Cudd_T_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + forEachRec(Cudd_E_const(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function); + forEachRec(Cudd_T_const(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function); } } template std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const { std::vector result; - std::cout << ddLabelVariableIndices << std::endl; decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0); return result; } @@ -546,7 +552,6 @@ namespace storm { uint64_t elseLabel = label; uint64_t thenLabel = label; - std::cout << "currentLevel " << currentLevel << " is in labels? " << ddLabelVariableIndices.get(currentLevel) << std::endl; if (ddLabelVariableIndices.get(currentLevel)) { elseLabel <<= 1; thenLabel = (thenLabel << 1) | 1; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index cab873353..e5af927e8 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -549,6 +549,18 @@ namespace storm { */ void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + /*! + * Composes the ADD with an explicit vector by performing a specified function between the entries of this + * ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ + void forEach(Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const; + /*! * Composes the (row-grouped) ADD with an explicit vector by performing a specified function between the * entries of this ADD and the explicit vector. @@ -646,18 +658,18 @@ namespace storm { private: /*! - * Performs a recursive step to perform the given function between the given DD-based vector and the given - * explicit vector. + * Performs a recursive step for forEach. * - * @param dd The DD to add to the explicit vector. + * @param dd The DD to traverse. * @param currentLevel The currently considered level in the DD. * @param maxLevel The number of levels that need to be considered. * @param currentOffset The current offset. * @param odd The ODD used for the translation. * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. + * @param function The callback invoked for every element. The first argument is the offset and the second + * is the value. */ - void composeWithExplicitVectorRec(DdNode const* dd, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + void forEachRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const; /*! * Splits the given matrix DD into the groups using the given group variables. diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 96dcbcc75..fc0829f22 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -884,16 +884,24 @@ namespace storm { template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector] (uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); }); } template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector, &offsets] (uint64_t const& offset, ValueType const& value) { + ValueType& targetValue = targetVector[offsets[offset]]; + targetValue = function(targetValue, value); + }); } template - void InternalAdd::composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + void InternalAdd::forEach(Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const { + forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function); + } + + template + void InternalAdd::forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const { // For the empty DD, we do not need to add any entries. if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) { return; @@ -901,24 +909,19 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentLevel == maxLevel) { - ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset]; - targetValue = function(targetValue, getValue(dd)); + function(currentOffset, getValue(dd)); } else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. - composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function); + forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. MTBDD thenNode = mtbdd_gethigh(dd); MTBDD elseNode = mtbdd_getlow(dd); - // Determine whether we have to evaluate the successors as if they were complemented. - bool elseComplemented = mtbdd_hascomp(elseNode) ^ negated; - bool thenComplemented = mtbdd_hascomp(thenNode) ^ negated; - - composeWithExplicitVectorRec(mtbdd_regular(elseNode), elseComplemented, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(mtbdd_regular(thenNode), thenComplemented, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + forEachRec(elseNode, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function); + forEachRec(thenNode, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function); } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 449ba0bbc..ccdc61414 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -553,6 +553,18 @@ namespace storm { */ void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const; + /*! + * Composes the ADD with an explicit vector by performing a specified function between the entries of this + * ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ + void forEach(Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const; + /*! * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices). * @@ -647,19 +659,18 @@ namespace storm { static std::shared_ptr createOddRec(BDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels); /*! - * Performs a recursive step to perform the given function between the given DD-based vector and the given - * explicit vector. + * Performs a recursive step for forEach. * - * @param dd The DD to add to the explicit vector. - * @param negated A flag indicating whether the DD node is to be interpreted as being negated. + * @param dd The DD to traverse. * @param currentLevel The currently considered level in the DD. * @param maxLevel The number of levels that need to be considered. * @param currentOffset The current offset. * @param odd The ODD used for the translation. * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. + * @param function The callback invoked for every element. The first argument is the offset and the second + * is the value. */ - void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + void forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const; /*! * Splits the given matrix DD into the labelings of the gropus using the given group variables. diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 5bb8cc758..c720483fc 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1084,7 +1084,7 @@ namespace storm { } template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { + SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // The solution sets. storm::dd::Bdd player1States = psiStates; @@ -1147,11 +1147,11 @@ namespace storm { player1StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables()); } - return GameProb01Result(player1States, player2States, player1StrategyBdd, player2StrategyBdd); + return SymbolicGameProb01Result(player1States, player2States, player1StrategyBdd, player2StrategyBdd); } template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates) { + SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates) { // Create the potential prob1 states of player 1. storm::dd::Bdd maybePlayer1States = model.getReachableStates(); @@ -1284,7 +1284,7 @@ namespace storm { } } - return GameProb01Result(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd); + return SymbolicGameProb01Result(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd); } template @@ -1568,9 +1568,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); + template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); // Instantiations for Sylvan (double). @@ -1608,9 +1608,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); + template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); // Instantiations for Sylvan (rational number). diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 79103700b..cff5887fc 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -10,7 +10,9 @@ #include "storm/storage/Scheduler.h" #include "storm/models/sparse/NondeterministicModel.h" #include "storm/models/sparse/DeterministicModel.h" + #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Bdd.h" #include "storm/solver/OptimizationDirection.h" @@ -542,9 +544,9 @@ namespace storm { std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template - struct GameProb01Result { - GameProb01Result() = default; - GameProb01Result(storm::dd::Bdd const& player1States, storm::dd::Bdd const& player2States, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + struct SymbolicGameProb01Result { + SymbolicGameProb01Result() = default; + SymbolicGameProb01Result(storm::dd::Bdd const& player1States, storm::dd::Bdd const& player2States, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { // Intentionally left empty. } @@ -597,7 +599,7 @@ namespace storm { * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); + SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -611,7 +613,7 @@ namespace storm { * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. */ template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional> const& player1Candidates = boost::none); + SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional> const& player1Candidates = boost::none); /*! * Performs a topological sort of the states of the system according to the given transitions. diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp index ac646d99a..b3a7c6ef4 100644 --- a/src/test/storm/utility/GraphTest.cpp +++ b/src/test/storm/utility/GraphTest.cpp @@ -227,7 +227,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + storm::utility::graph::SymbolicGameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -366,7 +366,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2. storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && game.getReachableStates(); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + storm::utility::graph::SymbolicGameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); ASSERT_TRUE(result.hasPlayer1Strategy()); ASSERT_TRUE(result.hasPlayer2Strategy()); @@ -538,7 +538,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { // The target states are those states where col == 2. storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates(); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); + storm::utility::graph::SymbolicGameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy());