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

*From*: Jones Martins <jonesmvc@xxxxxxxxx>*Date*: Tue, 9 May 2023 11:12:12 -0700 (PDT)*References*: <8a4e5219-e482-49b5-aa16-f31f9b673f6en@googlegroups.com> <E251BE92-59D4-4BB5-ABE8-70A1FC631289@gmail.com>

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.

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

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

**Re: [tlaplus] Liveness only when a certain condition holds***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Parser Error** - 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):