3/1/101Albert R Meyer, March 3, 2010 Mathematics for Computer Science MIT 6.042J/18.062J State Machines lec 5W.1 Albert R Meyer, March 3, 2010 State machines step by step processes (may step in response to input not today) lec 5W.2 Albert R Meyer, March 3, 2010 State machines The state graph of a 99-bounded counter: States: {0,1,…,99, overflow} 0 start state 1 2 overflow 99 Transitions: 0 i < 99 i i+1 99 overflow overflow overflow lec 5W.3 Albert R Meyer, March 3, 2010 Die Hard Picture source: http://movieweb.com/movie/diehard3/lec 5W.4 Albert R Meyer, March 3, 2010 Die Hard Simon says: 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. lec 5W.5 Albert R Meyer, March 3, 2010 Die Hard lec 5W.6 Image removed due to copyright restrictions. Supplies: Water 3 Gallon Jug 5 Gallon Jug Image by MIT OpenCourseWare.3/1/102Albert R Meyer, March 3, 2010 Die Hard Transferring water: 3 Gallon Jug 5 Gallon Jug lec 5W.7 Albert R Meyer, March 3, 2010 Die Hard Transferring water: 3 Gallon Jug 5 Gallon Jug lec 5W.8 Albert R Meyer, March 3, 2010 State: amount of water in jugs: (b,l) 0 b 5, 0 l 3 Start State: (0,0) Die hard state machine lec 5W.9 Albert R Meyer, March 3, 2010 State machines Die Hard Transitions: 1. Fill little jug: (b, l) (b, 3) for l < 3 2. Fill big jug: (b, l) (5, l) for b < 5 3. Empty little jug: (b, l) (b, 0) for l > 0 4. Empty big jug: (b, l) (0, l) for b > 0 lec 5W.10 Albert R Meyer, March 3, 2010 State machines 5. Pour big jug into little jug (i) If no overflow, then (b,l)(0,b+l) (ii) otherwise (b,l)(b(3l),3) 6. Pour little jug into big jug. Likewise b+l 3 lec 5W.11 Albert R Meyer, March 3, 2010 Die Hard Simon’s challenge: Disarm the bomb by putting precisely 4 gallons of water on the scale, or it will blow up. (You can figure out how)lec 5W.12 3/1/103Albert R Meyer, March 3, 2010 Die Hard once and for all What if have a 9 gallon jug instead? 3 Gallon Jug 5 Gallon Jug 9 Gallon Jug Can you do it? Can you prove it? lec 5W.20 Albert R Meyer, March 3, 2010 Preserved Invariants P(state) ::= “3 divides the number of gallons in each jug.” Die hard once and for all preserved invariant: lec 5W.22 P((b, l)) ::= (3|b AND 3|l) Albert R Meyer, March 3, 2010 Preserved Invariants Floyd’s Invariant Method (just like induction) Base case: Show P(start) Preservation case: Show if P(q) and , then P(r) Conclusion: P holds for all reachable states, including final state (if any) q r lec 5W.23 Albert R Meyer, March 3, 2010 Die Hard Once & For All Corollary: No state (4,x) is reachable, so Bruce Dies! lec 5W.24 Albert R Meyer, March 3, 2010 The Diagonal Robot the robot is on a grid y 0 1 2 3 210 x lec 5W.25 Albert R Meyer, March 3, 2010 The Diagonal Robot y 0 1 2 3 210 x it can move diagonally lec 5W.26 Water Image by MIT OpenCourseWare. Image by MIT OpenCourseWare. Image by MIT OpenCourseWare.3/1/104Albert R Meyer, March 3, 2010 The Diagonal Robot y 0 1 2 3 210 x can it get from (0,0) to (1,0)? ? GOAL lec 5W.27 Albert R Meyer, March 3, 2010 Robot Preserved Invariant P((x, y)) ::= x + y is even move adds ±1 to both x & y, preserving parity of x+y. Also, P((0, 0)) is true. NO! preserved invariant: lec 5W.28 Albert R Meyer, March 3, 2010 Robot Preserved Invariant So all positions (x,y) reachable from (0,0) have x + y even. But 1 + 0 = 1 is odd, so (1,0) is not reachable. lec 5W.29 Albert R Meyer, March 3, 2010 Robert W Floyd (19342001) Eulogy by Knuth: http://www.acm.org/pubs/membernet/stories/floyd.pdf Picture source: http://www.stanford.edu/dept/news/report/news/november7/floydobit-117.html lec 5W.38 Albert R Meyer, March 3, 2010 Team Problems Problems 1 & 2 lec 5W.39 Photograph removed due to copyright restrictions. Image by MIT OpenCourseWare.MIT OpenCourseWare http://ocw.mit.edu 6.042J /18.062J Mathematics for Computer Science Spring 2010 For information about citing these materials or our Terms of Use, visit: http://ocw.mit.edu/terms.