The timer discipline of Visualize.Layout.Force.Simulation (spec/06 §9.4), as a model.

What is abstracted: nodes, links and forces are gone; alpha is a three-valued heat (0 below alpha_min, 1 and 2 above) and alpha_target is target_hot (at or above alpha_min, or not). What is kept exactly: every message the GenServer handles, the deferred :start_simulation that init/1 enqueues, and the two kinds of tick message — a live one from the timer the server is waiting on, and a stale one from a timer that was cancelled after its message had already reached the mailbox.

Three constants select the intended behaviour (true, the default) or the defect the code shipped with; the negative tests in test/specs/ prove the checker finds each:

• guarded_deferred_start — :start_simulation does not arm a second timer when a :start already did.
• restart_keeps_stopped — :restart resets alpha but does not start a stopped simulation.
• tagged_ticks — a tick carries its timer's reference and a stale tick is ignored, so a stop followed by a start cannot leave two tick chains running.

env_active switches the client off, which is how the cooling-down property is stated: with no client acting, a target below alpha_min leads to a stopped simulation.