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