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

[钱晨 <allenhandora@xxxxxxxxx>]

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.