sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Some more test cases for PRCTL formula parsing

tempestpy_adaptions
Lanchid 12 years ago
parent
b66e1a34db
commit
3833c8af41
7 changed files with 84 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/formula/ProbabilisticNoBoundOperator.h
  2. 2
      src/formula/RewardNoBoundOperator.h
  3. 38
      src/parser/PrctlParser.cpp
  4. 65
      test/parser/PrctlParserTest.cpp
  5. 1
      test/parser/prctl_files/complexFormula.prctl
  6. 1
      test/parser/prctl_files/probabilisticNoBoundFormula.prctl
  7. 1
      test/parser/prctl_files/rewardNoBoundFormula.prctl

2
src/formula/ProbabilisticNoBoundOperator.h
View File

@ -69,7 +69,7 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = " P=? [";
std::string result = "P = ? [";
result += this->getPathFormula().toString();
result += "]";
return result;

2
src/formula/RewardNoBoundOperator.h
View File

@ -69,7 +69,7 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = " R=? [";
std::string result = "R = ? [";
result += this->getPathFormula().toString();
result += "]";
return result;

38
src/parser/PrctlParser.cpp
View File

@ -34,58 +34,58 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
freeIdentifierName = qi::lexeme[(qi::alpha | qi::char_('_'))];
//This block defines rules for parsing state formulas
stateFormula %= (andFormula | orFormula | notFormula | probabilisticBoundOperator | rewardBoundOperator | atomicProposition);
stateFormula = (andFormula | orFormula | notFormula | probabilisticBoundOperator | rewardBoundOperator | atomicProposition);
andFormula = (qi::lit("(") >> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[
qi::_val = phoenix::new_<storm::formula::And<double>>(qi::_1, qi::_2)];
orFormula = (qi::lit("(") >> stateFormula >> '|' >> stateFormula >> ')')[qi::_val =
orFormula = (qi::lit("(") >> stateFormula >> qi::lit("|") >> stateFormula >> qi::lit(")"))[qi::_val =
phoenix::new_<storm::formula::Or<double>>(qi::_1, qi::_2)];
notFormula = ('!' >> stateFormula)[qi::_val =
notFormula = (qi::lit("!") >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::Not<double>>(qi::_1)];
atomicProposition = (freeIdentifierName)[qi::_val =
phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
probabilisticBoundOperator = (
(qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("P") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
);
rewardBoundOperator = (
(qi::lit("R") >> qi::lit(">") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("R") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
);
//This block defines rules for parsing formulas with noBoundOperators
noBoundOperator %= (probabilisticNoBoundOperator | rewardNoBoundOperator);
probabilisticNoBoundOperator = ("P=?[" >> pathFormula >> ']')[qi::_val =
noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticNoBoundOperator<double> >(qi::_1)];
rewardNoBoundOperator = ("R=?[" >> pathFormula >> ']')[qi::_val =
rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)];
//This block defines rules for parsing path formulas
pathFormula %= (eventually | boundedEventually | globally | boundedUntil | until);
eventually = ('F' >> stateFormula)[qi::_val =
pathFormula = (eventually | boundedEventually | globally | boundedUntil | until);
eventually = (qi::lit("F") >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
boundedEventually = ("F<=" >> qi::int_ >> stateFormula)[qi::_val =
boundedEventually = (qi::lit("F") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
globally = ('G' >> stateFormula)[qi::_val =
globally = (qi::lit("G") >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
until = (stateFormula >> qi::lit("U") >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)];
boundedUntil = (stateFormula >> "U<=" >> qi::int_ >> stateFormula)[qi::_val =
boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)];
start %= (stateFormula | noBoundOperator);
start = (noBoundOperator | stateFormula);
}
qi::rule<Iterator, storm::formula::PctlFormula<double>*(), Skipper> start;

65
test/parser/PrctlParserTest.cpp
View File

@ -9,9 +9,8 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/PrctlParser.h"
#include <iostream>
TEST(PrctlParserTest, apOnly) {
TEST(PrctlParserTest, parseApOnlyTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/apOnly.prctl")
@ -22,11 +21,12 @@ TEST(PrctlParserTest, apOnly) {
ASSERT_EQ(prctlParser->getFormula()->toString(), "P");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, propositionalFormula) {
TEST(PrctlParserTest, parsePropositionalFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl")
@ -37,11 +37,12 @@ TEST(PrctlParserTest, propositionalFormula) {
ASSERT_EQ(prctlParser->getFormula()->toString(), "!(a && b)");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, probabilisticFormula) {
TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl")
@ -49,14 +50,19 @@ TEST(PrctlParserTest, probabilisticFormula) {
ASSERT_NE(prctlParser->getFormula(), nullptr);
storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlParser->getFormula());
ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER, op->getComparisonOperator());
ASSERT_EQ(0.5, op->getBound());
ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, rewardFormula) {
TEST(PrctlParserTest, parseRewardFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl")
@ -65,10 +71,59 @@ TEST(PrctlParserTest, rewardFormula) {
ASSERT_NE(prctlParser->getFormula(), nullptr);
storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlParser->getFormula());
ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [F<=42 !a]");
delete prctlParser->getFormula();
delete prctlParser;
}
TEST(PrctlParserTest, parseComplexFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G !b] || P > 0.900000 [F<=7 (a && b)]))");
delete prctlParser->getFormula();
delete prctlParser;
}

1
test/parser/prctl_files/complexFormula.prctl
View File

@ -0,0 +1 @@
(P<=0.5 [ F a ] & (R > 15 [ G !b ] | P>0.9 [F<=7 (a & b)]))

1
test/parser/prctl_files/probabilisticNoBoundFormula.prctl
View File

@ -0,0 +1 @@
P = ? [ F <= 42 !a ]

1
test/parser/prctl_files/rewardNoBoundFormula.prctl
View File

@ -0,0 +1 @@
R = ? [ a U <= 4 (b & !c) ]
Write Preview
Loading…
Cancel
Save