\documentstyle[10pt,epsf,fuzz]{article}

\input{./handout}

\newtheorem{defn}{Definition}
\newenvironment{spec}{
 \vspace*{8pt}
 \begin{center}
 \begin{minipage}{5in}
 \renewcommand{\baselinestretch}{1}
 }{
 \end{minipage}
 \end{center}
 \vspace*{8pt}
}
\def\nin{\in\hspace{-.13in}/}

\begin{document}

\handout{5}{20 September 1995}{Variations on State Machines}
\begin{symbolfootnotes}
\footnotetext[0]{\copyright 1995 Jeannette M. Wing} 
\end{symbolfootnotes}

The state machine model presented in the previous handout
is not suitable, appropriate, or natural for modeling all systems.
In this handout we look at different variations of the basic
model I've presented so far.\footnote{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.}

Which model you choose to use depends on what you are trying to model.
You certainly want to choose one that allows you to state as precisely
and concisely those things you care about.
Some models may make distinctions that you don't care about; some may
make assumptions that don't fit your problem.  But sometimes which you
choose is just a matter of taste.  When you decide what model
to use you should understand why you are choosing one over another.

Given a state machine, $M = (S, I, A, \delta)$,
in the first three sections, I am going to refine
some of $M$'s components.  First I'm going to give more structure
to states in $S$
(Section \ref{sec:state}), then to actions in $A$
(Section \ref{sec:actions}), and then generalize
the functionality of $\delta$ (Section \ref{sec:delta}).
In the fourth section I show how all these things can be used together.

Finally, in the last two sections I discuss other refinements
of state machine models that are often seen in practice.

\section{States Map Variables to Values}
\label{sec:state}

Let's revisit my integer counter example.

\centerline{\epsfbox{pictures/counter.ps}}

In the diagram above, I introduced the variable $x$ to ``hold'' the
value of the integer counter.  The notion of a state as having
variables that can have values of some type should be familiar to you
from your programming experience.

With respect to state machine models,
what I am doing is refining the
notion of what a machine state is; I am adding some internal structure
so that states are more than just named entities like {\em 2}, {\em off}, or {\em crashed}.
In general, each state in $S$ of a state machine, $M$,
is
a finite function from
a finite set, $Var$, of {\em variables} (sometimes called
``identifiers'' or ``names'') to a possibly infinite set, $Val$, of {\em Values}:

\begin{center}
$M = (\{ S: Var \ffun Val \}, I, A, \delta)$
\end{center}

Moreover, I am going to assume variables and values are {\em typed}
much like in a programming language.  Hence if the variable $x$ is of type
{\em int}, then I can map it to the integer value ``1'' but not the
real value ``3.14159''.

Counter's set of states, $S$, is a set of total functions mapping
$x$ to some integer value:

\begin{center}
$\{ s: \{x\} \rightarrow int | s(x) \geq 0 \}$
\end{center}

\noindent Since a state is a mapping from variables to values, $s(x)$
denotes the value of the variable $x$ in state $s$.

Suppose I want to write the state transition function for my Counter?
Then, as defined earlier,
let $S$ (my set of states) be the set of functions that map the variable
$x$ to an integer value.  Then similar to the SimpleCounter, I have

\begin{center}
$\delta_{inc} = \{ (s, a, s'): (S \times \{inc\} \times S) | s'(x) = s(x) + 1 \}$
\end{center}

Now suppose I have a counter that allows
state transitions only from states whose value for its state variable,
$x$, is an even number.  EvenCounter starts in the initial
state $x=0$ and whenever I {\em bump} its
state, I get to the next even number:

\centerline{\epsfbox{pictures/evencounter.ps}}

Let EvenCounter's set of states, $S$, be the same as for Counter.
EvenCounter's transition function $\delta$ is:

\begin{center}
$\delta_{bump} = \{ (s, a, s'): (S \times \{bump\} \times S) |  even(s(x)) \wedge s'(x) = s(x) + 2 \}$
\end{center}

\noindent where we assume the predicate {\em even} has been defined appropriately.
(Notice that some states in EvenCounter are unreachable.  Which ones?)

Unfortunately writing the state transition function as predicates over sets of pairs
of states and writing $s(x)$ and/or $s'(x)$ whenever I want to refer to the value of
a state variable becomes pretty
unwieldy
quickly.
By introducing two keywords, I will write the
state transition function for each action
in a more readable notation.  Here's what I write for Counter's {\em
inc}
action:

\begin{spec}
\begin{tabbing}
\indent {\em inc} \= \\
            \>{\bf pre} $true$\\
            \>{\bf post} $x' = x + 1$
\end{tabbing}
\end{spec}

\noindent and for EvenCounter's {\em bump} action:

\begin{spec}
\begin{tabbing}
\indent {\em bump} \= \\
            \>{\bf pre} $even(x)$\\
            \>{\bf post} $x' = x + 2$
\end{tabbing}
\end{spec}

\noindent The first line, which I'll call the {\em header},
gives the name of the action whose
state transition behavior I describe
in the subsequent two lines.  The second line gives a {\em
pre-condition}, which is just a predicate, and the third
line gives a {\em post-condition}, which is just another predicate.
The interpretation of the pre- and post-conditions is:
In order for the state transition to occur from
the state $s$ to the state $s'$
the pre-condition
must hold in $s$; after the state transition occurs, then the
post-condition must hold in $s'$.
The state transition cannot occur if the pre-condition is not met.
Post-conditions in general need to talk about
the values of state variables in both the state before the state
transition occurs (the ``pre-state'') and the state after it occurs
(the ``post-state'').  I use an unprimed variable to denote the value
of the variable in the pre-state and a primed variable to denote its
value in the post-state.  So, $x'$ really stands for $s'(x)$; $x$, for $s(x)$.

Here's how to visualize what the pre- and post-conditions capture:

\centerline{\epsfbox{pictures/pre-post.ps}}

\noindent For action $a$ to occur the pre-condition must hold in $s$.  If $a$
occurs,
the post-condition must hold in $s$ and $s'$.

In the Counter example, the {\em inc} action has the trivial
pre-condition, ``true.''  This means that the {\em inc} action can be
performed in any state in $S$.  EvenCounter's {\em bump}
action has a non-trivial
pre-condition.
Another typical non-trivial pre-condition is
requiring that a {\em pop} action not be performed on an empty stack.
We'll see other examples of non-trivial pre-conditions later.
{\em Inc}'s post-condition says that
the value of the integer counter is increased by one from its previous
value; {\em bump}'s post-condition says that the value is increased by two.

In general, for a given $M = (S, I, A, \delta)$, the
template\footnote{I will be elaborating on this template throughout this handout.} I'm using to describe $\delta_{action}$ is

\begin{spec}
\begin{tabbing}
\indent {\em action}\= \\
            \>{\bf pre} $\Phi(v)$\\
            \>{\bf post} $\Psi(v, v')$
\end{tabbing}
\end{spec}

\noindent where {\em action} is in $A$,
and $\Phi$ and $\Psi$ are (state)
predicates over a vector, $v$, of state variables.
%$\Phi$ is really a predicate over one state, $s$; $\Psi$, a predicate
%over two states, $s$ and $s'$, which are implicitly universally quantified;
%when you see a variable like $x$ in $\Phi$ it really stands
%for $s(x)$, i.e., the value of the variable $x$ in state $s$.
%To make this quantification explicit,
The above template
stands for the following part of the definition of
the state transition function, $\delta$:

\begin{center}
$\delta_{action} = \{ (s, a, s'): S \times \{action\} \times S | \Phi[s(v)/v] \wedge \Psi[s'(v)/v',s(v)/v] \}$
\end{center}

\noindent In English this says that the precondition ($\Phi$) has to
hold in the pre-state {\em and} the post-condition ($\Psi$) has to hold in the
pre/post-states\footnote{Recall that the post-condition is
defined over two states.}.

Other interpretations of pre/post-condition specifications are
possible.  I'm just giving you one reasonable one here.\footnote{This
one also is consistent with the discussion (in the State Machine
Basics handout)
about actions that cannot
occur.} For example, another
common one is where the conjunction used above is replaced by an implication.
Under this interpretation, which is used in Z and Larch, if the
pre-condition does not hold and you try to do the action then
anything can happen, i.e., ``all
bets are off.''  You could end up in an unexpected state, an error
state, or an undefined state.

\section{Actions}
\label{sec:actions}
\subsection{Actions with Arguments}

Now suppose I want to let my integer counter's {\em inc} action take an
integer argument.
We see it's even more difficult to draw
BigCounter's state transition diagram, only part of which is shown here:

\centerline{\epsfbox{pictures/bigcounter.ps}}

\noindent It's much easier and more concise to write the state transition
function
for {\em inc} as follows:

\begin{spec}
\begin{tabbing}
\indent {\em inc}\={\em (i: int)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $x' = x + i$
\end{tabbing}
\end{spec}

\noindent I've extended the header in my specification to include
a list of input arguments (and their types).
I've intentionally chosen syntax to look like
programming language notation.

The technical term for what I have done is {\em lambda abstraction}.
Using a single template
I've actually defined an infinite set of functions, one for each
integer $i$.  Instead of defining separate actions $inc_1, inc_2, \dots$
I've defined a family of actions $inc(i)$.

According to the above specification, there is nothing preventing the input integer argument
that I hand to {\em inc} from being negative.  Suppose I want
my counter to always increase in value, never decrease?
I can capture this by strengthening the pre-condition:

\begin{spec}
\begin{tabbing}
\indent {\em inc}\={\em (i: int)}\\
            \>{\bf pre} $i > 0$\\
            \>{\bf post} $x' = x + i$
\end{tabbing}
\end{spec}

I'll call this new machine FatCounter.  It's an example of a state
machine
with an action that has a non-trivial pre-condition.

\subsection{Actions with Results}

Sometimes actions produce results of interest to the
external
observer.  When I query my checking account balance, I expect the
result
to be displayed on the ATM screen or printed on a piece of paper.

Here's a Register with {\em read} and {\em write} actions.
{\em Read} returns the value of the register; {\em write} takes an
argument and modifies the register's state.  Its initial value is the
integer value 0.

\centerline{\epsfbox{pictures/register.ps}}

Here are the specifications of the actions:

\begin{spec}
\begin{tabbing}
\indent {\em read}\={\em ()/ok(int)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $result = x $\\
\\
\indent {\em write(i: int)/ok()}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $x' = i $
\end{tabbing}
\end{spec}

The first thing to notice is that I've introduced the word ``ok'' in
the header.
I've done this for two reasons.
The first is that I want to set myself up so that I can have a
convenient way to distinguish normal termination from exceptional
termination of a procedure, a feature supported by most advanced programming languages.
More on this later.
The second is a trivial point: For symmetry, I prefer writing
{\em read()/ok(1)} instead of {\em read()/1}.
Think of the instance of an action
as a procedure call.  Then the state transition labeled
{\em read()/ok(1)} corresponds to calling the {\em read} procedure and
getting
the integer 1 back.

What I am doing is adding
more structure to actions.
In general, a state transition is an {\em action instance}, which is
a pair of an {\em invocation
event} and {\em response event}.
An {\em invocation event} is the name of the action
plus the values of its input arguments; a {\em response event}
is the name of the termination condition (e.g., ok) plus the value of its
result.

An execution of a state machine is a sequence of alternating
states and action instances.
Some executions of the Register machine are:

\begin{verse}
$\langle x=0, write(1)/ok(), x=1, read()/ok(1), x=1\rangle$\\
$\langle x=0, write(1)/ok(), x=1, read()/ok(1), x=1, read()/ok(1), x=1,$\\
$~~~~~ write(5)/ok(), x=5, read()/ok(5), x=5\rangle$ \\
$\langle x=0, write(1)/ok(), x=1, write(7)/ok(), x=7, write(9001)/ok(), x=9001\rangle$
\end{verse}

For
the above executions, I have the following (event-based) traces:

\begin{verse}
$\langle write(1)/ok(), read()/ok(1)\rangle$\\
$\langle write(1)/ok(), read()/ok(1), read()/ok(1), write(5)/ok(), read()/ok(5)\rangle$ \\
$\langle write(1)/ok(), write(7)/ok(), write(9001)/ok()\rangle$
\end{verse}

\noindent What would I have for a state-based definition of trace?

The second thing to notice in the above specification
is that I've given in parentheses
the type of the result, if any, of each action.
The {\em read} action returns an {\em int} value; {\em write} doesn't
return anything.

The third thing to notice is that
in the post-condition I use a special reserved word {\em result} to stand
for the return value.  This trick works fine as long as an action
produces only one result.  It generalizes in the obvious way
in case an action produces more than one result.

Technical Aside 1: There is a subtle difference between an action,
which
is a member of the finite set $A$, and an action instance, which is a
member
of the possibly infinite set of state transitions, as defined by
$\delta$.
This difference is analogous in programming to the difference between the definition
(declaration) of a procedure and a call (invocation) of it.

Technical Aside 2: There are state machine models that treat invocation events
and response events as separate kinds of actions. Invocation
events could be viewed as {\em input actions}; response events, as
{\em output actions} (see the handout on State Machine Basics.)  These
models are mainly used for modeling classes of concurrent and
distributed systems.  For now, there is no compelling reason to
treat them separately.

\subsection{Actions that Terminate Exceptionally}

Many advanced programming languages support exception handling and
thus I should be able to specify the interface of a program that can
raise exceptions.

Consider the following Stack machine:

\centerline{\epsfbox{pictures/stack.ps}}

\noindent with {\em push} and {\em pop}
specified as follows:

\begin{spec}
\begin{tabbing}
\indent {\em push}\={\em (i: int)/ok()}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $st' = st \cat \langle i\rangle $\\
\\
\indent {\em pop()/ok(int)}\\
            \>{\bf pre} $st \neq \langle\rangle$\\
            \>{\bf post} $ st = st' \cat \langle result\rangle $
\end{tabbing}
\end{spec}

Here's how I specify
a more robust interface to Stack that allows {\em pop} to raise the
exception
{\em empty} if I try to perform the {\em pop} action on an empty stack ({\em push} stays the same):

\begin{spec}
\begin{tabbing}
\indent {\em pop()}\={\em /ok(int), empty()}\\
            \>{\bf pre} $true$\\
            \>{\bf post} \=$ st \neq \langle \rangle \Rightarrow (st = st' \cat \langle result\rangle  \wedge terminates = ok) ~\wedge$\\
                      \>\>$ st = \langle \rangle \Rightarrow (st = st' \wedge terminates = empty)$
\end{tabbing}
\end{spec}

The first thing to notice is the addition of the name of the
exceptional termination condition, {\em empty}, in the header.  For
each termination condition (normal and exceptional), I allow some kind
of result to be returned; here {\em empty} does not return any result.

The second thing to notice is the special reserved word, {\em
terminates}, which I introduced to hold the value of the termination
condition (``ok'' for normal termination and one of the exceptions
listed in the header for an exceptional termination).

From a software engineering perspective, there's usually a close
correlation between pre-conditions and exceptions.  It's common to
transform a ``check'' in the pre-condition to be a
``check'' in the post-condition.  From your programming experience,
this is the same as placing the responsibility on the callee rather
than the caller of a procedure.  With a pre-condition it's the
caller's
responsibility to check that the state of the system
satisfies the pre-condition before calling the procedure;
with an exception in lieu of the pre-condition, it's the
callee's responsibility by performing a (run-time) check and raise an
exception
in case the state of the system violates the condition.

Here's an example where upon exceptional termination an interesting
value is returned.
Consider a Table machine, which stores keys and values.
The state variable, $t$, stores the CMU telephone extensions of the 15-671 staff members:

\centerline{\epsfbox{pictures/table.ps}}

\noindent We can model
the state of the Table as a function from keys to values
\footnote{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.}.
The {\em insert} action returns an exception {\em already\_in}
if there already exists a value associated with the key
for which you are trying to insert a particular key-value
pair, $(k, v)$, and if so, it returns the current value
bound to that key, $k$:

\begin{spec}
\begin{tabbing}
\indent {\em insert(k: key}\={\em , v: value)/ok(), already\_in(value)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} \=$ k \nin~ dom~ t \Rightarrow (t' = t \cup \{k \mapsto v \} \wedge terminates = ok) ~\wedge$ \\
                      \>\>$ k \in dom~ t \Rightarrow (t' = t \wedge terminates = already\_in \wedge result = t(k) ~)$
\end{tabbing}
\end{spec}

\section{Nondeterminism}
\label{sec:delta}

%As mentioned in the State Machine Basics handout, I can model nondeterminism in two
%ways.  The simplest way is to change the functionality of $\delta$ so
%that it maps a state and an action to a set of states, rather than to a single state.

%\begin{center}
%$M = (S, I, A, \delta: S \times A \rightarrow \power S)$
%\end{center}

So far, $\delta$ has been a function, that is, for each state, $s$, and
action, $a$, $\delta$ mapped us to at most one next state.
Suppose I have a RandomCounter machine with an {\em inc} action that
takes
an integer argument:

\centerline{\epsfbox{pictures/randomcounter.ps}}

Here is the specification of {\em inc}:

\begin{spec}
\begin{tabbing}
\indent {\em inc(i: int)}\= \\
           \>{\bf pre} $i > 0$ \\
           \>{\bf post} $x' = x + i \vee x' = x + 2i$
\end{tabbing}
\end{spec}

According to the specification, {\em inc}
can either increment the counter's value by the value of its argument
$i$ or by twice that value.
Thus, there are two possible states
that you might end up in after doing the {\em inc} action given
some integer argument.  Since there is more than one, $\delta$
needs to map to a set of states\footnote{To make my point,
I am viewing $\delta$ as a function from (state, action) pairs
to a set of states, rather than as a relation on (state, action,
state) triples.}:

\begin{center}
$\delta(x=3, inc(4)) = \{x=7, x=11)\}$
\end{center}


As an observer, you don't know which state transition will occur when
you feed {\em inc} the integer 4.  You must be prepared to deal with
either
possibility.  The choice of which post-state is taken is made by the
machine itself.
Notice that the nondeterminism shows
up in the specification of {\em inc} in the use of logical disjunction
in the post-condition.

\section{Putting Everything So Far Together}

Suppose I have an integer set, $t$, and in its interface is a {\em choose} action
that doesn't take any arguments and removes and returns an element from $t$.

\centerline{\epsfbox{pictures/intset.ps}}

\noindent where {\em choose} is specified as follows:

\begin{spec}
\begin{tabbing}
\indent {\em choose}\={\em ()/ok(int)}\\
           \>{\bf pre} $t \neq \emptyset$\\
           \>{\bf post} $result \in t \wedge t' = t \setminus \{result\}$
\end{tabbing}
\end{spec}

\noindent The nondeterminism shows up in the specification for {\em
choose}
in the use of the set membership operator ($\in$) in the post-condition.
I don't know which element of $t$ will be returned; I know only that
some element will be returned.

You might notice that the labels on the arcs in the
state transition diagram above are different (by what is returned by {\em
choose});
however, most people would still view the state transition function
as nondeterministic because they would {\em abstract} from the
actual
value returned.  In other words they would define $\delta$ something like this:

\begin{center}
$\delta(t=\{2,3\}, choose()/ok(int)) = \{t=\{2\},t=\{3\}\}$
\end{center}

Finally, in a programming language that supports exception
handling
I would probably export a more robust interface for the {\em choose} action:

\begin{spec}
\begin{tabbing}
\indent {\em choose}\={\em ()/ok}\={\em (int), empty()}\\
           \>{\bf pre} $true$ \\
           \>{\bf post} $(t \neq \emptyset) \Rightarrow (result \in t \wedge t' = t\setminus\{result\} \wedge terminates = ok) ~\wedge$\\
           \>\>         $(t = \emptyset) \Rightarrow (t' = t \wedge terminates = empty)$
\end{tabbing}
\end{spec}

In general, the template I use for
each {\em action} in $A$ of $M = (S, I, A, \delta)$ is:

\begin{spec}
\begin{tabbing}
\indent {\em action}\={\em (inputs)/}$term_1(output_1), \ldots, term_n(output_n)$ \\
            \>{\bf pre} $\Phi(v)$\\
            \>{\bf post} $\Psi(v, v')$
\end{tabbing}
\end{spec}

\noindent where {\em inputs} is a list of arguments and their types,
$term_i$ is the name of one of $i$ termination conditions (including ``ok'')
and $output_i$ is the type of the result corresponding to $term_i$.  $\Phi$ and $\Psi$
are state predicates as defined earlier.  The reserved identifiers I
use are:
\begin{itemize}
\item {\em ok}, used in the header, to denote normal termination,
\item {\em result}, used in the post-condition, to denote the value
returned by an action, and
\item {\em terminates}, used in the post-condition, to denote the
value of
termination condition.  Its value can be any of the $term_i$,
including ``ok,''
listed
in the header.

\end{itemize}

I'm glossing over a number of technicalities here regarding state
variables to store input arguments and the type of the result
returned, depending on how an action terminates.

Finally,
for simplicity, let's assume actions return only normally
unless specified otherwise (by explicitly listing exceptional
conditions in their headers).  Under this default case, we
can avoid clutter in our specifications by not always having
to write ``{\em terminates = ok}'' in the post-conditions of our actions.

\section{Finite State Automata}
\subsection{Deterministic FSA}
If you ever took an automata theory course in Computer Science,
you have come across state machines.  A {\em deterministic finite
state automata (FSA)} is usually defined as follows:

\begin{center}
$M = (S, I, F, A, \delta)$
\end{center}

\noindent where $S$ is a finite set of states; $I \subseteq S$, the set of initial states, is restricted to be a
singleton set; $F \subseteq S$ is a finite set of {\em final} states; $A$ is a
finite set of actions, and $\delta: S \times A \pfun S$ is a deterministic function.

\begin{center}

\begin{tabular}{|l|l|}\hline
FSA terminology & State Machine terminology \\
\hline
alphabet & actions\\
string & trace$\dag$ \\
language L(M) & behavior Beh(M)\\ \hline
\end{tabular}

\end{center}

Here ``trace$\dag$'' means the trace of an execution ending in a final
state.
Sometimes the language of $M$ is called {\em regular} or a {\em regular set}
because it can be expressed as a regular expression using $\ast, \cup$,
and concatenation.  Just as with the behavior of a machine, the
language of an FSA 
can be infinite, i.e., there might be an infinite
number of strings accepted
by $M$.

\subsection{Nondeterministic FSA (NFSA)}

%As in Section \ref{sec:delta}
%we can modify $\delta$'s functionality to map a (state, action) pair
%to a set of states
%instead of a single state.
The only interesting thing to say here is to
refresh your knowledge about automata theory: It is always possible
to turn an NFSA into a deterministic FSA; and of course, every
deterministic FSA is an NFSA.

\section{Finite Executions and Infinite Behavior}

Recall the red and blue light example where the behavior
of the light is infinite because there are an infinite
number of traces associated with the light.  Also, some
of those traces are infinite (e.g., pressing red forever).

In some models of state machines, in particular, Communicating
Sequential Processes (CSP), which we will be covering in detail later
this term, infinite traces are not included in the machine's behavior.
This kind of model is sometimes called the {\em finite-trace model}.
The behavior of the machine is defined to be a possibly {\em infinite}
set of {\em finite} traces.

Why is this a reasonable model?  It has a simple structure which has
some nice mathematical properties.
%\footnote{Question: Is the language of an FSA or NFSA
%prefix-closed?  Answer: In general, no, because the language of an FSA
%contains only strings that end in a final state.}
Using this model may
help simplify your thinking about the system; you know every trace in
the behavior is finite so you don't have to worry about infinite
traces.
With a model that has both finite and infinite traces, whenever you
prove some property about the behavior it describes, you usually have
to structure your proof into two parts, one to handle the finite
trace case and one to handle the infinite trace case.  But perhaps the
most compelling intuitive argument for this model is that you can never {\em see} an
infinite execution; if you can't observe this behavior then why should
we model it?

What are some of the disadvantages of this model?
Because we cannot
talk about infinite traces, the biggest
disadvantage is that we cannot talk about certain properties
like deadlock and fairness.
To do so requires adding a lot of complicated structure to either
traces or
behaviors of a state machine.

We won't dwell on the advantages and disadvantages of this model here
since we'll see more of it later.


\end{document}