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

*From*: Willy Schultz <will62794@xxxxxxxxx>*Date*: Tue, 14 Sep 2021 08:32:02 -0700 (PDT)*References*: <f7a1388e-b405-4ceb-bb6c-dd62fb92bd00n@googlegroups.com> <0e26c2e5-dd2b-4b97-bddd-4205e4ec88e1n@googlegroups.com>

To follow up on this, you may be able to use TLC to check the CTL formula

AG(P1) => EF(P2)

with the following technique. You can check AG(P1) by simply checking that the formula []P1 holds. Separately, you can check EF(P2) via a simple "hack". The CTL formula EF(P2) is true iff there exists some system behavior such that F(P2) (written <>P2 in TLA+) holds. So, you can check the formula [](~P2) with TLC and see if the model checker returns a violation. If it does, then this means that there exists some behavior in which P2 holds at some point, so it means that EF(P2) must hold. If the model checker completes without a violation, it must mean that EF(P2) does not hold. So, this gives you a way to check EF(P2). I do not think you can do this in one step, though i.e. by checking a single temporal formula with TLC.

On Tuesday, September 14, 2021 at 9:33:58 AM UTC-4 Willy Schultz wrote:

To avoid any confusion, could you clarify what "SM1", "SM2", "s1" and "s2" are in your formula/specification? It's unclear to me what "(SM1 \ in s1)" and "(SM1 \in s2)" means given what you wrote.More generally, if you consider the following abstract CTL property (where P1 and P2 are state predicates):AG(P1) => EF(P2)I believe it is not possible to express this directly in TLA+ (or in LTL), since TLA+ can only express properties that hold for all behaviors of a system, whereas CTL formulas allow you to quantify over all behaviors of a system. (Or, at least, the formula is not expressible in a form that the model checker, TLC, can handle.) You may be able to use the model checker to check the above formula, though, with a bit of a "workaround". It would help to first be clear on the statement of your desired property, though.On Tuesday, September 14, 2021 at 7:51:27 AM UTC-4 uindc.st...@xxxxxxxxx wrote:I would like to model check this CTL specification as TP in TLA+AG(SM1.state =s1) -> EF (SM1.state =s2)Is this: (SM1 \ in s1) =>[] <> (SM1 \in s2) the correct translation?

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/a2834761-827e-415b-9301-1b124f6052bdn%40googlegroups.com.

**References**:**[tlaplus] CTL Property to Temporal Property***From:*Paulina Maurer

**[tlaplus] Re: CTL Property to Temporal Property***From:*Willy Schultz

- Prev by Date:
**[tlaplus] Re: CTL Property to Temporal Property** - Next by Date:
**[tlaplus] PlusCal resources?** - Previous by thread:
**[tlaplus] Re: CTL Property to Temporal Property** - Next by thread:
**[tlaplus] PlusCal resources?** - Index(es):