diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 6459d7a9d..faef55a4c 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -27,28 +27,28 @@ namespace storm {
unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_1)];
unaryExpression.name("unary expression");
- powerExpression = unaryExpression[qi::_val = qi::_1] >> -(qi::lit("^") > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1)];
+ powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
powerExpression.name("power expression");
- multiplicationExpression = powerExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> powerExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]);
+ multiplicationExpression = powerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
multiplicationExpression.name("multiplication expression");
- 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(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
+ plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
plusExpression.name("plus expression");
- relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
+ relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
relativeExpression.name("relative expression");
-
- 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(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&ExpressionParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
+
+ equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
equalityExpression.name("equality expression");
- andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
+ andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
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(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
+ orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
orExpression.name("or expression");
- iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+ iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
iteExpression.name("if-then-else expression");
expression %= iteExpression;
@@ -101,98 +101,14 @@ namespace storm {
return storm::expressions::Expression::createFalse();
}
}
-
- storm::expressions::Expression ExpressionParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- return e1.implies(e2);
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- return e1 || e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try{
- return e1 && e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- return e1 > e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- return e1 >= e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+
+ storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 < e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- return e1 <= e2;
- } catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
- }
- } else {
- return storm::expressions::Expression::createFalse();
- }
- }
-
- storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
- if (this->createExpressions) {
- try {
- if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
- return e1.iff(e2);
- } else {
- return e1 == e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::Or: return e1 || e2; break;
+ case storm::expressions::OperatorType::Implies: return e1.implies(e2); break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
@@ -202,10 +118,13 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 != e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::And: return e1 && e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -214,10 +133,16 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 + e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::GreaterOrEqual: return e1 >= e2; break;
+ case storm::expressions::OperatorType::Greater: return e1 > e2; break;
+ case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break;
+ case storm::expressions::OperatorType::Less: return e1 < e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -226,10 +151,14 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 - e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::Equal: return e1.hasBooleanReturnType() && e2.hasBooleanReturnType() ? e1.iff(e2) : e1 == e2; break;
+ case storm::expressions::OperatorType::NotEqual: return e1 != e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -238,10 +167,14 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 * e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::Plus: return e1 + e2; break;
+ case storm::expressions::OperatorType::Minus: return e1 - e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -250,10 +183,14 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 ^ e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::Times: return e1 * e2; break;
+ case storm::expressions::OperatorType::Divide: return e1 / e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -262,10 +199,13 @@ namespace storm {
}
}
- storm::expressions::Expression ExpressionParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+ storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
if (this->createExpressions) {
try {
- return e1 / e2;
+ switch (operatorType) {
+ case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
+ default: LOG_ASSERT(false, "Invalid operation."); break;
+ }
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
@@ -273,7 +213,7 @@ namespace storm {
return storm::expressions::Expression::createFalse();
}
}
-
+
storm::expressions::Expression ExpressionParser::createNotExpression(storm::expressions::Expression e1) const {
if (this->createExpressions) {
try {
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index 380644caf..874eba438 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -43,6 +43,83 @@ namespace storm {
void setAcceptDoubleLiterals(bool flag);
private:
+ struct orOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ orOperatorStruct() {
+ add
+ ("|", storm::expressions::OperatorType::Or)
+ ("=>", storm::expressions::OperatorType::Implies);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "or" precedence level.
+ orOperatorStruct orOperator_;
+
+ struct andOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ andOperatorStruct() {
+ add
+ ("&", storm::expressions::OperatorType::And);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "and" precedence level.
+ andOperatorStruct andOperator_;
+
+ struct equalityOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ equalityOperatorStruct() {
+ add
+ ("=", storm::expressions::OperatorType::Equal)
+ ("!=", storm::expressions::OperatorType::NotEqual);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "equality" precedence level.
+ equalityOperatorStruct equalityOperator_;
+
+ struct relationalOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ relationalOperatorStruct() {
+ add
+ (">=", storm::expressions::OperatorType::GreaterOrEqual)
+ (">", storm::expressions::OperatorType::Greater)
+ ("<=", storm::expressions::OperatorType::LessOrEqual)
+ ("<", storm::expressions::OperatorType::Less);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "relational" precedence level.
+ relationalOperatorStruct relationalOperator_;
+
+ struct plusOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ plusOperatorStruct() {
+ add
+ ("+", storm::expressions::OperatorType::Plus)
+ ("-", storm::expressions::OperatorType::Minus);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "plus" precedence level.
+ plusOperatorStruct plusOperator_;
+
+ struct multiplicationOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ multiplicationOperatorStruct() {
+ add
+ ("*", storm::expressions::OperatorType::Times)
+ ("/", storm::expressions::OperatorType::Divide);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "multiplication" precedence level.
+ multiplicationOperatorStruct multiplicationOperator_;
+
+ struct powerOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+ powerOperatorStruct() {
+ add
+ ("^", storm::expressions::OperatorType::Power);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "power" precedence level.
+ powerOperatorStruct powerOperator_;
+
// A flag that indicates whether expressions should actually be generated or just a syntax check shall be
// performed.
bool createExpressions;
@@ -80,20 +157,13 @@ namespace storm {
// Helper functions to create expressions.
storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
- storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- 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 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;
- storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createPowerExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
- storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+ storm::expressions::Expression createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
+ storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createTrueExpression() const;