--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.
LeslieOn 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.Thanks
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.