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

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

--
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/99B54A7C-F7A4-40BB-A93F-AE5198698553%40gmail.com.