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

Fixed the PrismParser so the exact format of PRISMs boolean expressions can now be parsed. 

Former-commit-id: bb08ec1646
tempestpy_adaptions
dehnert 11 years ago
parent
63601e0b8a
commit
39ec9401ef
4 changed files with 21 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. 36
      src/parser/PrismParser.cpp
  2. 5
      src/parser/PrismParser.h
  3. 4
      src/storage/expressions/BinaryBooleanFunctionExpression.cpp
  4. 2
      test/functional/parser/PrismParserTest.cpp

36
src/parser/PrismParser.cpp
View File

@ -88,10 +88,13 @@ namespace storm {
plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
plusExpression.name("plus expression");
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
relativeExpression.name("relative expression");
andExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("&")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And] | qi::lit("<=>")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff] | qi::lit("^")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor]) >> relativeExpression)[phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) [ qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [ phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff) [ qi::_val = phoenix::bind(&PrismParser::createIffExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createXorExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ] ];
equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
equalityExpression.name("equality expression");
andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
andExpression.name("and expression");
orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
@ -204,6 +207,7 @@ namespace storm {
qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -327,27 +331,15 @@ namespace storm {
}
}
storm::expressions::Expression PrismParser::createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1.iff(e2);
}
}
storm::expressions::Expression PrismParser::createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1 ^ e2;
}
}
storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1 == e2;
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1.iff(e2);
} else {
return e1 == e2;
}
}
}
@ -355,7 +347,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1 != e2;
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1 ^ e2;
} else {
return e1 != e2;
}
}
}

5
src/parser/PrismParser.h
View File

@ -246,8 +246,9 @@ namespace storm {
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::BinaryBooleanFunctionExpression::OperatorType>, Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
@ -277,8 +278,6 @@ namespace storm {
storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;

4
src/storage/expressions/BinaryBooleanFunctionExpression.cpp
View File

@ -90,9 +90,9 @@ namespace storm {
switch (this->getOperatorType()) {
case OperatorType::And: stream << " & "; break;
case OperatorType::Or: stream << " | "; break;
case OperatorType::Xor: stream << " ^ "; break;
case OperatorType::Xor: stream << " != "; break;
case OperatorType::Implies: stream << " => "; break;
case OperatorType::Iff: stream << " <=> "; break;
case OperatorType::Iff: stream << " = "; break;
}
stream << *this->getSecondOperand() << ")";
}

2
test/functional/parser/PrismParserTest.cpp
View File

@ -47,7 +47,7 @@ TEST(PrismParser, SimpleFullTest) {
R"(dtmc
module mod1
b : bool;
[a] true -> 1: (b'=true ^ false <=> b => false);
[a] true -> 1: (b'=true != false = b => false);
endmodule)";
storm::prism::Program result;

Write Preview
Loading…
Cancel
Save