search

Smattr / rumur

yet another model checker
The Unlicense
16 stars 5 forks source link

begin on rules is not optional #77

Open Smattr opened 5 years ago

Smattr commented 5 years ago

The following rule should be able to be parsed, but it generates a syntax error:

rule
  x := !x;
end;
Smattr commented 5 years ago

Unsurprisingly the cause of this is an ambiguity in the grammar. Bison recognises the token x as an expression and expects ==> to follow. What is surprising is that it turns out this bug also exists in CMurphi. One of my attempts at fixing this was to make begin non-optional on simple rules, however some of the CMurphi examples actually depend on this being optional. I don't know if users coincidentally never ran into this bug or simply realised that adding begin worked around it and didn't think anymore about it.

I don't see how to resolve this in the current implementation, because it requires more than one token of lookahead which Bison does not support in the lalr1 skeleton. Ultimately it may even be preferable to use a hand written parser (yuck). Resolving this one as WONTFIX as it seems this is simply intended behaviour.

Smattr commented 5 years ago

Re-opening as this is still an issue. We may need to switch to a GLR Bison parser to resolve this.

Smattr commented 4 years ago

Just an update that this is still an open problem. Cursory attempts to switch to Bison’s GLR skeleton indicate that its C++ variant is immature. It does not support several options that we are using.