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

[Maneet Bansal <maneet...@xxxxxxxxx>]

On Wednesday, 17 January 2018 01:02:33 UTC-8, Markus Alexander Kuppe  wrote:
> On 17.01.2018 09:40, Tony Zhang wrote:
> > 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!
> 
> Hi Tony,
> 
> create a new specification with TPCommit as the root module (File > Open
> Spec > Add new Spec...).
> 
> Cheers
> Markus

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?