[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: importing module into model

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?



On Tue, Feb 25, 2014 at 2:06 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
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.

On Sunday, February 23, 2014 3:13:41 PM UTC-8, Gideon Yuval wrote:
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.


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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.