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

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

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