Some invariants which is needed to move forward:

[jlouis]

Timers are lock-stepped to the model. So there is always a
relationship between a timer and its occurrence in the model.

(add a timer trigger which is module local and does the real thing)

• When a timer triggers, it is removed from the model.
• ASSERT: The timer which triggers is the one removed from the model.

(add a way to cancel timers correctly)

• When we cancel a timer, it is removed from the model.
• The SUT will call cancel_timer in this case.
• ASSERT: The timer we cancel is the one removed.

[jlouis]

This has already been built into the clustered EQC model.