Skip to content

Parsing Error Defaulting to CHOOSE #259

Description

@sepehr541

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

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions