Feature: generate multiple traces for an invariant violation using TLC

[danwt]

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. TLC does not continue exploring all states when using -continue. tlaplus/tlaplus#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.