Re: Toolbox 1.5.0 release candidates

Hi Markus,

great work! I noticed that when opening a TLA+ module, the Toolbox now pops up an alert box warning about every module that is not located in the current working directory or is one of the built-in standard modules but that is found via the user-defined TLA+ library paths. The text in the dialog box states that the Toolbox could not find these files, although it marks them as standard modules and explains that for standard modules, parsing continues normally despite this warning. This affects in particular all modules in the prover library, since they are not built into the Toolbox: in fact, we instruct users to add a suitable path when they install TLAPS.

While I understand the intention of warning users of potential incompatibilities when moving between different Toolbox installations, I wonder if this dialog box is the appropriate means. It may be confusing to the user since it looks like an error message, and also it is a one-time thing that may be forgotten when problems actually arise. Perhaps it would be more interesting to list the modules that a TLA+ project relies on (perhaps in a hierarchical view of the Spec Explorer, where currently one can only see the top-level module and models?), distinguishing between modules found in the current working directory (and/or explicitly listed relative or absolute paths?), modules found in the user-defined library path, and built-in modules?

Thanks,

Stephan

On Sunday, May 3, 2015 at 6:22:58 PM UTC+2, Markus Alexander Kuppe wrote:

Hi,

we are about to release the next Toolbox release (1.5.0). While we are finishing up the change log [1], we would like to ask the community to test the release candidate [2] (unless show stoppers are found, the release candidate will eventually just be renamed).

Almost 500 new commits make up the 1.5.0 since the last release in early 2014 (see commit 6639bd91f4bb4f2233c05720ecea1814686d6739 [3]). An incomplete high-level list of changes is:

Features:
======
* Distributed TLC in the Cloud (preview, lacks final documentation) [4]
* Portable specs (only store relative path names)
* Persistently store customized sash ratio in TLC Errors view
* Flip sort order in TLC Errors view. Sort variables alphabetically
* Make better use of screen estate on large displays
* Improved scalability and performance (order of magnitude) with TLC Liveness checking (milestone 1)
* Minor enhancements (see commit log)

Bugs:
====
* Liveness checking produces invalid counter-example [5]
* Negative seek offset Exception with Liveness checking [6]
* Liveness checking in simulation mode is buggy [7]
* Fixed several startup crashes and hangs
* Fixed race conditions when launching TLC [8], and in TLC Errors view

Technical:
======
* Drop Toolbox compatibility with Java < 1.7
* Better compatibility with recent Mac and Linux (switched to Eclipse foundation 4.4)
* Much improved test coverage
* Can switch to experimental liveness checking implementation in simulation mode (-Dtlc2.tool.Simulator.experimentalLiveness=true)
* Report statistics about behavior graph properties (-Dtlc2.tool.liveness.Liveness.statistics=true)
* Significantly extended code comments
* Sign distributed TLC workers to remove startup warning

Please report bugs by responding to this message or by opening issues at Codeplex [9].

Thanks
Markus

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#downloading
[2] http://tla.msr-inria.inria.fr/tlatoolbox/staged/products/ or https://bugzilla.tlaplus.net/tlatoolbox/staged/products/
[3] http://tlaplus.codeplex.com/SourceControl/changeset/6639bd91f4bb4f2233c05720ecea1814686d6739
[4] https://vimeo.com/97961350
[5] http://tlaplus.codeplex.com/workitem/8
[6] https://bugzilla.tlaplus.net/show_bug.cgi?id=293
[7] https://bugzilla.tlaplus.net/show_bug.cgi?id=40
[8] https://bugzilla.tlaplus.net/show_bug.cgi?id=98
[9] http://tlaplus.codeplex.com/workitem/list/basic