modelator-py icon indicating copy to clipboard operation
modelator-py copied to clipboard

Published 20 hours ago • verified publisher icon informalsystems

Feature: generate multiple traces for an invariant violation using TLC

Open danwt opened this issue 3 years ago • 0 comments

Users would like to generate multiple traces violating a single invariant using TLC.

It is possible to do this using TLC's '-continue' parameter. It just allows model checking to continue, using the same algorithm as normal but without the early breakout. This means

  1. https://github.com/tlaplus/tlaplus/issues/690
  2. TLC will continue to check unbounded state spaces.

this makes any solution that uses the technique a bit finicky.

Alternatives: use simulation mode.

danwt avatar Nov 07 '21 12:11 danwt