Hi Markus,
Here’s my summary for the web page of the changes in the new version:
Version 1.5.0 - 11 May 2015
- Distributed TLC in the Cloud--significantly improves
distributed TLC.
- Significantly speeds ups TLC's liveness checking.
- Improvements to the Decompose Proof command.
- Improvements to the TLC Errors view, including ability to
show trace in reverse order.
- Fixes all known bugs in TLC's liveness checking.
- Fixes bug in TLC that caused infinite looping if a recursively
defined operator is used as an operator argument in its own
definition.
Any suggestions for improvement?
Leslie
From: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx]
On Behalf Of Markus Alexander Kuppe
Sent: Tuesday, May 12, 2015 4:32 AM
To: tla...@xxxxxxxxxxxxxxxx
Subject: [tlaplus] Re: Toolbox 1.5.0 final released
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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsu...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.