Checking reachability

[Chris]

Hi,

I'm trying to show that every value can be chosen in a Paxos like setting.

Following the approach here: https://groups.google.com/g/tlaplus/c/A58EEr7YWGg

I've tried the following properties.

```

Values == {1,2}

Prop_1  ==  [](~Chosen(1))

Prop_2  ==  [](~Chosen(2))

Prop_n1 == ~[](~Chosen(1))

Prop_n2 == ~[](~Chosen(2))

```

With all of them being set in the PROPERTIES field in the config.

In testing both Prop_1 and Prop_2 produce counterexamples as expected.

However both Prop_n1 and Prop_n2 also produces counterexamples.

Why is this since I'd expect that if Prop_1 and Prop_2 are false (ie produce a counter-example) then negating them should be true?

Thanks,

Chris

[Stephan Merz]

A property P is valid if it holds in every run. In other words, P is not valid if and only if there exist runs that do not satisfy P (i.e., satisfy ~P). This does not mean that all runs satisfy ~P.

In your example, TLC tells you that there are some runs that satisfy Prop_1 / Prop_2 and some that do not.

Stephan

--
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/672137231.2107000.1653476007745%40mail.yahoo.com.

[Chris]

Ah my faulty assumption was that properties applied to all possible runs from a state, hence negating them is fine. However if I am interpreting you correctly, always and eventually just apply to states within the current run.

Is there any way to check some property over all runs, without resorting to parsing the counterexamples?

Thanks,

Chris

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B46B8446-3AC7-4F6F-A8B9-655AD9BB1333%40gmail.com.