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

Merge branch 'master' of https://sselab.de/lab9/private/git/storm 

Conflicts:
	src/parser/PrctlParser.cpp
main
gereon 13 years ago
parent
718608622f f6196c7429
commit
62713159ba
5 changed files with 102 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/And.h
  2. 2
      src/formula/Or.h
  3. 83
      src/parser/PrctlParser.cpp
  4. 39
      test/parser/PrctlParserTest.cpp
  5. 2
      test/parser/prctl_files/complexFormula.prctl

2
src/formula/And.h
View File

@ -129,7 +129,7 @@ public:
virtual std::string toString() const {
std::string result = "(";
result += left->toString();
result += " && ";
result += " & ";
result += right->toString();
result += ")";
return result;

2
src/formula/Or.h
View File

@ -127,7 +127,7 @@ public:
virtual std::string toString() const {
std::string result = "(";
result += left->toString();
result += " || ";
result += " | ";
result += right->toString();
result += ")";
return result;

83
src/parser/PrctlParser.cpp
View File

@ -34,31 +34,38 @@ namespace parser {
template<typename Iterator, typename Skipper>
struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> {
PrctlGrammar() : PrctlGrammar::base_type(start) {
freeIdentifierName = qi::lexeme[(qi::alpha | qi::char_('_'))];
freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
//This block defines rules for parsing state formulas
stateFormula %= orFormula;
stateFormula.name("state formula");
andFormula = notFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notFormula)[qi::_val =
andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)];
orFormula = andFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andFormula)[qi::_val =
andFormula.name("state formula");
orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
phoenix::new_<storm::formula::Or<double>>(qi::_val, qi::_1)];
notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") >> atomicStateFormula)[qi::_val =
orFormula.name("state formula");
notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
phoenix::new_<storm::formula::Not<double>>(qi::_1)];
notFormula.name("state formula");
atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")");
atomicStateFormula.name("state formula");
atomicProposition = (freeIdentifierName)[qi::_val =
phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
atomicProposition.name("state formula");
probabilisticBoundOperator = (
(qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
(qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
);
probabilisticBoundOperator.name("state formula");
rewardBoundOperator = (
(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
@ -69,29 +76,39 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
);
rewardBoundOperator.name("state formula");
//This block defines rules for parsing formulas with noBoundOperators
noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
noBoundOperator.name("no bound operator");
probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::ProbabilisticNoBoundOperator<double> >(qi::_1)];
probabilisticNoBoundOperator.name("no bound operator");
rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)];
rewardNoBoundOperator.name("no bound operator");
//This block defines rules for parsing path formulas
pathFormula = (eventually | boundedEventually | globally | boundedUntil | until);
eventually = (qi::lit("F") >> stateFormula)[qi::_val =
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
boundedEventually = (qi::lit("F") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val =
pathFormula = (boundedEventually | eventually | globally | boundedUntil | until);
pathFormula.name("path formula");
boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
globally = (qi::lit("G") >> stateFormula)[qi::_val =
boundedEventually.name("path formula");
eventually = (qi::lit("F") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
eventually.name("path formula");
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 >> qi::lit("U") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val =
globally.name("path formula");
boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)];
boundedUntil.name("path formula");
until = (stateFormula >> qi::lit("U") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)];
until.name("path formula");
start = (noBoundOperator | stateFormula);
start.name("PRCTL formula");
}
qi::rule<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> start;
@ -136,7 +153,37 @@ void storm::parser::PrctlParser::parse(std::string formulaString) {
PrctlGrammar<PositionIteratorType, BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
try {
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
} catch(const qi::expectation_failure<PositionIteratorType>& e) {
// If the parser expected content different than the one provided, display information
// about the location of the error.
const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
// Construct the error message including a caret display of the position in the
// erroneous line.
std::stringstream msg;
msg << pos.file << ", line " << pos.line << ", column " << pos.column
<< ": parse error: expected " << e.what_ << std::endl << "\t"
<< e.first.get_currentline() << std::endl << "\t";
int i = 0;
for (i = 0; i < pos.column; ++i) {
msg << "-";
}
msg << "^";
for (; i < 80; ++i) {
msg << "-";
}
msg << std::endl;
std::cerr << msg.str();
// Now propagate exception.
throw storm::exceptions::WrongFileFormatException() << msg.str();
}
if (result_pointer == nullptr) {
throw storm::exceptions::WrongFileFormatException() << "Syntax error in formula";
}
formula = result_pointer;
}

39
test/parser/PrctlParserTest.cpp
View File

@ -12,15 +12,16 @@
#include "src/parser/PrctlFileParser.h"
TEST(PrctlParserTest, parseApOnlyTest) {
std::string ap = "ap";
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("P");
prctlParser = new storm::parser::PrctlParser(ap);
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "P");
ASSERT_EQ(ap, prctlParser->getFormula()->toString());
delete prctlParser->getFormula();
delete prctlParser;
@ -36,7 +37,7 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a && b) || (a && !c))");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
delete prctlFileParser->getFormula();
delete prctlFileParser;
@ -91,7 +92,7 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b & !c))]");
delete prctlFileParser->getFormula();
delete prctlFileParser;
@ -123,8 +124,36 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G P > 0.900000 [F<=7 (a && b)]] || !P < 0.400000 [G !b]))");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(P <= 0.500000 [F a] & (R > 15.000000 [G P > 0.900000 [F<=7 (a & b)]] | !P < 0.400000 [G !b]))");
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"),
storm::exceptions::WrongFileFormatException
);
delete prctlParser;
}
TEST(PrctlParserTest, wrongFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlFileParser("& a"),
storm::exceptions::WrongFileFormatException
);
delete prctlParser;
}
TEST(PrctlParserTest, wrongFormulaTest2) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlFileParser("P>0 [ F & a ]"),
storm::exceptions::WrongFileFormatException
);
delete prctlParser;
}

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

@ -1 +1 @@
(P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ]))
P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ])
Write Preview
Loading…
Cancel
Save