How to run models on different modules in the same Spec

[Tony Zhang]

I'm new to TLA and have been following the video lectures. However, I am encountering a problem with the toolbox in Lectures 6 and 7.

As per the instructions, I created the modules TwoPhase and PaxosCommit, under the same spec called TCommit, which also contains a module named TCommit.
However, I am only able to run models using initial predicate "TCInit" and next-state relation "TCNext" belonging to TCommit.

If I supply, for instance, "TPInit" and "TPNext" belonging to TPCommit as the Init and Next arguments of the model, errors are detected. Apparently it can't find the definitions "TPInit"and "TPNext"?

Any help is appreciated. Thank you!

[Markus Alexander Kuppe]

Hi Tony,

create a new specification with TPCommit as the root module (File > Open
Spec > Add new Spec...).

Cheers
Markus

[Maneet Bansal]

Hi Markus,
I am experiencing the same problem as Tony. The solution you have provided does work. I have some questions if you can answer

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?

[Markus Kuppe]

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