-
Notifications
You must be signed in to change notification settings - Fork 20
Open
Description
When parsing the following, the parser correctly throws an error, but the error message notes that a CHOOSE expression is expected.
Not sure if there is a right default, but the essence of the issue here is the extra \, not a wrong keyword/expression.
---- MODULE Test ----
VARIABLES a
Op ==
/\\ a' = 1
==== pgo.parser.ParseFailureError:
parsing failed: 'CHOOSE' expected but '\' found at <specFile>:5.11
/\\ a' = 1
^
pgo.parser.ParseFailureError$.apply(ParsingErrors.scala:117)
pgo.parser.ParsingUtils.checkResult(ParsingUtils.scala:24)
pgo.parser.ParsingUtils.checkResult$(ParsingUtils.scala:8)
pgo.parser.TLAParser$.checkResult(TLAParser.scala:1362)
pgo.parser.TLAParser$.readModule(TLAParser.scala:1389)
compiler.Main$.parseTLAModule(Compiler.scala:154)
compiler.FooTests$.checkEqual(CompilerTests.scala:17)
compiler.FooTests$.tests$$anonfun$1$$anonfun$18(CompilerTests.scala:346)
Metadata
Metadata
Assignees
Labels
No labels