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

[Stephan Merz]

I am not completely sure if I understand your question, but without a fairness hypothesis there is always an execution that never performs any action and therefore will not satisfy any formula <>P unless P is true in the initial state.

Stephan

On 17 Jun 2022, at 04:06, 钱晨 <allenh...@gmail.com> wrote:

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8701ca11-e5c4-4354-9885-d877a3b81caen%40googlegroups.com.