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?