- ...far.
- Unlike in the last handout,
I'm not going to spell out each of the components of the state
machine for each of the examples given in this handout.
Also, I'm going to introduce some notation that I hope is minimal and
simple enough for you to be able to use in your homework problems.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...template
- I will be elaborating on this template throughout this handout.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...pre/post-states
- Recall that the post-condition is
defined over two states.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...here.
- This
one also is consistent with the discussion (in the State Machine
Basics handout)
about actions that cannot
occur.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...values
- I leave it to you to formalize this state machine.
You will see something similar when you get to the Birthday Book
example in Z.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...states
- To make my point,
I am viewing 2#2 as a function from (state, action) pairs
to a set of states, rather than as a relation on (state, action,
state) triples.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.