Merge pull request 'Reenable Bounded Globally' (#49) from fix_bounded_globally into main

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

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -122,7 +122,7 @@ namespace storm {
             eventuallyFormula.name("eventually formula");
             nextFormula = (qi::lit("X") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
             nextFormula.name("next formula");
-            globallyFormula = (qi::lit("G") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
+            globallyFormula = (qi::lit("G") > (-timeBounds) > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             globallyFormula.name("globally formula");
             hoaPathFormula = qi::lit("HOA:") > qi::lit("{")
                 > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)]
@@ -409,17 +409,11 @@ 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));
@@ -429,7 +423,6 @@ namespace storm {
                 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 {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -268,8 +268,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(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> 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> createHOAPathFormula(const std::string& automataFile) const;

src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp

@@ -299,7 +299,6 @@ namespace {
         EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
     }
 
-    /*
     TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) {
         // This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound)
         std::string formulasString = " <<friendlyRobot>> Pmax=? [ G<1 !\"crash\" ]";
@@ -345,7 +344,6 @@ namespace {
         result = checker->check(this->env(), tasks[8]);
         EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
     }
-    */
 
     // TODO: create more test cases (files)
 }