What is the recommended method of getting the Apalache/Option/Variants specs so a module can be parsed by SANY alone?

[ahelwer]

Suppose you have a .tla file that has snowcat type annotations, so imports some modules like Apalache/Option/Variants. However, this module also has a TLC model. How can TLC be told where to look for the Apalache/Option/Variants modules so the module parses correctly, and what is the recommended method of acquiring those modules?

[konnov]

Hi @ahelwer!

The answer depends on how you run TLC.

Command line

Consider the example spec t.tla:

---- MODULE t ----
EXTENDS Integers, Variants

VARIABLE
    \* @type: A(Int) | B(Str);
    v

Init == v = Variant("A", 0)

Next ==
    LET old == VariantGetUnsafe("A", v) IN
    v' = Variant("A", old + 1)

Inv == VariantGetUnsafe("A", v) < 10
==================

and the accompanying TLC config:

INIT Init
NEXT Next
INVARIANT Inv

Assuming that you have apalache.jar and tla2tools.jar in ~/Downloads, you could run TLC as follows:

java -cp ~/Downloads/tla2tools.jar:~/Downloads/apalache.jar tlc2.TLC t.tla

TLA+ Toolbox

In case of the TLA+ Toolbox, you could probably add apalache.jar to the libraries, similar to using TLA+ Community Modules.

VSCode extension

Actually, I don't know what to do there. The community modules are bundled with the extension. We could bundle the recent Apalache modules with the extension too.