[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Different trace for a temporal property violation (stuttering) using same seed and fp


If I have a temporal property violation trace, get the seed and fp from the TLC output and run TLC again using these parameters, should I get the same trace?

I'm getting random traces despite passing same seed and fp. For safety property violations, it's working fine.


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 on the web visit https://groups.google.com/d/msgid/tlaplus/0b475d7a-4f1b-4924-9ca5-ad92759e9764n%40googlegroups.com.