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