
\section{\label{trans2}Models and Simulations: II. Acceptance-Transition Systems}

     In the models described in section \ref{trans}, the only structures
associated with a state were transition functions (labelled or unlabelled).
In this section we add a set of ``acceptances'' for each state.

\subsection{\label{ATM}Acceptance-Transition Models}

     An ATM is a generalisation of a simple TM, characterised by a tuple
$(S, A, T, W)$.  $S$, $A$ and $T$ are defined as for a TM.  $W$ associates
set of ``acceptances'' with each state.
An acceptance (in a state $i$) is some subset
of $\dom T (i)$.  The acceptances $W (i)$ can be thought of as a set of
``substates'' of the state $i$.  There is no external way of telling which
substate is active---this is selected
non-deterministically by the system whenever it enters a new state.
{\em If} an acceptance $w \in W (i)$ is active, the system is prepared
to engage in any of the transitions in $w \lhd T (i)$, but it will
refuse any event outside $w$.  From this discussion we see that
$W$ is in $S \rightarrow \Pow \Pow A$.  It is convenient to require that
\begin{displaymath}
\bigcup_{w \in W (i)} w = \dom T (i).
\end{displaymath}
ie, there are no redundant transitions in $T (i)$ which the system never
offers to engage in.

     ATMs are very closely related to the Acceptance Trees of \cite{AT},
but we have no requirement that $W (i)$ be convex closed or
closed under union.  Those conditions are necessary if every process
must have a unique representation (as in a semantic domain), but
less important here, where an ATM is just one amongst many
possible parametrisations of a process.

     The system of CSP processes associated with an ATM is defined as
the (least) solution of
\begin{displaymath}
\function{Proc} (i) = \begin{array}{c} \ndchoice \\ w \in W (i) \end{array}
		      (e:w \rightarrow \function{Proc} (T (i) (e))) =
                      \begin{array}{c} \ndchoice \\ w \in W (i) \end{array}
		      R (w, T (i)) (\symbol{Proc})
\end{displaymath}

     Both ETMs and ATMs can express non-determinism.  In fact, any
divergence-free CSP process can be modelled both by an ATM and by
an ETM---often, by many.  The advantage of the ETM has already
been illustrated---it emerges naturally when internal events
are concealed.  The advantage of an ATM is that one can show
much more directly that it meets a particular CSP specification.

\subsubsection{Specifications}

     Suppose $\cal S$ is the partial function from $A^*$ to $S$
which maps the possible traces of the model, generated from
an inital state $i$, to the state of the model after engaging
in that trace.  The process associated with $i$ satisfies
\begin{displaymath}
\symbol{tr} \in \dom {\cal S} \land
(\exists w:W ({\cal S} (\symbol{tr})) \truethat
  w \cap \symbol{ref} = \emptyset)
\end{displaymath}

\subsubsection{Simulations}

     We give a simulation from ETMs to ATMs.  This can be used
to show that an ETM arising from event-concealment implements
a system modelled by an ATM.  This generalises the simulation
given in \ref{ETsim} to the case where the processes involved
aren't necessarily deterministic.

\begin{definition}
    Suppose $(S, A, T, U)$ is an ETM and $(S', A, T', W')$ is an ATM.
The relation $G$ from $S$ to $S'$ is a simulation if whenever
$i \infix{G}  i'$ the following clauses hold
\setcounter{equation}{0}
\begin{eqnarray}
  && \dom T (i) \subset \dom T' (i'), \\
  && \forall e:\dom T (i) \truethat T (i) (e) \infix{G}  T' (i') (e), \\
  && \forall j:U (i) \truethat j \infix{G}  i', \\
  && U (i) = \emptyset \Rightarrow
	   (\exists w':W' (i') \truethat \dom T (i) \supset w')
\end{eqnarray}
\end{definition}

\begin{theorem}
\label{th:ATMsim}
If $G$ is a simulation in this sense, and $\function{Proc}$ is the
system of processes associated with the ETM, and $\function{Proc}'$ is the
set of process associated with the ATM, then $i \infix{G} i'$
implies
\begin{displaymath}
\function{Proc} (i) \sqsupseteq \symbol{Proc}' (i')
\end{displaymath}
\end{theorem}
The proof is deferred to appendix \ref{sec:simproof}.

\subsection{\label{EATM}Extended Acceptance-Transition Models}

     Finally, suppose we are given a system modelled by an
acceptance-transition model, and are required to conceal some events in its
alphabet.  The ATM can be generalised to an extendeded
acceptance-transition model (EATM), in much the same way as the TM was
generalised to the ETM, to take account of this.

     An EATM is a tuple $(S, A, T, U, V)$, where $S$, $A$, $T$ and $U$
have the same properties as for an ETM, and $V$ associates a set of
pairs with each state in $S$.  Each pair consists of a set of unlabelled
transitions and an acceptance set.  A pair can be regarded as a sub-state
of the visible state, in the same sense that an acceptance was a sub-state
in the ETM.  Hence $V \in \Pow (\Pow S \times \Pow A)$.  $V$ is constrained by
\begin{eqnarray*}
\bigcup_{(u, w) \in V (i)} w = \dom T (i),
\bigcup_{(u, w) \in V (i)} u = U (i).
\end{eqnarray*}

     The system of CSP processes associated with an EATM is defined as
the (least) solution of
\begin{displaymath}
\function{Proc} (i) = \begin{array}{c} \ndchoice \\ (u, w) \in W (i) \end{array}
		      P (u, w, T (i)) (\symbol{Proc}).
\end{displaymath}

\subsubsection{Concealment}

If $\symbol{Proc}$ is the set of processes associated with an
ATM $(S, A, T, W)$, and
\begin{displaymath}
\symbol{Proc}' (i) = \function{Proc} (i) \setminus C
\end{displaymath}
for some $C \subset A$, then $(S, A, T', V')$ is an AETM for the system
$\symbol{Proc}'$, where
\begin{eqnarray*}
T' (i) & = & (A - C) \lhd T (i) \\
V' (i) & = & \{ (\ran ((\setvar{w} \cap C) \lhd T (i)), \setvar{w} - C)
		\suchthat \setvar{w} \in W (i) \}
\end{eqnarray*}

\subsubsection{Simulations \label{sec:EATMsim}}

     We give a simulation from EATMs to ATMs.  This can be used
to show that an EATM arising from event-concealment implements
a system modelled by an ATM.

\begin{definition}
\label{def:EATMsim}
    Suppose $(S, A, T, U, V)$ is an EATM and $(S', A, T', W')$ is an ATM.
The relation $G$ from $S$ to $S'$ is a simulation if whenever
$i \infix{G}  i'$ the following clauses hold
\setcounter{equation}{0}
\begin{eqnarray}
  && \dom T (i) \subset \dom T' (i'), \\
  && \forall e:\dom T (i) \truethat T (i) (e) \infix{G}  T' (i') (e), \\
  && \forall j:U (i) \truethat j \infix{G}  i', \\
  && \forall (u, w):V (i) \truethat u = \emptyset \Rightarrow
	   (\exists w':W' (i') \truethat w \supset w')
\end{eqnarray}
\end{definition}

\begin{theorem}
\label{th:EATMsim}
If $G$ is a simulation in this sense, and $\function{Proc}$ is the
system of processes associated with the EATM, and $\function{Proc}'$ is the
set of process associated with the ATM, then $i \infix{G} i'$
implies
\begin{displaymath}
\function{Proc} (i) \sqsupseteq \symbol{Proc}' (i')
\end{displaymath}
\end{theorem}
The proof is deferred to appendix \ref{sec:simproof}.

