效绵鼎 model to describe the behavior of systems digraphs where nodes represent states,and edges model transitions state: the current color of a traffic light the current values of all program variables the program counter 0 the value of register and output transition:("state change") o a switch from one color to another the execution of a program statement the change of the registers and output bits for a new input◼ model to describe the behavior of systems ◼ digraphs where nodes represent states, and edges model transitions ◼ state:  the current color of a traffic light  the current values of all program variables + the program counter  the value of register and output ◼ transition: (“state change”)  a switch from one color to another  the execution of a program statement  the change of the registers and output bits for a new input