TLA+ Toolbox 1.5.4 release

167 views
Skip to first unread message

Markus Alexander Kuppe

unread,
Oct 9, 2017, 10:06:08 AM10/9/17
to tla...@googlegroups.com
Hi,

a new TLA+ Toolbox 1.5.4 release has been made available [1][2]. Note
that 32-bit versions of the Toolbox are only available from [2]. We
strongly advise users of 64-bit computers not to use a 32-bit version.

As always, this release fixes several bugs, contains performance
improvements and introduces new features. See the change log [4] for a
description of high-level changes or check the noteworthy commits for a
more technical perspective [5].

A 1.5.3 Toolbox will automatically ask to update to 1.5.4 upon its next
startup and run a workspace migration. Users who prefer to start fresh
and install a 1.5.4 zip file can move or copy their existing
workspace/.metadata directory out of the 1.5.3 installation to
~/.tlaplus/.metadata in their HOME directory to preserve Toolbox
preferences and the list of specifications.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/releases/tag/v1.5.4
[2] https://tla.msr-inria.inria.fr/tlatoolbox/products/

[4] http://lamport.azurewebsites.net/tla/toolbox.html
[5]
https://github.com/search?&q=repo:tlaplus/tlaplus+merge:false+changelog&type=Commits&ref=searchresults

Markus Alexander Kuppe

unread,
Oct 19, 2017, 8:56:00 AM10/19/17
to tla...@googlegroups.com
On 09.10.2017 16:05, Markus Alexander Kuppe wrote:
Hi,

a new TLA+ Toolbox 1.5.4 release has been made available [1][2]. Note
that 32-bit versions of the Toolbox are only available from [2]. We
strongly advise users of 64-bit computers not to use a 32-bit version.

As always, this release fixes several bugs, contains performance
improvements and introduces new features. See the change log [4] for a
description of high-level changes or check the noteworthy commits for a
more technical perspective [5].

A 1.5.3 Toolbox will automatically ask to update to 1.5.4 upon its next
startup and run a workspace migration. Users who prefer to start fresh
and install a 1.5.4 zip file can move or copy their existing
workspace/.metadata directory out of the 1.5.3 installation to
~/.tlaplus/.metadata in their HOME directory to preserve Toolbox
preferences and the list of specifications.

Thanks
Markus
Hi,

the new 1.5.4 Toolbox bundles the book "Specifying Systems", the "PlusCal Manual" paper, the "The TLA+ cheat sheet" and finally the "The Operators of TLA+". All documents are accessible via the "Help" menu. However, the "The Operators of TLA+" paper is obsolete.

Please ignore "The Operators of TLA+" paper until removed in the next Toolbox release.

Thanks

Markus

Thomas Clifford

unread,
Jan 1, 2018, 3:44:17 PM1/1/18
to tlaplus
Good day,  I have just downloaded and installed the Win32/64 version of TLA+ Toolbox, v1.5.4, and I'm going through the 
hyperbook, at the point where it creates a OneBitClock.  It tells me the code given will show errors because the 'b' variable is not 
defined, but when I save the code without adding the 'VARIABLE b' line to the code, no error window or dialog pops up.
I also cannot find in any of the menus or preferences where to enable/disable the 'Parsing Errors view'.

I'm running Windows Pro 7, Sun Java 8_144.

Thank you and I look forward to learning more about correcting disconnects between process analysis / design / specification and the 
development of software.

Thomas Clifford

unread,
Jan 1, 2018, 4:00:29 PM1/1/18
to tlaplus
As an update, I just found, in Preferences, the preferences for "TLA+ Parser", and the box marked "Always pop up Parsing Errors View" *is* checked.

Thank you.

loki der quaeler

unread,
Jan 1, 2018, 4:04:22 PM1/1/18
to tlaplus
Is the Spec Status in the lower right accompanied with a bright-green or dark-red colored bar?

Under the Window menu, is there a "Parsing Errors" menu item?

Thomas Clifford

unread,
Jan 1, 2018, 4:10:30 PM1/1/18
to tlaplus
Loki,  The spec status shows "parsed" with a green background.
Under the Windows menu, there is a "Parsing Errors" selection, but it is greyed out.

Might it be that if you don't specify a 'VARIABLE'', it just assumes non-commands or certain keywords are commands, 
and all others are variables ?

Stephan Merz

unread,
Jan 2, 2018, 2:46:15 AM1/2/18
to tla...@googlegroups.com
Hello,

just to reproduce the behavior that you describe, I followed to the letter the instructions in section 2.3 of the hyperbook. Attached is the screenshot of the (expected) result. I am working in Mac OS (version 10.13.2), Toolbox v1.5.4, Oracle Java 8. If you could not resolve your issue, perhaps attach your TLA+ module.

Regards,
Stephan

Reply all
Reply to author
Forward
0 new messages