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

*From*: Jones Martins <jonesmvc@xxxxxxxxx>*Date*: Wed, 10 May 2023 12:46:57 -0700 (PDT)*References*: <8a4e5219-e482-49b5-aa16-f31f9b673f6en@googlegroups.com> <E251BE92-59D4-4BB5-ABE8-70A1FC631289@gmail.com> <545be17b-3555-477d-a506-dc7baf5ca99fn@googlegroups.com> <55724505-e203-4176-a2c8-72a1d95ef0f3n@googlegroups.com> <d49bbe36-1f70-545f-b251-7757e342f07c@gmail.com> <CABW84Kzv+Vb63e5WhgbwjcZjfckvH2dL5tpOebn7vy2ST3e8mQ@mail.gmail.com> <e68332b1-db5b-4814-b92d-db8435e1f539n@googlegroups.com>

Just to illustrate what is happening, I'm sharing 8 states out of the 17-state trace I got after verifying whether Spec satisfies Property (this time, with three nodes instead of two).

This trace is slightly edited for clarity, highlighting changed variables in green.

As a reminder, this is Property:

Property ==

[](

(/\ ThereIsAnElection

/\ []EveryoneStaysActiveDuringElection) =>

<>ElectionWorks

)

[](

(/\ ThereIsAnElection

/\ []EveryoneStaysActiveDuringElection) =>

<>ElectionWorks

)

According to the second condition in Property, state 8 shouldn't happen, because no element in 02_inElectionImpliesActive should be FALSE.

Alias 02_inElectionImpliesActive is defined as [ node \in NodeSet |-> InElection(node) => isActive[node] ],

whereas EveryoneStaysActiveDuringElection is defined as \A node \in NodeSet: InElection(node) => isActive[node].

1: <Initial predicate>

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

2: Fail

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

3: CheckCoordinator

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

4: Election0

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

5: Election1

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

6: Recover

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

7: Election2

/\ 00_inElection = <<TRUE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

8: Fail

/\ 00_inElection = <<TRUE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<FALSE, TRUE, TRUE>>

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

2: Fail

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

3: CheckCoordinator

/\ 00_inElection = <<FALSE, FALSE, FALSE>>

/\ 01_someNodeInElection = FALSE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

4: Election0

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

5: Election1

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

6: Recover

/\ 00_inElection = <<FALSE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

7: Election2

/\ 00_inElection = <<TRUE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<TRUE, TRUE, TRUE>>

8: Fail

/\ 00_inElection = <<TRUE, TRUE, FALSE>>

/\ 01_someNodeInElection = TRUE

/\ 02_inElectionImpliesActive = <<FALSE, TRUE, TRUE>>

...

Interestingly, checking Property2 == [](ThereIsAnElection => <>ElectionWorks) against

Next2 == Next /\ EveryoneStaysActiveDuringElection'

Spec2 == Init /\ [][Next2]_vars /\ Fairness

works just fine. (Thanks again, Hillel!)

So there's a problem in my definition of Property that I cannot find.

Best regards, and thanks again, everyone,

Jones

On Wednesday, 10 May 2023 at 16:11:15 UTC-3 Jones Martins wrote:

Hi everyone,I'm back to square one after increasing the number of nodes and checking whether Spec satisfies Property.TLC keeps showing state transitions that shouldn't happen, but checking whether Spec2 satisfies Property2 still works, so that has been my current approach.Best,JonesOn Tuesday, 9 May 2023 at 18:01:00 UTC-3 Jones Martins wrote:Hi Hillel,Your suggestion worked! That's the power of action constraints... The state space was different, though, and I'm not sure that's a problem.Before:Diameter: 22States found: 791Distinct: 355After:Diameter: 22States found: 704Distinct: 316JonesOn Tue, 9 May 2023 at 17:19, Hillel Wayne <hwa...@xxxxxxxxx> wrote:--I'd suggest a slightly different way of doing the same thing:

Next2 ==Next /\EveryoneStaysActiveDuringElection'

Spec2 == Init /\ [][Next2]_vars /\ Fairness

As for the initial problem, I think it's because

EveryoneStaysActiveDuringElectionis true when there isn't an election or if no nodes are part of the election, which the new version doesn't have. Maybe that's part of it?H

On 5/9/2023 2:44 PM, Jones Martins wrote:

Hi again,

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

Instead of verifying

Property ==

[](

(/\ 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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/55724505-e203-4176-a2c8-72a1d95ef0f3n%40googlegroups.com.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/EO9ff0OBqtA/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d49bbe36-1f70-545f-b251-7757e342f07c%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/baea1ec0-47a0-42b5-b250-20938dedac5fn%40googlegroups.com.

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

**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

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

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

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

**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):