Dear Gideon,
I think there was some hystersis in the TLC tools; got things to work after a while.
There is no hysteresis in TLC. Each run of TLC depends only on the input that TLC is given, not on anything that happened before. The input that the Toolbox gives to TLC depends only on the current state of the spec and the model. Dependence on anything else is a bug and should be reported by giving the exact sequence of events that produces the bug.
And I notice that the hirerachy puts models under modules, not modules under models.
Is the way to link modules, models, other modules, ... documented?
In order to do anything in the Toolbox, you have to open a spec. When you create a spec, you are asked for a root module. Hence, a spec contains a root module. That module may import other modules using the EXTENDS and INSTANCE statements, which are described in the Hyperbook. Once you have opened a spec, you can create models. Hence, a spec also has models. Since the contents of a model such as the behavioral spec and the values of constants are in general meaningful only for a particular specification, it would make no sense for a model to have multiple specifications.
If you feel this requires further documentation, I welcome suggestions for how and where to document it.
Thanks,
Leslie