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:
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