[tlaplus] -simulate mode and trace length

[Arseny Sher <arsv.sher@xxxxxxxxx>]

Hey. When running -simulate with default -depth 100 on single core mean length is 100 as expected (I think there is always a stuttering step in my spec):

$ java -cp /home/arseny/tla2tools.jar tlc2.TLC MCProposerAcceptorReconfig.tla -config models/MCProposerAcceptorReconfig_p2_a4_sim.cfg -workers 40 -simulate

Progress: 1481792 states checked, 3231 traces generated (trace length: mean=100, var(x)=0, sd=0)

However, with -workers 40 it becomes less:

java -cp /home/arseny/tla2tools.jar tlc2.TLC MCProposerAcceptorReconfig.tla -config models/MCProposerAcceptorReconfig_p2_a4_sim.cfg -workers 40 -simulate
...
Progress: 41591033 states checked, 90451 traces generated (trace length: mean=34, var(x)=4355, sd=66)

I wonder why?

-- cheers, arseny

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5b609527-03f4-4202-853c-6f0b3b6e75c1n%40googlegroups.com.