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

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

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