-
Notifications
You must be signed in to change notification settings - Fork 20
Open
Description
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
Labels
No labels