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

*From*: "'Chris' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Wed, 25 May 2022 10:53:27 +0000 (UTC)*References*: <672137231.2107000.1653476007745.ref@mail.yahoo.com>

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.

**Follow-Ups**:**Re: [tlaplus] Checking reachability***From:*Stephan Merz

- Prev by Date:
**[tlaplus] CfP: TLA+ Conference 2022 - Deadling July 01** - Next by Date:
**Re: [tlaplus] Checking reachability** - Previous by thread:
**Re: [tlaplus] Deadline CfP soon: TLA+ Conference 2022** - Next by thread:
**Re: [tlaplus] Checking reachability** - Index(es):