Good day, I have just downloaded and installed the Win32/64 version of TLA+ Toolbox, v1.5.4, and I'm going through thehyperbook, at the point where it creates a OneBitClock. It tells me the code given will show errors because the 'b' variable is notdefined, 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 thedevelopment of software.
On Thursday, October 19, 2017 at 8:56:00 AM UTC-4, Markus Alexander Kuppe wrote:On 09.10.2017 16:05, Markus Alexander Kuppe wrote:
Hi,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 Markusthe 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