TLA+ Toolbox 1.5.6 release

[Markus Alexander Kuppe]

Hi,

a new TLA+ Toolbox 1.5.6 release has been made available [1][2]. This release fixes an uncommon but serious bug in TLC that has existed since its initial implementation. The bug can cause TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either can cause TLC not to examine all reachable states. The error can occur in the following two cases:

The possible initial values of some variable var are specified by a subformula F(..., var, ...) in the initial predicate, for some operator F such that expanding the definition of F results in a formula containing more than one occurrence of var, not all occurring in separate disjuncts of that formula.

The possible next values of some variable var are specified by a subformula F(..., var', ...) in the next-state relation, for some operator F such that expanding the definition of F results in a formula containing more than one occurrence of var' , not all occurring in separate disjuncts of that formula.

An example of the first case is an initial predicate Init defined as follows:

VARIABLES x, ...
 
F(var) == \/ var \in 0..99 /\ var % 2 = 0
          \/ var = -1
  
Init == /\ F(x)
        /\ ...

The error would not appear if F were defined by:

F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}
          \/ var = -1

or if the definition of F(x) were expanded in Init :

Init == /\ \/ x \in 0..99 /\ x % 2 = 0
           \/ x = -1
        /\ ...

A similar example holds for case 2 with the same operator F and the next-state formula

Next == /\ F(x')
        /\ ...

If your specs are affected by the bug described above, you should re-run TLC on them.


Please consult the changelog for a list of all noteworthy changes [3].

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/releases/tag/v1.5.6
[2] https://tla.msr-inria.inria.fr/tlatoolbox/products/
[3] https://lamport.azurewebsites.net/tla/toolbox.html#155bug

[sglaser.com]

I think there is something in the Mac version of 1.5.6 that breaks it on High Sierra.

Running the freshly downloaded app causes the OS to complain that it’s damaged and shows an offer to move it into the trash for me.

The 1.5.5 release worked fine (I deleted 1.5.4 and installed from the web — upgrading directly from 1.5.4 hung doing the upgrade).

I download 105 MB TLAToolbox-1.5.6-macosx.cocoa.x86_64.zip (Mac link on the page below).

The sha1sum matches what your web page says.

Extract the zip either by double clicking it and letting MacOS do the work, by the command line unzip, or by unarchiver. All methods produce identical extractions.

I’m on the latest High Sierra version. MacBook Pro 13 with Touch Bar.

Java Version 9.0.4 (build 9.0.4+11) x86_64

  Model Name: MacBook Pro

  Model Identifier: MacBookPro13,2

  Processor Name: Intel Core i7

  Processor Speed: 3.3 GHz

  Number of Processors: 1

  Total Number of Cores: 2

  L2 Cache (per Core): 256 KB

  L3 Cache: 4 MB

  Memory: 16 GB

  Boot ROM Version: MBP132.0238.B00

  SMC Version (system): 2.37f20

  Serial Number (system): C02SR94VHF1R

  Hardware UUID: 27C5460A-6B7D-59CE-B133-BA3F7A866D9B

  System Version: macOS 10.13.3 (17D47)

  Kernel Version: Darwin 17.4.0

  Boot Volume: Macintosh HD

  Boot Mode: Normal

  Computer Name: steve-mac-13

  User Name: Steve Glaser (sglaser)

  Secure Virtual Memory: Enabled

  System Integrity Protection: Enabled

  Time since boot: 4 days 22:53

---

Steve Glaser
sgl...@sglaser.com

--
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.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hello,

I just reinstalled the version from GitHub on macOS 10.13.3 (High Sierra), without any problem.

It looks like you fell victim to Apple's increasingly tighter security measures [1] that intend to protect users from applications not downloaded from the Mac App Store and/or that do not carry a signature from a developer who is a member of Apple's developer program.

Please make sure that in Preferences -> Security & Privacy, you allow apps both from the App Store and from identified developers. Now, do a right-click (ctrl-click) on the Toolbox application and select Open. You'll see a dialog containing a warning that the application is from an unidentified developer, but nevertheless giving you the option to open the application. Click on "Open", and the Toolbox should start normally.

Note that this procedure is necessary only the first time you open the app, subsequently you can open it just by double clicking.

Hope this helps,

Stephan

[1] http://www.tech-recipes.com/rx/45404/mac-downloaded-app-is-damaged-and-cant-be-opened-error-solved/