In Case of Trouble

  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.

Getting Out of Trouble

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.

Backing Out of a Model

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.

Backing Out of a 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.

Backing Out of the Toolbox

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.

Reporting Problems

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 GitHub 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 entering the command echo %SYSTEMDRIVE%%HOMEPATH% in Command Prompt.  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.) 

↑ TLA+ Toolbox User's Guide