Something can be added to the Results Page to indicate if the spec has changed since the last run of the model.  More difficult is figuring out a nice, simple interface to allow the user to look at the saved, read-only version of the spec files on which the model was run.  One possibility is to add to the Spec explorer an extra level to list, for each model, any modules that have changed since the model was last run.  Clicking on the module name would raise a read-lonly module editor on that module--with something in the tab indicating which model the module was saved for.

(Items 1 and 67 from todo.txt)

The Model Checking Results page should list
 in the General section the information about probability of fingerprint
 collision that TLC prints after a run that finishes computing the 
reachable states.  (I think it prints it out in the event of a liveness 
error.)  It should say approximately something like: Probability of 
fingerprint collision: theoretical: 4.3E-15  pragmatic: 8.7E-15

In TLCProcessJob, the method JavaRuntime.getDefaultVMInstall() returns null on Mac OS. A non-null value is required to run TLC.

The help menu is not getting the focus if 
it doesn't already have the focus and it either is in or is being opened
 into a folder that has the focus.

The rename spec command doesn't do the 
right thing if a spec already exists that has the same name ignoring 
case but with different capitalization. In particular, a 
ResourcesException is thrown saying "A resource exists with a different 
case". If the spec being renamed is open at the time, then a 
RuntimeException is thrown saying "Specification newSpecName not found" 
and the toolbox returns to the welcome view.

In addition, if a spec is renamed to a name "newName" when there exists a
 folder newName.toolbox, this seems to cause the same problem.

There may be other renaming actions that can cause the same resource 
problems.

Entering an expression such as "1+" 
followed by nothing in fields of the model editor will result in a parse
 error message that says "Encountered ----". The parser finds "----" in 
the MC.tla file because that is the separator between sections. This 
should probably be replaced with something more useful for the user.

Add a new parameter that is a default line 
width for modules.  This should be put on a new Module Editor 
preferences page.   (it's not clear to me if any of the General 
preferences that apply to the module editor should be moved to this 
page.  That should be done only if they apply only to the module editor 
and not to anything else, such as the Model Editor.)   Its default value
 should be 77.  

The creation of a new module file by the Toolbox (for example, when 
opening a new spec with a new file) should use the parameter as follows.
  Let the value of this parameter be P.  Then

- The closing line of the module should consist of P "=" characters.

- The opening line of the module should consist of the following:

     N "-" characters,  1 space character,  "MODULE",  one space 
character,  
     the module name,  one space character,  M "-" characters
     
  where N and M are the smallest integers greater than or equal to 4 
such that:
    (a) M equals either N or N-1, and
    (b) The total number of characters in the line is greater than or 
equal to P
    
  I believe this means that, with Java notation,
     N  = Max(4, (Q / 2) + (Q%2))
     M  = Max(4, Q / 2)
   where Q = P - ("MODULE".length + ModuleName.length + 3)

Also, rename the items under TLA+ Preferences to remove "Preferences" 
from their names--e.g., change "TLA+ Parser Preferences" to "TLA+ 
Parser".

Rename the items under TLA+ Preferences to remove "Preferences" from
their names -- e.g., change "TLA+ Parser Preferences" to "TLA+ Parser".

I tried it in my linux (ubuntu Karmic) machine.
The toolbox, quickly used around 1 gb (1172 mb) of my virtual memory
before opening a file.
Having 1 GB of physical memory in my laptop,
only opening a spec file almost like forever.
I don't think it is a normal situation.

I tried to upgrade my machine using the latest stable kernel  
2.6.31-15-generic,
but the problem remains.

Other applications (such as netbeans, eclipse, mysql) run normally in my  
machine.
I'm not sure what went wrong.


Sincerely yours,
Ade Azurat (ade@cs.ui.ac.id)

We still have the problem that TLC might be
 running for weeks, and the user in the meantime changed the spec.  When
 TLC stops running, the model gets revalidated and stuff that was in the
 model configuration gets lost. Here is a possible solution:  Add the 
notion of a model being LOCKED, meaning that it cannot be changed in any
 way, meaning that it is read only and it doesn't change to conform to 
the current spec.  (This state actually exists in the toolbox now: it is
 called "model in use".)  In particular, it conforms to the copy of the 
spec that's salted away with the model.  Running the spec locks the 
model. There will also be a menu item that the user can select to lock 
the spec himself. (This will allow the user to protect himself from 
accidentally modifying or re-running a spec by mistake--perhaps losing a
 trace that took weeks for TLC to produce.) We must decide what should 
happen to the lock state when a TLC run completes. Should the user have 
to explicitly unlock it?  I suggest that it be unlocked when the run 
completes if and only if that run did not take too long--where "too 
long" is a user-settable preference.

When I change the spec to remove all 
variables and save it and then open an existing model, the model 
correctly opens with the "No behavior spec" option selected and the 
other options disabled.  However, when validating the Toolbox, it 
complains that the Init and Next formulas left over from the previous 
version (which I can't change because the option is disabled) are 
undefined.  We should make sure that no entry from a disabled field is 
ever put into the MC file.

After an error trace is generated from a 
run of TLC, the user should be able to enter one or more expressions for
 which he wants to see the value at each state of the trace.

At one point I think the column number of 
the cursor appeared at the bottom of the module editor. I may have 
removed this when turning the module editor into a multipage editor to 
include a pretty printed version of the module.

If the user renames or deletes a root file 
outside of the toolbox and then opens the spec, the toolbox displays a 
page that says

    Resource is out of sync with the file system: '/test/test10.tla'.

    Press F5 or select File -> Refresh to refresh the file.

Pressing F5 does nothing and File -> Refresh does not exist in the 
toolbox, so I guess this page is generated by eclipse code. The toolbox 
also shows the Parsing Error view which says "Could not find module."

I received the following problem report from a user here.  The problem
occurred when he unzipped the file using Cygwin's unzip command.  It
worked fine when he used WinZip.  He also said that when he unzipped
with WinZip, then produced a zip file with Cygwin and unzipped that
file with Cygwin, it worked fine.  This all happened on an XP system.

We should see if this is reproducible.  If it is, we should spend a
few milliseconds trying to figure out if there's a way to produce a
zip file that Cygwin will handle properly.  If we can't figure out
such a way, we should warn users not to unzip with Cygwin.  

-----

I tried to install the toolbox but I'm getting an error.  My operating
system is Windows XP. Here's what I did:

   - downloaded ZIP file from http://www.msr-inria.inria.fr/
        Projects/tools-for-formal-specs/toolbox.win32.win32.x86.zip

   - unzipped it to c:\, creating directory c:\tlatoolbox

   - installed Java (Java Version 6 Update 17).

   - rebooted computer

   - executed c:\tlatoolbox\toolbox.exe

   - got a pop up window that says "The Toolbox executable launcher was
     unable to locate its companion shared library"

When I try to produce a pdf version, the 
appropriate tab appears but it is blank.  While this could be a problem 
with my installation, it has worked in the past and I haven't changed 
anything in my LaTeX installation.  (Which doesn't mean that Windows 
didn't decide to change it for me.)  However, no log entry is produced, 
which is a bug even if the Toolbox is calling tla2tex correctly.   
Moreover, even if there were a problem with my LaTeX installation, 
TLATeX would write a .tex file and the Toolbox command isn't doing that.
  And furthermore, there is an old version of the pdf file in the 
.toolbox directory that the Toolbox isn't displaying.

Also, I don't remember if TLATeX produces an error message that the 
Toolbox is supposed to recognize and translate into an error warning for
 the user.  If that's not being done now, it should be implemented.

There will be two kinds of module files: .tla and .pcal files.  A root
or non-root file of a spec can be of either kind.  A .pcal file has a
derived .tla file that is produced by running the pcal translator,
which is done by calling pcal.trans.runMe().  For a pcal module,
"parsing" consists of running the pcal translator and then, if there
are no errors, parsing the resulting tla file.  (Thus, no additional
"translate on save" option is needed.)  

When the user opens a pcal module, the corresponding tla file should
be opened in another tab of the editor (but the pcal file's tab should
have the focus).  Eventually there will be a version of tla2tex for
pcal files.  There will then need to be two separate commands for
producing a pdf version of the pcal file and of the tla file.  (The
latter command should not be commonly used.)  For now, the "Produce
PDF Version" command will call tla2tex on the tla file.  

Should the user want to edit the tla file?  Normally, it's a bad idea
to edit derived files.  However, I can imagine the user wanting to add
debugging code to the algorithm.  Adding it to the TLA+ translation
might be a nice way to do this, since he will probably that code will
then be removed when he fixes the bug in the pcal file and translates
it.  I suggest that the default be to pop up a warning the first time
the user changes the tla file after it's translated.  We can have a
preference that allows him to disable that warning.  We could also
have a preference that makes the tla file read only.

Most command-line options will be specified by the options statement
in the pcal file.  Moreover, the most common options, which specify
fairness and termination, will eventually be eliminated by changes to
the language.  However, the user may want to specify some global
default options that will be passed to the translator as command-line
options.  A preference will be provided to specify that.  Its default
value will be -nocfg.  Since the ability to specify options for an
individual spec in the Spec Explorer has been implemented, we perhaps
we should keep it--letting the preference specify the initial setting
of that field.  Since those options will rarely be set by the user, it
doesn't make much difference what we do.

A read-only copy of the pcal file should be saved in the model's
subdirectory along with the tla file.  

The module is considered to have changed if either the pcal file or
the tla file has been changed since it was last translated or parsed.

I think this is a complete list of what has to be changed to handle
pcal files.

I regularly synchronize my home and office machines by copying files back 
and forth between them.   This means that I frequently overwrite .toolbox
directories.  If I open the Toolbox and it restores the previous state, it
fails to check if the models that it knew about when it was last run are
still there.  This causes bizarre behavior.  Often the Toolbox fails to
start the first time I try to open it.

By the way, is P4 higher or lower priority than P3?

Opening the spec and the (only) model (see 
attachments) gets the model in a state in which most of it thinks that 
TLC is running, except that the Model Checking Results page correctly 
reports its status as "Not running".  This state may have been produced 
by running the trace explorer, but running the trace explorer on another
 spec doesn't do that.

In Windows, you can create a new file by 
browsing to an existing directory, typing in the name of the file, and 
clicking on Open.  This opens the file if it exists, and creates it if 
it doesn't.  The Toolbox's file browser on the Mac doesn't offer the 
option of typing in a file name.

Jean-Charles reports that nothing appears 
on the Help menu at the top of the screen when the Toolbox is selected. 
 (That's where MAC is supposed to show the help choices.)

- Add a local help button (the ? inside a 
circle) that leads to help for the window. 

- When the user selects a state in the Error Trace, he sees the value of
 the expression as something like

     __trace_var_126403425857315000 = 12
     
   The user should not see a variable name like that.  Best would be to 
replace the variable name with the expression, the way it's shown in the
 Error Trace.  If this isn't easy, the Toolbox should use shorter 
variable names for the expressions.
   
- When nothing is selected in the Error-Trace window, the bottom text 
field says "No error information".  It should say something more 
helpful, like:

     Select line in Error Trace to show its value here.

If you click on the "parse" button when the
 file has been modified, the Toolbox asks if you want to save the file 
but neither saves it nor parses it when you answer "yes".

When no line in the Error Trace is 
selected, the text box below it should say

   Select line in Error Trace to show its value here.
   
It does not display this when the TLC Errors Window is first raised.  
Nor does it do that when the Explore or Restore button is pushed--unless
 a line in the Error Trace was already selected when that Button was 
pushed.

A name/expression or value that takes up 
multiple lines does not display properly in the trace viewer. In 
particular, only the first line shows.

The toolbox on Mac OS has an extra menu 
item entitled "TLA+ Toolbox." It has the menu items "About TLA+ 
Toolbox", "Preferences...", "Services", "Hide TLA+ Toolbox", Hide 
Others", "Show All", and "Quit TLA+ Toolbox." "Services" seems to be 
permanently grayed out. The Preferences menu item also appears in the 
File menu, which I think is fine. All menu items perform as expects, 
except for the "About TLA+ Toolbox" menu item which seems to do nothing.
 We are going to add an About item to the Help menu. It would be nice to
 be able to remove the one from the "TLA+ Toolbox" menu, but I'm not 
sure if this is possible.

a. There is no reason why the user cannot use the same model value in two
   different constant instantiations or in a constant instantiation and a 
   definition override.  Or uses a model value declared on the advanced
   page as a model value in a constant instantiation.  This requires
   checking that a model value is declared elsewhere before adding a
   CONSTANT declaration for it.  
   
   b. The correct order in which things should be written in the MC file are:
       - Declaration of advanced model values.
       - Declaration of the sets of model values that instantiate constants.
       - New User Definitions.
       - Everything Else, which is all of the form 
         newId_1234567 == some expression.
   However, the current structure of the toolbox makes it a nuisance to do
   this, and the current validator will disallow the models that this order
   is designed to allow.

Suppose the user starts to write a PlusCal 
algorithm, translates it and gets a PlusCal error, and then decides to 
delete the PlusCal code and just write the spec in TLA+.  There's no way
 for him to get rid of the PlusCal error message in the Parse Errors 
window.  In fact, even if I run the translator on another module, the 
PlusCal error remains in the Parse Error window--whether or not the 
other translation produces an error. (The only way to get rid of it is 
to go back to the original module, correct the PlusCall error, and 
re-run the translator.)  The best thing to do is probably to create a 
separate PlusCal Error Window.  Running the translator should first 
clear this window and remove all PlusCal error markers in the module on 
which the translator is run.  (I believe that if running the PlusCal 
translator creates a PlusCal error, then the file is not re-parsed, so 
only the PlusCal error window would need to be popped up.)

The Definitions Override menu allows the user to override the same definition multiple times.

For a big spec--in particular, for the 
farsite spec, after Parse the parse spec command gets disabled.  But 
parse module file still works.  Simon thinks it may be that the build 
infrastructure of Eclipse is deactivating builders under some 
conditions--for example, if a builder dies with an exception, it is 
deactivated. Perhaps it's also deactivated on a time-out.  The list of 
builders is attached to the project, so one can query the project or the
 project nature to find this out.  So, Simon assumes that for some 
reason, the builder is deactivated.

The parser is being launched in a separate thread, but Simon thinks that
 perhaps he's not doing it in the right way.

Closing the toolbox simply kills any 
running TLC.  Instead, it should warn the user that this will kill TLC 
and give him the option of canceling.  To do this, need to modify to 
CloseSpecHandler.execute() so it checks if editors have been closed 
successfully before exiting.  The model editor's method that gets called
 by the closeAllEditors method should return false. Another approach is 
to register another handler in place of this one when TLC is running, 
and having that handler call the current one only if the user says it's 
OK to stop TLC.

PlusCal translation needs to be examined.  
Here are some things that need to be fixed: 
     - There should be a more user-friendly way to specify translation 
options.  This involves:
       (a) Providing check-boxes or radio buttons for the common 
options.
       (b) Finding a more convenient way to add them than the current 
one (right-clicking in the Toolbox Explorer) and selecting properties.
       
     - Translation options are now attached to the spec; they should be 
attached to an individual module.  (It's possible for a single spec to 
have PlusCal algorithms in two different modules.)

If I select window / reset window layout in the Welcome Perspective, it produces a blank window instead of the Welcome View.

Here are some thoughts on enhancements to 
the Module Editor.

    - Add a preference to choose an Emacs-like keybinding.  This 
requires adding new commands that appear in the General/Editors/Keys, 
and options that choose from among sets of bindings.
    
    - Add editing commands (and invent bindings) for comments.  Perhaps 
copy the commands I use for boxing comments.
    
Note that Simon has bound toggle comments to Control-/, but that command
 doesn't appear either when I type Ctl-Shift-L or in tthe preferences 
keybinding options.

Enhance the Init/Next method of writing the spec to add lists of weakly and strongly fair actions.

When the user has chosen assigned a set of 
model values to a constant and specified symmetry, the default on the 
next page of the wizard should be to make the values untyped.  This may 
be hard to do because the second wizard page is created before the first
 page of the wizard is raised.  If it's hard, perhaps we should change 
the default to be to make the values untyped.  This is done in 
TypingWizardPage.createControl.

When creating a new spec, the Import 
Existing spec option is always checked and disabled.  It should be 
unchecked and disabled if the .toolbox directory does not already exist.
  However, if the .toolbox directory does exist, its present behavior of
 checking and enabling the box is the correct one.  If it's hard to have
 both behaviors, forget about this.

When the user clicks on File/Open 
Module/Choose TLA+ Module, the file browser that pops up should show the
 specification's directory.

TLC's liveness checking in simulation mode 
is seriously buggy. Unless Yuan volunteers to find the fix quickly 
(which seems unlikely), we'll have to tell users not to check liveness 
properties in simulation mode.  If Yuan does find the fix, we will 
probably have to fix a bug introduced by Simon that causes TLC to 
produce an error trace ending with

      State 5: <Action line 12, col 9 to line 12, col 20 of module 
Test2>
      x = 4

      State 6: Stuttering
      Back to state 1.

In at least one place, the Toolbox marks an
 error when the user starts entering a value, but doesn't remove the 
error marker when the user's typing removes the error.  Here are the 
cases I've found:

    - Write a model specifying Init and Next, leaving Temporal Formula 
empty. Then select Temporal Formula.  This produces an error because the
 Temporal
    Formula field is empty.  However, typing into that field doesn't 
make the error marker go away.
    - In TLC Options on the Advanced Options page, choose simulation 
node.  Then:
       (a) Enter a non-number.  Then delete that and enter a number.  Or
       (b) Enter a non-numeric seed or aril, then delete it or change it
 to a number. or else choose Model-checking mode and depth-first mode, 
then do the same
       thing with the depth field.  (Incidentally, there's no reason to 
check those fields at all when the appropriate option isn't chosen.)  
    - In the constant assignment section of the main model page, specify
 the value of a constant to be a set of model values one of which is 
SPECIFICATION.
      This produces an error marker which remains after that constant 
assignment is changed.
      
This isn't a big deal, because the errors go away when the model is 
validated.
    
A similar case occurs if one first enters a Temporal Formula and then 
chooses "Initial predicate and next-state relation".

If the user edits a module that is out of 
synch with the file system, the toolbox does not warn the user of this. 
When the user saves the module, a message pops up telling the user that 
the module is out of synch.

Files ending in .tla appear grayed out when
 browsing for a new spec or adding a module. It is still possible to 
select the grayed out items. They were not gray when the dialogs were 
"Open" dialogs but are gray now that the dialogs are "Save" dialogs.

A Mac 64-bit user requested drag-and-drop. 
 On a Friday morning, on Windows, with cloudy weather and an outside  
temperature around 0, here's what I observed:

- In the Toolbox module editor, if I select a piece of text and drag it,
 I get visual feedback that indicates I'm dragging it.  But when I 
release the mouse button to drop it, nothing happens.

- In Eclipse, drag-and-drop works when I edit a java file or an xml 
file, but not when I edit an html file.

Simon: do you know what's supposed to happen?  

I don't imagine the Eclipse code contains anything so retro as 
documentation, but perhaps someone has posted something about 
drag-and-drop  somewhere.  This is not worth worrying about now, but we 
should probably look into it when we start working on the editor.

Jean-Charles reports that on two out of 
three of the machines he tried running the Mac 64-bit version (by 
double-clicking on the icon), nothing happened.  He eventually found 
that the problem was that a file was not set to be executable--a problem
 that reports solving with

chmod +x (macosx.cocoa.x86_64-jc.macosx.cocoa.x86_64/) 
toolbox.app/Contents/MacOS/toolbox

I presume that the parenthesized text is supposed to indicate a 
super-directory of the directory in which the command was executed.

I believe he found this problem with both the original version that Dan 
created and a later one that I made.  I also have a vague recollection 
of this problem occurring on a different release.  If this can't be 
fixed, we need to add a warning about it on the web page.

Running validation on a model deletes the 
contents of MC.out. I think that the contents of that file should only 
be erased if TLC is going to be launched, not for validation.

We have the \* Generated at Thu Jan 28 
12:46:04 EST 2010 comment at the end of the file. Why not also have an 
automatic \* Last updated ... ?

After loading a spec's top module, why not 
have an option to load all (related) other modules, to avoid having to 
go through the menu one by one?

If I hold down Control and click on a 
symbol that's defined or declared in an extended module, the right thing
 happens if that module is open in a model editor.   If it isn't, 
nothing happens because the Toolbox throws: 

org.eclipse.ui.PartInitException: Unable to open editor, unknown editor 
ID: org.lamport.tla.toolbox.TLAEditorAndPDFViewer

Deleting a model does not remove the 
sources and data providers for that model from the tlc output source 
registry. If a user recreates a model with the same name, the output 
data from the old model appears.

Running the trace explorer should disable 
running of the model checker on the same model because both operations 
work on the same directory.

On a linux ubuntu machine, the new spec 
browse dialog and add module dialogs open to the directory containing 
the toolbox executable everytime. The new spec browse dialog should open
 to the most recently opened directory, and the add module dialog should
 open to the directory of the root module.

Jumping to the definition/declaration for a
 symbol does not work properly for a module that is not extended or 
included in the root module. I believe the toolbox looks for symbols in 
the symbol table for the root module. If the user is editing a module 
that is not currently extended or instanced by the root module, then the
 toolbox will not detect the hyperlink for symbols that are not in the 
symbol table of the root module. If the symbol happens to be in the 
symbol table for the root module, then the toolbox will incorrectly jump
 to the definition or declaration of that symbol in the spec.

For some reason, the file browser for the 
Save As command has a button to choose whether or not to display the 
selected folder.  (The Open New Module file browser doesn't have that 
option.)  I would use the Open New Module's file browser for the Save As
 command as well.  However, if there's some good reason for using a 
different browser, then the browser should by default open with the 
current folder shown.  Currently, it opens the first time with the 
current folder hidden.  Combined with bug 39, this is a disaster.

The Problem: I already have too many specs 
to be able to find easily the one I want to open.  I don't want to start
 deleting them because the I would lose the models I've defined.  

The Solution: The following two features.

1. The option of deleting a spec without deleting its .toolbox 
directory.  Let's call that "Deleting" and the current behavior 
"Expunging".  The simplest interface to use would be simply be to have 
Delete and Expunge options on the Spec Explorer menu.  However, no one 
would figure out from the name what they mean.  A more intuitive 
interface would be for Delete to raise a popup allowing the user to 
check or uncheck an "Allow spec to be reopened later" option.  (I 
suggest that the default be that the option is checked.)  Dan, Simon: 
which interface do you think is better?

Note: This suggestions a third possible option: deleting the module 
files as well as the .toolbox directory.  This is a bad idea because, to
 be useful, it should delete all the spec's modules, which is bad 
because (a) it's easy to forget that a spec imports a module that's used
 elsewhere and should be saved and (b) that option will almost always be
 used to delete an uncompleted spec, which is likely to be 
unparsable--so the Toolbox couldn't delete anything but the root module.

2. Add to the Open Spec menu the option Reopen Deleted Spec.   It would 
produce an alphabetically sorted list of all deleted (but not expunged) 
specs for the user to choose from.  Note that there are three reasons 
why that operation might fail: (a) the root module [or the .toolbox 
directory] no longer exists, (b) the user has created a new spec with 
the old name, or (c) the user has created a new spec with that root 
module.  Of course, (a) exists when opening an existing spec.  I suggest
 that (b) and (c) be made impossible by removing an old spec from the 
list if a new one is created with the same name or root file.  I also 
suggest that when the user opens a new spec with the name or root file 
of an old one, he be warned and given the option of canceling.

It is possible to implement feature 1 without feature 2, since the old 
spec can be reopened now with the Add New Spec option.  Feature 2 is 
still useful because it might be easier to find an old spec this way 
than by hunting through the file system.   However, we can start with 
just feature 1.

TLC's checkpoint files can take up lots of 
space.  The Toolbox should tell the user how much disk space his specs 
are using.  We will need to discuss what the best interface is for doing
 this.  Here are things that he should be able to see from the Toolbox:

- For each spec, the size of the .toolbox directory.  This should be a 
property of the spec, and it shouldn't be too hard for the user to go 
through all his specs in the Spec Explorer to see which ones are using 
lots of space.  The size should also be displayed for the currently open
 spec, in some way that is discrete if the size is small and becomes 
more obvious if it's big.

- For each spec, the space used be each model should be a property of 
that model.  The space used by a model should be displayed on one of the
 model pages--again, discretely if it's small and loudly if it's big.  
There should also be a button to delete the model's checkpoint.  (Is 
there anything else kept for the model that might be big enough to need 
deleting?)  It would be useful if the user could see the space taken up 
by each model of a spec without opening each of them.  (He is likely to 
want to find the guilty model when he sees that the spec is taking up a 
lot of space.)  This could be done as a model property in the Spec 
Explorer, which provides a menu option for one that pops up an error 
box.

When a spec is open, the Spec Explorer 
allows the user to display the models only of the open spec.  I presume 
that's a feature and not a bug.  (It would make sense to show them for 
unopened specs too, with commands like Open or Clone the model disabled,
 but that's not worth the bother.)  However, when I close the spec, I 
can still see that spec's models and their menu items are still active. 
 I don't know what Open does; the console shows that the Toolbox thinks 
it is opening the spec and then the model, but there's no sign that it 
has.  Clone and Delete actually perform the action (on the apparently 
closed spec), but then make the models invisible in the Spec Explorer.

Obviously, the fix is just not to display the models of any spec in the 
Spec Explorer when there's no spec open.

Renaming a spec should change the 
configuration file names for models of the spec. Currently it does not, 
so renaming a spec and then attempting to open a model that existed 
before the renaming throws a null pointer exception and does not open 
the model.

Load the following spec:

---------- MODULE Test2 -----------
EXTENDS Naturals, TLC
VARIABLE x
CONSTANT C 
Spec == (x=0) /\ [][x'=x+1]_x
Inv == x < 5
=================================

Set C to 44, check Inv as an invariant, and run the spec.   On the 
resulting error trace, add  C  as the expression to print, and hit 
Explore.  Everything is fine, and it prints 44.  Go to the Constants 
section, change the value of C to 22 and hit Finish.  BUT DO NOT SAVE 
THE MODEL.  Go back to the Results page, open the Error Trace window, 
and hit Explore.  It runs  fine, except it's still printing 44 rather 
than 22.   This indicates a minor bug: it should save the model before 
running TLC again.  Now the major bug.  Hit Explore again.  Nothing 
happens.  The Trace Explorer is wedged.  Closing and opening it again 
doesn't help.  The only way to unwedge it is to run the spec again, 
recreating the error trace from scratch.  When Explore is selected, the 
Toolbox seems to be writing empty TE.tla and TE.tlc files.  (Perhaps 
fixing the minor bug will prevent the major one.

The Trace Explorer reports an error if an 
expression to be printed contains a model value or a symbol defined in 
the Advanced model page's Additional Definitions section.  The problem 
seems to be that the expressions to be printed appear too early in the 
TE.tla file.  They should be the last things before the definition of 
the initial predicate and next-state relation.

The user should be able to specify which 
variables are hidden (not displayed) in the Trace Explorer.  (This 
should apply only to the view obtained by hitting Explore, not to the 
original trace obtained by hitting Restore.)  We need to discuss what 
the interface should be for this before implementing the feature.

Note: We were originally discussing adding the feature of changing the 
order in which variables are shown.  That's unnecessary.  The user can 
hide all the variables and then enter them in any order as expressions 
to be printed.

We should build our own About dialog. Some 
of the aspects of the eclipse provided about dialog should not be on 
there, such as Installation Details.

The trace explorer variables should appear before other variables in the order in which the user entered the expressions.

If the user enters expr into the evaluating
 constant expressions field, then the value val of expr correctly shows 
up in the value field, but <<!@$!@$!@$, val>> shows up in 
User Output. This occurs on Linux ubuntu.

If I have the PDF viewer tab selected in 
the Module Editor and I double click on a location in the coverage 
field, The Toolbox selects the right region in the .tla file, but it 
jumps to the PDF viewer rather than the .tla file viewer.

When the toolbox reports that TLC found an 
invariant violated, if the invariant is multi-line, it should print the 
message as

   Invariant <newline>
   the text of the invariant <newline>
   violated.
   
If the invariant is a single line (contains no newline characters), it 
should be printed as it now is:

   Invariant text-of-invariant violated
   
unless the text of the invariant is too long, in which case it should be
 printed as

   Invariant text-of-invariant<newline>
   violated.
   
How long is "too long" should be determined by experiment to ensure that
 the word "violated" is likely to be visible in the window.

Note: trailing spaces and newline characters should be removed from the 
invariant before trying to print it.

The following default settings should be 
made when creating  new model.  (The user can override them if he 
wants.)

1. If a spec contains the constant defaultInitValue, then it should  be 
set to a model value.  

2. If a spec contains a defined operator Spec whose level is temporal, 
then it should be made the temporal spec and that
     option chosen.  Otherwise, if it contains a defined operator Init 
whose level is state and a defined operator Next whose
     level is action, then they should be made the Init/Next spec.
     
These defaults (especially the first) will be most useful to specs that 
come from PlusCal algorithms.  We could limit their application to files
 that have PlusCal algorithms.  However, I suggest that we don't because
 the algorithm could be in an EXTENDed module.

I opened a spec and then did a SaveAs to 
save the root module under a different name in the same directory.  I 
then tried to open the root directory module.  It was not listed among 
the choices presented in the OpenModule menu.  When I clicked on 
AddModule, the browser came up showing the contents of the .toolbox 
directory.  When I selected the parent directory (that is, the spec's 
directory) and selected the root module from it, I go an error window 
saying 

   The provided module Euclid.tla is not located in the same directory 
as the root file.  Please select the module in \Euclid

Of course,  the module I selected, file Euclid.tla in directory 
...\Euclid, was the root file.

When I closed the spec and tried to reopen it, I got various errors 
saying the root file didn't exist and something indicating that it was 
looking in the .toolbox directory.

A user was confused when he edited his 
PlusCal file and hit translate without saving, and found that the spec 
he was running the model checker on hadn't changed.  This suggests that 
there should be a Save on Translate preference option that is selected 
by default.   We should probably also add a Translate on Save 
preference.

And this also raises the question of what should happen if the user 
tries to run the model checker (or validate a model) with an unsaved 
spec.  I suggest that the default behavior should be to raise a window 
asking the user if he wants to save it.  Note that this should be the 
case when there is any unsaved module that was part of the spec the last
 time the spec was parsed.

Now, to clone a model you have to go to the
 spec explorer--which means that no user will discover it by himself.  
And it's also inconvenient.  There should be an easy way to create a 
clone of the model.  Perhaps a Clone Model command on TLC Model Checker 
menu.

For some reason, Acrobat reader shows the 
pretty-printed version at an inconveniently large magnification.  I can 
reduce the size, but the next time I run the pretty-printer the pdf is 
shown at the same large magnification.  It would be nice if Acrobat 
could be called so it uses the magnification it had the last time--or at
 least the current magnification if it is already opened on the file.  
Alternatively (and perhaps in addition) it would be good to add a 
preference that specifies the magnification used when Acrobat opens the 
pdf file.  (This would have to be specified in a sufficiently generic 
way--e.g., as command-line arguments--so it could be used if the user 
has a different program for displaying pdf files.)

When computing the invariant on the initial
 state throws a stack overflow exception (because of an infinite 
recursion), TLC just reports

   %1%
   While working on the initial state:
   %2%
   
 I'm pretty sure it used to report the stack overflow, so this bug was 
probably added when the error reporting was rewritten.  However, the 
same useless error report is printed when TLC is run from a shell.

Created attachment 18 [details]
Modules and model

Running the Toolbox on the model for CastroLiskovBug produces an MC file that
reports an invariant failure, but the Toolbox reports that it has finished
without reporting an error (the statistics show one state left on the queue).

When  a model is locked, the user should 
still be able to open sections to examine them.   While a model is 
running, I'd like to see the model--for example, how many workers it's 
using, what the constraint is, etc.  It's a nuisance to start TLC and 
wonder what it's actually checking.  I just realized that I can do this 
by cloning the model.  But it would be better to make the model fully 
examinable, just not modifiable.   If that's hard, another possibility 
is to allow the user to unlock the running model and then relock it 
after opening the necessary sections.  This is dangerous, but the user 
would have to be pretty stupid to shoot himself in the foot.

When no spec is open and I select Open 
Spec/Add New Spec, the Browse button on the popup menu does nothing.  
However, if I do the same thing when a spec is open, the Browse button 
works fine.

When the checkpoints folder for a model 
contains a large number of files, the model editor becomes almost 
unusable. This occurs because the of a call to refreshLocal() in the 
method ModelHelper.getCheckpoints(). It refreshes the checkpoints 
folder, which in some case can mean refreshing the 1000s of files 
inside. This is slow. Based on the comments, this call to refreshLocal 
is sometimes necessary because the toolbox doesn't always recognize the 
checkpoint folder, but currently it occurs on every validation of the 
main model page, which is probably unnecessary. This call needs to be 
made more selectively.

Launching parsing by selecting the Parse 
Module/Spec menu item locks the UI while auto-parse on save runs in a 
separate thread. I think that parsing should always be run 
asynchronously.

Yuan has added a new run-time parameter to 
TLC: the number of megabytes of memory to be allocated to storing the 
fingerprints of found states.  This is specified with a new switch 
-fpmem ,as in

   -fpmem 100
   
The default value is 1/4 the maximum memory size that the JVW will 
assign to the program.   (This amount apparently grows with the Maximum 
JVM Heap Size parameter.)   This new parameter should appear both in the
 "How to Run" section of the Model Overview page and in the TLC model 
checker preferences page.  The user chooses the default by leaving the 
text box blank.  Only if the user specifies a values should the -fpmem 
argument be given to TLC.   

The parameter should be labeled Maximum FingerPrint Memory size in MB.

You can create such an error trace by 
checking deadlock in a spec that deadlocks in the initial state.

Why would I want to explore such an error trace?  Because it's a 
convenient way to evaluate expressions on a particular state.  (Perhaps 
that indicates a missing feature.)

The display of Invariants and  Properties 
on the Model Overview Page does weird and unsatisfying things when the 
one-line displayed entries get too wide.  In particular, the width of 
their column grows to accommodate the widest line, and cannot be shrunk 
even when the wide lines are eliminated--except by closing and reopening
 the model.   As I recall, there are serious problems trying to fix this
 with the Eclipse primitives.   So, I suggest the following change to 
ameliorate the problem:  On the displayed line, replace each sequence of
 spaces with a single space.

I was running a TLC model that, according 
to the log entry pasted below, ran TLC out of memory.  (Sorry for doing 
it this way, but I couldn't find the switch in the 747 cockpit that 
allows me to attach something to the bug report--though I'm sure I've 
stumbled upon it before.)   It would be nice if this could be prevented 
from crashing the Toolbox, but would simply cause it to report a TLC 
error.  Of course, if TLC running out of memory causes the Toolbox to 
run out of memory as well, this is likely to be impossible.  But I don't
 see why this should happen.  (Of course, I have a lot of trouble seeing
 why all the ways computer programs fail should happen.)   

eclipse.buildId=unknown
java.version=1.6.0_11
java.vendor=Sun Microsystems Inc.
BootLoader constants: OS=win32, ARCH=x86, WS=win32, NL=en_US
Framework arguments:  -product 
org.lamport.tla.toolbox.product.standalone.product
Command-line arguments:  -product 
org.lamport.tla.toolbox.product.standalone.product -data 
C:\users\lamport\tla\newtools\tla2-inria/../runtime-standalone.product 
-dev 
file:C:/users/lamport/tla/newtools/tla2-inria/.metadata/.plugins/org.eclipse.pde.core/standalone.product/dev.properties
 -os win32 -ws win32 -arch x86

!ENTRY org.eclipse.osgi 2 0 2010-04-22 09:21:38.625
!MESSAGE The following is a complete list of bundles which are not 
resolved, see the prior log entry for the root cause if it exists:
!SUBENTRY 1 org.eclipse.osgi 2 0 2010-04-22 09:21:38.625
!MESSAGE Bundle org.eclipse.jdt.launching.macosx_3.2.0.v20090527 [337] 
was not resolved.
!SUBENTRY 2 org.eclipse.jdt.launching.macosx 2 0 2010-04-22 09:21:38.625
!MESSAGE Platform filter did not match: (osgi.os=macosx)

!ENTRY org.eclipse.core.resources 2 10035 2010-04-22 09:21:39.750
!MESSAGE The workspace exited with unsaved changes in the previous 
session; refreshing workspace to recover changes.

!ENTRY org.eclipse.ui 2 0 2010-04-22 09:21:40.562
!MESSAGE Warnings while parsing the commands from the 
'org.eclipse.ui.commands' and 'org.eclipse.ui.actionDefinitions' 
extension points.
!SUBENTRY 1 org.eclipse.ui 2 0 2010-04-22 09:21:40.562
!MESSAGE Commands should really have a category: 
plug-in='org.lamport.tla.toolbox.tool.prover.ui', 
id='org.lamport.tla.toolbox.tool.prover.ui.checkStep.delegate', 
categoryId='org.eclipse.debug.ui.category.run'

!ENTRY org.eclipse.ui 4 4 2010-04-22 09:23:52.814
!MESSAGE Plugin org.lamport.tla.toolbox, extension 
org.eclipse.ui.perspectiveExtensions, id 
toolbox.view.ToolboxWelcomeView: Attribute 'relative' not defined.  This
 attribute is required when relationship="left".

!ENTRY org.eclipse.ui 4 4 2010-04-22 09:23:52.814
!MESSAGE Unable to process element: view in perspective extension: null

!ENTRY org.eclipse.ui 4 4 2010-04-22 09:24:31.268
!MESSAGE Plugin org.lamport.tla.toolbox, extension 
org.eclipse.ui.perspectiveExtensions, id 
toolbox.view.ToolboxWelcomeView: Attribute 'relative' not defined.  This
 attribute is required when relationship="left".

!ENTRY org.eclipse.ui 4 4 2010-04-22 09:24:31.268
!MESSAGE Unable to process element: view in perspective extension: null

!ENTRY org.eclipse.ui 4 4 2010-04-22 12:12:57.928
!MESSAGE Plugin org.lamport.tla.toolbox, extension 
org.eclipse.ui.perspectiveExtensions, id 
toolbox.view.ToolboxWelcomeView: Attribute 'relative' not defined.  This
 attribute is required when relationship="left".

!ENTRY org.eclipse.ui 4 4 2010-04-22 12:12:58.100
!MESSAGE Unable to process element: view in perspective extension: null

!ENTRY org.eclipse.ui 4 4 2010-04-22 12:13:51.304
!MESSAGE Plugin org.lamport.tla.toolbox, extension 
org.eclipse.ui.perspectiveExtensions, id 
toolbox.view.ToolboxWelcomeView: Attribute 'relative' not defined.  This
 attribute is required when relationship="left".

!ENTRY org.eclipse.ui 4 4 2010-04-22 12:13:51.319
!MESSAGE Unable to process element: view in perspective extension: null

!ENTRY org.lamport.tla.toolbox.tool.tlc 4 0 2010-04-23 23:14:47.975
!MESSAGE Error writing the TLC process output file for 
ByzPaxosConsensus___TinyModel.launch
!STACK 1
org.eclipse.core.runtime.CoreException: Could not write file: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC.out.

	at org.eclipse.core.internal.filesystem.Policy.error(Policy.java:55)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:386)

	at 
org.eclipse.core.internal.localstore.FileSystemResourceManager.write(FileSystemResourceManager.java:956)

	at 
org.eclipse.core.internal.resources.File.internalSetContents(File.java:320)

	at 
org.eclipse.core.internal.resources.File.appendContents(File.java:53)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink$1.run(FileProcessOutputSink.java:47)

	at 
org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1800)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink.appendText(FileProcessOutputSink.java:43)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.BroadcastStreamListener.streamAppended(BroadcastStreamListener.java:44)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.run(OutputStreamMonitor.java:257)

	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.notifyAppend(OutputStreamMonitor.java:267)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.fireStreamAppended(OutputStreamMonitor.java:116)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.read(OutputStreamMonitor.java:156)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.access$1(OutputStreamMonitor.java:134)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$1.run(OutputStreamMonitor.java:207)

	at java.lang.Thread.run(Thread.java:619)
Caused by: java.io.FileNotFoundException: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC.out
 (The process cannot access the file because it is being used by another
 process)
	at java.io.FileOutputStream.openAppend(Native Method)
	at java.io.FileOutputStream.<init>(FileOutputStream.java:177)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:377)

	... 15 more
!SUBENTRY 1 org.eclipse.core.filesystem 4 272 2010-04-23 23:14:49.928
!MESSAGE Could not write file: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC.out.
!STACK
 0
java.io.FileNotFoundException: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC.out
 (The process cannot access the file because it is being used by another
 process)
	at java.io.FileOutputStream.openAppend(Native Method)
	at java.io.FileOutputStream.<init>(FileOutputStream.java:177)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:377)

	at 
org.eclipse.core.internal.localstore.FileSystemResourceManager.write(FileSystemResourceManager.java:956)

	at 
org.eclipse.core.internal.resources.File.internalSetContents(File.java:320)

	at 
org.eclipse.core.internal.resources.File.appendContents(File.java:53)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink$1.run(FileProcessOutputSink.java:47)

	at 
org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1800)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink.appendText(FileProcessOutputSink.java:43)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.BroadcastStreamListener.streamAppended(BroadcastStreamListener.java:44)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.run(OutputStreamMonitor.java:257)

	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.notifyAppend(OutputStreamMonitor.java:267)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.fireStreamAppended(OutputStreamMonitor.java:116)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.read(OutputStreamMonitor.java:156)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.access$1(OutputStreamMonitor.java:134)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$1.run(OutputStreamMonitor.java:207)

	at java.lang.Thread.run(Thread.java:619)

!ENTRY org.lamport.tla.toolbox.tool.tlc 4 0 2010-04-23 23:22:10.093
!MESSAGE Error writing the TLC process output file for 
ByzPaxosConsensus___TinyModel.launch
!STACK 1
org.eclipse.core.runtime.CoreException: Could not write file: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC_TE.out.

	at org.eclipse.core.internal.filesystem.Policy.error(Policy.java:55)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:386)

	at 
org.eclipse.core.internal.localstore.FileSystemResourceManager.write(FileSystemResourceManager.java:956)

	at 
org.eclipse.core.internal.resources.File.internalSetContents(File.java:320)

	at 
org.eclipse.core.internal.resources.File.appendContents(File.java:53)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink$1.run(FileProcessOutputSink.java:47)

	at 
org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1800)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink.appendText(FileProcessOutputSink.java:43)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.TraceExplorerTraceSourceOutputSink.appendText(TraceExplorerTraceSourceOutputSink.java:53)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.BroadcastStreamListener.streamAppended(BroadcastStreamListener.java:44)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.run(OutputStreamMonitor.java:257)

	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.notifyAppend(OutputStreamMonitor.java:267)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.fireStreamAppended(OutputStreamMonitor.java:116)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.read(OutputStreamMonitor.java:156)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.access$1(OutputStreamMonitor.java:134)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$1.run(OutputStreamMonitor.java:207)

	at java.lang.Thread.run(Thread.java:619)
Caused by: java.io.FileNotFoundException: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC_TE.out
 (The process cannot access the file because it is being used by another
 process)
	at java.io.FileOutputStream.openAppend(Native Method)
	at java.io.FileOutputStream.<init>(FileOutputStream.java:177)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:377)

	... 16 more
!SUBENTRY 1 org.eclipse.core.filesystem 4 272 2010-04-23 23:22:10.093
!MESSAGE Could not write file: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC_TE.out.
!STACK
 0
java.io.FileNotFoundException: 
C:\users\lamport\papers\paxos\simple\byztla\ByzPaxosConsensus.toolbox\TinyModel\MC_TE.out
 (The process cannot access the file because it is being used by another
 process)
	at java.io.FileOutputStream.openAppend(Native Method)
	at java.io.FileOutputStream.<init>(FileOutputStream.java:177)
	at 
org.eclipse.core.internal.filesystem.local.LocalFile.openOutputStream(LocalFile.java:377)

	at 
org.eclipse.core.internal.localstore.FileSystemResourceManager.write(FileSystemResourceManager.java:956)

	at 
org.eclipse.core.internal.resources.File.internalSetContents(File.java:320)

	at 
org.eclipse.core.internal.resources.File.appendContents(File.java:53)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink$1.run(FileProcessOutputSink.java:47)

	at 
org.eclipse.core.internal.resources.Workspace.run(Workspace.java:1800)
	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.FileProcessOutputSink.appendText(FileProcessOutputSink.java:43)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.TraceExplorerTraceSourceOutputSink.appendText(TraceExplorerTraceSourceOutputSink.java:53)

	at 
org.lamport.tla.toolbox.tool.tlc.output.internal.BroadcastStreamListener.streamAppended(BroadcastStreamListener.java:44)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.run(OutputStreamMonitor.java:257)

	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.notifyAppend(OutputStreamMonitor.java:267)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.fireStreamAppended(OutputStreamMonitor.java:116)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.read(OutputStreamMonitor.java:156)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor.access$1(OutputStreamMonitor.java:134)

	at 
org.eclipse.debug.internal.core.OutputStreamMonitor$1.run(OutputStreamMonitor.java:207)

	at java.lang.Thread.run(Thread.java:619)

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:32:33.287
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space
	at java.util.Arrays.copyOf(Arrays.java:2882)
	at 
java.lang.AbstractStringBuilder.expandCapacity(AbstractStringBuilder.java:100)

	at 
java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:515)
	at java.lang.StringBuffer.append(StringBuffer.java:306)
	at 
org.eclipse.ui.editors.text.StorageDocumentProvider.setDocumentContent(StorageDocumentProvider.java:144)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.setDocumentContent(FileDocumentProvider.java:424)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.handleElementContentChanged(FileDocumentProvider.java:830)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$2.execute(FileDocumentProvider.java:274)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$SafeChange.run(FileDocumentProvider.java:163)

	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:134)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:32:38.444
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space
	at java.util.Arrays.copyOf(Arrays.java:2882)
	at 
java.lang.AbstractStringBuilder.expandCapacity(AbstractStringBuilder.java:100)

	at 
java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:515)
	at java.lang.StringBuffer.append(StringBuffer.java:306)
	at 
org.eclipse.ui.editors.text.StorageDocumentProvider.setDocumentContent(StorageDocumentProvider.java:144)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.setDocumentContent(FileDocumentProvider.java:424)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.handleElementContentChanged(FileDocumentProvider.java:830)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$2.execute(FileDocumentProvider.java:274)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$SafeChange.run(FileDocumentProvider.java:163)

	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:134)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:32:43.319
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space
	at java.util.Arrays.copyOf(Arrays.java:2882)
	at 
java.lang.AbstractStringBuilder.expandCapacity(AbstractStringBuilder.java:100)

	at 
java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:515)
	at java.lang.StringBuffer.append(StringBuffer.java:306)
	at 
org.eclipse.ui.editors.text.StorageDocumentProvider.setDocumentContent(StorageDocumentProvider.java:144)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.setDocumentContent(FileDocumentProvider.java:424)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.handleElementContentChanged(FileDocumentProvider.java:830)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$2.execute(FileDocumentProvider.java:274)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$SafeChange.run(FileDocumentProvider.java:163)

	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:134)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:36:25.073
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space
	at java.util.Arrays.copyOf(Arrays.java:2882)
	at 
java.lang.AbstractStringBuilder.expandCapacity(AbstractStringBuilder.java:100)

	at 
java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:515)
	at java.lang.StringBuffer.append(StringBuffer.java:306)
	at 
org.eclipse.ui.editors.text.StorageDocumentProvider.setDocumentContent(StorageDocumentProvider.java:144)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.setDocumentContent(FileDocumentProvider.java:424)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider.handleElementContentChanged(FileDocumentProvider.java:830)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$2.execute(FileDocumentProvider.java:274)

	at 
org.eclipse.ui.editors.text.FileDocumentProvider$SafeChange.run(FileDocumentProvider.java:163)

	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:134)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:36:30.011
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:36:34.026
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:36:38.105
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:36:42.120
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:40:27.937
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:40:32.047
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:40:36.078
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:40:40.109
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:40:44.172
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:43:47.566
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:43:51.613
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:43:55.613
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:44:30.285
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:46:51.273
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

!ENTRY org.eclipse.ui 4 0 2010-04-24 11:46:55.351
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable 
(java.lang.OutOfMemoryError: Java heap space)
	at org.eclipse.swt.SWT.error(SWT.java:3884)
	at org.eclipse.swt.SWT.error(SWT.java:3799)
	at 
org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:137)

	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3855)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3476)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
	at 
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

	at 
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)

	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:42)
	at 
org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

	at 
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)

	at 
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at 
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)

	at 
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)

	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1311)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1287)
Caused by: java.lang.OutOfMemoryError: Java heap space

The renumber proof command does not work if
 the proof contains steps that cannot have proofs (use/hide, instance, 
def). SANY does not seem to provide a way to get the location of the 
step number for these nodes, so this might motivate a change to SANY.

The Goto Declaration command does nothing 
with a subexpression name like Foo!2!(x).  The best one can do is to go 
to the definition of Foo if the user is  pointing at the "Foo".  

This will be difficult to fix and will require modifying how 
TLAHyperlinkDector.detectHyperlinks parses the region of the module 
being pointed at to obtain the operator name to look up.  Note that in 
Foo!Bar!<<!(x), the symbol to find is Foo!Bar, the "!<<!(x)"
 being a subexpression of that symbol's definition.  Since very few 
people will notice that this case isn't handled, fixing it has low 
priority.

Open a spec and run a TLC model on it, 
producing output on the TLC Console.  Then run the prover.  Clicking on 
the TLAPM Console raises the TLC Console.  There seems to be no way to 
get rid of it except to close the Toolbox.

Note: There should be a TLAPS Component as a bug attribute, but I don't 
know how to add one.

Goto Declaration (F3) and Show Declaration 
(F5) don't work if the cursor is on a symbol in a PICK or CASE statement
 of a proof.  They need to be tested to see if there are other places as
 well where they don't work.

I don't know what happened, but it's perhaps not a coincidence that this appeared after I partiallly fixed bug 88.

It takes the Toolbox much too long to parse
 and display TLC output when it gets long.  The only real examples I 
know of in which this is a problem are long uniprocess (sequential) 
PlusCal algorithms.  An example that illustrates the problem is in the 
module FindOp.tla appended to the TokenSpec class.  There are two kinds 
of output  involved:

- Error traces.   It can take effectively forever for TLC to process a 
long error trace.  Putting an "assert FALSE" statement at the end of the
 algorithm in FindOp.tla produces an error traces with about 1400 
states.  I have no idea how long it would take the Toolbox to process 
it, but I would guess it would be at least on the order of hours.

- Progress information.  I believe that it takes TLC about 20 seconds to
 process each progress report of FindOp.tla.  (TLC completes in about a 
second, so the problem is only in the final report.)  I believe that 
each progress report is about 1000 lines, where each line of output is a
 separate message.

Experimentation suggests that the majority of time taken processing the 
error trace is in displaying it.  However, a significant fraction 
(perhaps 1/3) is spent parsing the TLC output.  There seems to be no 
good reason for that--especially since the entire trace is just a single
 TLC message.  The parsing of TLC output needs to be completely 
rewritten so it is fast.  It's likely that displaying the trace cannot 
be made fast enough, in which case the user can be warned that the trace
 is long and given the option of displaying just a part of it.

When parsing the performance information is fast, we can figure out if 
displaying it is slow enough to require that something be done about it.

The following module produces a SANY error that is not reported by the Toolbox.

---- MODULE Test --------
Foo == 1

THEOREM TRUE
<1> QED
  BY DEF Foo.x'
================

As it says, the Launch Prover command (Ctl+G Ctl+P) does not check if the module has been saved.  It should.