Chapter 9 State Machines 9.1 State machines State machines are an abstract model of step-by-step processes, and accordingly, they come up in many areas of computer science. You may already have seen them in a digital logic course, a compiler course, or a probability course. 9.1.1 Basic definitions A state machine is really nothing more than a binary relation on a set, except that the elements of the set are called “states,” the relation is called the transition relation, and a pair (p, q) in the graph of the transition relation is called a transition. The transition from state p to state q will be written p −→ q. The transition relation is also called the state graph of the machine. A state machine also comes equipped with a designated start state. State machines used in digital logic and compilers usually have only a finite number of states, but machines that model continuing computations typically have an infinite number of states. In many applications, the states, and/or the transi-tions have labels indicating input or output values, costs, capacities, or probabili-ties, but for our purposes, unlabelled states and transitions are all we need.1 Example 9.1.1. A bounded counter, which counts from 0 to 99 and overflows at 100. The transitions are pictured in Figure 9.1, with start state zero. This machine isn’t much use once it overflows, since it has no way to get out of its overflow state. Example 9.1.2. An unbounded counter is similar, but has an infinite state set. This is harder to draw :-) Example 9.1.3. In the movie Die Hard 3: With a Vengeance, the characters played by Samuel L. Jackson and Bruce Willis have to disarm a bomb planted by the diaboli- cal Simon Gruber: 1We do name states, as in Figure 9.1, so we can talk about them, but the names aren’t part of the state machine. 135136 CHAPTER 9. STATE MACHINES 0 1 299 overflowstartstateFigure 9.1: State transitions for the 99-bounded counter. Simon: On the fountain, there should be 2 jugs, do you see them? A 5-gallon and a 3-gallon. Fill one of the jugs with exactly 4 gallons of water and place it on the scale and the timer will stop. You must be precise; one ounce more or less will result in detonation. If you’re still alive in 5 minutes, we’ll speak. Bruce: Wait, wait a second. I don’t get it. Do you get it? Samuel: No. Bruce: Get the jugs. Obviously, we can’t fill the 3-gallon jug with 4 gallons of water. Samuel: Obviously. Bruce: All right. I know, here we go. We fill the 3-gallon jug exactly to the top, right? Samuel: Uh-huh. Bruce: Okay, now we pour this 3 gallons into the 5-gallon jug, giving us exactly 3 gallons in the 5-gallon jug, right? Samuel: Right, then what? Bruce: All right. We take the 3-gallon jug and fill it a third of the way... Samuel: No! He said, “Be precise.” Exactly 4 gallons. Bruce: Sh - -. Every cop within 50 miles is running his a - - off and I’m out here playing kids games in the park. Samuel: Hey, you want to focus on the problem at hand? Fortunately, they find a solution in the nick of time. We’ll let the reader work out how. The Die Hard series is getting tired, so we propose a final Die Hard Once and For All. Here Simon’s brother returns to avenge him, and he poses the same challenge, but with the 5 gallon jug replaced by a 9 gallon one. We can model jug-filling scenarios with a state machine. In the scenario with a 3 and a 5 gallon water jug, the states will be pairs, (b, l) of real numbers such that� � 9.1. STATE MACHINES 137 0 ≤ b ≤ 5, 0 ≤ l ≤ 3. We let b and l be arbitrary real numbers. (We can prove that the values of b and l will only be nonnegative integers, but we won’t assume this.) The start state is (0, 0), since both jugs start empty. Since the amount of water in the jug must be known exactly, we will only con-sider moves in which a jug gets completely filled or completely emptied. There are several kinds of transitions: 1. Fill the little jug: (b, l) −→ (b, 3) for l < 3. 2. Fill the big jug: (b, l) −→ (5, l) for b < 5. 3. Empty the little jug: (b, l) −→ (b, 0) for l > 0. 4. Empty the big jug: (b, l) −→ (0, l) for b > 0. 5. Pour from the little jug into the big jug: for l > 0, (b + l, 0) if b + l ≤ 5,(b, l) −→ (5, l − (5 − b)) otherwise. 6. Pour from big jug into little jug: for b > 0, (0, b + l) if b + l ≤ 3,(b, l) −→ (b − (3 − l), 3) otherwise. Note that in contrast to the 99-counter state machine, there is more than one possible transition out of states in the Die Hard machine. Machines like the 99-counter with at most one transition out of each state are called deterministic. The Die Hard machine is nondeterministic because some states have transitions to sev-eral different states. Quick exercise: Which states of the Die Hard 3 machine have direct transitions to exactly two states? 9.1.2 Reachability and Preserved Invariants The Die Hard 3 machine models every possible way of pouring water among the jugs according to the rules. Die Hard properties that we want to verify can now be expressed and proved using the state machine model. For example, Bruce’s character will disarm the bomb if he can get to some state of the form (4, l). A (possibly infinite) path through the state graph beginning at the start state corresponds to a possible system behavior; such a path is called an execution of the state machine. A state is called reachable if it appears in some execution. The bomb in Die Hard 3 gets disarmed successfully because the state (4,3) is reachable. A useful approach in analyzing state machine is to identify properties of states that are preserved by transitions.138 CHAPTER 9. STATE MACHINES Definition 9.1.4. A preserved invariant of a state machine is a predicate, P , on states, such that whenever P (q) is true of a state, q, and q −→ r for some state, r, then P (r) holds. The Invariant Principle If a preserved invariant of a state machine is true for the start state, then it is true for all reachable states. The Invariant Principle is nothing more than the Induction Principle reformu-lated in a convenient form for state machines. Showing that a predicate is true in the start state is the base case of the induction, and showing that a predicate is a preserved invariant is the inductive step.2 Die Hard Once and For All Now back to Die Hard Once and For All. This time there is a 9 gallon
View Full Document
Unlocking...