State machine ($s_{t+1}=F(s_t)$)

A computational model with an internal state and transition rule, together with an initial state and optional observation and stopping functions. The state space need not be finite; a finite-state machine is the special case with finitely many states. A trace records observations along transitions. An interface providing only reset, update, stopping and observation operations does not by itself provide copying or rollback; a trace iterator can revisit saved observations without reversing machine effects.

A configuration of a system at one moment. In a transition system, a state is an element of its state space $S$, and a transition relation specifies permitted changes of state.