Eventual action

[vit...@ump.edu.my]

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.

[Stephan Merz]

Hello,

triyng to check eventual action as e.g. <><<hr = 1 => hr' = 2>>_hr (for HourClock example).

First, note that this formula is quite certainly not what you intend to verify. It is true of a behavior if eventually the variable hr changes value and its value in the first state is different from one. (An implication is true if the formula on its left-hand side is false.)

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?

Well, TLC's error message is pretty explicit here. As explained in Specifying Systems (chapter 14.2.4), TLC checks only a subset of temporal formulas, and <><<A>>_v is not part of that subset. TLC can check that each of the following formulas holds of the HourClock specification (with fairness):

   <>(hr = 2)

   []<><< hr=1 /\ hr' = 2 >>_hr

   <>[][ hr=1 => hr' = 2 ]_hr

Hope this helps,

Stephan

[vit...@ump.edu.my]

Dear Stephan,

very helpful, thank you!

Vitaliy.