Re: How do I create a TLC model for a specific module in a spec with the toolbox?

[Andrew Helwer <andrew...@xxxxxxxxx>]

I figured this out. The toolbox always creates a model for the single .tla file that serves as the top-level spec for that toolbox "specification". Creating another toolbox specification with SystemMC as this top-level spec let me create models for it.

On Saturday, March 31, 2018 at 7:09:17 PM UTC-7, Andrew Helwer wrote:

I have a spec open in the TLA Toolbox. It contains the following modules:

• System
• ComponentInterface
  
• SystemMC

I want to create a TLC model for the SystemMC module, but it keeps creating it for the System module instead.

Motivation:

The System spec is the "nice" spec of the system I am specifying, useful for documentation. It defines & uses an INSTANCE of ComponentInterface, which wraps some functionality (here, a hash function) that is messy to specify in an efficiently model-checkable way and so would reduce spec readability. I implement the ComponentInterface in the SystemMC spec, so I can model-check the System spec. However, when I create a new TLC model in the toolbox, it automatically creates it for the System spec. How do I get it to create a TLC model for the SystemMC spec instead? Thanks!

Andrew