Re: [tlaplus] Checking reachability

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 25 May 2022, at 12:53, 'Chris' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

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

--
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/672137231.2107000.1653476007745%40mail.yahoo.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/B46B8446-3AC7-4F6F-A8B9-655AD9BB1333%40gmail.com.