[BUG] Type annotations in MC_*.tla files

[istoilkovska]

Description

I have a module, let's call it Spec.tla and a module MC_Spec.tla which instantiates Spec.tla. I would like to use MC_Spec.tla to run model checking with Apalache. The variables in both modules are annotated, and so are the constants in Spec.tla. Most of the annotations use type aliases, which are defined in a third module, Spec_Definitions.tla. Running the type checker on Spec.tla says that the types are great, but on MC_Spec.tla, it complains that an already annotated operator is undefined.

Input specification

IBCCore.tla
MC_IBCCore.tla

The command line parameters used to run the tool

 apalache-mc typecheck IBCCore.tla

and

 apalache-mc typecheck MC_IBCCore.tla

Expected behavior

No errors for MC_IBCCore.tla.

Log files

apalache-mc typecheck IBCCore.tla

• detailed.log

17:15:13.458 [main] INFO  a.f.a.t.Tool$ - Type checking IBCCore.tla
17:15:13.766 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
17:15:15.376 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
17:15:15.377 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
17:15:15.377 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
17:15:15.507 [main] DEBUG a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > JSON output: /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/x/17.15-20.04.2021-5746884103650158326/out-pre-TypeCheckerSnowcat.json
17:15:18.443 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are great!
17:15:18.443 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
17:15:18.827 [main] DEBUG a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > JSON output: /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/x/17.15-20.04.2021-5746884103650158326/out-post-TypeCheckerSnowcat.json
17:15:18.828 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
17:15:18.829 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: Terminal
17:15:18.829 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: Terminal [OK]
17:15:18.829 [main] INFO  a.f.a.t.Tool$ - Type checker [OK]
17:15:18.830 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  5 sec
17:15:18.831 [main] INFO  a.f.a.t.Tool$ - Total time: 5.375 sec

• command line output:

Type checking IBCCore.tla                                         I@17:15:13.458
PASS #0: SanyParser                                               I@17:15:13.766
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/IBCCore.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Integers.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Sequences.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/IBCCoreDefinitions.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Naturals.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS18Relayer.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/Chain.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla
PASS #1: TypeCheckerSnowcat                                       I@17:15:15.377
> Running Snowcat .::.                                           I@17:15:15.377
> Your types are great!                                          I@17:15:18.443
> All expressions are typed                                      I@17:15:18.443
PASS #2: Terminal                                                 I@17:15:18.829
Type checker [OK]                                                 I@17:15:18.829
It took me 0 days  0 hours  0 min  5 sec                          I@17:15:18.830
Total time: 5.375 sec                                             I@17:15:18.831
EXITCODE: OK

apalache-mc typecheck MC_IBCCore.tla

• detailed.log

17:18:57.035 [main] INFO  a.f.a.t.Tool$ - Type checking MC_IBCCore.tla
17:18:57.283 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
17:18:59.016 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
17:18:59.017 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
17:18:59.017 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
17:18:59.117 [main] DEBUG a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > JSON output: /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/x/17.18-20.04.2021-999478169097429333/out-pre-TypeCheckerSnowcat.json
17:19:00.347 [main] ERROR a.f.a.t.t.p.LoggingTypeCheckerListener - [IBCCore.tla:430:29-430:49]: Undefined operator name E47084@GetChainByID. Introduce a type annotation.
17:19:00.348 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Snowcat asks you to fix the types. Meow.
17:19:00.348 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [FAIL]
17:19:00.348 [main] INFO  a.f.a.t.Tool$ - Type checker [FAILED]
17:19:00.349 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  3 sec
17:19:00.349 [main] INFO  a.f.a.t.Tool$ - Total time: 3.317 sec

• command line output

Type checking MC_IBCCore.tla                                      I@17:18:57.035
PASS #0: SanyParser                                               I@17:18:57.283
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/MC_IBCCore.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/IBCCoreDefinitions.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Integers.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Sequences.tla
Parsing file /private/var/folders/r3/_hxg4k0x4sgf0vh4jkv91hvh0000gn/T/Naturals.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/IBCCore.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS18Relayer.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/Chain.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla
Parsing file /Users/ilina/repositories/informal/ibc-rs/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla
PASS #1: TypeCheckerSnowcat                                       I@17:18:59.017
> Running Snowcat .::.                                           I@17:18:59.017
[IBCCore.tla:430:29-430:49]: Undefined operator name E47084@GetChainByID. Introduce a type annotation. E@17:19:00.347
> Snowcat asks you to fix the types. Meow.                       I@17:19:00.348
Type checker [FAILED]                                             I@17:19:00.348
It took me 0 days  0 hours  0 min  3 sec                          I@17:19:00.349
Total time: 3.317 sec                                             I@17:19:00.349
EXITCODE: OK

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

Additional context

[konnov]

This seems to be related to #645. The declarations sorter has a bug.

[konnov]

Fixed that in #777.