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

[Jones Martins <jonesmvc@xxxxxxxxx>]

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/545be17b-3555-477d-a506-dc7baf5ca99fn%40googlegroups.com.