From 91abc29c66fe2012c9b41b684f3fd13cf1ff7b37 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 14:43:06 +0100 Subject: [PATCH] reenabled bounded globally formulas --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 9 +-------- src/storm-parsers/parser/FormulaParserGrammar.h | 4 ++-- .../modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp | 2 -- 3 files changed, 3 insertions(+), 12 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 2aae130bd..53f3ba6c8 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/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 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()) { - 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(new storm::logic::GloballyFormula(subformula)); } } - */ std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 972f19028..6e720cea9 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -268,8 +268,8 @@ 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(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, 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 createGloballyFormula(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 createHOAPathFormula(const std::string& automataFile) const; diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index d8e9217dc..79217c614 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/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 = " <> 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) }