When people think of representing the execution of a system by a behavior (a sequence of states), they think of some kind of global clock that tells the system to change state each time it ticks. But that's not a good way to represent real systems. There is no single global clock that controls all systems. Every system would need its own clock. It's difficult to speak of relations between specifications, such as that one implements the other, if the two systems have different global clocks. It would be like trying to relate two interacting physical systems described in terms of two different physical clocks that ran at different, varying rates. A system is a physical device that operates in real time. Although all physical devices operate continuously, we can pretend that a digital system changes state instantaneously at discrete times. We can view the behavior that describe the execution as the frames of a video. (Readers born in the last millenium can think of it as a film.) The requirement for the video to be a valid representation is that every state the system reaches appears in at least one frame. A specification describes the set of all valid videos of correct system behaviors. If we speed up the camera's frame rate so that the same state appears on more frames, it's still a valid video of the same system, so it should still satisfy the specification. For any two system specifications A and B, specification A implements (or refines) specification B means that every valid video of both systems that satisfies A also satisfies B. Note that we can turn any valid video of A that shows the states of both systems into a valid video of both A and B by adding extra frames (stuttering steps of A) if necessary. Why should a video of one system show the state of another? Why should a video of an hour/minute clock show the seconds display? To answer this, we need to consider what a state is. When we say that a system execution is represented by a behavior, it's natural to assume that each of those states is an assignment of values to the variables that describe the system, and perhaps also to variables that describe how the system's environment interacts with it. But a TLA+ specification is a mathematical formula. Moreover, a semantics for any specification language translates any spec in that language to a mathematical formula. So let's look at what mathematical formulas mean. The formula x + y = 1 is an assertion about the values of the variables x and y . But it's not an assertion about a universe containing only the variables x and y . You write another formula x - y = z without having to say, hey I've now added the variable z to my universe of discourse. The formula x + y = 1 is implicitly an assertion about a universe described by the values of all possible variables. It just makes an assertion about the variables x and y . It doesn't imply that there are no other variables. It's now easy to see that a state should be an assignment of values to all possible variables. In TLA+, the names of all possible variables are all the identifiers allowed by the language. (If a module defines Init to equal some expression, then the universe still contains a variable named Init; we just can't use it in that module.) So our videos show the values of the (theoretically) infinite number of possible variables. The spec Spec == (v=0) /\ [][v' = v+1]_v(where v is declared to be a variable) allows infinitely many behaviors, because it allows behaviors in which every variable other than v can assume any value in any of its states. I hope it is now even more obvious why we shouldn't be able to write a spec that doesn't allow stuttering steps. A spec of an hour/minute clock asserting that the minute display changes with every step would say that the universe can contain no clock that displays seconds. That would be a really weird spec. This may sound terribly complicated, saying that the simple specification Spec above should allow so many behaviors. It shouldn't. When you were a child, it didn't seem complicated that the formula x + y = 1 allowed z , w , v , u etc. to have any values. It would have been complicated if the formula implied that those other variables didn't exist. |
||