[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: xmz...@xxxxxxxxx*Date*: Thu, 13 Apr 2017 14:48:50 -0700 (PDT)*Cc*: xmz...@xxxxxxxxx*References*: <b03b7da8-9946-443a-aebd-2f81fc0e3596@googlegroups.com> <99d6b2a8-7ee8-4d74-9335-fad92c787613@googlegroups.com>

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 definitionFalseTheorem == 1+2 = 4would that mean that 1+2 = 4 is always true? What is the difference between a definition and a theorem?

**References**:**Hourly clock spec: why it needs the temporal-logic operator box []***From:*xmz . . .

**Re: Hourly clock spec: why it needs the temporal-logic operator box []***From:*Leslie Lamport

- Prev by Date:
**Re: Differences between TLA+ Specification and Property Based Testing** - Next by Date:
**Re: Hourly clock spec: why it needs the temporal-logic operator box []** - Previous by thread:
**Re: Hourly clock spec: why it needs the temporal-logic operator box []** - Next by thread:
**Re: Hourly clock spec: why it needs the temporal-logic operator box []** - Index(es):