I found a fix, but I'm not very convinced...
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