--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 EveryoneStaysActiveDuringElection is 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+unsubscribe@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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d49bbe36-1f70-545f-b251-7757e342f07c%40gmail.com.