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

[tlaplus] Re: CTL Property to Temporal Property

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/0e26c2e5-dd2b-4b97-bddd-4205e4ec88e1n%40googlegroups.com.