Please send all the necessary information to debug the problem to
Markus Kuppe. That includes the the log file and the contents of the
spec's .toobox directory. (See the "Reporting Problems" section of
the "In Case of Trouble" help page for instructions on how to find the
log file.
After you've done that, you can try to recover. You can save the
model by typing Control-S in in the model. However, I doubt if that
will help because I suspect the model is corrupted. I suggest cloning
the model, deleting the original model, and running the clone. If that
doesn't work, try creating a new model from scratch and running it.
If that fails, try deleting the spec and creating it again.
If that doesn't fix the problem, see how broken your Toolbox is. Create a new spec whose body consists of
VARIABLE x
Init == x = {}
Next == x' = x \cup {1}
create a new model and run TLC on it.
Let us know what happens.
Leslie
Paul
Paul