Thank you very much for your answer.
Maybe I am not clear in my question. I can understand the spec. But I am just wondering where the box operator comes from.
In state equations of a physical system or in an automaton, two things are given, the initial state and the function to map the current state to the next state.
Initial state: hr = 1
Next state relation: hr' = IF hr # 12 THEN hr + 1 ELSE 1
The system starts in the initial state and the next state relation defines how the system evolves. Since the system follows this law, therefore the law is true.
Just wondering why there is a difference between TLA+ spec and the typical automaton definition.
Regards,
Xiaoming
On Thursday, April 13, 2017 at 11:28:47 AM UTC-7, Leslie Lamport wrote:
You say that HCnxt is, by definition, always true. By that reasoning, if the spec had defined HCini to equal hr = 1, would that always be true? How would you specify an hour clock that had to begin with hr = 1? And if I were to write the definition
FalseTheorem == 1+2 = 4
would that mean that 1+2 = 4 is always true? What is the difference between a definition and a theorem?