The Zenobius release

Changelog

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

Additional noteworthy changes

TLC Profiler

• Identify bottlenecks by marking expensive expressions and actions in terms of complexity (Screencast)
• Implicitly fixes Coverage result of zero included for set of variables "vars"

TLC

• Invalid violation of a liveness property because of bidirectional transitions in liveness graph due to inverse action e9ccb77
• Evaluate Initial Predicate expressions A /\ B /\ C in given order instead of A /\ C /\ B eb5d554
• Print error message when length of a behavior exceeds 2^15 states on-disk or 2^31 in-memory 28a0117
• Reduce fingerprint collision probability by randomly selecting irreducible polynomial at TLC startup (unless set on command-line with fp parameter)
• Correctly recreate error traces for specs using RandomElement operator from TLC's standard module
• Expose TLC runtime statistics and control in specs (diameter, states, distinct states, runtime, level, exit) through named registers for TLCGet and TLCSet 592056f 43e2b74
  • Warning: Using named registers can introduce unintended non-determinism
• Improve readability of progress output by showing thousands delimiters Contributor: P. White
• Visualize SANY's semantic graph with GraphViz: java [-Dtla2sany.explorer.DotExplorerVisitor.includeLineNumbers=true] -cp /path/to/tla2tools.jar tla2sany.SANY -d Spec.tla dot Screenshot
• Indicate TLC's process id (pid) in startup banner ea70206
• Inspection hatch to monitor states generated by a running TLC process: java -cp /path/to/tla2tools.jar tlc2.tool.management.StateMonitor [interval] 9ddffad b483440 (Screencast)
• Support suspension of (breadth-first) model checking via JMX API
• Opt-in usage data reporting
• Warn user if TLC is slowed down fa71d52 34c91e9 34c91e9

Performance & Scalability

• Multi-Threaded Simulation Mode 8355920 Contributor: will62794
• More efficiently generate the set of subsets for the TLA+ expression (SUBSET S) 4a62e5b
• Reduce worker contention by separating the trace file into N partial trace files where N is the number of workers 548ce71
• Speed-up TLC shutdown by calculating 'actual fingerprint collision probability' only if 'calculated probability' exceeds 1E-10 f12b10e
• Increase TLC throughput by ~10% by refactoring hot code-paths e6c8f6c 1bc2ab1
• Show active fingerprint set and state queue implementation in startup banner e974533 ea3feb5
• ByteArrayQueue prototype to increases throughput by reducing the critical section of the queue of unseen states 01b0e98
  • Activate with -Dtlc2.tool.ModelChecker.BAQueue=true Java system property

Command-line

• Accept absolute spec path on command-line
• Make tlc2.TLC the main-class attribute of the tla2tools.jar fac02ee
  • Set executable bit for tla2tools.jar to simplify command-line on Linux: /path/to/tla2tools.jar /path/to/spec
• Command-line TLC users please always pass -XX:+UseParallelGC Java 11 flag to not suffer performance penalty
  • OpenJ9 has been identified to provide worst performance in JVM shoot-out
• Retire tla.zip in favor of tla2tools.jar 2da02d3
  • TLC's tla-bin scripts have been updated accordingly
• Exit status is now non-zero in the case of any errors or property violations #277

CloudTLC

• Switch to Azure service principal authentication
  • Automatically handle Azure resource deletion as part of instance termination 5be0e77
• Gracefully terminate cloud resources when a CloudTLC run is terminated prematurely d593d0e
• Power-off instead of terminate CloudTLC instances tagged power_off to speed-up subsequent restart 22a7385
• Adds support for packet.net's t1.small.x86 budget baremetal instances 71a2530

Toolbox

Model Editor

• Better visualize coverage by coloring the editor 881f2e6
• Usability improvements to the model editor including:
  • What was previously the "Advanced Options" page has been split into two pages with the Advanced TLC Options occupying its own page now.
    • Neither of these pages are visible by default, and are accessed by hyperlink on the main model page; their open-or-closed state are saved with the model so that subsequent model openings will restore the view to the configuration last seen by the user.
  • The selection of the behavior spec is now performed via pulldown, as seen in this accompanying screencast..
  • The "How to run?" section of the main page has been simplified, as can be seen in the same screencast as above. Checkpoint related TLC options have been moved to the Advanced TLC Options page. A given worker, memory, and disk storage file count configuration can be saved as the default configuration to be used with new models.
  • Init and Next fields of the "What is the Behavior Spec" accept multi-line expressions
  • The "How to run" and the "What to check?" sections on the main page have been given full width of the page.
  • Similarly, the "State Constraint" section on the "Advance Options" page have been given full width.
  • The tables in the "Statistics" section of the "Model Checking Results" page now expand to fill the width of the page, and resize their columns to consume the available width when those tables resize.
  • The "General" section of the "Model Checking Results" page has been condensed to two lines. The top line, always visible, will show:
    • an "Awaiting..." text for an un-executed model.
    • once running, or ran, a Start time, an End time, a status, and potentially a last checkpoint time, and a mode denotation for Depth-first or Simulation runs.
  • ... and the second line will be visible should their be errors in execution, information about fingerprint collision, and/or zero counts on coverage.
  • The Evaluate Constant Expression section in the Results page can be moved to its own tab in the model editor via a preference checkbox in TLA+ Preferences → TLC Model Checker.
  • The Evaluate Constant Expression now features a toggle button to more easily jump in and out of Evaluate Constant model check mode (No behavior spec selected.)

TLA+ editor

• Add a preference to disable spec file modification history footer b7c1970 Contributor: C Jones

Spec Explorer

• Support deletion of additional modules

Trace Explorer

• TETrace operator to support self-referential error trace expression
  • Allows to e.g. export error traces to ShiViz visualization tool
• Supporting naming to compose trace expressions a34ef2c (Screencast)
• Map SANY errors back to Toolbox expression locations 9ae65ab (Screenshot)
• Add syntax highlighting and redo/undo in input boxes
• Allow customizable fonts for the Toolbox's Error Trace viewer
• Add header button to error trace to toggle tree expansion between collapse and expand all. Shift+Click returns to default two-level expansion 8640936 (Screencast)
• The edit button is enabled if the table contains one formula, regardless of whether that formula is selected; formulas are able to be drag reordered; changes (addition, editing, removal, and reordering) are now saved automatically. (All covered by Issue #9)
• There is a button in the Error-Trace section header which allows the 'linking' of the trace viewer with the spec editor; in the same way that one could previously double-click on a trace location to reveal the section of the specification in the spec editor, while the editor is linked this action can be done by a single click, as well as by navigating with the keyboard arrow keys. (Issue #289)

Misc

• Bundle Java 11 with the Toolbox to free users from installing Java manually
• The Toolbox application now has its custom icon displayed for it 4c7d0d5
• Show actual TLC command-line in .log file upon TLC launch 1efd390
• Improve GraphViz/dot output of state graph for better compatibility with 3rd party tool Cytoscape 50e83b3
• Additional modules can be removed from a specification by right clicking and choosing "Delete"; note that this removes them from the Toolbox specification, it does not affect them on the filesystem. cf4e038
• Add TLA+ user/discussion group to Toolbox's list of default RSS feeds
• Let Toolbox updater (p2) reject incompatible updates (skipping releases) to not break the installation
• Add new spec and its models from a zip file (zip names has to match root module name) d5d1960505f619aa8b7499c411c7bfc054d6d3bc (Screencast)
• Ship a set of specs as introductory examples with the Toolbox
• Sign Toolbox with official Apple certificate on macOS
• Homebrew cask versions for nightly Toolbox
• Models from foreign specs (another spec which exists in the Spec Explorer) can be cloned into the currently open spec via the TLC Model Checker → Clone Model → Foreign Model... menu item.

A note to macOS users

Startup on macOS version 10.14 (Mojave) will fail with "TLA+ Toolbox can't be opened because Apple cannot check it for malicious software.". Please make sure to follow the instructions outlined in GitHub issue #320 to address this problem.

Checksums

sha1sum	file
b0fca8d26568c5304b5e4d5ab40f3ffe1ed48ba1	TLAToolbox-1.6.0-linux.gtk.x86_64.zip
836c91cddf98088f7e2c8c2f711e95217d5530da	TLAToolbox-1.6.0-macosx.cocoa.x86_64.zip
ae09753744f462957709d94d735ef292e775a05b	TLAToolbox-1.6.0-win32.win32.x86_64.zip
aa4876bb4ae1275eb157fe67322fa69fd7452b7a	tla2tools.jar
d54307de60caf42e586b06d84994ec9cfcee0675	repository.zip (most of you don't want this)