Contents Getting Out of Trouble Reporting Problems
The Toolbox is far from perfect. Below are some hints for getting out of trouble if it misbehaves, and instructions for reporting bugs. Please be patient, we're doing the best we can. We and our other users would greatly appreciate any help you can give us. Click here to find out how you can help.
Errors in the Toolbox can cause it to get into a bad state. The best thing to do if this happens is to back out of what you were doing and try again. You should try to back out only as far as necessary.
If you try running TLC and nothing seems to be happening, see If Something Crashes. Looking at The TLC Console View can help you figure out what state TLC is in. It's possible that the problem is with the model. A problem with a model can also be caused by editing the model, or by editing and re-parsing the spec.
Closing the model (by clicking on the X in the model editor's tab) and re-opening it (with the TLC Model Checker/Open Model menu item) may solve the problem. If not, try cloning the model and deleting the original. (See the Models help page.) If the problem persists in the cloned model, try creating a new model. If that too has problems, try backing out of the spec.
If the Toolbox gets into a bad state when you're editing a module, or
when you have a problem with a TLC model that can't be solved by backing
out of the model, you should try backing out of the spec.
The first thing to try is closing the spec,
refresh the spec by right-clicking on its entry
in the Spec Explorer,
and re-opening the spec.
(See the Manipulating
Specs help page.)
If that doesn't work, try exiting from and then restarting the
Toolbox.
If that fails, delete the original spec.
However, if you have models that you don't want to lose, first make a
copy of the .toolbox directory under some other name.
If that works, try creating a new spec with the same root
module.
If you have saved a copy of the old .toolbox directory,
you can first restore that directory and see if you can open it with
the Import existing models option.
If not, you will have to try creating a new spec with the same modules
but without your saved models.
If you can't restore the spec, see if the problem exists with other
specs.
If it does, you will probably have to back out of the Toolbox.
If not, see if you can figure out what it is about that particular
spec that is causing the problem.
If all else fails, you will have to re-initialize the Toolbox. This is done by exiting the Toolbox
and deleting all its state information from the disk. However, before doing this, save the relevant
part of the Toolbox's .log file as described in Reporting Problems below.
The Toolbox keeps its state in a folder named workspace that it creates in the
folder from which you run the Toolbox. Deleting (or renaming) the workspace folder (when the Toolbox
is not running) causes the Toolbox
to start in its initial state the next time you execute it. It will then show no existing specs.
However, the information about the individual specs that existed when you deleted
the workspace folder is still there.
If you had a spec named SName ,
the state of that spec was saved in a folder named SName.toolbox .
If you open a spec with that name having the same root module, the Toolbox will give you
the option of reloading that state, which includes the state of all its models.
If you're lucky, that spec will work fine. If not, you'll have to delete the spec
(which deletes the .toolbox folder) and re-create
it from scratch. Of course, the module files will still be there.
We can't fix a problem with the Toolbox if we don't know about it. Please report any problem you encounter--be it a bug or something you found confusing or poorly explained. You can enter a bug report in our CodePlex bug database. However, please search the database first to make sure that we don't already know about it.
When reporting a bug, please include all details. It will be helpful if you can include the relevant part of the Toolbox's log, which is the file named .log. The .log file is in the .tlaplus/.metadata/ folder in your home directory. On Windows, you can find out where your home directory is located, by looking at the %HOMEPATH% environment variable. On Linux and Mac, check the $HOME variable. (The log contains enough timestamped entries for you to figure out what part of it relates to the problem you are reporting.)