Where to find the standard libraries

[burt]

Hi,

I'm using the TLA+ Toolbox on MacOS and would like to inspect the standard modules like Integers, Sequences and so on.

I know that the specs are printed in the book, but I would like to have the source code.

Where should I look for them on my file system?

Thanks for any hints,

Burt

 

[Markus Kuppe]

On 31.03.20 03:25, 'burt' via tlaplus wrote:
> I'm using the TLA+ Toolbox on MacOS and would like to inspect the
> standard modules like Integers, Sequences and so on.
> I know that the specs are printed in the book, but I would like to have
> the source code.
>
> Where should I look for them on my file system?

Hi,

you can ctrl+click (command+click?) a module name that appears on the
EXTENDS statement at the top of your spec. In other words, you can
click "Sequences" in "EXTENDS Foo, Bar, Sequences" to open Sequences.tla
in the Toolbox.

On disk, you find the standard modules in
plugins/org.lamport.tlatools_1.0.0.202003260241/tla2sany/StandardModules/ inside
your Toolbox directory. You can also find them online [1].

Markus

[1]
https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules

[burt]

Thanks