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

Eventual action


triyng to check eventual action as e.g. <><<hr = 1 => hr' = 2>>_hr (for HourClock example).
Syntax analyses shows no errors, but then TLC says:

"TLC threw an unexpected exception.
Temporal formulas containing actions must be of forms <>[]A or []<>A"

What formulation will be correct for eventual action?

Thank you.