Skip to content

The Xenophon release
Compare
Choose a tag to compare
@lemmy lemmy released this 18 Jul 08:00
· 2095 commits to master since this release
v1.5.7
bfdbe00

Changelog

The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The 1.5.7 milestone lists all completed issues.

Additional noteworthy changes

TLC

  • Reword and complete comments of TLA+ standard modules d2f54a1
  • IsABag inconsistent with Bags.tla when parameter is not a bag 5d15bde
  • BagsUnion operator of TLA+ standard module for BagUnion({b,b}) produces incorrect b (+) b as result bc0f7db
  • Correctly handle sequences as input to Bags operators
  • Provisional Randomization standard module
  • tlc2.Generator refactored into tlc2.TLC 6141aed
  • Correctly recreate error trace in BFS mode with RandomElement 3a618d7
  • Minimize the number of duplicate states that are generated as part of the initial predicate f3a98ce
  • Minimize the number of duplicate states that are generated as part of the next-state predicate fba4319
  • Indicate name of action which does not completely specified the successor state fddcdd4
  • Speed-up Cloud TLC by skipping instance provisioning 2bc2488
  • Colorize and label actions (arcs) in state graph visualization 7e80f1d (Screenshot) Contributor: will62794
  • Fix broken error traces with views 5a62945

PlusCal

  • Allow no intervening label between call and goto in PlusCal 188e1fd

Specification Editor

  • Show errors in PlusCal algorithm for assignments to undeclared variables 1e3f8fa
  • Editor command "Goto declaration" now also goes to declarations of TLA+ standard modules 103204a (Screencast)
  • Mouse hover help shows BNF and help for PlusCal statements dbeafb6
  • Show operation definition and comment in mouse hover help ad36f39
  • Code completion for PlusCal statements triggered by Ctrl+Space 13c772f (Screencast)
  • Code completion for operator definitions and declarations triggered by Ctrl+Space c31c2bd (Screencast)
  • Automatically transpile PlusCal to TLA+ on editor save 642b540 (Screencast)

Model Editor

  • Collapse, disable and annotate "Generals" and "Statistics" sections with "No behavior spec" 43d207d
  • Add undo and redo support to constant expression source viewer ff03c66
  • Add TLA+ syntax highlighting to constant expression source viewer fd93b56
  • Report the number of initial states as first item reported in the ResultPage's statistic table (with diameter of 0) 076f0c7
  • Show output/progress of remotely running Cloud TLC in Toolbox 593fc82

Misc

32 bits

32 bit (x86) variants of the TLA Toolbox have been discontinued with this release. fb68044

A note to Java 11 users (mostly macOS)

Please consider downloading a recent Toolbox nightly build (1.6.0) instead of the Toolbox 1.5.7 release below. The nightly builds do not suffer from a startup crash when the system Java VM is newer than Java10.

Assets 8