Hourly clock spec: why it needs the temporal-logic operator box []

[xmz...@xxxxxxxxx]

Hi All,

In the page 16 of TLA+ book, it writes:
    "To express (ii), we use the temporal-logic operator [] (pronounced box). the temporal formula []F asserts that formula F is always true."

HC == HCini /\ [][HCnxt]_hr

Also in the spec, HCnxt == hr' = IF hr# 12 THEN hr + 1 ELSE 1.

The next step relation is defined as the above formula., which by definition is always true. So my question is that why the spec needs the temporal-logic operator box to assert the next step relation is always true.

I just started reading the book and has zero knowledge of temporal logic. And the box operator looks very confusing to me. As the initial condition and the next step relation seem to be enough to define the behavior.

Thanks a lot,

Xiaoming