[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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?