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

[tlaplus] How can I check all histories about the TLA+ execution in toolbox?

I have recently written a 2PC specification in the toolbox, run a simple model on it(run a model with 3 participants) and successfully passed the model. 

While I cannot know whether all history goes to the end that satisfies the liveness requirement(such as all goes to commit state). So can I record all histories of the model check without writing a fairness function

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/8701ca11-e5c4-4354-9885-d877a3b81caen%40googlegroups.com.