Thanks
Am Dienstag, 31. März 2020 17:32:29 UTC+2 schrieb Markus Alexander 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