From 39ff3240d3f57d39b09f68bc6a636ff13df35794 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Wed, 10 Apr 2013 14:56:18 +0200
Subject: [PATCH] More convenient syntax for time bounded formulas, and
respective test cases.
---
src/formula/TimeBoundedOperator.h | 3 ++-
src/parser/CslParser.cpp | 20 ++++++++++++++++----
test/parser/CslParserTest.cpp | 16 +++++++++-------
3 files changed, 27 insertions(+), 12 deletions(-)
diff --git a/src/formula/TimeBoundedOperator.h b/src/formula/TimeBoundedOperator.h
index b14df9cbb..779d346e6 100644
--- a/src/formula/TimeBoundedOperator.h
+++ b/src/formula/TimeBoundedOperator.h
@@ -87,7 +87,8 @@ public:
virtual std::string toString() const {
std::string result = "[";
result += std::to_string(lowerBound);
- result += ";";
+ result += ",";
+ result += std::to_string(upperBound);
result += "]";
return result;
}
diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp
index 810788056..72cd2839a 100644
--- a/src/parser/CslParser.cpp
+++ b/src/parser/CslParser.cpp
@@ -100,8 +100,14 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
//This block defines rules for parsing probabilistic path formulas
pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until);
pathFormula.name("path formula");
- timeBoundedEventually = (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
- phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)];
+ timeBoundedEventually = (
+ (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
+ phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)] |
+ (qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val =
+ phoenix::new_<storm::formula::TimeBoundedEventually<double>>(0, qi::_1, qi::_2)] |
+ (qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val =
+ phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, std::numeric_limits<double>::infinity(), qi::_2)]
+ );
timeBoundedEventually.name("path formula (for probabilistic operator)");
eventually = (qi::lit("F") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
@@ -109,8 +115,14 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
globally = (qi::lit("G") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
globally.name("path formula (for probabilistic operator)");
- timeBoundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)
- [qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)];
+ timeBoundedUntil = (
+ (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)
+ [qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)] |
+ (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)
+ [qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(0, qi::_2, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)] |
+ (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)
+ [qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, std::numeric_limits<double>::infinity(), phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)]
+ );
timeBoundedUntil.name("path formula (for probabilistic operator)");
until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
diff --git a/test/parser/CslParserTest.cpp b/test/parser/CslParserTest.cpp
index 6ec438519..7b3a09cee 100644
--- a/test/parser/CslParserTest.cpp
+++ b/test/parser/CslParserTest.cpp
@@ -65,7 +65,7 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) {
TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
- cslParser = new storm::parser::CslParser("S >= 15 [ a & b ]")
+ cslParser = new storm::parser::CslParser("S >= 15 [ P < 0.2 [ a U<=3 b ] ]")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
@@ -75,7 +75,7 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
ASSERT_EQ(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
- ASSERT_EQ("S >= 15.000000 [(a & b)]", cslParser->getFormula()->toString());
+ ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString());
delete cslParser->getFormula();
delete cslParser;
@@ -100,13 +100,13 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
- cslParser = new storm::parser::CslParser("P = ? [ a U <= 4 b & (!c) ]")
+ cslParser = new storm::parser::CslParser("P = ? [ a U [3,4] b & (!c) ]")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
- ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]");
+ ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]");
delete cslParser->getFormula();
delete cslParser;
@@ -116,13 +116,15 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
TEST(CslParserTest, parseComplexFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
- cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])")
+ cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
-
- ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", cslParser->getFormula()->toString());
+ //NOTE: This test case is dependent on the string output of the double value infinity.
+ // In g++ and clang++ on Linux, it is "inf". If some compiler (or library) uses a different output, please
+ // notify me and I will restructure this test case.
+ ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F[7.000000,inf] (a & b)]]))", cslParser->getFormula()->toString());
delete cslParser->getFormula();
delete cslParser;