Grammar-Ambiguity

mCRL2's concrete syntax overloads tokens between the process algebra and the data language — most notably . (process sequential composition vs. the data "at"/indexing operator), + (process choice vs. data addition), and || (process parallel composition vs. data disjunction). Disambiguating the readings needs semantic information a context-free grammar doesn't have (the grammar alone can't tell a declared action a(1) from a data application), so merc_syntax's grammar always takes the greedier data-expression reading. In every case the misparse lands in the same place — a Condition node's condition field, the one DataExpr slot in the process grammar with no delimiter (no brackets, no [...]) bounding how far it extends, so the parser happily keeps consuming ./+/|| as data operators straight past the point where the concrete syntax actually meant to hand control back to the process algebra.

The . case: a(1) . true -> delta should parse as an unconditional action step a(1) followed by a guarded delta, but a(1) . true reads just as well as one data expression (. as the "at" operator), so that's the reading the grammar commits to:

disambiguate recognizes a as a declared action name, peels it off the At chain, and rebuilds the Sequence/Condition shape on the right.

The +/|| case is the same swallow one level up, and it compounds: (true) -> a(1) + (false) -> b(2) should be two guarded choice branches, but the parser folds the second guard straight into the first clause's then, because a(1) + (false) is itself just as valid a data expression (+ as addition) as the two Conditions the concrete syntax intended:

Note the misparse nests one Condition inside the other's then, not a top-level Binary { op: Add, .. } sitting beside it — disambiguate has to walk into an as-parsed then looking for exactly this shape before it can split it back into sibling Choice branches. P || cond -> Q (parallel composition guarding a condition) is the same bug with Disj/Parallel in place of Add/Choice. A single-action hide/block/allow application can also appear as the swallowed operand and is recovered the same way, re-attaching its action set to the rebuilt Hide/Block/Allow node.

Known limitation. ||_ (LeftMerge) has no data-operator equivalent in the grammar at all, so it can't reach this swallow through the same mechanism. comm/rename use from -> to pairs inside their set argument, and -> isn't valid DataExpr syntax, so comm (and a multi-action allow entry, a|b) fail to parse in the ambiguous position rather than being silently misparsed — rename happens to already parse correctly there (the malformed DataExpr attempt backs out, falling back to its own dedicated grammar rule) with nothing to fix.

See also Precedence: Pest (merc) vs. dparser (mCRL2) for a different, unrelated class of grammar disagreement between the two parsers — this page is about a token-overload ambiguity merc_syntax resolves itself after parsing; that one is about the two parsers disagreeing on what a single unambiguous-looking expression even means.