Merge pull request 'boundedGlobally' (#19) from next_formulae into main

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/19

src/storm-parsers/parser/FormulaParser.cpp

@@ -60,7 +60,7 @@ namespace storm {
             storm::utility::openFile(filename, inputFileStream);
             
             std::vector<storm::jani::Property> properties;
-            
+
             // Now try to parse the contents of the file.
             try {
                 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
@@ -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;

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,20 @@ namespace storm {
             }
         }
 
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            if (timeBounds && !timeBounds.get().empty()) {
+                std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
+                std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
+                for (auto const& timeBound : timeBounds.get()) {
+                    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));
+                }
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
+            }
         }
 
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -228,7 +228,7 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
             std::shared_ptr<storm::logic::Formula const> createAtomicLabelFormula(std::string const& label) const;
             std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createGloballyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
             std::shared_ptr<storm::logic::Formula const> createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
             std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
             std::shared_ptr<storm::logic::Formula const> createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const;

src/storm/logic/BoundedGloballyFormula.cpp

@@ -0,0 +1,280 @@
+#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 {
+        BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> 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<Formula const> const& subformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> const& subformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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 {
+            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);
+        }
+
+        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<bool>(lb)) {
+                    return true;
+                }
+            }
+            return false;
+        }
+
+        bool BoundedGloballyFormula::hasLowerBound(unsigned i) const {
+            return static_cast<bool>(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<bool>(ub)) {
+                    return true;
+                }
+            }
+            return false;
+        }
+
+        bool BoundedGloballyFormula::hasUpperBound(unsigned i) const {
+            return static_cast<bool>(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<storm::RationalNumber>(); }
+            checkNoVariablesInBound(this->getLowerBound(i));
+            storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational();
+            STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), 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::RationalNumber>(), 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<uint64_t>(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<uint64_t>(bound);
+        }
+
+        template <>
+        double BoundedGloballyFormula::getNonStrictUpperBound(unsigned i) const {
+            double bound = getUpperBound<double>(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<uint64_t>(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<double>(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<uint64_t>(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" ;
+            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;
+        }
+    }
+}

src/storm/logic/BoundedGloballyFormula.h

@@ -0,0 +1,76 @@
+#pragma once
+
+#include <boost/optional.hpp>
+
+#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<Formula const> const& subformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference);
+            BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
+            BoundedGloballyFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
+
+            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;
+
+
+
+            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 <typename ValueType>
+            ValueType getLowerBound(unsigned i = 0) const;
+
+            template <typename ValueType>
+            ValueType getUpperBound(unsigned i = 0) const;
+
+            template <typename ValueType>
+            ValueType getNonStrictUpperBound(unsigned i = 0) const;
+
+            template<typename ValueType>
+            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<std::shared_ptr<Formula const>> subformula;
+            std::vector<TimeBoundReference> timeBoundReference;
+            std::vector<boost::optional<TimeBound>> lowerBound;
+            std::vector<boost::optional<TimeBound>> upperBound;
+        };
+    }
+}

src/storm/logic/CloneVisitor.cpp

@@ -28,6 +28,34 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
         }
 
+        boost::any CloneVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const {
+            std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
+            std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> subformulas;
+                for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                    subformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula(i).accept(*this, data)));
+                }
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedGloballyFormula>(subformulas, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
+                std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedGloballyFormula>(subformula, lowerBounds, upperBounds, timeBoundReferences));
+            }
+        }
+
         boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
             std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
             std::vector<TimeBoundReference> timeBoundReferences;

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;

src/storm/logic/Formula.cpp

@@ -115,6 +115,10 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isBoundedGloballyFormula() const {
+            return false;
+        }
+
         bool Formula::isLongRunAverageOperatorFormula() const {
             return false;
         }
@@ -373,6 +377,14 @@ namespace storm {
             return dynamic_cast<NextFormula const&>(*this);
         }
 
+        BoundedGloballyFormula& Formula::asBoundedGloballyFormula() {
+            return dynamic_cast<BoundedGloballyFormula&>(*this);
+        }
+
+        BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const {
+            return dynamic_cast<BoundedGloballyFormula const &>(*this);
+        }
+
         LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() {
             return dynamic_cast<LongRunAverageOperatorFormula&>(*this);
         }

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;
@@ -172,7 +173,10 @@ namespace storm {
             
             NextFormula& asNextFormula();
             NextFormula const& asNextFormula() const;
-            
+
+            BoundedGloballyFormula& asBoundedGloballyFormula();
+            BoundedGloballyFormula const& asBoundedGloballyFormula() const;
+
             LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula();
             LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;
 

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;

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;

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;

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"

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;

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<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areGloballyFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getSubformula().isPathFormula();
+            }
+            result && boost::any_cast<bool>(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<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed();

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;

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;
         }

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;

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<bool>(f.getSubformula(i).accept(*this, data));
+                }
+            } else {
+                result = result && boost::any_cast<bool>(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())) {

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;

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.");
         }

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;

src/storm/modelchecker/AbstractModelChecker.cpp

@@ -63,7 +63,9 @@ namespace storm {
         template<typename ModelType>
         std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> 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<typename ModelType>
+        std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
+        }
+
         template<typename ModelType>
         std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");

src/storm/modelchecker/AbstractModelChecker.h

@@ -57,12 +57,13 @@ namespace storm {
             // The methods to compute probabilities for path formulas.
             virtual std::unique_ptr<CheckResult> computeProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask);
-            
+
             // The methods to compute the rewards for path formulas.
             virtual std::unique_ptr<CheckResult> computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask);

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,18 @@ namespace storm {
             return result;
         }
 
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> 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<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+
+            auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>());
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
+            return result;
+        }
+
         template<typename SparseSmgModelType>
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI");

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h

@@ -39,6 +39,7 @@ namespace storm {
             std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
+            std::unique_ptr<CheckResult> computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask) override;
 
             std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;

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,50 @@ namespace storm {
                 return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x));
             }
 
+            template<typename ValueType>
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> 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);
+
+                // Relevant states are safe states - the psiStates.
+                storm::storage::BitVector relevantStates = psiStates;
+
+                // Initialize the solution vector.
+                std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::one<ValueType>());
+
+                // Reduce the matrix to relevant states
+                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+
+                std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(submatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+                storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
+                clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
+                clippedStatesOfCoalition.complement();
+
+                // Use the bounded globally game vi helper
+                storm::modelchecker::helper::internal::BoundedGloballyGameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
+                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+                if (produceScheduler) {
+                    viHelper.setProduceScheduler(true);
+                }
+
+                // 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, constrainedChoiceValues);
+/*                    if (produceScheduler) {
+                        scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates));
+
+                    }*/
+                }
+
+                viHelper.fillResultVector(x, relevantStates);
+
+                STORM_LOG_DEBUG("x = " << x);
+
+                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
+            }
+
             template class SparseSmgRpatlHelper<double>;
 #ifdef STORM_HAVE_CARL
             template class SparseSmgRpatlHelper<storm::RationalNumber>;

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

@@ -39,6 +39,7 @@ namespace storm {
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> 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<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> 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<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);

src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp

@@ -0,0 +1,117 @@
+#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 <typename ValueType>
+                BoundedGloballyGameViHelper<ValueType>::BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
+                    _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
+                    prepareSolversAndMultipliers(env);
+                    _x = x;
+
+                    if (this->isProduceSchedulerSet()) {
+                        if (!this->_producedOptimalChoices.is_initialized()) {
+                            this->_producedOptimalChoices.emplace();
+                        }
+                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
+                    }
+
+                    for (uint64_t iter = 0; iter < upperBound; iter++) {
+                        if(iter == upperBound - 1) {
+                            _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues);
+                        }
+                        performIterationStep(env, dir);
+                    }
+
+                    x = _x;
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
+                    if (!_multiplier) {
+                        prepareSolversAndMultipliers(env);
+                    }
+
+                    // multiplyandreducegaussseidel
+                    // Ax = x'
+                    if (choices == nullptr) {
+                        _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition);
+                    } else {
+                        // Also keep track of the choices made.
+                        _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition);
+                    }
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates)
+                {
+                    std::vector<ValueType> filledVector = std::vector<ValueType>(psiStates.size(), storm::utility::zero<ValueType>());
+                    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 <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::setProduceScheduler(bool value) {
+                    _produceScheduler = value;
+                }
+
+                template <typename ValueType>
+                bool BoundedGloballyGameViHelper<ValueType>::isProduceSchedulerSet() const {
+                    return _produceScheduler;
+                }
+
+                template <typename ValueType>
+                std::vector<uint64_t> const& BoundedGloballyGameViHelper<ValueType>::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 <typename ValueType>
+                std::vector<uint64_t>& BoundedGloballyGameViHelper<ValueType>::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 <typename ValueType>
+                storm::storage::Scheduler<ValueType> BoundedGloballyGameViHelper<ValueType>::extractScheduler() const{
+                    auto const& optimalChoices = getProducedOptimalChoices();
+                    storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
+                    for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
+                        scheduler.setChoice(optimalChoices[state], state);
+                    }
+                    return scheduler;
+                }
+
+                template class BoundedGloballyGameViHelper<double>;
+#ifdef STORM_HAVE_CARL
+                template class BoundedGloballyGameViHelper<storm::RationalNumber>;
+#endif
+            }
+        }
+    }
+}

src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h

@@ -0,0 +1,71 @@
+#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 <typename VT> class Scheduler;
+    }
+
+    namespace modelchecker {
+        namespace helper {
+            namespace internal {
+
+                template <typename ValueType>
+                class BoundedGloballyGameViHelper {
+                public:
+                    BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
+
+                    void prepareSolversAndMultipliers(const Environment& env);
+
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
+
+                    /*!
+                     * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
+                     */
+                    void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates);
+
+                    /*!
+                     * 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<ValueType> extractScheduler() const;
+
+                private:
+                    void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+
+                    /*!
+                     * @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<uint64_t> 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<uint64_t>& getProducedOptimalChoices();
+
+                    storm::storage::SparseMatrix<ValueType> _transitionMatrix;
+                    storm::storage::BitVector _statesOfCoalition;
+                    std::vector<ValueType> _x;
+                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
+
+                    bool _produceScheduler = false;
+                    boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+                };
+            }
+        }
+    }
+}

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@@ -20,7 +20,7 @@ namespace storm {
                 }
 
                 template <typename ValueType>
-                void GameViHelper<ValueType>::prepareSolversAndMultipliersReachability(const Environment& env) {
+                void GameViHelper<ValueType>::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 <typename ValueType>
                 void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
-                    prepareSolversAndMultipliersReachability(env);
+                    prepareSolversAndMultipliers(env);
                     ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
                     uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
                     _b = b;
@@ -71,7 +71,7 @@ namespace storm {
                 template <typename ValueType>
                 void GameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
                     if (!_multiplier) {
-                        prepareSolversAndMultipliersReachability(env);
+                        prepareSolversAndMultipliers(env);
                     }
                     _x1IsCurrent = !_x1IsCurrent;
 

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -21,7 +21,7 @@ namespace storm {
                 public:
                     GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
 
-                    void prepareSolversAndMultipliersReachability(const Environment& env);
+                    void prepareSolversAndMultipliers(const Environment& env);
 
                     void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
 
@@ -30,7 +30,7 @@ namespace storm {
                      */
                     void fillResultVector(std::vector<ValueType>& 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);

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<ExportJsonType> rewardBounds;
+
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                boost::optional<storm::expressions::Expression> lower, upper;
+                boost::optional<bool> 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 bounded globally 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 bounded 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;

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;