Skip to content

Parsing Error in EXCEPT is misleading #257

Description

@sepehr541

When an undefined operator is called after the >=, the parser blames the > when it expected ].
The actual issue is the undefined operation used.

MRE

EXTENDS Sequences, Naturals
VARIABLES a

Op1(arg) == 1

Op2(result) ==
         /\ a' = [a EXCEPT !.b = Len(a') >= Op3(a)]

output:

  pgo.parser.ParseFailureError: 
  parsing failed: ']' expected but '>' found at <specFile>:9.43
            /\ a' = [a EXCEPT !.b = Len(a') >= Op3(a)]
                                            ^
    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:133)
    compiler.FooTests$.checkEqual(CompilerTests.scala:17)
    compiler.FooTests$.tests$$anonfun$1$$anonfun$18(CompilerTests.scala:387)

when Op3 is changed to Op1, which is defined, the parser behaves as expected:

EXTENDS Sequences, Naturals
VARIABLES a

Op1(arg) == 1

Op2(result) ==
         /\ a' = [a EXCEPT !.b = Len(a') >= Op1(a)]

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