State Machines PDF

State Machines Keunhyuk Yeom Dept. of Computer Engineering Pusan National University [email protected]  State Machines  This lecture will describe how to model systems using State Machines  State Machine Basics  mot...

State Machines Keunhyuk Yeom Dept. of Computer Engineering Pusan National University [email protected]  State Machines  This lecture will describe how to model systems using State Machines  State Machine Basics  motivation, basic concepts, notation, simple examples  State Machine Variations  modeling complex systems, variables, actions, non-determinism  Reasoning about State Machines  invariants and constraints  Statecharts  a specific, popular graphical approach  Two Types(or Models) of State Machines  Moore machine  Mealy machine  Equivalence Test 2 Computer Engineering, Pusan National University  Why State Machines?  Goal: provide simple abstractions of complex systems  All computer systems are state machines  registers and memory are state  changes are transitions between states  a program defines the way in which initial states are transformed into final states  a programming language determines a set of programs (and hence, a set of machines)  Primary challenge will be to represent these very complex machines with simpler (more abstract) machines that we can reason about 3 Computer Engineering, Pusan National University  State Machines Are Used  When it is possible to abstract away irrelevant details, leaving only a small number of states  When we want to examine every possibility using model checking  For communication protocols and complex distributed algorithms (e.g., cache coherency) 4 Computer Engineering, Pusan National University  Some Notes  State machines are the modeling foundation for all of the other forms of modeling that we will be looking at (including Z, CSP, Temporal Logic, etc.)  No standard notation, although the concepts are widely agreed upon  Level of rigor will vary depending on needs and mood 5 Computer Engineering, Pusan National University  Informally...  A state machine captures the idea that a system progresses through a set of states by performing (or responding to) a set of actions.  Thus there are two key concepts  States  Actions  A state machine definition must say  what the possible states are  what initial states the machine may start in  what the possible actions are  how the state changes when actions occur 6 Computer Engineering, Pusan National University  What is a State?  A snapshot of the system  values of memory, registers  Set of values for variables  snapshot of running program's data  Control location(s)  snapshot of where a program is in its execution sequence(s)  Contents of communication channels  snapshot of a communication state 7 Computer Engineering, Pusan National University  A (Very) Simple State Machine  World's simplest (and most boring) state machine stop  States: {stop}  Actions: {}  Initial state: {stop} 8 Computer Engineering, Pusan National University  Another Simple Example alarm beep  States: {alarm}  Actions: {beep}  Initial state: {alarm} 9 Computer Engineering, Pusan National University  A More Interesting Example key gas brake M1 off idle moving crashed  States: {off, idle, moving, crashed}  Actions: {key, gas, brake}  Initial state: {off} 10 Computer Engineering, Pusan National University  A Small Variation key gas brake M2 off idle moving crashed key  One action may cause alternative transitions from the same state  This is referred to as non-determinism  Also note: machine now has a possibly infinite number of steps that it can take 11 Computer Engineering, Pusan National University  Formal Definition  A state machine M is a 4-tuple (S, A, I, T) with S : is a finite or infinite set of states I  S: is a finite set of initial states A : is a finite set of actions T : state transition “relation” over S x A x S  When S is finite, M is a finite state machine Notes: T is often represented by the symbol (Greek Delta). T is sometimes written in the form S x A  S, making it a true relation. 12 Computer Engineering, Pusan National University  Transitions  (s1, a, s2) is in T when there is an arrow a from s1 to s2 labeled a s1 s2  T is a relation because of nondeterminism (two arrows from the same source and with the same label, to different targets)  When T is a function we say M is a deterministic state machine  Actions are sometimes called labels, actions, or state transitions  A is sometimes called the alphabet of M 13 Computer Engineering, Pusan National University  Car Example (M1)  S = { off, idle, moving, crashed }  I = { off }  A = { key, gas, brake }  T = { (off, key, idle), (idle, gas, moving), (moving, brake, crashed) } Car == ( { off, idle, moving, crashed }, { off }, { key, gas, brake }, { (off, key, idle), (idle, gas, moving), (moving, brake, crashed) } ) 14 Computer Engineering, Pusan National University  Executions  Each triple, (s,a,s') in T is called a step of M  An execution is a finite or infinite sequence , where s0 is an initial state of M, and for all i, (si, ai+1, si+1 ) is in T (note must end in a state if finite and non-empty)  Examples     For a finite execution, the last state is called a final state of M (note: may be different elsewhere)  A state is reachable if it is a final state of a finite execution 15 Computer Engineering, Pusan National University  Traces  A (event-based or action-based) trace is the sequence of actions of an execution  < key, gas, brake >    A (state-based) trace is the sequence of states of an execution, or the sequence for each si  I.  < off, idle, moving, crashed>   16 Computer Engineering, Pusan National University  Behavior  The behavior of a machine M, (Beh(M)), is the set of all traces of M. Event based:  {, , , }  {, , , , ,...>  Note: a finite state machine can have infinite behavior 17 Computer Engineering, Pusan National University  Infinite State Machines  In general, state machines may not have a finite numbers of states  Example: integer counter inc inc inc 0 1 2 3 18 Computer Engineering, Pusan National University  Informally We want something like this: SimpleCounter == ( {0, 1, 2,...}, {0}, {inc}, {(0,inc,1), (1,inc,2), (2,inc,3),...} ) But "..." is not very precise Solution: you already know how 19 Computer Engineering, Pusan National University  Using Sets and Logic to Describe State Machines  The set of states is easy:   The transition for inc can be described by: Tinc == { (s,a,s'):  x {inc} x s' = s + 1 } where Tinc is the part of T that deals with inc  In general, we have T = Ta a A  So, SimpleCounter == (, {0}, {inc}, { (s,a,s'):  x {inc} x s' = s + 1 }) 20 Computer Engineering, Pusan National University  Interfaces and Environments  What is the difference between these machines? tick push-A left right blue red tock push-B  In general, a machine operates in an environment that can either observe an event or cause an event to occur.  Sometimes it helps to distinguish between observed and initiated events, or input and output actions 21 Computer Engineering, Pusan National University  Scalability  State can get huge for very simple systems  Often need more compact representations  Describe the set of states from which a transition appears through a predicate  Describe the `target’ through the changes to the source  Use text and not pictures  Focus on specialized aspects (such as event traces) 22 Computer Engineering, Pusan National University  Unexpected Actions  Consider the following machine push-A blue red push-B  What happens if I push button B when the machine is in the blue state?  Nothing happens  It is undefined -- anything can happen  It is an error  It can't happen 23 Computer Engineering, Pusan National University  The Story So Far  State machine basics  the state machine as 4-tuple  graphical notation  executions, behavior, traces  finite and infinite state machines  the problem of complexity & abstraction  In the Next, we will talk about  variables  preconditions, postconditions  input/output (arguments & results)  exceptions  nondeterminism  FSAs 24 Computer Engineering, Pusan National University  Recall: Infinite State Machines  In general, state machines may not have a finite numbers of states  Example: integer counter inc inc inc inc 0 1 2 3  How can we write this state machine down? 25 Computer Engineering, Pusan National University  Variables  We can use variables to "collapse" a large number of states  First step is to consider a "state" as representing the values of some variables inc inc inc inc x=0 x=1 x=2 x=3  Represented as a single box we have: inc Counter x: Int 26 Computer Engineering, Pusan National University  Multiple Variables  More generally, each state can be characterized in terms of the values that a set of variables take inc-x inc-x inc-x x=0 x=1 x=2 y=0 y=0 y=0 inc-y x=0 y=1 inc-y inc-x inc-y Counter x: Int y: Int 27 Computer Engineering, Pusan National University  State Space as a Function Space  We can model each state as a function.  Example  For the machine below one possible state might be: { (x 3), (y 5) }  note this is a function  Suppose after some operations the state changes to: { (x 4), (y 8) }  still a function, but a different one from below  So the state space is the set of all functions, and any individual state is one of those functions. inc-x inc-y Counter2 x: Int y: Int 28 Computer Engineering, Pusan National University  More Formally  For certain state machines we take the 4- tuple to be M = ( {S: Var Val}, I, A, T )  That is, the state is a (partial) function from variables to values  In practice, Var will be finite, although Val may be infinite  We will also insist that variables be typed  For the counter examples S = { {x}  } and S = { {x,y}  }  What about the transition relation? { (s,a,s'): S x {inc} x Ss'(x) = s(x) + 1 } 29 Computer Engineering, Pusan National University  EvenCounter bump bump bump x=0 x=2 x=4 x=1 x=3 bump EvenCounter x: Int 30 Computer Engineering, Pusan National University  EvenCounter  Set of states for EvenCounter is same as for Counter  Transition function { (s,a,s'): S x {bump} x S even(s(x))  s'(x) = s(x) + 2 }  This kind of specification is accurate, but unwieldy 31 Computer Engineering, Pusan National University  Alternative Notation  Counter header inc pre true precondition post x' = x + 1 postcondition  EvenCounter bump pre even(x) post x' = x + 2 32 Computer Engineering, Pusan National University  Pre- and Post-Conditions  Meaning is that a transition cannot occur unless the precondition is satisfied, and then the final state value (s') will be related to the initial state value (s) as defined by the postcondition.  We will use x and x', to stand for s(x) and s'(x), respectively. a S s s' pre(s) is true post(s,s') is true 33 Computer Engineering, Pusan National University  Arguments  Suppose want to give inc an argument inc1 x=1 inc1 x=0 inc2 x=2 x=3 inc3 inc(i:Z) BigCounter 34 Computer Engineering, Pusan National University  Using Pre-Post Notation  One possibility inc (i: ) pre true post x' = x + i  Another possibility (FatCounter) inc (i: ) pre i > 0 post x' = x + i 35 Computer Engineering, Pusan National University  Output  How can we handle output?  Ans: add more structure to actions  Specifically: an action becomes a pair (invocation event, response event)  We will also take this opportunity to distinguish between normal and error output values 36 Computer Engineering, Pusan National University  Example: Register write(1) / ok() read() / ok(1) x=1 x=0 write(2) / ok() x=2 read() / ok(0) write(2) / ok() read() / ok(2) read() / ok(Z) write(i:) / ok() Register 37 Computer Engineering, Pusan National University  Exceptions  We can extend our notation to allow for exceptional (or error) results  Example: pop()/ok(Z), empty() 38 Computer Engineering, Pusan National University  Nondeterminism  Thus far the transition relation has been a function  But we can allow for flexibility using a relation (recall: nondeterminism)  Example: inc(4) x=7 x=3 inc(4) x = 11 inc(i:int) pre i > 0 post x' = x + i  x' = x + 2i 39 Computer Engineering, Pusan National University  Finite State Automata  FSA = {S, I, F, A, T)  S, I, A, T are as before except I must be a singleton set  F is the set of final states  Notational relationship FSA State Machine alphabet actions string trace (ending in final state) language L(M) behavior Beh(M) 40 Computer Engineering, Pusan National University  Basic Features of Statecharts  State  Boxes with rounded corners  Transition  Arc  event[condition] / action1; action2  e[c] : the condition c is tested at the instant the event e occurs  [c] : the condition c is tested at each instant of time when the system is in the transition’s source state STATE_A STATE_B event[condition] /action1; action2 41 Computer Engineering, Pusan National University  Statecharts vs. STD 42 Computer Engineering, Pusan National University  The Hierarchy of States  Clustering, multi-level, default (entrance) state  Structuring for managing and understanding U G/A S T F  Priority  Higher-level transitions G/A S E  Refer state name F  Basically  state_name  Same child state name and different parent state name  parent_state.child_state 43 Computer Engineering, Pusan National University  Orthogonality  And-state and event broadcasting  Defined event in the higher level state U W G Y S X E F E F[in(Y)] T F/E Z  Conditions and events related to states  en(S)  The moment of entrance of state S : event  ex(S)  The moment of exiting of state S : event  in(S)  In state S : condition 44 Computer Engineering, Pusan National University  Branching Connectors  Condition Connectors  Branch by condition  Switch Connectors  Branch by event 45 Computer Engineering, Pusan National University  Compacting Connectors  Junction Connectors  Branch/join (within one step)  Attention to use (confusing to understand) E1 and E2 S3 S1 S3 S1 E1/A1 /A1 E1 and E3 E2 E3/A2 /A1;A2 S2 S2 46 Computer Engineering, Pusan National University  More about Transitions  Fork/Join construct with AND-state  Similar to Junction connectors 47 Computer Engineering, Pusan National University  Event and Condition Expressions  Event expression  event1 {and/or} event2  not event (Not recommend)  event[condition]  all(event_array), any(event_array) E[C]  event_array is a event array  Condition expression  [exp1 {= | # | > | < | = } exp2] e.g [ 4 > x]  [all(cond_array)], [any(cond_array)]  cond_array is a condition array 48 Computer Engineering, Pusan National University  Time Related Expression  Introducing timing information into a statechart  Timeout event  tm(E,T)  E : event, T : integer expression  event will occur T time units after the latest occurrence of the E e.g. tm(en(A_STATE), 10)  Scheduled actions  sc!(G,T)  G : action, T : integer expression  G is performed T time units from the present instant e.g. sc!(if NO_SIGNAL then ISSUE_DISCONNECTED_MSG, 3) 49 Computer Engineering, Pusan National University  State Machine  Describe the Behavior of System  Basic Elements s s’  States  Transition between States  Types  Basic Type: Moore Machine, Mealy Machine  Extended Type: State Diagram, RSML(Requirement Statement Machine Language), etc.  Checking Methods  Equivalence Test (동치 검사)  Model Checking (모델 검사) 50 Computer Engineering, Pusan National University  Moore Machine (1/3)  Outputs are printed when we reach a state,  that is, the outputs depends on the present state  Moore machine M = (I, O, S, d, , )  I : Set of Input  O : Set of Output  S : Set of States  dS : initial(default) State  : S  I S : Transition Function, that is, (s,i) = s’  : S O : Output Function, that is, (s) = o 51 Computer Engineering, Pusan National University  Moore Machine (2/3)  Example: M = (I, O, S, d, , )  I = {a,b}  O = {x,y}  S = {0,1,2}  d=0   is defined as follows: (0,a) = 1 (0,b) = 0 (1,a) = 2 (1,b) = 1 (2,a) = 2 (2,b) = 0   is defined as follows: (0) = x (1) = y (2) = y 52 Computer Engineering, Pusan National University  Moore Machine (3/3)  State Transition Table  State Transition Diagram  For given input abbaaa, What is the output of this machine ? 53 Computer Engineering, Pusan National University  Mealy Machine (1/3)  Outputs are printed when there is a transition from state to state  Outputs are a function of the present state and the value of inputs  Output is associated with transition from present i/o state to next state s s’  Mealy Machine M = (I, O, S, d, , )  I : Set of Input  O : Set of Output  S : the Set of States  dS : Initial(default) State  : S  I S : Transition Function, that is, (s,i) = s’  : S  I O : Output Function, that is, (s,i) = o 54 Computer Engineering, Pusan National University  Mealy Machine (2/3)  Example: M = (I, O, S, d, , )  I = {0,1}  O = {0,1}  S = {s,t}  d=s  Transition function  is defined as follows: (s,0) = s (s,1) = t (t,0) = t (t,1) = s   is defined as follows: (s,0) = 0 (s,1) = 1 (t,0) = 1 (t,1) = 0 55 Computer Engineering, Pusan National University  Mealy Machine (3/3)  State Transition Table  State Transition Diagram  Given input 10101, the Output of this Machine ? 56 Computer Engineering, Pusan National University  Equivalence Test (1/3)  Two State Machines MA MB  Equivalence of Two machines  When the input 101110 is given, What are the outputs of two machines, MA and MB ?  For given input 01011, the outputs of MA and MB ?  Are the outputs of two machines, MA and MB , equivalent for all inputs ? 57 Computer Engineering, Pusan National University  Equivalence Test (2/3)  Equivalence test  Decide whether the Outputs of two machines are always Same for All inputs  Application Domain  System Optimization  Checking Accuracy  ……  Method of Test  Check that the Outputs are always the same through Product Machine of two machines  …… 58 Computer Engineering, Pusan National University  Equivalence Test (3/3)  Given two Machines  MA = (IA, OA, SA, dA, A, A)  MB = (IB, OB, SB, dB, B, B)  Product machine M = MA  MB = (I, O, S, d, , )  I = IA = IB : Set of Input  O = {0,1} : Set of Output, where OA = OB  S = SA  SB = {(sA, sB) | sASA, sBSB} : Set of States  dS : Initial State of Product Machine where d = (dA,dB)  : S  I S : Transition Function, that is, ((sA,sB), i) = (A (sA, i), B (sB, i))  : S  I O : Output Function, that is, (s, i) = A (sA, i)  B (sB, i)  1 when the outputs of two machines are the same for input i in state s. Otherwise, 0 59 Computer Engineering, Pusan National University  Example  Represent Machine MA = (IA, OA, SA, dA, A, A) formally. MA  IA = {0,1}  OA = {0,1}  SA = {s0, s1, s2}  dA = s0  Transition function A: A (s0,0) = s0  A(s0,1) = s1 A (s1,0) = s0  A(s1,1) = s2 A (s2,0) = s0  A(s2,1) = s2  Output Function A:  A(s0, 0) = 0 A (s0, 1) = 0  A(s1, 0) = 0 A (s1, 1) = 0  A(s2, 0) = 0 A (s2, 1) = 1 60 Computer Engineering, Pusan National University  Example (cont.)  Represent Machine MB = (IB, OB, SB, dB, B, B) formally. M B  IB = {0,1}  OB = {0,1}  SB = {t0, t1, t2, t3}  d B = t0  transition function B B (t0, 0) = t0 B (t0,1) = t1 B (t1, 0) = t0 B (t1,1) = t2 B (t2, 0) = t0 B (t2,1) = t3 B (t3, 0) = t0 B (t3,1) = t3  output function B B (t0,0) = 0 B (t0,1) = 0 B (t1,0) = 0 B (t1,1) = 0 B (t2,0) = 0 B (t2,1) = 1 B (t3,0) = 0 B (t3,1) = 1 61 Computer Engineering, Pusan National University  Example (cont.)  What’s the formal representation of Product Machine M = MA  MB = (I, O, S, d, , ) ?  I = {0,1}  O = {0,1}  S = {(s0, t0), (s0, t1), (s0, t2), (s0, t3), (s1, t0), (s1, t1), (s1, t2), (s1, t3), (s2, t0), (s2, t1), (s2, t2), (s2, t3) }  d = (s0, t0) 62 Computer Engineering, Pusan National University  Example (cont.) ((s0, t0), 0) = (s0, t0) ((s0, t0), 1) = (s1, t1) ((s0, t1), 0) = (s0, t0) ((s0, t1), 1) = (s1, t2) ((s0, t2), 0) = (s0, t0) ((s0, t2), 1) = (s1, t3) ((s0, t3), 0) = (s0, t0) ((s0, t3), 1) = (s1, t3) ((s1, t0), 0) = (s0, t0) ((s1, t0), 1) = (s2, t1) ((s1, t1), 0) = (s0, t0) ((s1, t1), 1) = (s2, t2) ((s1, t2), 0) = (s0, t0) ((s1, t2), 1) = (s2, t3) ((s1, t3), 0) = (s0, t0) ((s1, t3), 1) = (s2, t3) ((s2, t0), 0) = (s0, t0) ((s2, t0), 1) = (s2, t1) ((s2, t1), 0) = (s0, t0) ((s2, t1), 1) = (s2, t2) ((s2, t2), 0) = (s0, t0) ((s2, t2), 1) = (s2, t3) ((s2, t3), 0) = (s0, t0) ((s2, t3), 1) = (s2, t3) 63 Computer Engineering, Pusan National University  Example (cont.) ((s0, t0), 0) = 1 ((s0, t0), 1) = 1 ((s0, t1), 0) = 1 ((s0, t1), 1) = 1 ((s0, t2), 0) = 1 ((s0, t2), 1) = 0 ((s0, t3), 0) = 1 ((s0, t3), 1) = 0 ((s1, t0), 0) = 1 ((s1, t0), 1) = 1 ((s1, t1), 0) = 1 ((s1, t1), 1) = 1 ((s1, t2), 0) = 1 ((s1, t2), 1) = 0 ((s1, t3), 0) = 1 ((s1, t3), 1) = 0 ((s2, t0), 0) = 1 ((s2, t0), 1) = 0 ((s2, t1), 0) = 1 ((s2, t1), 1) = 0 ((s2, t2), 0) = 1 ((s2, t2), 1) = 1 ((s2, t3), 0) = 1 ((s2, t3), 1) = 1 64 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  State Transition Diagram of Product Machine M = MA  MB 65 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  Reachability Analysis  Set of Reachable States from current state Y image (Y, ) = {s’ | s  (s ∈ Y)  (s, s’) ∈}  Set of All Reachable States from initial state Y0 = {d} repeat Yi+1 = Yi ∪ image(Yi, ) until (Yi+1 = Yi)  P(d): Set of all reachable states  All reachable states from initial state d of product machine  that is, P(d) = Yi 66 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  Find the set of all reachable states, P(d), in machine M  Y0 = {(s0, t0)}  Y1 = Y0 ∪ image (Y0, ) = {(s0, t0), (s1, t1)}  Y2 = Y1 ∪ image (Y1, ) = {(s0, t0), (s1, t1), (s2, t2)}  Y3 = Y2 ∪ image (Y2, ) = {(s0, t0), (s1, t1), (s2, t2), (s2, t3)}  Y4 = Y3 ∪ image (Y3, ) = {(s0, t0), (s1, t1), (s2, t2), (s2, t3)}  P(d) = Y3 = {(s0, t0), (s1, t1), (s2, t2), (s2, t3)} 67 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  Set of All Reachable States  P(d) = {(s0,t0), (s1,t1), (s2,t2), (s2,t3)} 68 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  Equivalence in state s= (sA, sB)  E(s) = i  A(sA,i)  B(sB ,i)  i.e., the Outputs of two machines are the same in the state of Product machine, s = (sA, sB), for all input i  P(d): the Set of all Reachable States  All reachable states from initial state d of product machine  Equivalence in all Reachable States  dS  sS  sP(d)  E(s)  Equivalence condition of two machines  If two machines are Equivalent in all Reachable States, then they are Equivalent. 69 Computer Engineering, Pusan National University  Example (cont.) - Equivalence Test  Decide whether two machines are equivalent ?  P(d) = {(s0, t0), (s1, t1), (s2, t2), (s2, t3)}  Equivalence in state (s0, t0)  For input 0: A(s0, 0)  B(t0, 0)  For input 1: A(s0, 1)  B(t0, 1)  Equivalence in state (s1, t1)  For input 0: A(s1, 0)  B(t1, 0)  For input 1: A(s1, 1)  B(t1, 1)  Equivalence in state (s2, t2)  For input 0: A(s2, 0)  B(t2, 0)  For input 1: A(s2, 1)  B(t2, 1)  Equivalence in state (s2, t3)  For input 0: A(s2, 0)  B(t3, 0)  For input 1: A(s2, 1)  B(t3, 1)  They are Equivalent in all reachable states. Therefore, 70 two machines are Equivalent.Computer Engineering, Pusan National University  Example  Decide that two machines are equivalent. 0/0 0/0 1/0 0/0 1/0 t0 t1 s0 s1 1/1 1/1 0/0 1/1 t2 0/0  Draw the State Transition Diagram of Product Machine  Describe the Set of Reachable States  Decide whether two machines are Equivalent or not 71 Computer Engineering, Pusan National University  Cannibals and Missionaries Problem (1/5)  Two missionaries and two cannibals must cross a river using a boat which can carry at most two people, under the constraint that, for both banks, if there are missionaries present on the bank, they cannot be outnumbered by cannibals (if they were, the cannibals would eat the missionaries). The boat cannot cross the river by itself with no people on board. 72 Computer Engineering, Pusan National University  Cannibals and Missionaries Problem (2/5)  Modeling the problem with Finite State Machine  Describe 3-tuple (M,C,B) in each state, where  M = {0,1,2} : # of missionaries in the right side of river,  C = {0,1,2} : # of cannibals in the right side of river,  B = {L,R} : the location of boat  State  Initial state is (2,2,R)  Final state is (0,0,L)  All possible combinations on board  (0,1) : cannibal 1  (0,2) : cannibal 2  (1,0) : missionary 1  (1,1) : missionary 1, cannibal 1  (2,0) : missionary 2 73 Computer Engineering, Pusan National University  Cannibals and Missionaries Problem (3/5)  Modeling with Finite State Machine 74 Computer Engineering, Pusan National University  Cannibals and Missionaries Problem (4/5)  Moving Sequence with Finite State Machine 75 Computer Engineering, Pusan National University  Cannibals and Missionaries Problem (5/5)  three missionaries and three cannibals  Initial state is (3,3,R)  Final state is (0,0,L)  How to move? 76 Computer Engineering, Pusan National University