If S is finite, then M is a finite state machine.
I is sometimes defined so that it can be an infinite subset of S (when of course S is infinite). A is sometimes called the alphabet of M. Elements in A are sometimes called events or operations. In other models A may be infinite. Sometimes is defined to be a function, , rather than a relation.
However, by our having be a relation, we can more easily model nondeterminism. Recall that it's equivalent to view the type of as ; thus, given a state and an action, we can move to possibly more than one next state.
(Aside: the action component, a, of a triple, (s, a, s'), in , is sometimes just viewed as the label for the state transition from s to s'. Thus, sometimes these kinds of state machines are called labeled state transition systems.)
Applying the above definition of a state machine, we have for the Car:
Car = (