mCRL2
mCRL2 copied to clipboard
mCRL2org
removing the val operator from the syntax
Issue migrated from trac ticket # 1133
component: Core: Parse Library | priority: major
2013-02-15 17:44:37: @wiegerw created the issue
Currently the 'val' operator is used to disambiguate state formulas containing data expressions. This is an unnecessary complication for the user, and it should be solved by modifying the grammar and the type checker.
The problem can only partly be solved in the grammar, by adding appropriate priorities to data expressions and parenthesized expressions in action formulas, state formulas and pbes expressions (see also the attached grammar). For example:
ActFrm:
| DataExpr $right 7
| '(' ActFrm ')' $right 8
However, this introduces a problem that needs to be addressed in the type checker. In the state formula
mu X. X
the parser can/should not decide whether the X in the right hand side is a data expression or a state formula.
2016-11-17 10:24:40: @wiegerw changed component from Core: Type-checker Library to Core: Parse Library
2016-11-17 10:24:40: @wiegerw commented
This problem has been reduced to a parser problem. At the moment it cannot be solved completely, since the ability of DParser to report ambiguities seems to be only a heuristic that cannot be relied upon.
2016-11-18 14:11:27: @wiegerw commented
(In r14291) - Added an example of a modal formula that can currently not be parsed. It has to do with the ambiguity function of DParser, that unexpectedly isn't triggered.
Addresses #1135.
2016-11-18 14:25:20: @wiegerw commented
(In r14292) - Commented out the entries for data expressions without val in the syntax. In principle the current solution should work, but it relies on the DParser ambiguity function. And it turns out that this function is not guaranteed to be called. So the removal of 'val' from the syntax is still an open problem.
Addresses #1135.