Skip to content
Snippets Groups Projects
Select Git revision
  • db269535b7cebccb4270b8a505ac9be605021522
  • master default protected
  • towards_1.8.0
  • updateTLC
  • 1.1.0-stups
  • 1.0.2-stups
  • 1.0.1-stups
  • 1.0.0-stups
8 results

tlatools

  • Open with
  • Download source code
  • Your workspaces

      A workspace is a virtual sandbox environment for your code in GitLab.

      No agents available to create workspaces. Please consult Workspaces documentation for troubleshooting.

  • user avatar
    Markus Alexander Kuppe authored
    The error/exception - such as an OutOfMemoryError - shows up on the
    console, but does not terminate TLC.  A user thus might miss the
    error/exception and incorrectly assume that the spec satisfies the
    liveness properties.
    
    The effect of this fix can be studied with unit test
    CodePlexBug09EWD749FL2Test that terminates with a meaningful "ran
    out of memory" message instead of showing TLC regular success
    message despite going out of memory (run test with -Xmx56m).
    
    Fixes Github issue #1
    https://github.com/tlaplus/tlaplus/issues/1
    
    [Bug][TLC][Changelog]
    db269535
    History
    Name Last commit Last update