# Bug 2

Summary: Product: Add way to tell if spec has changed since last run of a model, and to look at old spec if it has. TLA+ Toolbox Leslie Lamport TLC Component Dan Ricketts RESOLVED FIXED enhancement simon P3 unspecified x86 64-bit Windows ---

 Leslie Lamport 2009-11-18 02:42:11 UTC 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) Simon Zambrovski 2009-11-18 13:38:27 UTC I would make it transparently to the user. If the user clicks on the marker that is pointing to a changed file, the unchanged version should be shown. Dan Ricketts 2009-11-18 15:09:36 UTC When a user clicks on an action in the error trace or coverage table, what should happen? I think if the module has not been changed, the action should be highlighted in the writable version of the module. If the module has been changed, it should be highlighted in the read-only version. Leslie Lamport 2009-11-19 02:56:39 UTC It's not at all clear what the interface should be. If the user clicks on an error trace produced 6 months ago, he would reasonably expect it to show the saved module. On the other hand, suppose the user runs the model, clicks on the location of one error, corrects that error, saves the module, then clicks on the location of the next error. He would not be happy to find himself in the read-only saved version of the module. My initial thought is that, right next to the notification that the spec has been changed, there should be two buttons the user can push: one choosing the current spec and the other the original spec. (They could both be enabled if he has chosen "original spec" for a different model.) Whichever one he chooses, it's the modules of that spec that appear in all editor views. But that's just my initial thought. I expect I'll find problems with it if I think harder. Leslie Lamport 2010-01-26 12:05:52 UTC Here's Dan's and my current view on how saved modules should be handled. 1. Define the current version of a module to be the one in an open editor window, if there is one; else it's the version in the file. If the version of a module saved after running a model is not the current version, then the user should be able to open the saved version by using an option on the TLC Model Checker menu. Clicking on that option shows a list of all modules in the spec for which the saved version of he currently selected model is not the same as the current one. Clicking on one of them opens a read-only editor on that version as a separate tab in the model's view. 2. If the user double clicks on an action in the error-trace view, then this takes the user to the indicated location in the saved module iff (a) the saved version is not the current version and (b) the saved module is open in a tab in the model. Dan Ricketts 2010-06-15 12:08:53 UTC I implemented what is described in comment 4 with a modification to item 2. That item is now If the user double clicks on an action in the error-trace view, then this takes the user to the indicated location in the saved module iff the saved module is open in a tab in the model. The toolbox does not check if the saved version is not the current version.

# Bug 3

Summary: Product: Add reporting of fingerprint collision probability TLA+ Toolbox Dan Ricketts TLC Component Dan Ricketts RESOLVED FIXED enhancement P3 unspecified All All ---

 Dan Ricketts 2009-11-18 13:56:34 UTC 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

# Bug 4

Summary: Product: Cannot get the default VM install on Mac OS to run TLC TLA+ Toolbox Dan Ricketts TLC Component Simon Zambrovski RESOLVED FIXED blocker simon P1 unspecified x86 32-bit Mac OS ---

 Dan Ricketts 2009-11-19 13:24:59 UTC In TLCProcessJob, the method JavaRuntime.getDefaultVMInstall() returns null on Mac OS. A non-null value is required to run TLC. Simon Zambrovski 2009-11-27 22:51:38 UTC On Leopard, Carbon, 32Bit delivers the code, run in Eclipse (not RCP) IVMInstall install = JavaRuntime.getDefaultVMInstall(); System.out.println(install); -> org.eclipse.jdt.internal.launching.macosx.MacOSXVMInstall@31d55cc System.out.println(install.getInstallLocation()); -> /System/Library/Frameworks/JavaVM.framework/Versions/1.5.0/Home Simon Zambrovski 2009-11-27 23:01:00 UTC The same platform / installation delivers null in RCP mode. (In reply to comment #1) > On Leopard, Carbon, 32Bit delivers the code, run in Eclipse (not RCP) > > IVMInstall install = JavaRuntime.getDefaultVMInstall(); > System.out.println(install); > -> org.eclipse.jdt.internal.launching.macosx.MacOSXVMInstall@31d55cc > System.out.println(install.getInstallLocation()); > -> /System/Library/Frameworks/JavaVM.framework/Versions/1.5.0/Home Simon Zambrovski 2009-11-27 23:02:23 UTC Another reference describing the same bug: http://www.eclipse.org/forums/index.php?t=msg&goto=495006&S=af54b9bdf2bc342a1f3154a501e149b5 Dan Ricketts 2009-11-28 16:13:07 UTC I posted the message that you linked to in the last comment. Simon Zambrovski 2009-12-16 16:36:20 UTC Added the plugin dependency to org.eclipse.jdt.launching.macosx to enable Mac OSx support. Could someone try if it solved the problem? Simon Zambrovski 2009-12-17 13:55:51 UTC Adding a mandatory reference to the OS-dependent plugin was wrong and didn't allow to run the dependent plugin on other platforms. But I made the reference "optional" (click on properties in the plugin.xml editor, dependency tab). Please try if it works.

# Bug 5

Summary: Product: The help view does not always receive focus when the user clicks help TLA+ Toolbox Dan Ricketts TLA+ Toolbox Help Dan Ricketts RESOLVED FIXED normal simon P3 unspecified All All ---

 Dan Ricketts 2009-11-19 15:01:30 UTC 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. Dan Ricketts 2009-11-19 15:48:23 UTC This is now fixed by activating the help view in HelpHandler after it is opened by displayDynamicHelp(). In cases where the view already receives focus, this has no effect. In cases when it previously did not receive focus, activating the help view gives it focus.

# Bug 6

Summary: Product: The rename spec command does not behave properly TLA+ Toolbox Dan Ricketts Core Component Dan Ricketts RESOLVED FIXED normal simon P3 unspecified All All --- mylyn/context/zip

 Dan Ricketts 2009-11-19 16:09:23 UTC 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. Dan Ricketts 2009-11-27 16:51:01 UTC I changed the renaming validation method to check if any specifications exist that have the same name but a different case. I cannot reproduce the problem that I said occured when there exists a folder newName.toolbox that has not been opened as a specification and the user renames an open specification to "newName". I will assume that I made this problem up, so the rename spec bug has been fixed. Dan Ricketts 2009-11-27 16:51:03 UTC Created attachment 2 [details] mylyn/context/zip

# Bug 7

Summary: Product: Parsing errors in the MC file contain "Encountered ----" sometimes TLA+ Toolbox Dan Ricketts TLC Component Dan Ricketts NEW --- minor simon P4 unspecified All All ---

 Dan Ricketts 2009-11-25 15:09:36 UTC 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. Leslie Lamport 2009-11-27 23:29:22 UTC I wouldn't bother worrying about that. The message is nicely ambiguous, since it could be interpreted to mean that the parser encountered something that it either can't or isn't bothering to tell you what. More confusing is the stack trace part of the message that talks about line numbers in the MC file. I'd suggest subtracting the suitable number from the line numbers so numbers from 1 through the number of lines in the expression correspond to what the user typed. This will leave most of the line numbers in the stack trace negative, which will tell the user that these are not lines he should expect to see. However, this has low priority.

# Bug 8

Summary: Product: Add module-editor line width preference TLA+ Toolbox Leslie Lamport TLA+ Editor Dan Ricketts RESOLVED FIXED enhancement simon P4 unspecified All All ---

 Leslie Lamport 2009-11-30 02:10:38 UTC 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". Simon Zambrovski 2009-11-30 11:54:50 UTC The preference renaming is moved to the separate Bug 9. Simon Zambrovski 2009-11-30 12:02:26 UTC What is to do with those numbers, M, N, P and Q? The formulas are not needed for determination of width of new modules (it is trivial, since the content of the module is stored in a template). I don't see any other purpose of the editor width, beyond the usage in the formater. Writing a formater is a task which is usually more than finding out how long the line is. The GENERAL setting of the TEXT EDITOR (not TLA+ Editor) should not be changed.

# Bug 9

Summary: Product: Rename Preference Pages TLA+ Toolbox Simon Zambrovski Core Component Dan Ricketts RESOLVED FIXED minor simon P3 unspecified All All --- mylyn/context/zip

 Simon Zambrovski 2009-11-30 11:55:46 UTC Rename the items under TLA+ Preferences to remove "Preferences" from their names -- e.g., change "TLA+ Parser Preferences" to "TLA+ Parser". Dan Ricketts 2009-12-10 12:53:42 UTC Created attachment 3 [details] mylyn/context/zip

# Bug 10

Summary: Product: Eclipse buttons don't work on Linux ubuntu 9.10 TLA+ Toolbox Simon Zambrovski Core Component Dan Ricketts RESOLVED FIXED critical bugzilla.tlaplus.net, simon P3 unspecified x86 64-bit Linux --- 116

 Simon Zambrovski 2009-11-30 17:16:33 UTC 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) Dan Ricketts 2009-12-04 17:22:57 UTC This is not a memory issue. The physical memory usage of the toolbox on startup was only 60MB on his machine. He was unable to open a spec because the Finish button did not work properly on the New Spec Wizard on his machine. In particular, clicking on it does nothing. There is at least one other way to actually select Finish: hold Control and press Enter. It turns out this is an eclipse bug. The same thing occurs with some buttons in eclipse on ubuntu Karmic. This problem is listed many times on bug lists. For example, https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257 https://bugs.launchpad.net/gtk/+bug/442078/comments/28 https://bugs.launchpad.net/ubuntu/+source/eclipse/+bug/443004 From what I've gathered from these bug lists, the most recent release of ubuntu (and maybe some past releases) contains an updated version of gtk, which I've learned is a widget toolkit for greating GUIs. The second link explains that if eclipse had used gtk properly in the past, then this new version would not cause problems, but evidently, eclipse has been using gtk in strange ways that only happened to work on past version but don't work on this new version. The button clicking bug is just one of the problems that exists in eclipse on the newest version of ubuntu. Some of the messages in the first link explain that eclipse 3.5.2 and 3.6 appear to fix the problem, but these versions are still in development. We could get one of the builds of 3.5.2 and use this as the new target platform, but since its not officially released, who knows what bugs this would introduce. This seems like a bad option to me. According to a message on the first link, the target date to release 3.5.2 is February 26, 2010. The GTK developers included a flag that allows the previous behavior of GTK to be used by an application. This flag is set by setting the the environment variable GTK_NATIVE_WINDOWS=1 . I tried this on the linux machine I've been using in Orsay, and it does seem to fix the problem. The only way I've found to set this is to run the command export GTK_NATIVE_WINDOWS=1 in a shell and then run the toolbox from that shell. It would be annoying for the user to have to do this every time, so it might be better to just include those two commands in a shell script that the user would run. We could do this while waiting for eclipse 3.5.2 to be released. Or maybe there is a nicer way to set this flag that I haven't found. Another option as Leslie suggested is to just put a message in every wizard and dialog explaining what to do if clicking on a button doesn't work. Unfortunately, there may be issues with widgets in the toolbox besides buttons that we haven't discovered. Any thoughts on this? Dan Ricketts 2009-12-10 12:44:31 UTC This is a slightly updated description of the bug. Some buttons don't work properly on Eclipse and the Toolbox on some platforms. In particular, any platform that uses GTK+ version 2.18 (the latest version) will experience this bug. The desktop environment GNOME uses GTK+ as its base widget toolkit, and the latest version of GNOME (released in September, 2009) uses GTK+2.18. GNOME is the default desktop environment for Fedora, Debian, Ubuntu, and OpenSolaris, so those systems with the latest version of GNOME probably experience the problem. We don't have a distribution for Solaris, so I guess that's not an issue right now. The wikipedia page for GTK+ lists a few other desktop environments that use GTK+ and can run on Linux machines. They are Xfce, LXDE, and ROX Desktop. They don't seem to be very widely used, but we can note those on the website just in case. The complete extent of the bug is not clear. However, from the bug forums and from my tests in Orsay, I believe that the button problem only occurs with the default button in a dialog or wizard. The default button is usually a different color and can be selected by pressing Enter (when they work properly). On platforms with the bug clicking on these buttons will cause the button to appear pressed, but nothing else will happen. If this happens, the user should try one or more of the following: 1.) Press Enter 2.) Hold Control and press Enter 3.) Let the mouse hover over the button and press Enter 4.) Let the mouse hover over the button and press Space There may be other ways to select the buttons, but these are the one's that people have mentioned in the bug forums. Its also worth noting that if a user experiences any other strange behavior with a widget on one of those platforms, then there's a good chance its the same bug. Some of the posts on the bug forums mentioned other problems with GTK+ 2.18 besides the buttons. I don't believe these problems are relevant to the Toolbox, but there may be some other non-button problems that are. The workaround provided by the GTK+ developers is to set GDK_NATIVE_WINDOWS=true in a shell before launching the toolbox (or eclipse) from that shell. This causes GTK+ to behave as it did before 2.18. The real fix will be provided in Eclipse 3.5.2 which is scheduled for release on February 26, 2010. Dan Ricketts 2010-02-02 15:12:20 UTC The trace explorer buttons for Explore and Restore seem to be affected by this bug. Markus Alexander Kuppe 2011-05-11 16:45:40 UTC Once fixed the system specific Instructions for Linux [0] can be removed from the web page. [0] http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#downloading Markus Alexander Kuppe 2011-07-01 20:08:42 UTC The new Maven/Tycho based build has upgraded the toolbox dependency to Eclipse 3.6, marking as fixed.

# Bug 11

Summary: Product: Add the notion of a model being locked TLA+ Toolbox Dan Ricketts TLC Component Dan Ricketts RESOLVED FIXED enhancement simon P3 unspecified All All ---

 Dan Ricketts 2009-11-30 18:18:27 UTC 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. Dan Ricketts 2009-12-02 17:57:10 UTC I'll add a field to the TLC preference page that specifies how long the model must run in order to remain locked when TLC terminates. I'll add a lock and an unlock button to the toolbars that currently contain the buttons for running, validating, and stopping. I think there should be a notion of an explicit user lock and an automatic lock. A user lock occurs when the user clicks on the lock button. An automatic lock occurs when TLC starts. A model with a user lock can only be unlocked when the user clicks the unlock button. A model with an automatic lock can be unlocked if TLC terminates in less than the specified time or if TLC terminates in more than the specified time and the user clicks the unlock button after TLC completes. If a user locks a model while there is an automatic lock (he clicks the lock button while the model is running), then the user lock replaces the automatic lock. When the model is locked, all fields in the model editor will be disabled (they will have the grayed out look, and the user will not be able to edit them). The lock button will be enabled when TLC is running and the unlock button will be disabled. When TLC is not running, the unlock button will be enabled only when the model is locked and the lock button will be enabled only when the model is unlocked. Leslie Lamport 2009-12-02 23:38:13 UTC This sounds good. Dan Ricketts 2009-12-07 11:23:17 UTC Should the user be able to rename the model when it is locked? Leslie Lamport 2009-12-07 19:14:44 UTC It doesn't matter whether or not the user is allowed to rename a locked model. (If he is allowed to remain it, that shouldn't unlock it.)

# Bug 12

Summary: Product: Toolbox checking unselected behavior spec options. TLA+ Toolbox Leslie Lamport Core Component Dan Ricketts RESOLVED FIXED normal simon P3 unspecified x86 64-bit Windows --- a spec

 Leslie Lamport 2009-12-02 23:44:42 UTC 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. Dan Ricketts 2009-12-03 00:10:14 UTC I can't seem to reproduce this error. Can you send me the spec and model that caused this problem? Dan Ricketts 2009-12-07 11:25:32 UTC Since this does not seem to be reproducible, I'm marking it as worksforme. Leslie Lamport 2009-12-21 02:39:24 UTC Created attachment 4 [details] a spec see description Leslie Lamport 2009-12-21 02:50:29 UTC Open a new spec with this root file. Create a model for it, assigning arbitrary small integer values to M and N and using Init and Next as the initial predicate and next-state action. Add the invariant (x=y) => x = GCD(M, N) Run the model. It will produce an error, which you can ignore. Now enter ===== right before the CONSTANTS declaration and save the module. Go to the model and validate it. Depending on the Toolbox's mood, you'll get 5 or 7 errors. If you get 7 errors, two of them will be complaining about Init and Spec. But you may get only 5, in which case it is correctly complaining about the bad Invariant. However, it's impossible to remove the invariant because the invariant section can't be opened. This is not a terrible problem; one just has to add a variable to the spec. But it's a nuisance--especially if the randomly occurring complaint about Init and Spec occurs. Leslie Lamport 2009-12-21 16:01:12 UTC The statement in my previous comment that the 5 errors in the Invariant are not a bug was wrong. You can't check invariants or other properties if there's no spec, so they should be ignored in that case. Other parts of the model that should be disabled and ignored when there's no behavioral spec are: - Recover from Checkpoint - Number of workers - State and Action constraint - TLC Options Dan Ricketts 2010-01-27 15:40:14 UTC I don't believe that number of workers makes any difference. The toolbox was already disabling the invariants and properties sections but was not ignoring them when it launched TLC. It now ignores them. It also ignores checkpoint recovery, state and action contraints, and anything in the TLC Options section. I found that disabling the State Constraints, Action Constraints, and TLC Options sections creates some bizarre behavior on the Advanced Options page, so I decided not to do this.

# Bug 13

Summary: Product: Trace exploration TLA+ Toolbox Dan Ricketts TLC Component Dan Ricketts RESOLVED FIXED enhancement simon P3 unspecified All All ---

 Dan Ricketts 2009-12-07 11:22:48 UTC 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. Dan Ricketts 2009-12-07 17:00:12 UTC Currently, I think the TLC Error View should contain a section that looks the same as the invariants or the properties sections. This would require some re-implementation of the lower part of the view's sash form, but I think this would be a nice interface. In addition to the Add, Edit, and Remove buttons, the section will contain a run button. I'm not yet sure where the best place for this button is. Its necessary to determine if an expression contains primed variables. We could do this by providing the user with a checkbox for each expression that indicates if it has primed variables. We could also run SANY to determine if an expression has primed variables. This would require running SANY once to determine which expressions have primed variables, once to parse the initial predicate and next-state relations that are generated for exploring the trace, and once when TLC runs. I think it is preferable to provide the user with a checkbox and display the error produced by TLC if the user makes the wrong selection. Clicking the run button will execute the trace explorer, unless one of the following conditions is true: 1.) The model is unlocked and the spec is not parsed. 2.) The model has a validation error (If the validation error is in the spec, init and next, invariants, properties, or constraints sections, this should not prevent the user from running the trace explorer, although this might be a little more difficult to implement). If one of these conditions is true, then an error window will pop up explaining the error. If neither is true, the following steps will occur: 1.) The toolbox will run SANY to validate the expressions. If there are errors, these will be displayed as red error bubbles (the same as in the model editor). 2.) If SANY finds no errors, TLC will be run to evaluate the expression at each state of the trace (If the expression contains primed variables, then it cannot be evaluated for the last state of the trace). 3.) If TLC produces an error evaluating the expressions at any state, then I think this error should be appended to the existing message in the error box at the top of the error view. Another option is to have a separate box for reporting errors from evaluating expressions for trace exploration. A third option is to display the errors in error bubbles as with validation errors. 4.) If TLC does not produce an error, then the existing error trace will be replaced with a new error trace. Each state will be identical to the corresponding state in the previous trace except that there will be one additional row for each expression that was evaluated. The left column of a row corresponding to an expression will have the expression and the right column will have its value. If an expression contains primed variables, then the value column of its row in the final state will have something like "--" to indicate that it cannot be evaluated. A while ago Leslie and I discussed the meaning of primed variables when exploring the error trace. I'm not sure if we came to a conclusion on this point, but I think that if an expression contains the primed value of a variable x, then the value of that expression at state number z should use the value of x in state number z+1. For example, consider the following trace. STATE 1: /\ x = 0 /\ y = 0 STATE 2: /\ x = 1 /\ y = 0 STATE 3: /\ x = 2 /\ y = 1 STATE 4: /\ x = 3 /\ y = 3 If the user wants to evaluate the expression x'+y, then I think he should see the following trace. STATE 1: /\ x = 0 /\ y = 0 \* x'+y = 1 STATE 2: /\ x = 1 /\ y = 0 \* x'+y = 2 STATE 3: /\ x = 2 /\ y = 1 \* x'+y = 4 STATE 4: /\ x = 3 /\ y = 3 \* x'+y = "--" The other option, which would be easier to implement, but which makes less sense to me would be to display the following trace. STATE 1: /\ x = 0 /\ y = 0 \* x'+y = "--" STATE 2: /\ x = 1 /\ y = 0 \* x'+y = 1 STATE 3: /\ x = 2 /\ y = 1 \* x'+y = 2 STATE 4: /\ x = 3 /\ y = 3 \* x'+y = 4 In the preceding trace, the value of x' in the second state is equal to the value of x in the second state instead of the value of x in the third state. Dan Ricketts 2009-12-07 17:30:49 UTC 1.) Create three new files in the model folder, TE.tla, TE.cfg, TE.out (TE stands for trace explorer, might need to choose something that the user is less likely to choose as a module name). 2.) For each expression the user enters for trace exploration, assign an identifier that is unlikely to appear in the spec. Declare these identifiers as variables in TE.tla. Alternatively, the user could be responsible for assigning identifiers to expressions. 3.) Fill TE.cfg and TE.tla with the values of constants, additional definitions, definition overrides, and additional model values. 4.) Write the initial predicate and next-state relation to TE.cfg and TE.tla. This is best illustrated with an example. The trace is the following: STATE 1: /\ x = 0 /\ y = 0 STATE 2: /\ x = 1 /\ y = 0 STATE 3: /\ x = 2 /\ y = 1 STATE 4: /\ x = 3 /\ y = 3 The user wants to evaluate two expressions: x + y x' > y The file TE.tla will define two new variables: VARIABLES sum, big The variables are named "sum" and "big" for the simplicity of this example. In reality they will be something like "trace_2348902347238", unless the user is responsible to assigning labels to the expressions. The file will also define two new identifiers: sum_def == x + y big_def == x' >y We define the initial predicate and next-state relation as follows: TInit == /\ x = 0 /\ y = 0 /\ sum = sum_def /\ big = "--" TNext == \/ /\ x = 0 /\ y = 0 /\ x' = 1 /\ y' = 0 /\ sum' = sum_def' /\ big' = big_def \/ /\ x = 1 /\ y = 0 /\ x' = 2 /\ y' = 1 /\ sum' = sum_def' /\ big' = big_def \/ /\ x = 2 /\ y = 1 /\ x' = 3 /\ y' = 3 /\ sum' = sum_def' /\ big' = big_def The expression defined by big_def has primed variables so the variable big takes the value "--" in the initial state predicate. The expression defined by sum_def does not contain primed variables. This will produce an error trace by defining the invariant: ~(x=3/\y=3) The TLC Error View will have to alter this error trace if it is to display it in the way I described in the previous comment. In particular, the value of big must be shifted up one state and the last state should have that big = "--". Thus, the value of big in the second state will be displayed with the first state in the error view. The toolbox will call TLC on the root file TE.tla with config file TE.cfg and write its output to TE.out. Dan Ricketts 2009-12-07 18:15:23 UTC One question that I forgot to put in the first comment. When the model is unlocked, should running the trace explorer cause module files to be recopied to the model directory? Leslie Lamport 2009-12-07 19:57:57 UTC  Currently, I think the TLC Error View should contain a section that looks the same as the invariants or the properties sections. This would require some re-implementation of the lower part of the view's sash form, but I think this would be a nice interface. In addition to the Add, Edit, and Remove buttons, the section will contain a run button. I'm not yet sure where the best place for this button is. The button should be the same place as the Add/Edit/Remove buttons. And it should be an "explore" button. The button to restore the original trace (see below) should be in the same place. Its necessary to determine if an expression contains primed variables. We could do this by providing the user with a checkbox for each expression that indicates if it has primed variables. We could also run SANY to determine if an expression has primed variables. This would require running SANY once to determine which expressions have primed variables, once to parse the initial predicate and next-state relations that are generated for exploring the trace, and once when TLC runs. The second run of SANY isn't necessary. If the expressions parse correctly in the first parse, then the initial predicate and next-state actions that the Toolbox creates will also parse correctly. (This isn't completely trivial, but it's easy to ensure. For example, the first module that SANY parses should declare the new variables to make sure that they are legal variable names.) I think it is preferable to provide the user with a checkbox and display the error produced by TLC if the user makes the wrong selection. Since it doesn't require an extra parse, the Toolbox should determine this by itself. Clicking the run button will execute the trace explorer, unless one of the following conditions is true: 1.) The model is unlocked and the spec is not parsed. 2.) The model has a validation error (If the validation error is in the spec, init and next, invariants, properties, or constraints sections, this should not prevent the user from running the trace explorer, although this might be a little more difficult to implement). It's not worth worrying about this. The explorer should be run only if there is no validation error. If one of these conditions is true, then an error window will pop up explaining the error. If neither is true, the following steps will occur: 1.) The toolbox will run SANY to validate the expressions. If there are errors, these will be displayed as red error bubbles (the same as in the model editor). 2.) If SANY finds no errors, TLC will be run to evaluate the expression at each state of the trace (If the expression contains primed variables, then it cannot be evaluated for the last state of the trace). 3.) If TLC produces an error evaluating the expressions at any state, then I think this error should be appended to the existing message in the error box at the top of the error view. Another option is to have a separate box for reporting errors from evaluating expressions for trace exploration. A third option is to display the errors in error bubbles as with validation errors. The original error should not be destroyed or mucked with. Remember That it might have taken TLC a week to produce that message. I suggest that in case trace exploration yields an error, that error should replace the original error in the window--with some clear indication that the error occurred in trace exploration. If the exploration also produces an error trace, then that trace should be displayed in the trace view. If the trace explorer succeeds on the next try, the original error message is restored. When the user clicks on the button to restore the original trace (see below), that should also restore the original error message. 4.) If TLC does not produce an error, then the existing error trace will be replaced with a new error trace. This replacement is not permanent. The original error trace must be saved, and there must be a button that permits the use to restore it. Each state will be identical to the corresponding state in the previous trace except that there will be one additional row for each expression that was evaluated. The left column of a row corresponding to an expression will have the expression and the right column will have its value. If an expression contains primed variables, then the value column of its row in the final state will have something like "--" to indicate that it cannot be evaluated. A while ago Leslie and I discussed the meaning of primed variables when exploring the error trace. I'm not sure if we came to a conclusion on this point, but I think that if an expression contains the primed value of a variable x, then the value of that expression at state number z should use the value of x in state number z+1. For example... Yes, that's correct 1.) Create three new files in the model folder, TE.tla, TE.cfg, TE.out (TE stands for trace explorer, might need to choose something that the user is less likely to choose as a module name). TE is fine. As with MC, the user shouldn't be allowed to create a module named TE. 2.) For each expression the user enters for trace exploration, assign an identifier that is unlikely to appear in the spec. Declare these identifiers as variables in TE.tla. Alternatively, the user could be responsible for assigning identifiers to expressions. It's better to have the user choose the identifier. If the user defines Sum2 == x'+y Then the error trace would contain something like STATE 1: /\ x = 0 /\ y = 0 /\ Sum2 = 1 STATE 2: /\ x = 1 /\ y = 0 /\ Sum2 = ... One reason for this is that it would be good to allow the user to change which variables' values are displayed and in what order. If this feature is implemented, Sum2 would be treated as just another variable like x and y. Dan Ricketts 2010-01-27 11:43:23 UTC When the trace from the trace explorer is shown for a given model, it will continue to be shown in the error view for that model unless model checking is run, the restore button is pressed, or the error hyperlink on the results page is pressed. Closing and re-opening the toolbox, switching to another model and back, closing and re-opening using the menu item in the TLC menu will show in the error whatever errors were previously there for that model (errors from the trace explorer or errors from model checking). I decided to make the hyperlink on the results page restore the original error/trace in case the trace explorer somehow messes up the error view so that the restore button does not appear.

# Bug 14

Summary: Product: The column numbers do not appear in module editor TLA+ Toolbox Dan Ricketts TLA+ Editor Dan Ricketts RESOLVED FIXED minor simon P3 unspecified All All ---

 Dan Ricketts 2009-12-07 13:53:32 UTC 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. Dan Ricketts 2010-01-29 13:13:01 UTC I created a class TLAMultiPageEditorActionBarContributor that acts as the contributor class for the TLAEditorAndPDFViewer class that is the editor for TLA modules. The contributor adds the cursor position to the status line at the bottom of the toolbox when a text editor is active. I also re-added the Content Assist and Content Tip menu items to the edit menu that I had removed when I made the editor for tla modules into a multi page editor. I'm not sure what the Content Tip item does, but it was there before.

# Bug 15

Summary: Product: Rename or deleting root file outside toolbox produces incorrect editor page TLA+ Toolbox Dan Ricketts TLA+ Editor Markus Alexander Kuppe NEW --- minor bugzilla.tlaplus.net, simon P3 unspecified All All ---

# Bug 98

Summary: Product: Toolbox incorrectly reports which invariant is violated if some members of the list of invariants are unchecked TLA+ Toolbox Chris Newcombe TLC Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All All --- Screenshot of unselected, yet checked invariant

 Chris Newcombe 2011-04-03 20:39:29 UTC Toolbox incorrectly reports which invariant is violated if some members of the list of invariants are unchecked Running Version 1.2.1 of 29 September 2010 (32-bit), on Windows 7 (64-bit). First bug: I have a list of 3 invariants to be checked (in the Model Overview page). When all of them are enabled (checked), everything seems to work fine. I temporarily unchecked the second (middle) invariant in the list (first time I’ve used this feature). I ran the model-checker, knowing that the 3rd invariant in the list would be violated by my current spec/model. The toolbox incorrectly reported that the second (unchecked) invariant was the one that was violated. Examining the TLC error trace, I am sure that it was really the 3rd invariant that was violated. i.e. Model checking appears to have been done correctly, but the toolbox incorrectly reported which invariant was violated. Presumably due to a bug in the handling of unchecked invariants. Second related bug: After the above problem, I completely removed the middle (unchecked) invariant, by clicking the 'Remove' button. I re-ran the model checker. The toolbox again incorrectly reported that the (now removed) second invariant was the one that was violated. I then removed all of the invariants (leaving an empty list). I added back one invariant -- the one I knew would fail. Again the toolbox reported that the wrong invariant was violated -- it reported that the original 1st invariant was violated, when that invariant didn't even appear in the list anymore. Leslie Lamport 2011-04-09 21:18:18 UTC I was able to reproduce this bug on my Windows 7 64-bit machine with a 4-core Intel Xeon CPU. It does not occur on my Vista 32-bit 2-core machine. Also, when I tried to reproduce the bug again on my 64-bit machine, it didn't occur. The bug is in the Toolbox, not in TLC. It smells like a concurrency bug--especially since I have observed that the 64-bit machine seems to be good at revealing concurrency bugs, probably because it uses a weaker memory model than the 32-bit one. The code that finds and reads the TLC output is too complicated and requires too much knowledge of the Eclipse infrastructure for me to understand. Markus Alexander Kuppe 2015-02-23 11:34:44 UTC Another incarnation is that TLC checks *no* invariant even though a (single one) is checked in the model editor. I have yet to reproduce this though. Markus Alexander Kuppe 2015-03-05 09:02:57 UTC Created attachment 198 [details] Screenshot of unselected, yet checked invariant I got bitten by this again yesterday. The Toolbox checked the TypeOK invariant even though it wasn't selected (see screenshot). I wonder if it even checked the selected ones. Markus Alexander Kuppe 2015-03-18 18:25:22 UTC http://tlaplus.codeplex.com/SourceControl/changeset/b00cb4336eeed3fd82cfd0d8170bc57c305a40e2 causes the Toolbox to properly lock the workspace before it writes files to launch the model checker. This makes sure that it can't interfer with other background operations that write to files. I hope that this change addresses this bug too. Markus Alexander Kuppe 2015-03-20 16:41:13 UTC Below is an updated stacktrace with current line numbers: Negative seek offset at java.io.RandomAccessFile.seek(Native Method) at tlc2.util.BufferedRandomAccessFile.seek(BufferedRandomAccessFile.java:212) at tlc2.tool.liveness.DiskGraph.getNode(DiskGraph.java:169) at tlc2.tool.liveness.DiskGraph.getPath(DiskGraph.java:310) at tlc2.tool.liveness.LiveWorker.printTrace(LiveWorker.java:603) at tlc2.tool.liveness.LiveWorker.checkComponent(LiveWorker.java:373) at tlc2.tool.liveness.LiveWorker.checkSccs(LiveWorker.java:163) at tlc2.tool.liveness.LiveWorker.run(LiveWorker.java:613) Markus Alexander Kuppe 2015-05-12 13:55:45 UTC Fixed with 1.5.0 Markus Alexander Kuppe 2015-10-06 06:53:59 UTC The fix in 1.5.0 turns out to be incomplete. Thus, a workaround has been put in place [1] that caches the invariant list upon model checking start-up as fall-back. [1] https://tlaplus.codeplex.com/SourceControl/changeset/72a66a7ecd246018aaf5c1bfbe89dbe2280cb46d

# Bug 100

Summary: Product: Toolbox in confused state after system restart during model-checking TLA+ Toolbox Chris Newcombe TLC Component Dan Ricketts RESOLVED WONTFIX normal simon P3 unspecified x86 64-bit Windows ---

 Chris Newcombe 2011-04-03 20:45:54 UTC Running Version 1.2.1 of 29 September 2010 (32-bit) on Windows 7 Enterprise 64-bit, on a 4-proc 4GB ThinkPad laptop. Sequence of events: 1. TLC was checking a model. (I can't remember if it was doing it in the background.) 2. I had to do a system restart to install an update of some unrelated software (Adobe Reader). 3. After the restart I ran the toolbox and found that: - TLC is not running (not surprising, as I haven't restarted it.) - The Model Overview tab says "(model checking is in progress)" - The "How to run" options are all greyed out. The "Checkpoint Id" and "Checkpoint Size" are populated with reasonable values, but they are greyed-out. - The "Model Checking Results" tab says "Current Status: Not running" and "Errors detected: No Errors". The "State space progress" box lists the last few state reports (from before the system restart) - The 'Stop model checker' button (small red square) was enabled, but had no apparent effect when clicked. Note: I did previously stop this TLC run, and restart from a checkpoint, without any problems. But I didn't do a system-restart that time. I worked around this by cloning the model. So it's not a severe problem, just confusing at first. The cloned model initially had 1 error, that there was no checkpoint state. I realized that this was because the 'restart from checkpoint' box was already checked for the clone (it was also checked on the original model). I unchecked the box, and could then run TLC as normal. Leslie Lamport 2011-04-07 20:12:20 UTC This is a known behavior, documented in the Help pages, for which the Toolbox provides the repair menu item for a model in the spec explorer.

# Bug 101

Summary: Product: Absolute path names in .toolbox directory files prevents opening existing specs that have been moved. TLA+ Toolbox Leslie Lamport Core Component Dan Ricketts RESOLVED WORKSFORME normal simon P2 unspecified All Windows ---

 Leslie Lamport 2011-04-07 20:14:38 UTC A Spec's .toolbox directory has data files containing absolute path names of files. This causes havoc if one copies an existing spec--for example, from another machine--and tries to open it without copying it to a directory with exactly the same path name. A possible bug fix is to rewrite the offending files when opening the new spec. See the comments preceding Spec.createNewSpec(...).

# Bug 102

Summary: Product: Incorrect links in displayed PlusCal translator error message TLA+ Toolbox Leslie Lamport Core Component Leslie Lamport ASSIGNED --- minor simon P4 unspecified x86 64-bit Windows --- this is a tla file

 Leslie Lamport 2011-04-17 21:35:32 UTC In the soon-to-be-attached example, the PlusCal translator reports missing labels in two locations. When the Toolbox displays that message, it seems to attach links to the two locations that both refer to the first location. Leslie Lamport 2011-04-17 21:36:59 UTC Created attachment 26 [details] this is a tla file Leslie Lamport 2013-06-11 10:44:20 UTC I just noticed that this was filed under the wrong component. It looks like yet another bug in the Toolbox's parsing of output of the programs it calls.

# Bug 103

Summary: Product: I/O and backend calls not sufficiently decoupled from UI (main) thread TLA+ Toolbox Markus Alexander Kuppe TLA+ Editor Markus Alexander Kuppe NEW --- normal daniel.bmore.ricketts, simon P3 unspecified All Linux ---

 Markus Alexander Kuppe 2011-05-04 14:28:38 UTC File > Open Spec > a fairly large spec causes the UI to hang. This is due to parsing the model in the UI thread. Same happens, if File > Parse Spec is clicked. The appropriate command handles have to take care of decoupling the parsing from the UI thread by using a short-lived Thread or an org.eclipse.core.runtime.jobs.Job. Simon Zambrovski 2011-05-06 20:59:28 UTC I remeber a discussion between Leslie and me regarding this issue. I also remember that we decided to touch this place on demand only, because Lesli ensured me that the biggest spec he ever saw was 64KB and Sany parses it in very few seconds, so it is acceptable for the user to wait. There are several issues to solve if running the SANY in a separate thread/job. 1. There is the synchronization issue with the Parse Status 2. During Parsing, the SpecObj and is not available, which means that the most parts of smart editor functions doesn't work. Since we developed A MINIMAL parser integration solution, it worked for us and it is ok to improve it in the current iteration. I would address another important issue if you touch this place. Currently SANY runs a complete reparse, which is a litte dump. Large specs consists of many individual TLA+ modules and a modification usually doesn't affect all the modules. So instead of parsing the spec starting from root module every time, it would be better to only affected modules. I remember Leslie and me discussed this issue and we even tried to implement it, but then we left it as it is and decided to implement the easiest parsing solution and improve it later. So, in short: YES, I vote for decoupling parsing from UI thread. Markus Alexander Kuppe 2011-05-11 15:19:20 UTC *** Bug 78 has been marked as a duplicate of this bug. *** Markus Alexander Kuppe 2011-06-27 13:25:07 UTC More candidates: org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage.RunAction.run() org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.doSave(IProgressMonitor) Markus Alexander Kuppe 2011-06-30 11:03:02 UTC org.lamport.tla.toolbox.tool.tlc.traceexplorer.TraceExplorerComposite.doExplore() Markus Alexander Kuppe 2011-07-01 19:58:47 UTC org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.CloneModelContributionItem.getContributionItems() Markus Alexander Kuppe 2011-07-01 19:59:05 UTC *** Bug 137 has been marked as a duplicate of this bug. *** Markus Alexander Kuppe 2011-07-01 20:17:57 UTC *** Bug 110 has been marked as a duplicate of this bug. *** Markus Alexander Kuppe 2011-07-01 20:18:10 UTC org.lamport.tla.toolbox.tool.tla2tex.handler.ProducePDFHandler.execute(ExecutionEvent)

# Bug 104

Summary: Product: Bundle-RequiredExecutionEnvironment is set to J2SE-1.4 although Java5 API is used TLA+ Toolbox Markus Alexander Kuppe TLA Tools Markus Alexander Kuppe RESOLVED FIXED normal P3 unspecified All All --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-09 10:14:35 UTC org.lamport.tla.toolbox.* bundles use Java5 API but their BREE is set to Java 1.4. Markus Alexander Kuppe 2011-05-09 10:18:14 UTC BREE has been set to Java 1.5 Markus Alexander Kuppe 2011-05-09 10:18:16 UTC Created attachment 27 [details] mylyn/context/zip

# Bug 105

Summary: Product: org.lamport.tla.toolbox.tool.prover uses Java 1.6 API TLA+ Toolbox Markus Alexander Kuppe TLA Tools Markus Alexander Kuppe RESOLVED FIXED normal P3 unspecified All All --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-09 10:23:53 UTC java.lang.String.isEmpty() is not avaiable in Java 5 Markus Alexander Kuppe 2011-05-09 10:34:39 UTC Fix released by replacing isEmpty() with length() == 0 Markus Alexander Kuppe 2011-05-09 10:34:40 UTC Created attachment 28 [details] mylyn/context/zip

# Bug 106

Summary: Product: Test dependencies not satisfied causing compiler errors in o.l.t.toolbox and o.l.t.toolbox.tool.tlc.ui TLA+ Toolbox Markus Alexander Kuppe TLA Tools Markus Alexander Kuppe RESOLVED FIXED normal P3 unspecified x86 64-bit Linux --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-09 12:29:50 UTC Both bundles may _optionally_ depend on package "junit.framework" to satisfy the build time dependency but allow Junits absence at runtime. Markus Alexander Kuppe 2011-05-09 12:45:16 UTC Fix released Markus Alexander Kuppe 2011-05-09 12:45:17 UTC Created attachment 29 [details] mylyn/context/zip

# Bug 107

Summary: Product: Distributed TLC based on RMI broken TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All All ---

 Markus Alexander Kuppe 2011-05-09 12:46:48 UTC Refactorings broke the RMI based distributed version of TLC. Markus Alexander Kuppe 2011-05-09 12:51:27 UTC Hi Simon, what's the reason you have deprecated all RMI related code? I have hacked it to get back working and our manual tests appear to work. Real tests are pending though. Simon Zambrovski 2011-05-09 21:39:39 UTC Somehow Yuan and me decided that we are not able to make TLC work in distributed mode. From this point on I tried to push all the refactorings through both code bases: the single machine TLC, which I could test and through the distributed part wchi I could not test. In order to distuinguish the one from another, I marked TLC parts as depricated... I assume it was a mistake. Markus Alexander Kuppe 2011-05-31 11:37:51 UTC Fixed in HEAD (more performance tests pending)

# Bug 108

Summary: Product: Add framework to run automated UI tests TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED enhancement simon P3 unspecified All All --- 120

 Markus Alexander Kuppe 2011-05-11 15:15:33 UTC Automated UI tests are a great time saver especially when developing for multiple OS. SWTBot [0] allows to easily write UI tests that can be executed automatically. [0] http://eclipse.org/swtbot/ Markus Alexander Kuppe 2011-05-31 11:40:20 UTC Framework released to HEAD

# Bug 109

Summary: Product: Automatically detect pdflatex on the system TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- enhancement simon P3 unspecified All All ---

 Markus Alexander Kuppe 2011-05-11 15:36:18 UTC If pdflatex is not on the system path, an incomprehensible dialog pops up complaining that pdflatex cannot be found ("No such file or directory"). To make it easier for the user, either: a) Find pdflatex automatically (CDT has facilities to located system binaries) b) Generate PDF directly in Java c) Improve error dialog with a direct link to the Preferences > TLA+ Prefs > PDF Viewer

# Bug 110

Summary: Product: "Produce PDF Version" handler executes PDF generation on the UI thread TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED DUPLICATE normal simon P3 unspecified All All ---

 Markus Alexander Kuppe 2011-05-11 15:38:21 UTC Canceling a long or stuck operation is impossible since the buttons don't work. Markus Alexander Kuppe 2011-07-01 20:15:16 UTC org.lamport.tla.toolbox.tool.tla2tex.PDFHandlerThreadingTest has been added as a test case, though not activated yet. Markus Alexander Kuppe 2011-07-01 20:17:57 UTC *** This bug has been marked as a duplicate of bug 103 ***

# Bug 111

Summary: Product: NullPointerException when using spaces in application path (path to TLC java process) TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All Mac OS --- 157

 Markus Alexander Kuppe 2011-05-11 16:12:00 UTC When using a space in the app path on Mac OS X, Toolbox throws a NPE while executing a model check. Changing the path name to not contain a whitespace appears to prevent this error (even thought the path gets renamed back to spaces again) Markus Alexander Kuppe 2011-05-17 16:35:58 UTC See bug# 82 (same code area) Markus Alexander Kuppe 2011-07-18 13:04:17 UTC Fixed by bug #116

# Bug 112

Summary: Product: Open spec wizard accepts specs with illegal names TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All All --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-11 16:13:10 UTC Add a marker to the new spec wizard forbidding illegal names (like -) Markus Alexander Kuppe 2011-05-31 11:41:08 UTC Fixed in HEAD, verified on Mac, Windows XP, Linux Markus Alexander Kuppe 2011-05-31 11:41:09 UTC Created attachment 40 [details] mylyn/context/zip

# Bug 113

Summary: Product: Toolbox does not shut down gracefully with model checks still running TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- normal simon P3 unspecified All All ---

# Bug 115

Summary: Product: Open .tla from the system by double clicking in TLA Toolbox TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- enhancement simon P3 unspecified All All --- 116

 Markus Alexander Kuppe 2011-05-11 16:34:07 UTC This feature has been added with Eclipse 3.6 (Helios release) [0]. [0] https://bugs.eclipse.org/4922 Markus Alexander Kuppe 2011-08-04 09:57:33 UTC See Eclipse bug https://bugs.eclipse.org/4922 Markus Alexander Kuppe 2011-08-04 10:28:49 UTC Documentation can be found on the Eclipse wiki: - http://help.eclipse.org/helios/index.jsp?topic=/org.eclipse.platform.doc.isv/guide/product_open_file.htm - http://wiki.eclipse.org/Eclipse/OpenFileFeature

# Bug 116

Summary: Product: Upgrade to recent Eclipse RCP version TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED major simon P3 unspecified All All --- 115, 10

 Markus Alexander Kuppe 2011-05-11 16:45:13 UTC The Toolbox ships on top of Eclipse 3.5 (2009). This bugs require a more recent version of Eclipse. Since this change potentially introduces new bugs, it shouldn't be done lightheadedly though. Markus Alexander Kuppe 2011-07-18 10:15:22 UTC Fixed a while ago with the introduction of an automated build

# Bug 117

Summary: Product: Adobe PDF opens up in a separate windows instead of embedded editor TLA+ Toolbox Markus Alexander Kuppe TLATEX Component Markus Alexander Kuppe NEW --- minor simon P4 unspecified All Windows ---

 Markus Alexander Kuppe 2011-05-11 16:51:24 UTC It has been reported that on Windows 7 a generated PDF does not open up inside the Toolbox editor but in a separate Adobe windows.

# Bug 118

Summary: Product: "Translate PlusCal Algorithm" handle may only be enabled if spec indeed contains a PlusCal definition TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- enhancement simon P3 unspecified All All ---

 Markus Alexander Kuppe 2011-05-11 16:55:52 UTC Markus Alexander Kuppe 2011-05-17 16:31:11 UTC LL comment: Even go further and do not show the translation button unless the current spec contains a PlusCal spec.

# Bug 119

Summary: Product: German keyboard layout does not match ASCII values TLA+ Toolbox Markus Alexander Kuppe TLA+ Editor Markus Alexander Kuppe NEW --- normal simon P4 1.3 All Mac OS ---

 Markus Alexander Kuppe 2011-05-11 19:08:34 UTC A user reported that: "The first time I tried to create a example project but I could not type “[ ]” It seems that TLA+ is not recognizing special chars like “[ ] { }”, when input method in Mac OS X is set to German. If you set it to English it works."

# Bug 120

Summary: Product: Automated product build TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED enhancement simon P3 1.3 All All --- 108

 Markus Alexander Kuppe 2011-05-12 13:32:11 UTC TLA+ Toolbox currently is build manually from inside the development environment. A headless build should replace this task. Markus Alexander Kuppe 2011-05-31 11:41:32 UTC Fix released to SVN run "mvn install" in the tla2-inria/ folder to build products

# Bug 121

Summary: Product: Renaming spec broken, causing inconsistent projects even after Toolbox restart TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED major simon P3 unspecified All All --- 58

 Markus Alexander Kuppe 2011-05-17 16:39:21 UTC Renaming a spec causes the renamed spec to vanish from the spec explorer. After restarting the toolbox both the renamed as well as the new spec show up. If the underlying fix proves difficult, greying out "Rename" from the context menu should be considered. Markus Alexander Kuppe 2011-07-14 18:57:23 UTC Is a spec rename even supposed to change the name of the root .tla file as well as the module name inside? Markus Alexander Kuppe 2011-07-18 11:20:31 UTC Fixed in HEAD

# Bug 122

Summary: Product: Generated PDF does not show in embedded browser hard locking the Toolbox TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- normal simon P3 unspecified x86 64-bit Linux ---

 Markus Alexander Kuppe 2011-05-18 08:22:30 UTC On Ubuntu Natty 11.04 producing a PDF causes the progress bar to come up which hard locks at approximately 50%. No multipage editor with the embedded browser is ever shown. The only option to recover from this situation is to forcefully kill the Toolbox (which might cause data loss). Markus Alexander Kuppe 2011-05-18 08:46:14 UTC It appears as if reinstalling "xulrunner-1.9.2" fixed the hard lock issue. It must have somehow reseted the file handling in Mozilla Firefox (purging ~/.mozilla/eclipse did not help). Now the editor page opens up, but instead of showing the PDF, it prompts to save the file to disk.

# Bug 123

Summary: Product: Statusline should indicate "unparsed" state on dirty editor TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- enhancement simon P3 unspecified All All --- Protocol Bernhard Schildendorfer Report Bernd Wittman

 Markus Alexander Kuppe 2011-05-18 08:30:32 UTC "[...] it was not possible to enter behavior spec in the model for an existing specification. Although the Spec Status was displayed as “parsed”, the input fields were disabled. It turned out that the specification contained errors, but the spec status was displayed wrong because it was a new specification. After parsing the spec manually, an error occurred because of [...]" (Bernhard Schildendorfer) Markus Alexander Kuppe 2011-05-18 08:37:55 UTC "Changes in the TLA-Module-Window are not indicated in the “Spec Status” Field at the bottom of the window. From my point of view, each editing action should be indicated in the “Spec Status” as “unknown” or similar (independently of the file-save-status). Also, by executing the TLC Model Checker, no “Do you want to save the modified resources” announcement is displayed in reference to changes in the TLA-Module-Window." (Bernd Wittmann) Markus Alexander Kuppe 2011-05-18 09:41:28 UTC Created attachment 30 [details] Protocol Bernhard Schildendorfer see page 4 to 5 Markus Alexander Kuppe 2011-05-18 09:49:39 UTC Created attachment 31 [details] Report Bernd Wittman see page 2

# Bug 124

Summary: Product: PDF editor pages stays empty with error message indicating that the file could not be loaded TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- normal simon P3 1.3 x86 64-bit Windows 7 --- Report Silvia Straihammer

 Markus Alexander Kuppe 2011-05-18 08:36:40 UTC "If I generate PDF to view the tla-File, the program asks me if I want to open or save the pdf-File. But the pdf is already stored in the same directory as the tla-File. If I click on the “open”-Button it lasts a relative long time until it opens the external Reader and the pdf-viewer says: “The navigation to the website was aborted”. Why is it necessary to download the pdf-File?" (Silvia Straithammer) The report does not really indicate if this happened on Vista or Windows 7. Will leave it as Windows 7 for now. Markus Alexander Kuppe 2011-05-18 09:51:06 UTC Created attachment 32 [details] Report Silvia Straihammer

# Bug 125

Summary: Product: Toolbox fails to detect default VM installation on first run TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal leuschel, simon P3 1.3 All Mac OS --- 157

 Markus Alexander Kuppe 2011-05-19 18:52:07 UTC It has been reported, that the Toolbox fails to start if not installed into Applications/. Verification pending... Markus Alexander Kuppe 2011-06-10 18:51:54 UTC While running performance tests, I have made following observations (Mac OS X 10.0.6 x86_64): a) Toolbox does not have to be installed in Applications/ b) First toolbox run model checking throws an NPE c) A toolbox restart fixes the NPE irregardless of where it is installed Markus Alexander Kuppe 2011-06-10 18:59:44 UTC Job 'TLC run for Model_1' terminated with status: { Error } !ENTRY org.eclipse.core.jobs 4 2 2011-06-10 18:59:05.167 !MESSAGE An internal error occurred during: "TLC run for Model_1". !STACK 0 java.lang.NullPointerException at org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob.run(TLCProcessJob.java:108) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55) Markus Alexander Kuppe 2011-06-10 19:01:15 UTC The root cause appears to be that the toolbox fails to find the default VM installation (org.eclipse.jdt.launching.JavaRuntime.getDefaultVMInstall()) on its first run. Updating bug title to reflect this. Markus Alexander Kuppe 2011-06-22 16:10:09 UTC If bundle "org.eclipse.jdt.launching.macosx" is missing, eclipse fails to detect/find the VM on Mac. Markus Alexander Kuppe 2011-07-01 20:00:16 UTC *** Bug 133 has been marked as a duplicate of this bug. *** Markus Alexander Kuppe 2011-07-18 13:04:21 UTC Fixed by bug #116

# Bug 126

Summary: Product: NPE in Add Spec handler when parent directory does not exist TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 1.3 All All --- mylyn/context/zip

# Bug 131

Summary: Product: tlc2.util.BigInt.equals causes java.lang.StackOverflowError TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All All --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-27 10:02:40 UTC -- Error Log from JUnit -- Class: tlc2.util.ByteUtilsTest Method: test5 Actual: null Expected: null Stack Trace: java.lang.StackOverflowError at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) at tlc2.util.BigInt.equals(BigInt.java:34) Markus Alexander Kuppe 2011-05-27 10:17:45 UTC Fix released to HEAD, verified on Linux Markus Alexander Kuppe 2011-05-27 10:17:48 UTC Created attachment 35 [details] mylyn/context/zip

# Bug 132

Summary: Product: Open Saved Module menu item not grayed out TLA+ Toolbox Leslie Lamport TLC Component Markus Alexander Kuppe NEW --- minor simon P5 unspecified All All ---

 Leslie Lamport 2011-05-29 17:23:12 UTC Open Saved Module item on the The TLC Model Checker menu should be grayed out if no model is selected. Currently, it's not grayed out but clicking on it does nothing. This will confuse naive users who have no idea what that command does. (They'll probably still be confused if they use that command when it is enabled, but at least they have a chance of figuring it out--and may perhaps go to the help pages to find out.)

# Bug 133

Summary: Product: Internal Error when running TLC on Mac TLA+ Toolbox Michael Leuschel TLC Component Markus Alexander Kuppe RESOLVED DUPLICATE enhancement simon P3 1.3 All Mac OS ---

 Michael Leuschel 2011-05-30 16:44:01 UTC I am trying to run TLC from the TLA toolbox 1.3.1 on Mac OS X 10.6.7. Whenever I try to run TLC I get the error message: An internal error occurred during: "TLC run for Model_1". java.lang.NullPointerException This happens both using the 32-bit and the 64-bit version. The Hardware is a MacBook Pro Core2Duo 3.06 GHz. It happens with all my specifications and models (which ran successfully on 1.1.0 from Feb 5, 2010). I have also tried creating new specifications from scratch; without success. (As a side-not: the "About TLA Toolbox" menu command seems to perform no action.) Markus Alexander Kuppe 2011-05-30 17:38:01 UTC (In reply to comment #0) > I am trying to run TLC from the TLA toolbox 1.3.1 on Mac OS X 10.6.7. > Whenever I try to run TLC I get the error message: > > An internal error occurred during: "TLC run for Model_1". > java.lang.NullPointerException > > This happens both using the 32-bit and the 64-bit version. > The Hardware is a MacBook Pro Core2Duo 3.06 GHz. > It happens with all my specifications and models (which ran successfully on > 1.1.0 from Feb 5, 2010). > I have also tried creating new specifications from scratch; without success. Hi Michael, this appears to be an incarnation of bug #111 and potentially bug #125 too. Can you try and check if the workarounds mentioned on those bugs solve your issue? Basically make sure that the toolbox is installed into Applcations/ and that the path to the toolbox does not contain whitespaces. > (As a side-not: the "About TLA Toolbox" menu command seems to perform no > action.) This already gets tracked in bug #27. Thanks Markus Markus Alexander Kuppe 2011-07-01 20:00:16 UTC *** This bug has been marked as a duplicate of bug 125 ***

# Bug 134

Summary: Product: Distributed TLC does not compile on Java 1.5 TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 1.3 All Linux --- mylyn/context/zip

 Markus Alexander Kuppe 2011-05-31 09:25:14 UTC Description Resource Path Location Type The constructor IOException(String, EOFException) is undefined MemFPSet2.java /tlatools/src/tlc2/tool/fp line 235 Java Problem Description Resource Path Location Type The constructor IOException(String, IOException) is undefined DiskFPSet.java /tlatools/src/tlc2/tool/fp line 147 Java Problem Description Resource Path Location Type The method getLiveRef() is undefined for the type UnicastRef TLCServer.java /tlatools/src/tlc2/tool/distributed line 157 Java Problem Markus Alexander Kuppe 2011-05-31 11:35:09 UTC Fix released to HEAD Markus Alexander Kuppe 2011-05-31 11:35:11 UTC Created attachment 39 [details] mylyn/context/zip

# Bug 135

Summary: Product: NPE startup crash requiring Toolbox restart (happens randomly) TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 unspecified All Linux --- Console output mylyn/context/zip mylyn/context/zip

 Markus Alexander Kuppe 2011-05-31 11:52:21 UTC !ENTRY org.eclipse.ui 4 0 2011-05-31 01:10:00.273 !MESSAGE Unhandled event loop exception !STACK 0 java.lang.NullPointerException at org.lamport.tla.toolbox.util.SpecLifecycleManager$1.invoke(SpecLifecycleManager.java:30) at org.lamport.tla.toolbox.util.SpecLifecycleManager.sendEventWithVeto(SpecLifecycleManager.java:80) at org.lamport.tla.toolbox.util.SpecLifecycleManager.sendEvent(SpecLifecycleManager.java:64) at org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager.addSpec(WorkspaceSpecManager.java:156) at org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager.(WorkspaceSpecManager.java:97) at org.lamport.tla.toolbox.Activator.getSpecManager(Activator.java:297) at org.lamport.tla.toolbox.ui.contribution.SizeControlContribution.updateSize(SizeControlContribution.java:90) at org.lamport.tla.toolbox.ui.contribution.SizeControlContribution.createControl(SizeControlContribution.java:78) at org.eclipse.jface.action.ControlContribution.fill(ControlContribution.java:97) at org.eclipse.jface.action.ToolBarManager.update(ToolBarManager.java:353) at org.eclipse.jface.action.ToolBarManager.createControl(ToolBarManager.java:111) at org.eclipse.ui.internal.menus.TrimContributionManager$ToolBarTrimProxy.dock(TrimContributionManager.java:88) at org.eclipse.ui.internal.menus.TrimContributionManager.update(TrimContributionManager.java:232) at org.eclipse.ui.internal.WorkbenchWindow.updateLayoutDataForContents(WorkbenchWindow.java:3784) at org.eclipse.ui.internal.WorkbenchWindow.setLayoutDataForContents(WorkbenchWindow.java:3795) at org.eclipse.ui.internal.WorkbenchWindow.createDefaultContents(WorkbenchWindow.java:1113) at org.eclipse.ui.internal.WorkbenchWindowConfigurer.createDefaultContents(WorkbenchWindowConfigurer.java:625) at org.eclipse.ui.application.WorkbenchWindowAdvisor.createWindowContents(WorkbenchWindowAdvisor.java:268) at org.eclipse.ui.internal.WorkbenchWindow.createContents(WorkbenchWindow.java:999) at org.eclipse.jface.window.Window.create(Window.java:431) at org.eclipse.ui.internal.Workbench$20.runWithException(Workbench.java:1032) at org.eclipse.ui.internal.StartupThreading$StartupRunnable.run(StartupThreading.java:31) 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.application.WorkbenchAdvisor.openWindows(WorkbenchAdvisor.java:803) at org.eclipse.ui.internal.Workbench$28.runWithException(Workbench.java:1384) at org.eclipse.ui.internal.StartupThreading$StartupRunnable.run(StartupThreading.java:31) 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.runUI(Workbench.java:2316) 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) Markus Alexander Kuppe 2011-05-31 11:53:01 UTC Created attachment 41 [details] Console output Markus Alexander Kuppe 2011-05-31 11:55:57 UTC I suspect the call to org.eclipse.core.runtime.IConfigurationElement.createExecutableExtension(String) in org.lamport.tla.toolbox.util.SpecLifecycleManager.SpecLifecycleManager() to return null on Eclipse <= 3.5. Eclipse bugzilla searches turn up empty though. Markus Alexander Kuppe 2011-05-31 11:55:58 UTC Created attachment 42 [details] mylyn/context/zip Markus Alexander Kuppe 2011-05-31 11:56:35 UTC To activate assertions in Eclipse follow http://tech.puredanger.com/2007/01/17/eclipse-assertions/ Leslie Lamport 2011-05-31 12:06:51 UTC To avoid having to go to the Web to find out how to enable/disable assertions, here's the explanation from http://tech.puredanger.com/2007/01/17/eclipse-assertions/ When using the JDK 1.4+ assert keyword, it’s nice in Eclipse to enable them for all your launch configurations at once. The easiest way to do this is to specify a default VM argument for your installed JDK. You can do this by going to Windows -> Preferences -> Java -> Installed JREs. Then select your JDK and click the Edit… button. In the “Default VM Arguments” box, add -ea. Markus Alexander Kuppe 2011-06-21 15:52:04 UTC Changed ProverUIActivator.start(BundleContext) to access the preference store from inside the UI thread to prevent SWT invalid thread access exceptions. Markus Alexander Kuppe 2011-07-01 19:56:00 UTC Changes in comment #6 seem to have done the trick, closing as fixed. Markus Alexander Kuppe 2011-07-01 19:56:01 UTC Created attachment 54 [details] mylyn/context/zip

# Bug 136

Summary: Product: NPE in UIHelper.runCommand() if workbench window is inactive TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe NEW --- normal simon P3 1.3 All All ---

# Bug 160

Summary: Product: java.lang.ArithmeticException: / by zero in Graph window when column value is 0 TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 1.3 All All ---

# Bug 163

Summary: Product: NPE in SimpleFilenameToStream resolver when run from inside signed jar (required by web start) TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED normal simon P3 1.3 All All --- mylyn/context/zip

 Markus Alexander Kuppe 2011-07-07 10:52:43 UTC java.lang.ExceptionInInitializerError at tlc2.tool.distributed.TLCWorker.main(TLCWorker.java:161) 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 com.sun.javaws.Launcher.executeApplication(Launcher.java:1804) at com.sun.javaws.Launcher.executeMainClass(Launcher.java:1750) at com.sun.javaws.Launcher.doLaunchApp(Launcher.java:1512) at com.sun.javaws.Launcher.run(Launcher.java:130) at java.lang.Thread.run(Thread.java:662) Caused by: java.lang.NullPointerException at util.SimpleFilenameToStream.getInstallationBasePath(SimpleFilenameToStream.java:61) at util.SimpleFilenameToStream.(SimpleFilenameToStream.java:45) ... 10 more Error: Failed to start worker at coconut for server coconut.local. null Markus Alexander Kuppe 2011-07-07 15:51:31 UTC Fix released to HEAD (Lesson confirmed: never ever use File in your application, use InputStream instead) Markus Alexander Kuppe 2011-07-07 15:51:32 UTC Created attachment 60 [details] mylyn/context/zip`

# Bug 164

Summary: Product: Add custom system properties to TLCServer process launched from within Toolbox TLA+ Toolbox Markus Alexander Kuppe Core Component Markus Alexander Kuppe RESOLVED FIXED enhancement simon P3 unspecified All All --- mylyn/context/zip

 Markus Alexander Kuppe