Re: [tlaplus] Where to find the standard libraries

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1a7a2386-b3f8-b927-6df1-1258a0d93655%40lemmster.de.