TLC Simulation mode seems to report bogus violation

[saffroy]

Consider the following trivial spec:

-------------------------------- MODULE bug2 --------------------------------
EXTENDS Naturals

VARIABLE x

A == x' = IF x > 0 THEN x-1 ELSE x

Spec == (x = 5) /\ [][A]_x /\ WF_x(A)

Prop == <>[](x = 0)

=============================================================================

In the toolbox (1.5.7) I select Spec as the temporal formula for the spec, and Prop must hold for every behaviour.

This checks fine in model checking mode, but simulation mode reports an error on temporal properties!

Strangely, if I change Prop like this:

Prop == <>[](x = 1)

Then simulation mode no longer reports an error. But of course model checking mode complains!

Is this a TLC bug, or am I missing something?

[lemmy]

Not a regression in recent versions:

TLC2 Version 2.03 of 10 March 2011
Running Random Simulation with seed 8799409219208267402.
Parsing file MC.tla
Parsing file Github204.tla
Parsing file /home/markus/src/TLA/tla/tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /home/markus/src/TLA/tla/tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /home/markus/src/TLA/tla/tlatools/class/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Github204
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module MC
Starting... (2018-11-01 20:05:54)
Implied-temporal checking--satisfiability problem has 1 branches.
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
x = 5

State 2: <Action line 8, col 6 to line 8, col 34 of module Github204>
x = 4

State 3: <Action line 8, col 6 to line 8, col 34 of module Github204>
x = 3

State 4: <Action line 8, col 6 to line 8, col 34 of module Github204>
x = 2

State 5: <Action line 8, col 6 to line 8, col 34 of module Github204>
x = 1

State 6: <Action line 8, col 6 to line 8, col 34 of module Github204>
x = 0

State 7: Stuttering
Back to state 6.

The number of states generated: 7
Simulation using seed 8799409219208267402 and aril 0
Finished. (2018-11-01 20:05:54)

Running simulation (-Dtlc2.tool.Simulator.experimentalLiveness=true) with the LiveCheck implementation used by exhaustive search instead of its default LiveCheck1 does not report a bogus liveness violation.

Changing LiveCheck1 line 141 to not add an (outgoing) transition to the last state of the trace - similar to what is done in LiveCheck#checkTrace - fixes this problem:

if (i < stateTrace.size() - 1) {
    destNode.addTransition(destNode, slen, alen, os.checkAction(destState, destState));
}

---

Related, LiveCheck1#comStack - of type ObjectStack - is apparently not thread safe and thus occasionally either leads to a deadlock or a NullPointerException as observed by tlc2.tool.simulation.SimulatorTest.testLivenessViolation():

Implied-temporal checking--satisfiability problem has 1 branches.
Computed 1 initial states...
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerException
java.lang.NullPointerException
    at tlc2.tool.liveness.LiveCheck1.extractComponent(LiveCheck1.java:854)
    at tlc2.tool.liveness.LiveCheck1.checkComponent(LiveCheck1.java:812)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:805)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkSccs(LiveCheck1.java:795)
    at tlc2.tool.liveness.LiveCheck1.checkTrace(LiveCheck1.java:504)
    at tlc2.tool.SimulationWorker.simulateRandomTrace(SimulationWorker.java:402)
    at tlc2.tool.SimulationWorker.run(SimulationWorker.java:225)

[saffroy]

Thanks for confirming, and for suggesting the workaround!