[BUG] Parser error when using EXCEPT and @

[istoilkovska]

Description

Running Snowcat gives the following parse error:

Error by TLA+ parser: CrossChainValidation_draft_001.tla:366:1-375:21: Annotation error: identifier expected but '\' found E@13:00:51.300

I suspect that the following line is problematic:
packetCommitments' = [packetCommitments EXCEPT ![upcomingEvent.chain] = @ \ {upcomingEvent.packet}]

Input specification

https://github.com/informalsystems/cross-chain-validation/blob/ilina/type_annotations/tla/CrossChainValidation_draft_001.tla

The command line parameters used to run the tool

apalache-mc typecheck CrossChainValidation_draft_001.tla

Expected behavior

No parser error, because the both the Toolbox and VSCode plugin do not report parse errors.

Log files

detailed.log

13:05:52.145 [main] INFO  a.f.a.t.Tool$ - Type checking CrossChainValidation_draft_001.tla
13:05:52.487 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
13:05:52.868 [main] ERROR a.f.a.t.Tool$ - Error by TLA+ parser: CrossChainValidation_draft_001.tla:366:1-375:21: Annotation error: identifier expected but '\' found
13:05:52.870 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  0 sec
13:05:52.870 [main] INFO  a.f.a.t.Tool$ - Total time: 0.727 sec

command line output:

Type checking CrossChainValidation_draft_001.tla                  I@13:05:52.145
PASS #0: SanyParser                                               I@13:05:52.487
Parsing file /Users/ilina/repositories/informal/cross-chain-validation/tla/CrossChainValidation_draft_001.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Integers.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Sequences.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Naturals.tla
Error by TLA+ parser: CrossChainValidation_draft_001.tla:366:1-375:21: Annotation error: identifier expected but '\' found E@13:05:52.868
It took me 0 days  0 hours  0 min  0 sec                          I@13:05:52.870
Total time: 0.727 sec                                             I@13:05:52.870
EXITCODE: ERROR (99)

System information

• Apalache version: 0.15.2-SNAPSHOT build v0.15.1-4-gb68618c
• OS: Mac OS 11.2.3
• JDK version: Java SE Development Kit 1.8.0_261

[istoilkovska]

By removing line 362, which is a comment containing the symbol '@', this parse error disappears. It also disappears when the '@' in the comment is replaced by the expression for which it is a placeholder.

[konnov]

I see what is happening here. There is a piece of TLA code that contains @ and got commented. It's related to #718. We have to rework the annotation parser.

[konnov]

Yes, the annotation parser tries to treat @ \ ... as an annotation and fails. I don't think it is a good idea to ignore @ \ in this case, as we may otherwise miss a problem in a real annotation.

[konnov]

What we could do is to issue a warning instead of throwing an error.

[lemmy]

@ works great for Java, where it doesn't appear in the language. Why don't you choose a symbol other than @ for TLA+ type annotations, though - one that doesn't appear in the TLA+ language (EXCEPT or the infix operator in the TLC module)? Consider, for example, a PlusCal algorithm where an @ can appear in various places.

[konnov]

I also thought about that, but it looks like TLA+ is using almost all of the available symbols except maybe the pound sign and euro sign :-)

[lemmy]

A few of the symbols commonly found in programming languages don't often appear in TLA+: ^^type(...)

[konnov]

I am just rewriting the lexer for the annotations, so it treats @<identifier> as a single token. I guess, it will remove these weird cases in the comments.