Toolbox 1.5.0 release candidates

[Markus Alexander Kuppe]

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

[Andrew Helwer]

Excited to see the portable specs feature! From a quick look at the RC, I like then new font and color scheme.

Along the same lines of improving portability and version control system friendliness, what do you think about removing the default created/modified footer?

[Leslie Lamport]

         Along the same lines of improving portability and version control system friendliness,
         what do you think about removing the default created/modified footer?

Would you please explain why removing the footer would enhance portability or help with version control.

Thanks,

Leslie

[Markus Alexander Kuppe]

On 04.05.2015 09:51, Andrew Helwer wrote:
> Along the same lines of improving portability and version control system
> friendliness, what do you think about removing the default
> created/modified footer?

Hi Andrew,

when you create a spec, just delete the footer once and it's gone for
good. The Toolbox doesn't touch the footer when it's not there anymore.

Btw. for those wanting the footer, Toolbox 1.5.0 combines the footer
update and the actual change into a single undo keystroke (Ctrl-z).

Cheers
Markus

[Andrew Helwer]

Also happy to see the undo function include the footer now.

There are three concerns with the footer. First, it is auto-generated, and as best practice you shouldn't store auto-generated components in version control - especially components which often change. Second, it duplicates information found both in file metadata and (in greater detail) the version control log itself - this is more of a philosophical objection against denormalized data. Third, it will cause merge conflicts any time two users edit a spec concurrently - even if their edits are to completely different parts of the file.

Andrew

[Leslie Lamport]

   There are three concerns with the footer.  First, it is
   auto-generated, and as best practice you shouldn't store
   auto-generated components in version control -

By that reasoning, one should never store a checksum inside a
version-controlled file.  This is a very reasonable position, assuming
that a version control system could never ever have a bug that
corrupts a file.

   Second, it duplicates information found both in file metadata and (in
   greater detail) the version control log itself

Given your first objection, I presume that you are too young to have
learned one fact of digital life: Any piece of information about a
file not contained within the file will eventually become separated
from the file and lost.  That is why, if you write code based on a
TLA+ spec, a copy of that spec should be embedded as a comment within
the code.  Unfortunately, the method with which information is encoded
in a file is an important piece of information that cannot be
contained in the file.  Hence, all files will eventually become
unreadable.  My solution has been to encode all my source files in
ASCII, which I seem to have correctly predicted will outlive me.

   Third, it will cause merge conflicts any time two users edit a spec
   concurrently - even if their edits are to completely different parts
   of the file.

This is a valid objection, though a minor one in light of the fact
that a timestamp is added to an existing file only if it already has
one.  If people find it enough of a nuisance, it should be easy enough
to add a preference to disable timestamping.  (And perhaps one to add
a timestamp even if it doesn't already exist.)  On the other hand,
a version control system written by someone who is not so egotistical
as to believe that his system will be used forever would provide some
method for properly handling such timestamps.

Leslie

[Stephan Merz]

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

[Markus Alexander Kuppe]

On 05.05.2015 10:18, Stephan Merz wrote:

> 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?

Hi Stephan,

for your info: Extending the spec explorer to show a spec's modules
below the top-level element has already been on my wish-list. I just
didn't get around to implementing it in 1.5.0 whichI wanted to get out
of the door because it reached a somewhat complete feature set.

Cheers
Markus

[Andrew Helwer]

Is there a dev mailing list I can join?

On Sunday, May 3, 2015 at 9:22:58 AM UTC-7, Markus Alexander Kuppe wrote:

[Markus Alexander Kuppe]

On 06.05.2015 19:25, Andrew Helwer wrote:
> Is there a dev mailing list I can join?

Hi Andrew,

there is no dev list. The group of people working on the Toolbox, TLC
and TLAPM is sufficiently small for direct communication.

What part of the project are you interested in?

Cheers
Markus

[Andrew Helwer]

I most often use the IDE and TLC, so it would be those eventually. For now I'm interested in the user onboarding experience though, which is probably best-served by the website and maybe a web demo.

[Y2i]

Thank you Markus.  I'm really happy about the new release, especially considering that the last update was released more than a year ago.  Great work!

Yuri

[Robert Shore]

Summary: Cannot create new spec with symbolic link in path.

Version: toolbox 1.5 dated 4-May
Host: Linux 3.13.0-46-generic #79-Ubuntu SMP Tue Mar 10 20:06:50 UTC 2015 x86_64 x86_64 x86_64 GNU/Linux

Details: menu => File => Open spec => Add New Spec. If the root-module file path contains a symbolic link, the toolbox reports an internal error. The log is the following:
!ENTRY org.eclipse.core.jobs 4 2 2015-05-11 19:02:22.819
!MESSAGE An internal error occurred during: "NewSpecWizard job".
!STACK 0
org.eclipse.core.runtime.AssertionFailedException: assertion failed:
        at org.eclipse.core.runtime.Assert.isTrue(Assert.java:110)
        at org.eclipse.core.runtime.Assert.isTrue(Assert.java:96)
        at org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper.storeRootFilename(PreferenceStoreHelper.java:33)
        at org.lamport.tla.toolbox.spec.Spec.createNewSpec(Spec.java:162)
        at org.lamport.tla.toolbox.ui.handler.NewSpecHandler$1.run(NewSpecHandler.java:110)
        at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)

Workaround: Make sure that the file path contains no symbolic links

[Markus Alexander Kuppe]

On 12.05.2015 12:02, Robert Shore wrote:
> Summary: Cannot create new spec with symbolic link in path.
>
> Version: toolbox 1.5 dated 4-May
> Host: Linux 3.13.0-46-generic #79-Ubuntu SMP Tue Mar 10 20:06:50 UTC
> 2015 x86_64 x86_64 x86_64 GNU/Linux
>
> Details: menu => File => Open spec => Add New Spec. If the root-module
> file path contains a symbolic link, the toolbox reports an internal
> error. The log is the following:
> !ENTRY org.eclipse.core.jobs 4 2 2015-05-11 19:02:22.819
> !MESSAGE An internal error occurred during: "NewSpecWizard job".
> !STACK 0
> org.eclipse.core.runtime.AssertionFailedException: assertion failed:
> at org.eclipse.core.runtime.Assert.isTrue(Assert.java:110)
> at org.eclipse.core.runtime.Assert.isTrue(Assert.java:96)
> at
> org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper.storeRootFilename(PreferenceStoreHelper.java:33)
> at org.lamport.tla.toolbox.spec.Spec.createNewSpec(Spec.java:162)
> at
> org.lamport.tla.toolbox.ui.handler.NewSpecHandler$1.run(NewSpecHandler.java:110)
> at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
>
> Workaround: Make sure that the file path contains no symbolic links

Thanks Robert, we will add it to the list of known problems for 1.5.0.
Hopefully we will be able to remove this restriction in a subsequent
release.

Btw. this restriction is also present in 1.4.8 when one adds a module.
Thus, to avoid inconsistencies the symlink check is now done when the
spec gets imported.

Thanks
Markus

[Robert Shore]

Right. For some reason I didn't notice it until now; I was probably overwhelmed with the TLA+learning experience.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/qOY8Iqcg7nM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Markus Alexander Kuppe]

Hi,

the final 1.5.0 TLA+ Toolbox release has been made available today [1][2][3].

The 1.4.8 will automatically ask to update to 1.5.0 upon the next Toolbox startup (the release candidate will *not* update automatically. Please delete the release candidate manually and install the final one afterwards).

See the list of changes [4] for details on the seven bugfixes since the release candidate.

Thanks
Markus

[1] https://tlaplus.codeplex.com/releases/view/614836
[2] https://tla.msr-inria.inria.fr/tlatoolbox/products/
[3] https://bugzilla.tlaplus.net/tlatoolbox/products/
[4] https://tlaplus.codeplex.com/SourceControl/list/changesets


--

[Leslie Lamport]

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

--
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+u...@googlegroups.com.

[ret2...@gmail.com]

I am still getting 'NewSpecWizard job' has encountered a problem. An internal error occurred during "NewSpecWizard job":

Clicking on details shows nothing - no trace. Disappointed.