[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Checking reachability


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?



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.