Re: [tlaplus] How to run models on different modules in the same Spec

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 22.04.2018 13:35, Maneet Bansal wrote:
> 1. Does that mean a model always checks root module for the entry points?
> 2. Is there is a way to change the root module for specification, so that I don't have to create a new specification for new modules?
> 3. Is there any best practice for managing the common modules. I mean if we need a new specification to run each module, then should I keep all my modules in some directory that is shared by all the specifications???? 
> 4. As far as I understand, a specification is a group of modules. Is there a way to manage the modules so that it is easy to know which all modules a specification is using?

Hi Maneet,

with the current Toolbox there is a strict 1 to 1 connection between the
specification (S1) and its root module (R). In other words, a
specification has a fixed root module and 0 to n additional modules (M1
...Mn). The same applies to models. A model is directly associated with
its specification and thus the root module R.

In case you want to check one of the additional modules M1 of the
specification S1, you will have to create a new specification S2 and
make the additional module M1 the specification's root module.

With that said: On the file system lever however, R and M1 to Mn can all
coexist inside the same directory (D). The same is true for the
specifications S1 to Sn which can all be created inside of the directory
D. Just choose a unique name for each specification which the Toolbox
will enforce.


If you additionally want to reference common modules, the Toolbox has
support for library locations [1] either at the specification level or
at the global Toolbox level.

Cheers
Markus

[1]
https://tla.msr-inria.inria.fr/tlatoolbox/doc/gettingstarted/tla-preferences.html