From 56e70c3417e93e54c08a7901e7e707bdd5b5596a Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 13:57:18 +0100 Subject: [PATCH 01/26] setBoundedGloballyFormulasAllowed in FragmentSpecification.* --- src/storm/logic/FragmentSpecification.cpp | 10 ++++++++++ src/storm/logic/FragmentSpecification.h | 4 ++++ 2 files changed, 14 insertions(+) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 1e7e1f357..dc93f7f9c 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -68,6 +68,7 @@ namespace storm { rpatl.setUntilFormulasAllowed(true); rpatl.setGloballyFormulasAllowed(true); rpatl.setNextFormulasAllowed(true); + rpatl.setBoundedGloballyFormulasAllowed(true); return rpatl; } @@ -316,6 +317,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areBoundedGloballyFormulasAllowed() const { + return boundedGloballyFormula; + } + + FragmentSpecification& FragmentSpecification::setBoundedGloballyFormulasAllowed(bool newValue) { + this->boundedGloballyFormula = newValue; + return *this; + } + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { return atomicExpressionFormula; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 8ac56b885..f097e940f 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -52,6 +52,9 @@ namespace storm { bool areBoundedUntilFormulasAllowed() const; FragmentSpecification& setBoundedUntilFormulasAllowed(bool newValue); + bool areBoundedGloballyFormulasAllowed() const; + FragmentSpecification& setBoundedGloballyFormulasAllowed(bool newValue); + bool areAtomicExpressionFormulasAllowed() const; FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue); @@ -176,6 +179,7 @@ namespace storm { bool nextFormula; bool untilFormula; bool boundedUntilFormula; + bool boundedGloballyFormula; bool atomicExpressionFormula; bool atomicLabelFormula; From c1ab2ca8d9ade908ab1483161df120738f941274 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 14:31:30 +0100 Subject: [PATCH 02/26] created class BoundedGloballyFormula --- src/storm/logic/BoundedGloballyFormula.cpp | 28 +++++++++++++++++++ src/storm/logic/BoundedGloballyFormula.h | 25 +++++++++++++++++ src/storm/logic/Formula.cpp | 4 +++ src/storm/logic/Formula.h | 1 + src/storm/logic/FormulaVisitor.h | 1 + src/storm/logic/FormulasForwardDeclarations.h | 1 + 6 files changed, 60 insertions(+) create mode 100644 src/storm/logic/BoundedGloballyFormula.cpp create mode 100644 src/storm/logic/BoundedGloballyFormula.h diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp new file mode 100644 index 000000000..e397117ef --- /dev/null +++ b/src/storm/logic/BoundedGloballyFormula.cpp @@ -0,0 +1,28 @@ +#include "storm/logic/BoundedGloballyFormula.h" +#include "storm/logic/FormulaVisitor.h" + +namespace storm { + namespace logic { + BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { + // Intentionally left empty. + } + + bool BoundedGloballyFormula::isBoundedGloballyFormula() const { + return true; + } + + bool BoundedGloballyFormula::isProbabilityPathFormula() const { + return true; + } + + boost::any BoundedGloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const { + out << "G < "; + this->getSubformula().writeToStream(out); + return out; + } + } +} \ No newline at end of file diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h new file mode 100644 index 000000000..97f7e26fb --- /dev/null +++ b/src/storm/logic/BoundedGloballyFormula.h @@ -0,0 +1,25 @@ +#ifndef STORM_BOUNDEDGLOBALLYFORMULA_H +#define STORM_BOUNDEDGLOBALLYFORMULA_H + +#include "storm/logic/UnaryPathFormula.h" + +namespace storm { + namespace logic { + class BoundedGloballyFormula : public UnaryPathFormula { + public: + BoundedGloballyFormula(std::shared_ptr const &subformula); + + virtual ~BoundedGloballyFormula() { + // Intentionally left empty. + } + + virtual bool isBoundedGloballyFormula() const override; + virtual bool isProbabilityPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override; + virtual std::ostream &writeToStream(std::ostream &out) const override; + }; + } +} + +#endif //STORM_BOUNDEDGLOBALLYFORMULA_H diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index d8b399e34..d5359875a 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -79,6 +79,10 @@ namespace storm { return false; } + bool Formula::isBoundedGloballyFormula() const { + return false; + } + bool Formula::isGloballyFormula() const { return false; } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 294637c2e..24c288619 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -71,6 +71,7 @@ namespace storm { virtual bool isGloballyFormula() const; virtual bool isEventuallyFormula() const; virtual bool isReachabilityProbabilityFormula() const; + virtual bool isBoundedGloballyFormula() const; // Reward formulas. virtual bool isCumulativeRewardFormula() const; diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index 6bf5b8c50..23673ff50 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/src/storm/logic/FormulaVisitor.h @@ -16,6 +16,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0; diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index 2d1661418..1a6611f13 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/src/storm/logic/FormulasForwardDeclarations.h @@ -11,6 +11,7 @@ namespace storm { class BinaryPathFormula; class BinaryStateFormula; class BooleanLiteralFormula; + class BoundedGloballyFormula; class BoundedUntilFormula; class ConditionalFormula; class CumulativeRewardFormula; From c14292218229fe91a2474e84ff890833eb2a6fa3 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:12:48 +0100 Subject: [PATCH 03/26] Set up BoundedGloballyFormula to methods of Formula.* --- src/storm/logic/Formula.cpp | 17 +++++++++++++---- src/storm/logic/Formula.h | 5 ++++- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index d5359875a..70379b8ba 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -79,10 +79,6 @@ namespace storm { return false; } - bool Formula::isBoundedGloballyFormula() const { - return false; - } - bool Formula::isGloballyFormula() const { return false; } @@ -119,6 +115,10 @@ namespace storm { return false; } + bool Formula::isBoundedGloballyFormula() const { + return false; + } + bool Formula::isLongRunAverageOperatorFormula() const { return false; } @@ -377,6 +377,15 @@ namespace storm { return dynamic_cast(*this); } + // TODO: find out why these casts are not valid + BoundedGloballyFormula& Formula::asBoundedGloballyFormula() { + return dynamic_cast(*this); + } + + BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const { + return dynamic_cast(*this); + } + LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 24c288619..62aab0dde 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -173,7 +173,10 @@ namespace storm { NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; - + + BoundedGloballyFormula& asBoundedGloballyFormula(); + BoundedGloballyFormula const& asBoundedGloballyFormula() const; + LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula(); LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const; From 5030efd3639889ac5b20f96f8cb996dfc3767daf Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:13:09 +0100 Subject: [PATCH 04/26] Set up BoundedGloballyFormula to methods of FormulaInformationVisitor.* --- src/storm/logic/FormulaInformationVisitor.cpp | 4 ++++ src/storm/logic/FormulaInformationVisitor.h | 1 + 2 files changed, 5 insertions(+) diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 41976aa57..41417eeed 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -24,6 +24,10 @@ namespace storm { boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return FormulaInformation(); } + + boost::any FormulaInformationVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { FormulaInformation result; diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index 617386961..ecf5a1ab7 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/src/storm/logic/FormulaInformationVisitor.h @@ -15,6 +15,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; From 1fb1368a144cce812ac4e9b999c4d77531b57459 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:13:22 +0100 Subject: [PATCH 05/26] Set up BoundedGloballyFormula to methods of FragmentChecker.* --- src/storm/logic/FragmentChecker.cpp | 10 ++++++++++ src/storm/logic/FragmentChecker.h | 1 + 2 files changed, 11 insertions(+) diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 06772b6ba..df79d22a5 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -57,6 +57,16 @@ namespace storm { return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } + boost::any FragmentChecker::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areGloballyFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getSubformula().isPathFormula(); + } + result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; + } + boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index c6e6100ee..0b0d179aa 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/src/storm/logic/FragmentChecker.h @@ -16,6 +16,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; From 9976b927f9a6a3e9b0a6988da74e1d46e7f47046 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:14:01 +0100 Subject: [PATCH 06/26] small changes and added TODOs in class BoundedGloballyFormula --- src/storm/logic/BoundedGloballyFormula.cpp | 2 ++ src/storm/logic/BoundedGloballyFormula.h | 7 ++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp index e397117ef..f874befba 100644 --- a/src/storm/logic/BoundedGloballyFormula.cpp +++ b/src/storm/logic/BoundedGloballyFormula.cpp @@ -3,6 +3,7 @@ namespace storm { namespace logic { + // TODO: add 'k' as input to formula, maybe as TimeBound? BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { // Intentionally left empty. } @@ -21,6 +22,7 @@ namespace storm { std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const { out << "G < "; + // TODO: write "{<, <=} k" this->getSubformula().writeToStream(out); return out; } diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h index 97f7e26fb..e1fdf4592 100644 --- a/src/storm/logic/BoundedGloballyFormula.h +++ b/src/storm/logic/BoundedGloballyFormula.h @@ -1,5 +1,5 @@ -#ifndef STORM_BOUNDEDGLOBALLYFORMULA_H -#define STORM_BOUNDEDGLOBALLYFORMULA_H +#ifndef STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H +#define STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H #include "storm/logic/UnaryPathFormula.h" @@ -17,9 +17,10 @@ namespace storm { virtual bool isProbabilityPathFormula() const override; virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override; + virtual std::ostream &writeToStream(std::ostream &out) const override; }; } } -#endif //STORM_BOUNDEDGLOBALLYFORMULA_H +#endif /* STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H */ From ff8c52080800e2f9115308eb3bff090bec5c89ce Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:14:28 +0100 Subject: [PATCH 07/26] added class BoundedGloballyGameViHelper --- .../internal/BoundedGloballyGameViHelper.cpp | 169 ++++++++++++++++++ .../internal/BoundedGloballyGameViHelper.h | 79 ++++++++ 2 files changed, 248 insertions(+) create mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp create mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp new file mode 100644 index 000000000..a2be16070 --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -0,0 +1,169 @@ +#include "BoundedGloballyGameViHelper.h" + +#include "storm/environment/Environment.h" +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + +#include "storm/utility/SignalHandler.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + BoundedGloballyGameViHelper::GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + } + + template + void BoundedGloballyGameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { + _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); + _x1IsCurrent = false; + } + + template + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + prepareSolversAndMultipliersReachability(env); + // TODO: parse k from the formula + uint64_t k = 3; + _b = b; + + _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x2 = _x1; + + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + uint64_t iter = 0; + std::vector result = x; + while (iter < k) { + ++iter; + performIterationStep(env, dir); + + if (storm::utility::resources::isTerminate()) { + break; + } + } + x = xNew(); + + // TODO: do we have to do that by using boundedGlobally? + if (isProduceSchedulerSet()) { + // We will be doing one more iteration step and track scheduler choices this time. + performIterationStep(env, dir, &_producedOptimalChoices.get()); + } + } + + template + void BoundedGloballyGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + if (!_multiplier) { + prepareSolversAndMultipliersReachability(env); + } + _x1IsCurrent = !_x1IsCurrent; + + // multiplyandreducegaussseidel + // Ax + b + if (choices == nullptr) { + //STORM_LOG_DEBUG("\n" << _transitionMatrix); + //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld())); + //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b)); + //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew())); + _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); + //std::cin.get(); + } else { + // Also keep track of the choices made. + _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); + } + + // compare applyPointwise + storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { + if(storm::solver::maximize(dir)) { + if(a > b) return a; + else return b; + } else { + if(a > b) return a; + else return b; + } + }); + } + + template + void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector psiStates) + { + std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + uint bitIndex = 0; + for(uint i = 0; i < filledVector.size(); i++) { + if (psiStates.get(i)) { + filledVector.at(i) = result.at(bitIndex); + bitIndex++; + } + } + result = filledVector; + } + + template + void BoundedGloballyGameViHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + template + bool BoundedGloballyGameViHelper::isProduceSchedulerSet() const { + return _produceScheduler; + } + + template + std::vector const& BoundedGloballyGameViHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + std::vector& BoundedGloballyGameViHelper::getProducedOptimalChoices() { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + storm::storage::Scheduler BoundedGloballyGameViHelper::extractScheduler() const{ + auto const& optimalChoices = getProducedOptimalChoices(); + storm::storage::Scheduler scheduler(optimalChoices.size()); + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { + scheduler.setChoice(optimalChoices[state], state); + } + return scheduler; + } + + template + std::vector& BoundedGloballyGameViHelper::xNew() { + return _x1IsCurrent ? _x1 : _x2; + } + + template + std::vector const& BoundedGloballyGameViHelper::xNew() const { + return _x1IsCurrent ? _x1 : _x2; + } + + template + std::vector& BoundedGloballyGameViHelper::xOld() { + return _x1IsCurrent ? _x2 : _x1; + } + + template + std::vector const& BoundedGloballyGameViHelper::xOld() const { + return _x1IsCurrent ? _x2 : _x1; + } + + template class BoundedGloballyGameViHelper; +#ifdef STORM_HAVE_CARL + template class BoundedGloballyGameViHelper; +#endif + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h new file mode 100644 index 000000000..f8b079847 --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -0,0 +1,79 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" + +namespace storm { + class Environment; + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + namespace internal { + + template + class BoundedGloballyGameViHelper { + public: + BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + + void prepareSolversAndMultipliersReachability(const Environment& env); + + // TODO: add 'k' as input of the method - maybe the type TimeBound from the formula + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + + /*! + * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates + */ + void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); + + /*h + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setProduceScheduler(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isProduceSchedulerSet() const; + + storm::storage::Scheduler extractScheduler() const; + + private: + void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + + std::vector& xNew(); + std::vector const& xNew() const; + + std::vector& xOld(); + std::vector const& xOld() const; + bool _x1IsCurrent; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector const& getProducedOptimalChoices() const; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector& getProducedOptimalChoices(); + + storm::storage::SparseMatrix _transitionMatrix; + storm::storage::BitVector _statesOfCoalition; + std::vector _x1, _x2, _b; + std::unique_ptr> _multiplier; + + bool _produceScheduler = false; + boost::optional> _producedOptimalChoices; + }; + } + } + } +} From 4aee59a15a9f37085708c866ceb9d79d5087bd83 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:15:04 +0100 Subject: [PATCH 08/26] set up SparseSmgRpatlHelper for bounded globally --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 40 ++++++++++++++++++- .../rpatl/helper/SparseSmgRpatlHelper.h | 1 + 2 files changed, 40 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 779392a3e..263b131d6 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -7,7 +7,7 @@ #include "storm/utility/vector.h" #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h" - +#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h" namespace storm { namespace modelchecker { @@ -106,6 +106,44 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(x)); } + template + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + auto solverEnv = env; + solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); + + // Initialize the solution vector. + std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); + + // Relevant states are safe states - the psiStates. + storm::storage::BitVector relevantStates = psiStates; + + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(psiStates, psiStates); + + // Reduce the matrix to relevant states + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, psiStates, psiStates, false); + + storm::storage::BitVector clippedStatesOfCoalition(psiStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + clippedStatesOfCoalition.complement(); + + // here is the bounded globally game vi helper used + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); + std::unique_ptr> scheduler; + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + + viHelper.performValueIteration(env, x, b, goal.direction()); + viHelper.fillResultVector(x, psiStates); + + // TODO: i am not sure about that ~psiStates are correct - but I think (~psiStates are unsafe like the ~phiStates before) + // maybe I should create another method for this case + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~psiStates)); + } + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } + template class SparseSmgRpatlHelper; #ifdef STORM_HAVE_CARL template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 119eec84a..5c39767f7 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -39,6 +39,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); + static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); From 5ace260ecbd2f8b184a71ff3cdcaf0fe75427ecc Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 16:15:28 +0100 Subject: [PATCH 09/26] set up SparseSmgRpatlModelChecker for bounded globally --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 16 ++++++++++++++++ .../rpatl/SparseSmgRpatlModelChecker.h | 1 + 2 files changed, 17 insertions(+) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 767df179e..03d6999ef 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -116,6 +116,8 @@ namespace storm { return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula())); } else if (formula.isNextFormula()) { return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula())); + } else if (formula.isBoundedGloballyFormula()) { + return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -173,6 +175,20 @@ namespace storm { return result; } + template + std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + return result; + } + + + template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index 28b25f9e6..a27e580c5 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -39,6 +39,7 @@ namespace storm { std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; From dbc0cacb4567b358ccc4e194b13e33ab923e00ff Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:31:20 +0100 Subject: [PATCH 10/26] added bounded globally to AbstractModelChecker --- src/storm/modelchecker/AbstractModelChecker.cpp | 9 ++++++++- src/storm/modelchecker/AbstractModelChecker.h | 3 ++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index be7b14ae6..803ddc711 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -63,7 +63,9 @@ namespace storm { template std::unique_ptr AbstractModelChecker::computeProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isBoundedUntilFormula()) { + if (formula.isBoundedGloballyFormula()) { + return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula())); + } else if (formula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(env, checkTask.substituteFormula(formula.asBoundedUntilFormula())); } else if (formula.isReachabilityProbabilityFormula()) { return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula())); @@ -79,6 +81,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } + template + std::unique_ptr AbstractModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); + } + template std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 59149711c..578b83f15 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -57,12 +57,13 @@ namespace storm { // The methods to compute probabilities for path formulas. virtual std::unique_ptr computeProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask); + virtual std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask); - + // The methods to compute the rewards for path formulas. virtual std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); virtual std::unique_ptr computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); From ef415d4347985306239676bff8a6e9bfc3377d57 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:33:20 +0100 Subject: [PATCH 11/26] added needed methods to class BoundedGloballyFormula --- src/storm/logic/BoundedGloballyFormula.cpp | 260 ++++++++++++++++++++- src/storm/logic/BoundedGloballyFormula.h | 62 ++++- 2 files changed, 311 insertions(+), 11 deletions(-) diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp index f874befba..736625d4e 100644 --- a/src/storm/logic/BoundedGloballyFormula.cpp +++ b/src/storm/logic/BoundedGloballyFormula.cpp @@ -1,11 +1,34 @@ #include "storm/logic/BoundedGloballyFormula.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + #include "storm/logic/FormulaVisitor.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace logic { - // TODO: add 'k' as input to formula, maybe as TimeBound? - BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { - // Intentionally left empty. + BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : UnaryPathFormula(subformula), subformula({subformula}), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) { + STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); + } + + BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : UnaryPathFormula(subformula), subformula({subformula}), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(timeBoundReferences.size() == upperBound.size()); + assert(timeBoundReferences.size() == lowerBound.size()); + } + + // TODO handle the input for a vector of subformulas to UnaryPathFormula + BoundedGloballyFormula::BoundedGloballyFormula(std::vector> const& subformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : UnaryPathFormula(subformulas.at(0)), subformula({subformula}), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(subformula.size() == timeBoundReference.size()); + assert(timeBoundReference.size() == lowerBound.size()); + assert(lowerBound.size() == upperBound.size()); + STORM_LOG_THROW(this->getDimension() != 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one dimension."); + for (unsigned i = 0; i < timeBoundReferences.size(); ++i) { + STORM_LOG_THROW(hasLowerBound(i) || hasUpperBound(i), storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound in each dimension."); + } } bool BoundedGloballyFormula::isBoundedGloballyFormula() const { @@ -20,10 +43,237 @@ namespace storm { return visitor.visit(*this, data); } + bool BoundedGloballyFormula::isMultiDimensional() const { + assert(timeBoundReference.size() != 0); + return timeBoundReference.size() > 1; + } + + bool BoundedGloballyFormula::hasMultiDimensionalSubformulas() const { + assert(subformula.size() != 0); + return subformula.size() > 1; + } + + unsigned BoundedGloballyFormula::getDimension() const { + return timeBoundReference.size(); + } + + Formula const& BoundedGloballyFormula::getSubformula() const { + STORM_LOG_ASSERT(subformula.size() == 1, "The subformula is not unique."); + return *subformula.at(0); + } + + Formula const& BoundedGloballyFormula::getSubformula(unsigned i) const { + if (subformula.size() == 1 && i < getDimension()) { + return getSubformula(); + } else { + return *subformula.at(i); + } + } + + TimeBoundReference const& BoundedGloballyFormula::getTimeBoundReference(unsigned i) const { + assert(i < timeBoundReference.size()); + return timeBoundReference.at(i); + } + + bool BoundedGloballyFormula::isLowerBoundStrict(unsigned i) const { + assert(i < lowerBound.size()); + if (!hasLowerBound(i)) { return false; } + return lowerBound.at(i).get().isStrict(); + } + + bool BoundedGloballyFormula::hasLowerBound() const { + for(auto const& lb : lowerBound) { + if (static_cast(lb)) { + return true; + } + } + return false; + } + + bool BoundedGloballyFormula::hasLowerBound(unsigned i) const { + return static_cast(lowerBound.at(i)); + } + + bool BoundedGloballyFormula::hasIntegerLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return true; } + return lowerBound.at(i).get().getBound().hasIntegerType(); + } + + bool BoundedGloballyFormula::isUpperBoundStrict(unsigned i) const { + return upperBound.at(i).get().isStrict(); + } + + bool BoundedGloballyFormula::hasUpperBound() const { + for (auto const& ub : upperBound) { + if (static_cast(ub)) { + return true; + } + } + return false; + } + + bool BoundedGloballyFormula::hasUpperBound(unsigned i) const { + return static_cast(upperBound.at(i)); + } + + bool BoundedGloballyFormula::hasIntegerUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound().hasIntegerType(); + } + + storm::expressions::Expression const& BoundedGloballyFormula::getLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound(); + } + + storm::expressions::Expression const& BoundedGloballyFormula::getUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound(); + } + + template <> + double BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return 0.0; } + checkNoVariablesInBound(this->getLowerBound()); + double bound = this->getLowerBound(i).evaluateAsDouble(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + double BoundedGloballyFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound()); + double bound = this->getUpperBound(i).evaluateAsDouble(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + storm::RationalNumber BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return storm::utility::zero(); } + checkNoVariablesInBound(this->getLowerBound(i)); + storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + storm::RationalNumber BoundedGloballyFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + storm::RationalNumber bound = this->getUpperBound(i).evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + uint64_t BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return 0; } + checkNoVariablesInBound(this->getLowerBound(i)); + int_fast64_t bound = this->getLowerBound(i).evaluateAsInt(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return static_cast(bound); + } + + template <> + uint64_t BoundedGloballyFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + int_fast64_t bound = this->getUpperBound(i).evaluateAsInt(); + STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return static_cast(bound); + } + + template <> + double BoundedGloballyFormula::getNonStrictUpperBound(unsigned i) const { + double bound = getUpperBound(i); + STORM_LOG_THROW(!isUpperBoundStrict(i) || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + return bound; + } + + template <> + uint64_t BoundedGloballyFormula::getNonStrictUpperBound(unsigned i) const { + int_fast64_t bound = getUpperBound(i); + if (isUpperBoundStrict(i)) { + STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + return bound - 1; + } else { + return bound; + } + } + + template <> + double BoundedGloballyFormula::getNonStrictLowerBound(unsigned i) const { + double bound = getLowerBound(i); + STORM_LOG_THROW(!isLowerBoundStrict(i), storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict lower bound from strict lower-bound."); + return bound; + } + + template <> + uint64_t BoundedGloballyFormula::getNonStrictLowerBound(unsigned i) const { + int_fast64_t bound = getLowerBound(i); + if (isLowerBoundStrict(i)) { + return bound + 1; + } else { + return bound; + } + } + + void BoundedGloballyFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { + STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); + } + std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const { - out << "G < "; - // TODO: write "{<, <=} k" + out << "G" ; + if (this->isMultiDimensional()) { + out << "^{"; + } + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (i > 0) { + out << ", "; + } + if (this->getTimeBoundReference(i).isRewardBound()) { + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } else if (this->getTimeBoundReference(i).isStepBound()) { + out << "steps"; + } + if (this->hasLowerBound(i)) { + if (this->hasUpperBound(i)) { + if (this->isLowerBoundStrict(i)) { + out << "("; + } else { + out << "["; + } + out << this->getLowerBound(i); + out << ", "; + out << this->getUpperBound(i); + if (this->isUpperBoundStrict(i)) { + out << ")"; + } else { + out << "]"; + } + } else { + if (this->isLowerBoundStrict(i)) { + out << ">"; + } else { + out << ">="; + } + out << getLowerBound(i); + } + } else { + if (this->isUpperBoundStrict(i)) { + out << "<"; + } else { + out << "<="; + } + out << this->getUpperBound(i); + } + out << " "; + } + if (this->isMultiDimensional()) { + out << "}"; + } this->getSubformula().writeToStream(out); + return out; } } diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h index e1fdf4592..644bd950c 100644 --- a/src/storm/logic/BoundedGloballyFormula.h +++ b/src/storm/logic/BoundedGloballyFormula.h @@ -1,13 +1,19 @@ -#ifndef STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H -#define STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H +#pragma once + +#include #include "storm/logic/UnaryPathFormula.h" +#include "storm/logic/TimeBound.h" +#include "storm/logic/TimeBoundType.h" + namespace storm { namespace logic { class BoundedGloballyFormula : public UnaryPathFormula { public: - BoundedGloballyFormula(std::shared_ptr const &subformula); + BoundedGloballyFormula(std::shared_ptr const& subformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); + BoundedGloballyFormula(std::shared_ptr const& subformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); + BoundedGloballyFormula(std::vector> const& subformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); virtual ~BoundedGloballyFormula() { // Intentionally left empty. @@ -18,9 +24,53 @@ namespace storm { virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override; + + + bool isMultiDimensional() const; + bool hasMultiDimensionalSubformulas() const; + unsigned getDimension() const; + + Formula const& getSubformula() const; + Formula const& getSubformula(unsigned i) const; + + TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const; + + bool isLowerBoundStrict(unsigned i = 0) const; + bool hasLowerBound() const; + bool hasLowerBound(unsigned i) const; + bool hasIntegerLowerBound(unsigned i = 0) const; + + bool isUpperBoundStrict(unsigned i = 0) const; + bool hasUpperBound() const; + bool hasUpperBound(unsigned i) const; + bool hasIntegerUpperBound(unsigned i = 0) const; + + storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; + storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; + + template + ValueType getLowerBound(unsigned i = 0) const; + + template + ValueType getUpperBound(unsigned i = 0) const; + + template + ValueType getNonStrictUpperBound(unsigned i = 0) const; + + template + ValueType getNonStrictLowerBound(unsigned i = 0) const; + + + virtual std::ostream &writeToStream(std::ostream &out) const override; + + private: + static void checkNoVariablesInBound(storm::expressions::Expression const& bound); + + std::vector> subformula; + std::vector timeBoundReference; + std::vector> lowerBound; + std::vector> upperBound; }; } -} - -#endif /* STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H */ +} \ No newline at end of file From e1599efc6f2111245a4ad538ba564843ae0f56b6 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:34:19 +0100 Subject: [PATCH 12/26] added upperBound to valueIteration of BoundedGloballyGameViHelper --- .../internal/BoundedGloballyGameViHelper.cpp | 28 +++++++------------ .../internal/BoundedGloballyGameViHelper.h | 3 +- 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index a2be16070..5ad26ce62 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -13,7 +13,7 @@ namespace storm { namespace internal { template - BoundedGloballyGameViHelper::GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + BoundedGloballyGameViHelper::BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { } template @@ -23,12 +23,9 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliersReachability(env); - // TODO: parse k from the formula - uint64_t k = 3; _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x2 = _x1; @@ -40,22 +37,22 @@ namespace storm { } uint64_t iter = 0; - std::vector result = x; - while (iter < k) { + while (iter < upperBound) { ++iter; + performIterationStep(env, dir); - if (storm::utility::resources::isTerminate()) { +/* if (storm::utility::resources::isTerminate()) { break; - } + }*/ } + x = xNew(); - // TODO: do we have to do that by using boundedGlobally? - if (isProduceSchedulerSet()) { +/* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. performIterationStep(env, dir, &_producedOptimalChoices.get()); - } + }*/ } template @@ -68,12 +65,7 @@ namespace storm { // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - //STORM_LOG_DEBUG("\n" << _transitionMatrix); - //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld())); - //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b)); - //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew())); _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); - //std::cin.get(); } else { // Also keep track of the choices made. _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); @@ -94,7 +86,7 @@ namespace storm { template void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector psiStates) { - std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + std::vector filledVector = std::vector(psiStates.size(), storm::utility::zero()); uint bitIndex = 0; for(uint i = 0; i < filledVector.size(); i++) { if (psiStates.get(i)) { diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index f8b079847..413dfb56a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,8 +23,7 @@ namespace storm { void prepareSolversAndMultipliersReachability(const Environment& env); - // TODO: add 'k' as input of the method - maybe the type TimeBound from the formula - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates From 023e067c598fb55bab4ede5b663188d9f5dcce1c Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:37:50 +0100 Subject: [PATCH 13/26] added bounded globally formulas to other classes --- src/storm-parsers/parser/FormulaParser.cpp | 4 +- src/storm/logic/CloneVisitor.cpp | 28 +++++++++++ src/storm/logic/CloneVisitor.h | 1 + src/storm/logic/Formula.cpp | 1 - src/storm/logic/Formulas.h | 1 + .../LiftableTransitionRewardsVisitor.cpp | 18 +++++++ .../logic/LiftableTransitionRewardsVisitor.h | 1 + src/storm/logic/ToExpressionVisitor.cpp | 4 ++ src/storm/logic/ToExpressionVisitor.h | 1 + src/storm/storage/jani/JSONExporter.cpp | 48 +++++++++++++++++++ src/storm/storage/jani/JSONExporter.h | 1 + 11 files changed, 105 insertions(+), 3 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp index 37dad72d3..485a4bb18 100644 --- a/src/storm-parsers/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -60,7 +60,7 @@ namespace storm { storm::utility::openFile(filename, inputFileStream); std::vector properties; - + // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); @@ -70,7 +70,7 @@ namespace storm { storm::utility::closeFile(inputFileStream); throw e; } - + // Close the stream in case everything went smoothly and return result. storm::utility::closeFile(inputFileStream); return properties; diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 103c47fc0..57c8ce377 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -28,6 +28,34 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f)); } + boost::any CloneVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + if (f.hasLowerBound(i)) { + lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i))); + } else { + lowerBounds.emplace_back(); + } + if (f.hasUpperBound(i)) { + upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i))); + } else { + upperBounds.emplace_back(); + } + timeBoundReferences.push_back(f.getTimeBoundReference(i)); + } + if (f.hasMultiDimensionalSubformulas()) { + std::vector> subformulas; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + subformulas.push_back(boost::any_cast>(f.getSubformula(i).accept(*this, data))); + } + return std::static_pointer_cast(std::make_shared(subformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, lowerBounds, upperBounds, timeBoundReferences)); + } + } + boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h index 5ff29e816..61578bdca 100644 --- a/src/storm/logic/CloneVisitor.h +++ b/src/storm/logic/CloneVisitor.h @@ -16,6 +16,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 70379b8ba..b4e6c13bc 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -377,7 +377,6 @@ namespace storm { return dynamic_cast(*this); } - // TODO: find out why these casts are not valid BoundedGloballyFormula& Formula::asBoundedGloballyFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h index f054794e7..cc59b93b6 100644 --- a/src/storm/logic/Formulas.h +++ b/src/storm/logic/Formulas.h @@ -5,6 +5,7 @@ #include "storm/logic/BinaryPathFormula.h" #include "storm/logic/BinaryStateFormula.h" #include "storm/logic/BooleanLiteralFormula.h" +#include "storm/logic/BoundedGloballyFormula.h" #include "storm/logic/BoundedUntilFormula.h" #include "storm/logic/CumulativeRewardFormula.h" #include "storm/logic/EventuallyFormula.h" diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index ce17bb60e..a61dccf7c 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -30,6 +30,24 @@ namespace storm { return true; } + boost::any LiftableTransitionRewardsVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { + return false; + } + } + + bool result = true; + if (f.hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < f.getDimension(); ++i) { + result = result && boost::any_cast(f.getSubformula(i).accept(*this, data)); + } + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; + } + boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { for (unsigned i = 0; i < f.getDimension(); ++i) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h index bbac6b7c2..52a791237 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.h +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h @@ -22,6 +22,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index 8eb8444fc..1e6852d84 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -47,6 +47,10 @@ namespace storm { return result; } + boost::any ToExpressionVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h index 675dbbcba..b68b5c438 100644 --- a/src/storm/logic/ToExpressionVisitor.h +++ b/src/storm/logic/ToExpressionVisitor.h @@ -16,6 +16,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 586c81051..84b0ed3c9 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -212,6 +212,54 @@ namespace storm { ExportJsonType opDecl(f.isTrueFormula() ? true : false); return opDecl; } + boost::any FormulaToJaniJson::visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Jani export of multi-dimensional bounded globally formulas is not supported."); + ExportJsonType opDecl; + opDecl["op"] = "G"; + opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); + + bool hasStepBounds(false), hasTimeBounds(false); + std::vector rewardBounds; + + for (uint64_t i = 0; i < f.getDimension(); ++i) { + boost::optional lower, upper; + boost::optional lowerExclusive, upperExclusive; + if (f.hasLowerBound(i)) { + lower = f.getLowerBound(i); + lowerExclusive = f.isLowerBoundStrict(i); + } + if (f.hasUpperBound(i)) { + upper = f.getUpperBound(i); + upperExclusive = f.isUpperBoundStrict(i); + } + ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); + + auto tbr = f.getTimeBoundReference(i); + if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { + STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); + hasStepBounds = true; + opDecl["step-bounds"] = propertyInterval; + } else if(tbr.isRewardBound()) { + ExportJsonType rewbound; + rewbound["exp"] = buildExpression(model.getRewardModelExpression(tbr.getRewardName()), model.getConstants(), model.getGlobalVariables()); + if (tbr.hasRewardAccumulation()) { + rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName()); + } else { + rewbound["accumulate"] = constructStandardRewardAccumulation(tbr.getRewardName()); + } + rewbound["bounds"] = propertyInterval; + rewardBounds.push_back(std::move(rewbound)); + } else { + STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of globally formulas with multiple time bounds is not supported."); + hasTimeBounds = true; + opDecl["time-bounds"] = propertyInterval; + } + } + if (!rewardBounds.empty()) { + opDecl["reward-bounds"] = ExportJsonType(rewardBounds); + } + return opDecl; + } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Jani export of multi-dimensional bounded until formulas is not supported."); ExportJsonType opDecl; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 9408cff82..437c10c6c 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -52,6 +52,7 @@ namespace storm { virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const; From 66f893edcb5e68dad03c6af5e0da9206258dabad Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:39:27 +0100 Subject: [PATCH 14/26] changed globally formula grammar and added the case for bounded globally formulas for createGloballyFormula --- .../parser/FormulaParserGrammar.cpp | 17 ++++++++++++++--- src/storm-parsers/parser/FormulaParserGrammar.h | 2 +- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 7b51a552d..1be01078f 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -62,7 +62,7 @@ namespace storm { eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); - globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula = (qi::lit("G") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; globallyFormula.name("globally formula"); nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; @@ -324,8 +324,19 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { + if (timeBounds && !timeBounds.get().empty()) { + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (auto const& timeBound : timeBounds.get()) { + lowerBounds.push_back(std::get<0>(timeBound)); + upperBounds.push_back(std::get<1>(timeBound)); + timeBoundReferences.emplace_back(*std::get<2>(timeBound)); + } + return std::shared_ptr(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); + } else { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } } std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index ad76aa87f..75903d04a 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -228,7 +228,7 @@ namespace storm { std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; From 50c7a69f94830e5626490b538e2625c58a8fc9fe Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:41:14 +0100 Subject: [PATCH 15/26] added bounds to computeBoundedGlobally Probabilities and parse upperBound to the game vi helper, additional little changes --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 36 ++++++++++++++----- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- 2 files changed, 28 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 263b131d6..094f36f18 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -107,7 +107,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); @@ -117,30 +117,48 @@ namespace storm { // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(psiStates, psiStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, psiStates, psiStates, false); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, true); - storm::storage::BitVector clippedStatesOfCoalition(psiStates.getNumberOfSetBits()); - clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - // here is the bounded globally game vi helper used + // Use the bounded globally game vi helper storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); std::unique_ptr> scheduler; if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIteration(env, x, b, goal.direction()); - viHelper.fillResultVector(x, psiStates); + // TODO: the lower bounds are not used at the moment + if(lowerBound != 0) + { + STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); + } + + STORM_LOG_DEBUG("upperBound = " << upperBound); + + // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones + if(upperBound == 0) + { + x = std::vector(relevantStates.size(), storm::utility::one()); + } else { + viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); + } + + viHelper.fillResultVector(x, relevantStates); // TODO: i am not sure about that ~psiStates are correct - but I think (~psiStates are unsafe like the ~phiStates before) // maybe I should create another method for this case if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~psiStates)); + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); } + + STORM_LOG_DEBUG("x = " << x); + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 5c39767f7..e6a36f2af 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -39,7 +39,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); - static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); + static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); From 489d8a5fd2a2061421d703ad892472d1c902445c Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:42:23 +0100 Subject: [PATCH 16/26] added bounds to model checker and parse it for probability calculation of bounded globally formulas --- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 03d6999ef..774ef0014 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -182,13 +182,11 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); return result; } - - template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); From 8df4a99770d2aeb83eab97c17718ac40ac0e0ea8 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 17:54:46 +0100 Subject: [PATCH 17/26] small changes, but did not fix the bug --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 4 ++-- .../rpatl/helper/internal/BoundedGloballyGameViHelper.cpp | 4 +--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 094f36f18..7fb39bf1d 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -120,7 +120,7 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, true); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); @@ -133,7 +133,7 @@ namespace storm { viHelper.setProduceScheduler(true); } - // TODO: the lower bounds are not used at the moment + // TODO: the lower bounds are not used if(lowerBound != 0) { STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 5ad26ce62..177301730 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -36,9 +36,7 @@ namespace storm { this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } - uint64_t iter = 0; - while (iter < upperBound) { - ++iter; + for (uint64_t iter = 0; iter < upperBound; iter++) { performIterationStep(env, dir); From 64861445feb3673ea03359701612ff49ab884106 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 12:59:47 +0100 Subject: [PATCH 18/26] bug fix bounded globally --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 17 ++++++----- .../internal/BoundedGloballyGameViHelper.cpp | 30 ++++++++++++++----- .../internal/BoundedGloballyGameViHelper.h | 4 +-- 3 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 7fb39bf1d..7571a0862 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -111,14 +111,15 @@ namespace storm { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - // Initialize the solution vector. - std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + // Initialize the solution vector. + //std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); + //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + std::vector b = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -142,10 +143,12 @@ namespace storm { STORM_LOG_DEBUG("upperBound = " << upperBound); // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones - if(upperBound == 0) + if(upperBound > 0) { - x = std::vector(relevantStates.size(), storm::utility::one()); - } else { +/* x = std::vector(relevantStates.size(), storm::utility::one()); + } else {*/ + STORM_LOG_DEBUG("b = " << b); + STORM_LOG_DEBUG("x = " << x); viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 177301730..f4bfbabb2 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -19,16 +19,25 @@ namespace storm { template void BoundedGloballyGameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); +/* _x1IsCurrent = false; +*/ } template void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliersReachability(env); _b = b; +/* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); +*/ + _x1 = x; _x2 = _x1; +/* STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); @@ -37,15 +46,20 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { - performIterationStep(env, dir); +/* STORM_LOG_DEBUG("After iteration " << iter << ":"); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ /* if (storm::utility::resources::isTerminate()) { break; }*/ } +/* x = xNew(); +*/ + x = _x1; /* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. @@ -58,18 +72,18 @@ namespace storm { if (!_multiplier) { prepareSolversAndMultipliersReachability(env); } - _x1IsCurrent = !_x1IsCurrent; +/* _x1IsCurrent = !_x1IsCurrent;*/ // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, choices, &_statesOfCoalition); } - // compare applyPointwise +/* // compare applyPointwise storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { if(storm::solver::maximize(dir)) { if(a > b) return a; @@ -78,7 +92,7 @@ namespace storm { if(a > b) return a; else return b; } - }); + });*/ } template @@ -129,7 +143,7 @@ namespace storm { return scheduler; } - template +/* template std::vector& BoundedGloballyGameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; } @@ -147,7 +161,7 @@ namespace storm { template std::vector const& BoundedGloballyGameViHelper::xOld() const { return _x1IsCurrent ? _x2 : _x1; - } + }*/ template class BoundedGloballyGameViHelper; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 413dfb56a..1553d369f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -45,12 +45,12 @@ namespace storm { private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - std::vector& xNew(); +/* std::vector& xNew(); std::vector const& xNew() const; std::vector& xOld(); std::vector const& xOld() const; - bool _x1IsCurrent; + bool _x1IsCurrent;*/ /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. From 02bc7f3f694a4eb3862c8c35dff6e273b3a9e7a5 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 16:39:30 +0100 Subject: [PATCH 19/26] added assert for using lowerBounds --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 1be01078f..72a8721af 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -333,6 +333,7 @@ namespace storm { upperBounds.push_back(std::get<1>(timeBound)); timeBoundReferences.emplace_back(*std::get<2>(timeBound)); } + STORM_LOG_ASSERT(lowerBounds.size() == 0, "Lower bounds are not implemented for globally formulas."); return std::shared_ptr(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); } else { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); From 0ea549864f26b85a0cde669a1b33706abc5866bf Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 17:29:10 +0100 Subject: [PATCH 20/26] fixed assert for using lowerBounds --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 72a8721af..3a45a9682 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -329,11 +329,11 @@ namespace storm { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { + STORM_LOG_ASSERT(!std::get<0>(timeBound), "Lower bounds are not implemented for globally formulas."); lowerBounds.push_back(std::get<0>(timeBound)); upperBounds.push_back(std::get<1>(timeBound)); timeBoundReferences.emplace_back(*std::get<2>(timeBound)); } - STORM_LOG_ASSERT(lowerBounds.size() == 0, "Lower bounds are not implemented for globally formulas."); return std::shared_ptr(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); } else { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); From 5e040553a65d8da017c2b8581f03a1465c6b1ad5 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 17:32:01 +0100 Subject: [PATCH 21/26] changed error message --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 3a45a9682..9d5f0283e 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -329,7 +329,7 @@ namespace storm { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { - STORM_LOG_ASSERT(!std::get<0>(timeBound), "Lower bounds are not implemented for globally formulas."); + STORM_LOG_ASSERT(!std::get<0>(timeBound), "Cannot use lower time bounds (or intervals) in globally formulas."); lowerBounds.push_back(std::get<0>(timeBound)); upperBounds.push_back(std::get<1>(timeBound)); timeBoundReferences.emplace_back(*std::get<2>(timeBound)); From bcd67c63f743383253a6a76253f4cd15a9c0d50e Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 17:41:19 +0100 Subject: [PATCH 22/26] removed "...Reachability" from GameViHelper and BoundedGloballyGameViHelper --- .../rpatl/helper/internal/BoundedGloballyGameViHelper.cpp | 6 +++--- .../rpatl/helper/internal/BoundedGloballyGameViHelper.h | 2 +- .../modelchecker/rpatl/helper/internal/GameViHelper.cpp | 6 +++--- src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index f4bfbabb2..f40387fc0 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -17,7 +17,7 @@ namespace storm { } template - void BoundedGloballyGameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { + void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); /* _x1IsCurrent = false; @@ -26,7 +26,7 @@ namespace storm { template void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); _b = b; /* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -70,7 +70,7 @@ namespace storm { template void BoundedGloballyGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { if (!_multiplier) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); } /* _x1IsCurrent = !_x1IsCurrent;*/ diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 1553d369f..62a709f15 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -21,7 +21,7 @@ namespace storm { public: BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); - void prepareSolversAndMultipliersReachability(const Environment& env); + void prepareSolversAndMultipliers(const Environment& env); void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 8c354d945..e0fd4eee8 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -20,7 +20,7 @@ namespace storm { } template - void GameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { + void GameViHelper::prepareSolversAndMultipliers(const Environment& env) { // TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper // -> clip statesofcoalition // -> compute b vector from psiStates @@ -32,7 +32,7 @@ namespace storm { template void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; @@ -71,7 +71,7 @@ namespace storm { template void GameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { if (!_multiplier) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index d46f9049c..9e0ed3285 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -21,7 +21,7 @@ namespace storm { public: GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); - void prepareSolversAndMultipliersReachability(const Environment& env); + void prepareSolversAndMultipliers(const Environment& env); void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); From 0fd952c6f7eb5ced4beb813b98f36265c5160127 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 18:00:20 +0100 Subject: [PATCH 23/26] removed b --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 19 ++----------------- .../internal/BoundedGloballyGameViHelper.cpp | 7 +++---- .../internal/BoundedGloballyGameViHelper.h | 4 ++-- 3 files changed, 7 insertions(+), 23 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 7571a0862..c02f393d0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -115,11 +115,8 @@ namespace storm { storm::storage::BitVector relevantStates = psiStates; // Initialize the solution vector. - //std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); - //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); - std::vector b = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -134,22 +131,10 @@ namespace storm { viHelper.setProduceScheduler(true); } - // TODO: the lower bounds are not used - if(lowerBound != 0) - { - STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); - } - - STORM_LOG_DEBUG("upperBound = " << upperBound); - - // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones + // in case of upperBound = 0 the states which are initially "safe" are filled with ones if(upperBound > 0) { -/* x = std::vector(relevantStates.size(), storm::utility::one()); - } else {*/ - STORM_LOG_DEBUG("b = " << b); - STORM_LOG_DEBUG("x = " << x); - viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); + viHelper.performValueIteration(env, x, goal.direction(), upperBound); } viHelper.fillResultVector(x, relevantStates); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index f40387fc0..6e08f8277 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -25,9 +25,8 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliers(env); - _b = b; /* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); */ @@ -77,10 +76,10 @@ namespace storm { // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, choices, &_statesOfCoalition); } /* // compare applyPointwise diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 62a709f15..512031b49 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,7 +23,7 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound); + void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates @@ -66,7 +66,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2, _b; + std::vector _x1, _x2; std::unique_ptr> _multiplier; bool _produceScheduler = false; From f6829dd109be7833a54d08a0a85cf2fcffff9a27 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 18:14:49 +0100 Subject: [PATCH 24/26] clean up BoundedGloballyGameViHelper --- .../internal/BoundedGloballyGameViHelper.cpp | 66 ++----------------- .../internal/BoundedGloballyGameViHelper.h | 11 +--- .../rpatl/helper/internal/GameViHelper.h | 2 +- 3 files changed, 7 insertions(+), 72 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 6e08f8277..37a04da9c 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -19,23 +19,12 @@ namespace storm { template void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); -/* - _x1IsCurrent = false; -*/ } template void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliers(env); -/* - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); -*/ - _x1 = x; - _x2 = _x1; - -/* STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("_x1 = " << _x1); - STORM_LOG_DEBUG("_x2 = " << _x2);*/ + _x = x; if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { @@ -46,24 +35,9 @@ namespace storm { for (uint64_t iter = 0; iter < upperBound; iter++) { performIterationStep(env, dir); -/* STORM_LOG_DEBUG("After iteration " << iter << ":"); - STORM_LOG_DEBUG("_x1 = " << _x1); - STORM_LOG_DEBUG("_x2 = " << _x2);*/ - -/* if (storm::utility::resources::isTerminate()) { - break; - }*/ } -/* - x = xNew(); -*/ - x = _x1; - -/* if (isProduceSchedulerSet()) { - // We will be doing one more iteration step and track scheduler choices this time. - performIterationStep(env, dir, &_producedOptimalChoices.get()); - }*/ + x = _x; } template @@ -71,27 +45,15 @@ namespace storm { if (!_multiplier) { prepareSolversAndMultipliers(env); } -/* _x1IsCurrent = !_x1IsCurrent;*/ // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); } - -/* // compare applyPointwise - storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(storm::solver::maximize(dir)) { - if(a > b) return a; - else return b; - } else { - if(a > b) return a; - else return b; - } - });*/ } template @@ -142,26 +104,6 @@ namespace storm { return scheduler; } -/* template - std::vector& BoundedGloballyGameViHelper::xNew() { - return _x1IsCurrent ? _x1 : _x2; - } - - template - std::vector const& BoundedGloballyGameViHelper::xNew() const { - return _x1IsCurrent ? _x1 : _x2; - } - - template - std::vector& BoundedGloballyGameViHelper::xOld() { - return _x1IsCurrent ? _x2 : _x1; - } - - template - std::vector const& BoundedGloballyGameViHelper::xOld() const { - return _x1IsCurrent ? _x2 : _x1; - }*/ - template class BoundedGloballyGameViHelper; #ifdef STORM_HAVE_CARL template class BoundedGloballyGameViHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 512031b49..c13286e41 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -30,7 +30,7 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); - /*h + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ void setProduceScheduler(bool value); @@ -45,13 +45,6 @@ namespace storm { private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); -/* std::vector& xNew(); - std::vector const& xNew() const; - - std::vector& xOld(); - std::vector const& xOld() const; - bool _x1IsCurrent;*/ - /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. * @return the produced scheduler of the most recent call. @@ -66,7 +59,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2; + std::vector _x; std::unique_ptr> _multiplier; bool _produceScheduler = false; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 9e0ed3285..3a1343f90 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -30,7 +30,7 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - /*h + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ void setProduceScheduler(bool value); From 59c5aeadeab8f3212f3444bbb0847cec683df98a Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Mar 2021 18:32:23 +0100 Subject: [PATCH 25/26] changed message for boundedGloballyFormula --- src/storm/storage/jani/JSONExporter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 84b0ed3c9..7de2329b7 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -236,7 +236,7 @@ namespace storm { auto tbr = f.getTimeBoundReference(i); if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { - STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); + STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of bounded globally formulas with multiple step bounds is not supported."); hasStepBounds = true; opDecl["step-bounds"] = propertyInterval; } else if(tbr.isRewardBound()) { @@ -250,7 +250,7 @@ namespace storm { rewbound["bounds"] = propertyInterval; rewardBounds.push_back(std::move(rewbound)); } else { - STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of globally formulas with multiple time bounds is not supported."); + STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of bounded globally formulas with multiple time bounds is not supported."); hasTimeBounds = true; opDecl["time-bounds"] = propertyInterval; } From 027ed523cd7bc2a797ae7555a19b8c4e8878fe87 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 11 Mar 2021 11:49:35 +0100 Subject: [PATCH 26/26] added constrainedChoiceValues for boundedGloballyFormulas --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 14 +++++++------- .../internal/BoundedGloballyGameViHelper.cpp | 7 +++++-- .../helper/internal/BoundedGloballyGameViHelper.h | 2 +- 3 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index c02f393d0..ca6e53ea2 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -120,6 +120,8 @@ namespace storm { // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + std::vector constrainedChoiceValues = std::vector(submatrix.getRowCount(), storm::utility::zero()); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); @@ -134,17 +136,15 @@ namespace storm { // in case of upperBound = 0 the states which are initially "safe" are filled with ones if(upperBound > 0) { - viHelper.performValueIteration(env, x, goal.direction(), upperBound); + viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); +/* if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + + }*/ } viHelper.fillResultVector(x, relevantStates); - // TODO: i am not sure about that ~psiStates are correct - but I think (~psiStates are unsafe like the ~phiStates before) - // maybe I should create another method for this case - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - } - STORM_LOG_DEBUG("x = " << x); return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 37a04da9c..9a4db040e 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -22,7 +22,7 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); _x = x; @@ -34,6 +34,9 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { + if(iter == upperBound - 1) { + _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + } performIterationStep(env, dir); } @@ -47,7 +50,7 @@ namespace storm { } // multiplyandreducegaussseidel - // Ax + b + // Ax = x' if (choices == nullptr) { _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); } else { diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index c13286e41..d2eb985dc 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,7 +23,7 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); - void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound); + void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates