Hello,
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.