importing module into model

[Gideon Yuval]

I copied the one-bit clock from the book, got it to parse. Changed the = 1 tp = "xyz", as in the book, and it seems the TLC model checker doesn't care. Opening the model checker, there is no sign that the TLA module is in the model, and no obvious way to import it. Am I missing something obvious? the only visible way to put something in the model is to type the whole thing into teh box.

Thanks

[Gideon Yuval]

Hand-to-hand combat got it to work; but removing the "b \in {0,1}" from the model got me:

---

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException: Attempted to check equality of string "xyz" with non-string:

0

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 6, column 16 to line 6, column 20 in 

--

Is this a bug?

Thanks

[Leslie Lamport]

Hi Gideon,

 

It is impossible to answer your question without complete information on
what you did.  This information includes:

 

 - The exact spec. 
 - The exact model that you executed.
 - Exactly what result was produced by running that model, including any
   error trace and error message.

It appears that Google groups allows you to attach one (perhaps more) files
to your post.  I presume you can use this to attach the .tla file and any
screen shots that you wish.

Leslie

 

On Sunday, February 23, 2014 3:13:41 PM UTC-8, Gideon Yuval wrote:

[Gideon Yuval]

I think there was some hystersis in the TLC tools; got things to work after a while. And I notice that the hirerachy puts models under modules, not modules under models.

Is the way to link modules, models, other modules, ... documented?

Thanks

/Gideon

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/BVi-guUygLM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.

[Leslie Lamport]

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