TLA+ | The way to specify

I'm using Version 1.2.1 of 29 September 2010 (32-bit)
Running on Windoes 7 Enterprise 64-bit, on a 4-proc 4GB ThinkPad laptop.

Sequence of events:

1. TLC was checking a model. (I can't remember if it was doing it in the background.)

2. I had to do a system restart to install an update of some unrelated software (Adobe Reader).

3. After the restart I ran the toolbox and found that:

- TLC is not running (not surprising, as I haven't restarted it.)

- The Model Overview tab says "(model checking is in progress)"

- The "How to run" options are all greyed out. The "Checkpoint Id" and "Checkpoint Size" are populated with reasonable values, but they are greyed-out.

- The "Model Checking Results" tab says "Current Status: Not running" and "Errors detected: No Errors". The "State space progress" box lists the last few state reports (from before the system restart)

Note: I did previously stop this TLC run, and restart from a checkpoint, without any problems. But I didn't do a system-restart that time.

thanks,

Chris

When a problem occurs, try using Help.  The Welcome View that you saw
when you first ran the Toolbox told you to read the explanation of
how to use Help.  However, like most users, you probably didn't
or else forgot what it said.  So, 

- Open the Toolbox and close any open spec.

- Click Help/Dynamic Help

The Help page you get will tell you to click on Getting Started.  From
there you can click on Using Help.  That page explains that, from any
Help page, you can get to the main Help menu by clicking on Contents at
the bottom of the page.   Do that.

On the Contents page, you will see:

   Model Checking / Validating and Checking a Model

Go to the Validating and Checking a Model page.  (You can get there
directly from the Contents page or by going through the Model Checking
page.)  The table of contents of that page contains a link to the the
section "If Something Crashes".  Go to that section and follow the
directions you will find there.