Other print behavior: TLC executes print statements multiple times if they occur after a nondeterministic value initialization. For example, this prints "Hello" twice:
EXTENDS Integers, TLC
VARIABLES clock
Init == /\ clock \in {0, 1}
/\ Print("Hello", TRUE)
Tick == clock' = 1 - clock
Spec == Init /\ [][Tick]_<<clock>>
Whereas this prints "Hello" only once:
EXTENDS Integers, TLC
VARIABLES clock
Init == /\ Print("Hello", TRUE)
/\ clock \in {0, 1}
Tick == clock' = 1 - clock
Spec == Init /\ [][Tick]_<<clock>>
A deterministic Init will also only print "Hello" once:
EXTENDS Integers, TLC
VARIABLES clock
Init == /\ clock = 0
/\ Print("Hello", TRUE)
Tick == clock' = 1 - clock
Spec == Init /\ [][Tick]_<<clock>>
For this case though, like Stephen said trace reconstruction seems to be the culprit.
On Thursday, May 14, 2015 at 1:50:49 AM UTC-7, Leslie Lamport wrote:
Stephan is correct. Note that when model checking a non-deterministic spec such as a multi-process algorithm, even in the absence of errors, print statements may be executed in an unexpected order.