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

Re: [tlaplus] Liveness only when a certain condition holds



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.