业务描述

这个业务是描述时间小时状态值的变动，12小时制，到12后，下一个值回到1.

解析

所以系统状态值范围1..12，
规则是：下一次状态值变动是+1，
系统变量hr，状态变化是递增加1，到达12后，下一个值变为1，如此循环下去。

代码例子

EXTENDS Naturals
VARIABLE hr
HCini  ==  hr \in (1 .. 12)
HCnxt  ==  hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC  ==  HCini /\ [][HCnxt]_hr
--------------------------------------------------------------
THEOREM  HC => []HCini

总结

上面简单的例子，容易说明清楚，TLA+在描述什么。
最后的THEOREM解释一下，

在 TLA+ 中，THEOREM HC => []HCini 是一个定理声明，它的含义可以通过对其中的符号进行解释来理解。

THEOREM: 表示这是一个定理声明，即要证明的命题。
HC: 是一个逻辑表达式或谓词，表示一个条件。
=>: 是逻辑蕴含符号，表示如果前提成立，则结论也成立。
[]: 是 Temporal Logic of Actions（动作时态逻辑，简称 TLA）中的“always”运算符，表示对后面的表达式进行无限次的全局性质检验。
HCini: 是一个逻辑表达式或谓词，表示一个初始条件。
因此，THEOREM HC => []HCini 的含义可以解释为：“如果 HC 是成立的，那么 HCini 是一个全局性质，即在任何时刻都满足的初始条件。”

这个定理声明表达了一个关于系统行为的性质，它指出只要 HC 是满足的，那么在任何执行序列中，初始条件 HCini 都会一直成立。换句话说，HC 是 HCini 的强保证。

要验证这个定理是否成立，您需要使用 TLA+ 工具进行模型检验或形式化证明。