Skip to content

Commit

Permalink
- Removed the empty regular formula 'nil' from the grammar. It was al…
Browse files Browse the repository at this point in the history 
…ready disabled for a long time

- Added some priorities to PBES expressions, and put them in a range separate from data expressions

- Fixed compile error in dparser.cpp


git-svn-id: https://svn.win.tue.nl/repos/MCRL2/trunk@13744 21252fe5-60e8-0310-8ff0-c1ae1001594e
  • Loading branch information
@wiegerw
wiegerw committed Sep 2, 2015
1 parent a601eee commit 7432cda
Show file tree
Hide file tree
Showing 3 changed files with 20 additions and 22 deletions.
2 changes: 1 addition & 1 deletion libraries/core/source/dparser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,7 @@ bool is_all_of_type(D_ParseNode* nodes[], int n, const char* type, const core::p
{
for (int i = 0; i < n; i++)
{
core::parse_node node = make_node(nodes[i], table);
core::parse_node node(nodes[i]);
if (table.symbol_name(node) != type)
{
return false;
Expand Down
39 changes: 19 additions & 20 deletions libraries/core/source/mcrl2_syntax.g
View file
Original file line number Diff line number Diff line change
Expand Up @@ -243,14 +243,14 @@ BesEqnDecl: FixedPointOperator BesVar '=' BesExpr ';' ; // Boolean fixe
BesVar: Id ; // BES variable

BesExpr
: 'true' // True
: BesVar // Boolean variable
| 'true' // True
| 'false' // False
| BesExpr ('=>' $binary_op_right 2) BesExpr // Implication
| BesExpr ('||' $binary_op_right 3) BesExpr // Disjunction
| BesExpr ('&&' $binary_op_right 4) BesExpr // Conjunction
| '!' BesExpr $unary_right 5 // Negation
| '(' BesExpr ')' // Brackets
| BesVar // Boolean variable
;

BesInit: 'init' BesVar ';' ; // Initial BES variable
Expand All @@ -274,28 +274,28 @@ PropVarInst: Id ( '(' DataExprList ')' )? ; // Instantiated

PbesInit: 'init' PropVarInst ';' ; // Initial PBES variable

DataValExpr: 'val' '(' DataExpr ')'; // Marked data expression
DataValExpr: 'val' '(' DataExpr ')' ; // Marked data expression

PbesExpr
: DataValExpr // Boolean data expression
| DataExpr // Boolean data expression
| '(' PbesExpr ')' // Brackets
| 'true' $left 20 // True
| 'false' $left 20 // False
| 'forall' VarsDeclList '.' PbesExpr $unary_right 0 // Universal quantifier
| 'exists' VarsDeclList '.' PbesExpr $unary_right 0 // Existential quantifier
| PbesExpr ('=>' $binary_op_right 2) PbesExpr // Implication
| PbesExpr ('||' $binary_op_right 3) PbesExpr // Disjunction
| PbesExpr ('&&' $binary_op_right 4) PbesExpr // Conjunction
| '!' PbesExpr $unary_right 5 // Negation
| Id ( '(' DataExprList ')' )? // Instantiated PBES variable or data application
: DataExpr // Boolean data expression
| DataValExpr $left 30 // Boolean data expression
| '(' PbesExpr ')' $left 30 // Brackets
| 'true' $left 30 // True
| 'false' $left 30 // False
| Id ( '(' DataExprList ')' )? $left 30 // Instantiated PBES variable or data application
| 'forall' VarsDeclList '.' PbesExpr $unary_right 21 // Universal quantifier
| 'exists' VarsDeclList '.' PbesExpr $unary_right 21 // Existential quantifier
| PbesExpr ('=>' $binary_op_right 22) PbesExpr // Implication
| PbesExpr ('||' $binary_op_right 23) PbesExpr // Disjunction
| PbesExpr ('&&' $binary_op_right 24) PbesExpr // Conjunction
| '!' PbesExpr $unary_right 25 // Negation
;

//--- Action formulas

ActFrm
: DataValExpr $left 30 // Boolean data expression
| DataExpr // Boolean data expression
: DataExpr // Boolean data expression
| DataValExpr $left 30 // Boolean data expression
| MultAct $left 30 // Multi-action
| '(' ActFrm ')' $left 30 // Brackets
| 'true' $left 30 // True
Expand All @@ -314,7 +314,6 @@ ActFrm
RegFrm
: ActFrm // Action formula
| '(' RegFrm ')' $left 40 // Brackets
| 'nil' $left 40 // Empty regular formula
| RegFrm ('+' $binary_op_left 31) RegFrm // Alternative composition
| RegFrm ('.' $binary_op_right 32) RegFrm // Sequential composition
| RegFrm '*' $unary_right 33 // Iteration
Expand All @@ -324,8 +323,8 @@ RegFrm
//--- State formulas

StateFrm
: DataValExpr $left 50 // Boolean data expression
| DataExpr // Boolean data expression
: DataExpr // Boolean data expression
| DataValExpr $left 50 // Boolean data expression
| '(' StateFrm ')' $left 50 // Brackets
| 'true' $left 50 // True
| 'false' $left 50 // False
Expand Down
1 change: 0 additions & 1 deletion libraries/modal_formula/include/mcrl2/modal_formula/parse.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,6 @@ struct regular_formula_actions: public action_formulas::detail::action_formula_a
regular_formulas::regular_formula parse_RegFrm(const core::parse_node& node) const
{
if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "ActFrm")) { return parse_ActFrm(node.child(0)); }
else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "nil")) { return regular_formulas::nil(); }
else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "RegFrm") && (symbol_name(node.child(2)) == ")")) { return parse_RegFrm(node.child(1)); }
else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "RegFrm") && (symbol_name(node.child(1)) == "*")) { return trans_or_nil(parse_RegFrm(node.child(0))); }
else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "RegFrm") && (symbol_name(node.child(1)) == "+")) { return trans(parse_RegFrm(node.child(0))); }
Expand Down

0 comments on commit 7432cda

Please sign in to comment.