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

*From*: Jones Martins <jonesmvc@xxxxxxxxx>*Date*: Tue, 9 May 2023 12:44:49 -0700 (PDT)*References*: <8a4e5219-e482-49b5-aa16-f31f9b673f6en@googlegroups.com> <E251BE92-59D4-4BB5-ABE8-70A1FC631289@gmail.com> <545be17b-3555-477d-a506-dc7baf5ca99fn@googlegroups.com>

Hi again,

I found a fix, but I'm not very convinced...

Instead of verifying

Property ==

[](

(/\ ThereIsAnElection

/\ EveryoneStaysActiveDuringElection) =>

<>ElectionWorks

)

[](

(/\ ThereIsAnElection

/\ EveryoneStaysActiveDuringElection) =>

<>ElectionWorks

)

I created a new formula Next2, where there's a modified version of my Fail(node) action (not contained in the first post): Fail2(node) == ~InElection(node) /\ Fail(node).

Then I modified Property into Property2 and verified that Spec == Init /\ [][Next2]_vars /\ Fairness satisfies Property2:

Property2 ==

[](ThereIsAnElection => <>ElectionWorks)

And it worked!

Interestingly, I went to verify that Spec satisfies Property, and it also worked?! Color me surprised!

The only thing I changed in the actual specification was in the Recover(node) action (also not contained in the first post). I realized stuttering was happening where it shouldn't when verifying Property2. That's not the problem I was having before, and I can't see why this modification would fix that.

Conclusion:

- the spec was incorrect;

- I still don't know why TLC returned the counterexamples that it did before;

- creating an alternative spec to verify certain properties is quite a good approach;

Jones

On Tuesday, 9 May 2023 at 15:12:12 UTC-3 Jones Martins wrote:

Hi Andrew and Stephan,Andrew, yes, the same thing happens, unfortunately.Stephan, I did try that before, but I forgot to add the second [], for some reason, and it still doesn't "filter" behaviors properly, although that's where I believe the problem is.I also tried changing the formula's formatting by writing it in one line, adding parentheses, but that's not the issue either.I don't doubt there's an error in my specification, but I expected that, if we define some property as []( (A /\ []B) => <>C ), TLC would ignore behaviors where either A is false or []B is false at some state before checking that <>C.Jones

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/55724505-e203-4176-a2c8-72a1d95ef0f3n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Liveness only when a certain condition holds***From:*Hillel Wayne

**References**:**[tlaplus] Liveness only when a certain condition holds***From:*Jones Martins

**Re: [tlaplus] Liveness only when a certain condition holds***From:*Stephan Merz

**Re: [tlaplus] Liveness only when a certain condition holds***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] Liveness only when a certain condition holds** - Next by Date:
**Re: [tlaplus] Liveness only when a certain condition holds** - Previous by thread:
**Re: [tlaplus] Liveness only when a certain condition holds** - Next by thread:
**Re: [tlaplus] Liveness only when a certain condition holds** - Index(es):