---- MODULE hourclock ---- \* TODO: two clocks EXTENDS Naturals (*--algorithm hourclock variable hr = 1; \* hour begin A: while TRUE do if hr = 12 then hr := 1; else with x = 1 do hr := hr + x; end with; end if; end while; end algorithm; *) ====