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

*From*: "'Chris' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Wed, 25 May 2022 11:53:04 +0000 (UTC)*References*: <672137231.2107000.1653476007745.ref@mail.yahoo.com> <672137231.2107000.1653476007745@mail.yahoo.com> <B46B8446-3AC7-4F6F-A8B9-655AD9BB1333@gmail.com>

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

-----Original Message-----

From: Stephan Merz <stephan.merz@xxxxxxxxx>

To: tlaplus@xxxxxxxxxxxxxxxx

Sent: Wed, May 25, 2022 12:01 pm

Subject: Re: [tlaplus] Checking reachability

From: Stephan Merz <stephan.merz@xxxxxxxxx>

To: tlaplus@xxxxxxxxxxxxxxxx

Sent: Wed, May 25, 2022 12:01 pm

Subject: Re: [tlaplus] Checking reachability

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/A58EEr7YWGgI'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.

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.

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

**References**:**[tlaplus] Checking reachability***From:*'Chris' via tlaplus

**Re: [tlaplus] Checking reachability***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Checking reachability** - Next by Date:
**[tlaplus] TLA+ video course: Can't add invariants/property from imported module** - Previous by thread:
**Re: [tlaplus] Checking reachability** - Next by thread:
**[tlaplus] TLA+ video course: Can't add invariants/property from imported module** - Index(es):