%\documentclass[9pt,twocolumn]{IEEEtran} %!PN
\documentclass[12pt]{IEEEtran}
%\documentclass[12pt]{article}

\usepackage{../../tex/lineno}\runninglinenumbers\modulolinenumbers[5]

%\documentclass[12pt]{IEEEtran} %!PN
%\documentstyle[twocolumn]{IEEEtran}
%\documentstyle[12pt,twoside,draft]{IEEEtran}
%\documentstyle[9pt,twocolumn,technote,twoside]{IEEEtran}

\usepackage{latexsym}
\usepackage[final]{graphicx,epsfig}
\usepackage{../../tex/wrapfig,url,amssymb,../../tex/cite,times}


\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}

\setcounter{page}{1}



%\usepackage{fancyheadings,cite}
%\headrulewidth 0.0pt
%\footrulewidth 0.0pt
%\rhead{}
%\rfoot{}
%\lhead{}
%\lfoot{}
%\chead{{\tt {\footnotesize Draft to be submitted
% to Journal of Automated Software Engineering (\url{http://www.wkap.nl/journalhome.htm/0928-8910});
%WP:00/powell/paper(\today).}}}
%\thispagestyle{fancy}

% Over-full v-boxes on even pages are due to the \v{c} in author's name
\vfuzz2pt % Don't report over-full v-boxes if over-edge is small

% THEOREM Environments ---------------------------------------------------
\newtheorem{thm}{Theorem}[subsection]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
%\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
%\theoremstyle{remark}
%\newtheorem{rem}[thm]{Remark}
%\numberwithin{equation}{subsection}
% MATH -------------------------------------------------------------------
%\DeclareMathOperator{\RE}{Re} \DeclareMathOperator{\IM}{Im}
%\DeclareMathOperator{\ess}{ess}


\newcommand{\eps}{\varepsilon}
\newcommand{\To}{\longrightarrow}
\newcommand{\h}{\mathcal{H}}
\newcommand{\s}{\mathcal{S}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\W}{\mathcal{W}}
\newcommand{\X}{\mathcal{X}}
\newcommand{\BOP}{\mathbf{B}}
\newcommand{\BH}{\mathbf{B}(\mathcal{H})}
\newcommand{\KH}{\mathcal{K}(\mathcal{H})}
\newcommand{\Real}{\mathbb{R}}
\newcommand{\Complex}{\mathbb{C}}
\newcommand{\Field}{\mathbb{F}}
\newcommand{\RPlus}{\Real^{+}}
\newcommand{\Polar}{\mathcal{P}_{\s}}
\newcommand{\Poly}{\mathcal{P}(E)}
\newcommand{\EssD}{\mathcal{D}}
\newcommand{\Lom}{\mathcal{L}}
\newcommand{\States}{\mathcal{T}}
\newcommand{\abs}[1]{\left\vert#1\right\vert}
\newcommand{\set}[1]{\left\{#1\right\}}
\newcommand{\seq}[1]{\langle #1\rangle}
\newcommand{\norm}[1]{\left\Vert#1\right\Vert}
\newcommand{\essnorm}[1]{\norm{#1}_{\ess}}
\newcommand{\qOut}{\mbox{{\em qOut}}}
\newcommand{\qIn}{\mbox{{\em qIn}}}
\newcommand{\notvdash}{\mbox{$\not\,\vdash$}}

\newcommand{\fig}[1]{Figure~\ref{fig:#1}}
\newcommand{\eq}[1]{Equation~\ref{eq:#1}}
\newcommand{\bfig}[1]{(\fig{#1})}
\newcommand{\tion}[1]{\S\ref{sec:#1}}
\newcommand{\btion}[1]{(\tion{#1})}
\newcommand{\DO}{$\downarrow$}
\newcommand{\UP}{$\uparrow$}
\newcommand{\flexibility}{\mbox{\em flexibility}}
\newcommand{\usability}{\mbox{\em usability}}
\newcommand{\performance}{\mbox{\em performance}}
\newcommand{\up}{\mbox{\em up}}
\newcommand{\down}{\mbox{\em down}}
\newcommand{\steady}{\mbox{\em steady}}
\newcommand{\unknown}{\mbox{\em unknown}}
\newcommand{\arrived}{\mbox{\em arrived}}
%\newcommand{\left}{\mbox{\em left}}
\newcommand{\dex}{\mbox{\em dex}}
\newcommand{\implies}{\mbox{\em implies}}
\newcommand{\andand}{\mbox{\em and}}
\newcommand{\andone}{\mbox{\em and\/}001}
\newcommand{\Inputs}{\mbox{\em Inputs}}
\newcommand{\Outputs}{\mbox{\em Outputs}}
\newcommand{\now}{\mbox{\em now}}
\newcommand{\later}{\mbox{\em later}}
%\newcommand{\day}{\mbox{\em day}}
\newcommand{\sunday}{\mbox{\em sunday}}
\newcommand{\monday}{\mbox{\em monday}}
\newcommand{\tuesday}{\mbox{\em tuesday}}
\newcommand{\Occurrence}{\mbox{\em Occurrence}}
\newcommand{\Order}{\mbox{\em Order}}
\newcommand{\Absence}{\mbox{\em Absence}}
\newcommand{\Universality}{\mbox{\em Universality}}
\newcommand{\Existence}{\mbox{\em Existence}}
\newcommand{\BoundedExistence}{\mbox{\em Bounded Existence}}
\newcommand{\Precedence}{\mbox{\em Precedence}}
\newcommand{\Response}{\mbox{\em Response}}
\newcommand{\ChainResponse}{\mbox{\em Chain Response}}
\newcommand{\ChainPrecedence}{\mbox{\em Chain Precedence}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\bd}{\begin{description}}
\newcommand{\ed}{\end{description}}
\renewcommand{\bar}[1]{\overline{#1}}

\renewcommand{\baselinestretch}{1.67}
%%% ----------------------------------------------------------------------


%NEW STUFF
%\makeatletter
%\def\fnum@figure{\sffamily\small\figurename~\thefigure}
%\def\fnum@table{\em\tablename~\thetable}
%\makeatother
\newtheorem{theorem}{Theorem}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{heuristic}{Heuristic}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{problem}{Problem}
\newenvironment{PROOF}{\noindent {\bf Proof\,\ }}{\hfill\mbox{\ $\square$} \bigskip}
%\newenvironment{problem}{\begin{center}
%        \begin{tabular}[t]{@{\hspace{0.5 in}}p{1 in}rcl@{}}}{\end{center}}
\newcommand{\minimize}[1]{minimize & & {#1} & }
\newcommand{\maximize}[1]{maximize & & {#1} & }
\newcommand{\subjectto}[3]{subject to & {#1} & {#2} & {#3}}
\newcommand{\andsubjectto}[3]{ & {#1} & {#2} & {#3}}
\newcommand{\probnumber}[1]{\end{tabular}\hfill\mbox{{#1}}}
%\newcommand{\keywords}[1]{\vspace{0.75in}\noindent
%        \makebox[1.25in][l]{Keywords:}\parbox[t]{4.25in}{{\em {#1}}}}
\newcommand{\CRcategories}[1]{\vspace{0.75in}\noindent
        \makebox[1.25in][l]{CR categories:}\mbox{${#1}$}}

%\newcommand{\QED}{$\square$}
\newcommand{\sptree}{{SP2}}
\newcommand{\rapture}{Rapture}
\newcommand{\PQ}{\mbox{{\em PQ\/}}}

\newcommand{\implic}{\mbox{\ \ $\Longr7ightarrow$}}
\renewcommand{\bar}[1]{\overline{#1}}
%\renewcommand{\bar}[1]{{\cal\}#1}
\newcommand{\wt}[1]{\lambda({{#1}})}
\newcommand{\wta}[2]{\lambda_{#1}({{#2}})}
\newcommand{\bigvalue}{\Delta}
\newcommand{\leng}[1]{\lambda({{#1}})}
\newcommand{\mincutint}[1]{{\cal I}({{#1}})}
\newcommand{\deletemin}[1]{\mbox{{\em deletemin\/}}({{#1}})}
\newenvironment{mainproof}{%\vskip{1mm}
        \noindent {\bf Proof of Theorem~\ref{T:main}\,\ }}
        {\hfill\mbox{\ $\square$} \bigskip}

\newenvironment{timnote}
{ \noindent {\bf NOTE to TIM:} \\ \em }{ }

\newenvironment{mikenote}
{ \noindent {\bf NOTE to MIKE:} \\ \em }{ }

\newenvironment{note}
{ \noindent {\bf NOTE:} \\ \em }{ }

\newcommand{\setuptabs}{
\hspace*{.3in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.1in}
\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}
\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\=\hspace*{.2in}\kill
}
%%%--------------------------------------------------------------------------
%be\renewcommand{\baselinestretch}{1.67}
\markboth{Houle, Menzies, Powell:  Fast Search for   Temporal Properties;
submitted to IEEE Trans. on
SE, \today }{ }

\begin{document}

\title{A Fast Search for  Temporal Properties of Requirements}
\author{ Michael E. Houle
\thanks{  Michael Houle is with IBM Japan  Tokyo Research Laboratory
     1623-14 Shimotsuruma, Yamato-shi
     Kanagawa-ken 242-8502,
         Japan. Dr. Houle is on leave from
the Basser  Department of  Computer Science, The University
of Sydney,Sydney, NSW, 2006, Australia
     \protect\url{meh@cs.usyd.edu.au}},
     Tim Menzies\thanks{ Tim Menzies is with the
Lane Department of Computer Science \& Electrical
Engineering, West Virginia University PO Box 6109,
Morgantown, WV 26506-6109, \protect\url{tim@menzies.com}},
John Powell\thanks{John  Powell is with the Jet Propulsion
Laboratory Quality Assurance Office, Mail Stop: 125-233
4800 Oak Grove Drive Pasadena CA 91109-8099,
\protect\url{john.powell@ivv.nasa.gov}},
\thanks{Much of this work was performed
while Menzies \& Powell worked at the NASA/WVU Software
Research Laboratory, IV\&V Facility, Fairmont, West
Virginia, partially supported by NASA through cooperative
agreement \#NCC 2-979.}\thanks{An earlier and shorter version of
this paper (that lacked the proofs in the appendix of this
paper) appeared at ICSE 2001 as {\em Fast Formal Analysis
of Requirements via ``Topoi Diagrams''}~\cite{me00q}.
 }}



\maketitle
%\copyrightspace
%
% If you want to print drafts of the paper with a draft
% notice in the copyright space, comment out the \copyrightspace
% line above and include the \submitspace line below instead.
%
%\submitspace{$^*$ }


% Page number on the initial page can be omitted in both the review and
% final submission (and should be removed in the final submission).  The
% line below does that.

\thispagestyle{empty}  % suppresses page number on first page

% In the review submission, page numbers should appear (they can be omitted
%  from the first page).  The pagestyle command below puts them in.
% In the final submission of accepted papers, page numbers should be
%  omitted; remove or comment out the pagestyle line below to omit them.

%\pagestyle{plain}

% Use \section* instead of \section to suppress numbering for
% the abstract, acknowledgements, and references.

\begin{abstract}
Early testing of requirements can decrease the cost of
removing errors in software projects. However, unless done
carefully, that testing process can significantly add to
the cost of requirements analysis.  We show here that
requirements expressed as {\em topoi diagrams} can be built
and tested cheaply -- using our SP2 algorithm, the formal
temporal properties of a large class of topoi can be explored
very quickly, in time nearly linear in the number of nodes
and edges in the diagram.   Topoi diagrams cannot express
certain complex concepts such as iteration and sub-routine
calls.  Hence, there are some limitations to our approach
is more useful for requirements engineering than for
traditional model checking domains.
\end{abstract}


\section{Introduction}The case for more formality in
requirements engineering is overwhelming. Many errors in
software can be traced back to errors in the
requirements~\cite{reifer79}. Often, the conception of a
system is improved as a direct result of the discovery of
inadequacies in the current conception. The earlier such
inadequacies are found, the better, since the cost of
removing errors at the requirements stage can be orders of
magnitude cheaper than the cost of removing errors in the
final system~\cite{schnieder98}.

The  benefit of formally checking a system is that a formal
analysis can find more errors than standard testing. A
single formal first-order query is equivalent to many
white-box or black-box test inputs.

The cost of testing requirements engineering may be
impractically high. These costs include
the {\em modeling cost}, the {\em
execution cost}, the {\em personnel
cost}, and the {\em development brake}.
The {\em modeling cost} is incurred when
analysts create the
 {\em systems model}, and the {\em
properties model} needed for formal analysis. Both models
need to be expressed in some machine-readable form. The
properties model is often much smaller than the systems
model and contains a formal temporal logic\footnote{
Temporal logic is classical logic  augmented with some
 temporal
operators such as
 $\square X$ (always $X$ is true),
$\lozenge X$ (eventually $X$ is true), $\bigcirc  X$ ($X$
is true at the next time point), $X \bigcup Y$: ($X$ is
true until $Y$ is true).  } description of the invariants
that must be tested in the systems  model.

A rigorous analysis of formal properties
has a high {\em execution cost}, since it
implies
a full-scale search through the systems model.  For example,
if a given systems model has $n$
variables, each of which may take on a finite number of unique
values $m$, then the size of the state space associated with that
model is $m^n$.
This space can be too large to explore,
even on today's fast machines. Despite extensive research
into speeding up this search (see our {\em Related Work} section),
analysts often must
painstakingly
rework the systems and properties models into more abstract
and succinct forms
that are small enough to permit formal analysis.

Analysts skilled in formal methods must be recruited or trained.
Since such analysts are generally hard to find and retain,
formal methods have a high {\em personnel cost}.


The above costs can be so high that the requirements must
be frozen for some time while one performs the formal
analysis. Hence, one of the costs of formal analysis is
{\em development brake} that  slows down the requirements
process. Slowing down the requirements process is
unacceptable for fast moving software companies.



\begin{figure*}
\begin{center}
\includegraphics[width=4in]{topoi.eps}
\end{center}
\caption{An example topoi
from~\protect\cite{dieng95}.
The formal  semantics for topoi
is described below. Informally, we say that
$+$ indicates ``encourages'' while
$-$ indicates ``discourages''.
}\label{fig:topoi}
\end{figure*}

Ideally, a method for reducing the cost of testing
requirements would eliminate the execution cost and reduce
the cost and skill involved in building the properties and
systems models.  If achievable, such a method would also
reduce the personnel cost, since it would not require such
highly-skilled analysts.  Having reduced the personnel,
modelling, and execution costs, this hypothetical method
would inevitably decrease the development brake.

Some progress has already been made in reducing the cost of
properties modelling using {\em temporal logic patterns}.
Dwyer et.al.~\cite{dwyer97,dwyer98a} have identified
patterns within the temporal logic formula seen in many
real-world properties models. For each pattern, they have
defined an expansion from the intuitive pseudo-English form
of the pattern to a formal temporal logic formula. In this
way, analysts are shielded from the complexity of formal
logics. For example, the simple pseudo-English statement

\[always(brake=on)\;between(danger=seen)\;
and(car=stop)\]

\noindent can be automatically expanded into the more
arcane formal statement:
\begin{eqnarray}\nonumber
&&\square ((danger=seen\; \wedge\; !(car=stop)\;
\wedge\lozenge\; (car=stop))\\\nonumber && \rightarrow
(brake=on\;\cup \;(car=stop)))
\end{eqnarray}
One drawback with temporal logic patterns is that while
complex temporal formula can be automatically generated
from intuitive pseudo-English, the execution cost remains.
That is, even though we can quickly build the properties
model, we may not be able to explore all of that model.

In this article, we argue that we can greatly reduce the
execution cost for a class of systems models seen in the
requirements stage. We assume that temporal logic patterns have reduced
the modelling cost of the properties. Hence, what remains is
the modelling cost of the system and the execution cost.
The key to
this reduction is SP2, a new algorithm for generating {\em
time series} (defined below)  from {\em topoi},
which are statements of gradual influences between
variables~\cite{dieng95}. Topoi can represented graphically
by {\em topoi diagrams}, an example of which is shown in
\fig{topoi}. The experience of Dieng~\cite{dieng95}
and Menzies~\cite{me95} is that domain experts
can sketch topoi  very quickly and so (for
requirements that are topoi-compatible) our approach also
reduces the systems modelling cost.

These cost-reduction benefits can only be realized if we
accept certain restrictions. Specifically,  the systems
model must be expressed as topoi diagrams. Topoi are not
very expressive, and exclude statements such as first-order
assertions, iterations, sub-routine calls, and assignments.
Due to these language limitations, our approach is not
suited to domains that need the excluded statements, such
as complex protocols seen in  concurrent processes.
\begin{figure*}
\begin{minipage}{.20\linewidth}
\includegraphics[width=1.5in]{thin.eps}
\end{minipage}\hfill
\begin{minipage}{.25\linewidth}
\includegraphics[width=1.7in]{qoc2.eps}
\end{minipage}\hfill
\begin{minipage}{.25\linewidth}
\includegraphics[width=1.75in]{law1.eps}
\end{minipage}\hfill
\begin{minipage}{.20\linewidth}
\includegraphics[width=1.5in]{sym.eps}
\end{minipage}

{\small
\begin{minipage}{.20\linewidth}
 \fig{egs}.i: {
A soft-goal graph: the
{\em and} node denotes that both {\em sharing of information}
and {\em task switching} are enabled by
{\em flexible work patterns}}.
\end{minipage}\hfill
\begin{minipage}{.25\linewidth}
\fig{egs}.ii: {
A
questions-options-criteria graph;
from \protect\cite{shum94}.\\~\\
}
\end{minipage}\hfill
\begin{minipage}{.25\linewidth}
\fig{egs}.iii: {
Topoi from \fig{law1}.~\\~\\~\\
}
\end{minipage}\hfill
\begin{minipage}{.20\linewidth}
\fig{egs}.iv: {
The Smythe '87 theory. From \protect\cite{smythe87}:
statements of gradual knowledge relating to
 laboratory experiments on mammals.
}
\end{minipage}}
\caption{Sample topoi diagrams.}\label{fig:egs}
\end{figure*}

These restrictions are not fatal to the modeling process,
at least at the requirements stage. We will show via
example that topoi diagrams are sufficient to represent a
wide range of diagrams seen in certain approaches to
requirements engineering and recording design rationales.
Hence, when we say that this approach is practical and
useful, we really mean {\em practical and useful for early
life cycle requirements discussions only}.




%XXX stress the hasitly drawn thing


\section{About Topoi}

Our approach assumes that requirements systems
models  are expressed in the form
of {\em topoi}; i.e.  statements of gradual
statements such as  (i)~the more X, the
more Y; (ii)~the less X the less Y; (iii)~the more X, the less Y; or
(iv)~the less X the less Y.
Dieng et.al. offer many examples of
topoi  from
numerous examples from their records of interviews with
experts~\cite{dieng95}.
For example: {\em
the more there is water infiltration in the roadway body, the
worse the
foundation risks to be}; and
{\em if there is a punctual undressing and if the roadway is between
five and fifteen
years old, then the causes
'too old coating' is all the more certain since the
roadway is older.}

Our experience has always been that the systems modeling cost with topoi
is very low.
Topoi graphs can be quickly generated in the requirements stage.
Two feuding stakeholders with two marker pens and one whiteboard
can generate many, many topoi in just a few hours.

\subsection{Example Topoi}

Topoi graphs
can be found in many domains.
\fig{topoi} showed a topoi from an insurance domain
using the graphical notation of
Dieng's 3DKAT tool.
%\newcommand{\myfig*}[2]{\begin{figure*}\begin{center}\includegraphics{#1.eps}\end{center}\caption{#2}}\label{fig:#1}\end{figure*}}
\fig{egs}.i show some
Mylopoulos-style {\em soft-goal} graphs~\cite{mylo99}.
Soft-goal graphs represent
gradual knowledge about non-functional requirements.
In \fig{egs}.i, an expert describes how to increase
business flexibility.
\fig{egs}.ii shows  a ``questions-options-criteria'' (QOC)
graph from the  design rationale community~\cite{shum94}. In  such QOC
graphs, questions suggest options and deciding on a certain option can
raise other  questions.   Options   shown  in  a  box denote  selected
options.  Options are assessed  by  criteria and criteria  are gradual
knowledge;  i.e. they {\em  tend to support}  or {\em  tend to reject}
options.  QOCs   can succinctly  summarize   lengthy debates; e.g. 480
sentences  uttered in  a  debate between   two  analysts on  interface
options  can be    displayed    in  a   QOC   graph  on    a    single
page~\cite{maclean96}.
\begin{figure}
{\small {\bf
\begin{verbatim}
if guilty  then jail.
if age < 7 then infant.
if infant or moron
   then not legally_responsible.
if legally_responsible and guilty
   then jail.
if motive and means and opportunity and witnesses
   then guilty.
if guilty and not legally_responsible
   then not jail.
\end{verbatim}
}}
\caption{Rule-based requirements from a legal system.}\label{fig:law1}
\end{figure}
\fig{egs}.iii shows topoi generated from the requirements
of a rule-based legal system, shown in \fig{law1}.
This translation assumes that
propositions in the rule base are modelled as a belief/strength
pair such as infant/$X$, where $X$ is some continuous number.

\subsection{Topoi are Over-generalized and Over-constrained}

 Topoi edges constrain the values
of the connected variables and, often, they are {\em
over-constrained}; i.e. they cannot be all simultaneously
satisfiable. To use a topi, we must therefore ignore some
of their features.  For example, consider \fig{egs}.i and
the case of {\em flexibility} and {\em usability}
increasing while {\em performance} decreases. Note that we
can explain {\em flexability} increasing, but only if we
can avoid the contradictory conclusion offered by the edge
from {\em usability}.

Ignoring inconsistencies when it is convenient to do so
runs the risk of excessive {\em over-generalization}; i.e.
more conclusions many be reachable in the abstract model
than in the real system being modelled. A pre-experimental
concern is that informal topoi are so over-generalized that
we could use them to infer any properties at all
(researchers in qualitative simulation call this the   {\em
chatter} problem~\cite{kuipers86}). This concern is not
always correct. While topoi are over-generalized, they may
still be restrictive enough to be useful. For example,
recall \fig{egs}.i and the fragment:
\[\usability\stackrel{-}{\rightarrow}\flexibility \stackrel{-}{\leftarrow}\performance\]
Note that there is no way to explain the output of
increased {\em flexibility}
($\{\mbox{$\flexibility\uparrow$}\}$) from the input of
increased {\em usability} and {\em performance}
($\{\mbox{$\usability\uparrow$},
\mbox{$\performance\uparrow$}\}$).

For another example, consider \fig{s89} which was generated
by Smythe who extracted the list of gradual influences
claimed by a set of articles from different authors
discussing human internal physiology~\cite{smythe89}.
Feldman~\& Compton, then Menzies, showed that despite
over-generalization, \fig{s89} could be used to detect a
large number of previously-unnoticed errors published in
international refereed
journals~\cite{fecosm89b,me97a,me96b}. Interestingly, these
faults were found using the tables of data published to
support those theories; i.e. those experiments reported
observations that could not be reproduced via  \fig{s89}.

For a last example of the utility of topoi, we discuss
below experiments where a topoi-based search for temporal
properties out-performed a state-of-the-art model checker
(SPIN~\cite{holzmann97}).

\subsection{Comprehension Problems}

Topoi seem quite simple, but often defy manual analysis,
possibly  due to their over-constrained and
over-generalized nature. For example, Menzies' topoi
tester~\cite{me95} found behaviors in very small topoi
(\fig{egs}.iv) that had not seen after days of manual
analysis. The difficulty in generating possible topoi
behavior gets worse as the topoi gets more complicated.
When collected from multiple stakeholders, gradual
statements can be quite complex, quite large, and contain
feedback loops. For example, consider \fig{s89}. A reviewer
of one draft of this paper commented that this figure was
hard to read, and that is our point. Our experience has
been that, at no magnification, can a manual inspection
confidently explore the dense maze of interactions within
topoi as complicated as \fig{s89}.
\begin{figure}[!t]
\begin{center}
\includegraphics[width=3in]{big.eps}
\end{center}
\caption{A large topoi with many loops.}\label{fig:s89}
\end{figure}

Automatic methods are often used when  manual methods fail.
Such automatic methods require a presice semantics for the
models being processed.


\subsection{Topoi: Formal Semantics}

Formally, we say that
a topoi is a directed,
possibly cyclic  graph $G$ containing vertices and edges
\mbox{$<V,E>$}.
 $E$ are the connectors between variables and are one of a set of
 pre-defined
 types; e.g. \(\stackrel{+}{\rightarrow}\)
 or \(\stackrel{-}{\rightarrow}\).
That is:
 \begin{eqnarray}
 E_i&=& V_i \stackrel{+}{\rightarrow}  V_j \; or\;
V_i \stackrel{-}{\rightarrow}  V_j\nonumber\\
 G &=&<V, E>\nonumber
 \end{eqnarray}


The vertices of a topoi
can be assigned a finite number of values;
e.g.
 {\em
up}, {\em down} or {\em steady}. These values model the sign of
the first derivative of these variables (i.e. the rate of change
in each value). {\em X}~\(\stackrel{+}{\rightarrow}\)~{\em Y}
denotes that {\em Y} being {\em up} or {\em down} could be
explained by {\em X} being {\em up} or {\em down} respectively.
That is:
\begin{eqnarray}\label{eq:+}
  V_i \stackrel{+}{\rightarrow}  V_j & \equiv &
\left\{  \begin{array}{lcl}
                V_i\uparrow &\implies &V_j\uparrow\\
                V_i\downarrow &\implies&V_j\downarrow\\
                \end{array} \right.
                \end{eqnarray}
(where  $\uparrow$ and $\downarrow$ denote up and down
respectively.)

{\em X}~\(\stackrel{-}{\rightarrow}\)~{\em Y} denotes that {\em
Y} being {\em up} or {\em down} could be explained by {\em X}
being {\em down} or {\em up} respectively. That is:
\begin{eqnarray}\label{eq:-}
 V_i \stackrel{-}{\rightarrow}  V_j & \equiv &
\left\{  \begin{array}{lcl}
                V_i\uparrow\; & \implies &\;V_j\downarrow\\
                V_i\downarrow\; & \implies &\;V_j\uparrow\end{array}
                \right.
                \end{eqnarray}


Tacit  in our topoi diagrams  are conjunctions of influences.   We
can view topoi as influences splashing around pipes that
connect tubs. Pairs of competing influences can cancel out.
That is, we can explain the level of water in a tub remaining
steady via conjunction of competing upstream influences; e.g.
                \begin{equation}\label{eq:0}
\left(
\begin{array}{c}
(V_i\uparrow\; \implies\; V_j\uparrow)\\
\andand \\
 (V_k\downarrow \;\implies \;V_j\downarrow)
\end{array}
\right)
\implies
\left(
\begin{array}{l}
(V_i\uparrow \wedge V_k\downarrow) \\
\implies \\
(V_j=\steady)
\end{array}
\right)
\end{equation}



This formal semantics is sufficient to guide the translation of topoi
for a formal model checker such as SPIN. \fig{prom1}
shows the results of such a translation
of \fig{egs}.iv.
In this figure, all the nodes have the values {\em up}, {\em down},
{\em steady} and {\em unknown} (which is a placeholder for the initial
conditions). Also,
for convenience,
all systems model inputs $X$ are declared to be $X_{\mbox{chg}}$
variables with values
{\em
arrived, left} denoting the differences between these variables in different
experiments. For example, if we increase the injections of {\em dex},
then we also say that ${\dex}_{\mbox{chg}}=\arrived$.


\begin{figure}[!t]
{\tiny {\bf
\begin{verbatim}
#define DOWN    0
#define STEADY  1
#define UP  2
#define UNDEF   3
#define ARRIVED 0
#define LEFT    1

byte chg_cold_swim = UNDEF /* chg_cold_swim = {ARRIVED,LEFT} */
byte chg_dex = UNDEF       /* chg_dex = {ARRIVED,SWIM}       */
byte cold_swim = UNDEF     /* cold_swim = {DOWN,STEADY,UP}   */
byte dex = UNDEF           /* dex = {DOWN,STEADY,UP}         */
byte temp = UNDEF          /* temp = {DOWN,STEADY,UP}        */
byte nna = UNDEF           /* nna = {DOWN,STEADY,UP}         */
byte acth = UNDEF          /* acth = {DOWN,STEADY,UP}        */
byte cortico = UNDEF       /* cortico = {DOWN,STEADY,UP}     */

active proctype smythe() {
      if
        ::dex == UNDEF -> dex = DOWN
        ::dex == UNDEF -> dex = STEADY
        ::dex == UNDEF -> dex = UP
      fi;
      if
        ::cold_swim == UNDEF -> cold_swim = DOWN
        ::cold_swim == UNDEF -> cold_swim = STEADY
        ::cold_swim == UNDEF -> cold_swim = UP
      fi;
      if
        ::chg_dex == UNDEF -> chg_dex = ARRIVED
        ::chg_dex == UNDEF -> chg_dex = LEFT
      fi;
      if
        ::chg_cold_swim == UNDEF -> chg_cold_swim = ARRIVED
        ::chg_cold_swim == UNDEF -> chg_cold_swim = LEFT
      fi;
      if
        ::chg_dex == ARRIVED -> temp = UP
        ::chg_dex == LEFT -> temp = DOWN
      fi;
      if
        ::chg_cold_swim == ARRIVED -> nna = UP
        ::chg_cold_swim == LEFT -> nna = DOWN
      fi;
      do
        ::(chg_cold_swim == ARRIVED && temp == UP) -> nna = STEADY
        ::(chg_cold_swim == LEFT && temp == DOWN) -> nna = STEADY
        ::temp == DOWN -> nna = UP
        ::temp == UP -> nna = DOWN
        ::temp == DOWN -> acth = UP
        ::temp == UP -> acth = DOWN
        ::nna == UP -> acth = UP
        ::nna == DOWN -> acth = DOWN
        ::acth == UP -> cortico = UP
        ::acth == DOWN -> cortico = DOWN
        ::cortico == UP -> temp = UP
        ::(cortico == UP && chg_dex == LEFT) -> temp = STEADY
        ::cortico == DOWN -> temp = DOWN
        ::(cortico == DOWN && chg_dex == ARRIVED) -> temp = STEADY
        ::(temp == UP && nna == UP) -> acth = STEADY
        ::(temp == DOWN && nna == DOWN) -> acth = STEADY
      od;
}
\end{verbatim}
}}
\caption{\fig{egs}.iv expressed in the PROMELA language used in SPIN
model checker~\cite{holzmann97}.}\label{fig:prom1}
\end{figure}

\subsection{Model Checking and Topoi}

We can test topoi using libraries of expected or desired behavior.
Such libraries can be quickly built via interviews with users.
We have found it useful to structure these interviews in an OO framework.
After
generating use cases and particular scenarios,
we ask our users to clarify
exactly what are the expected inputs and required outputs for each scenario.
This generates two artifacts. Firstly, it leads to a topoi graph describing how
they think influences
should propagate around a systems model.
Secondly, it leads to the formulation of properties models of the form:
\mbox{{\em When I do this, I expect to see that}}
or, in the language of temporal logic used in (e.g.) SPIN:
\begin{equation}\label{eq:a}
\square\left(Inputs \rightarrow  \lozenge\; Outputs\right)
\end{equation}
i.e. always the {\em inputs} lead, eventually, to the {\em outputs}.

We encounter problems if we use \eq{a} to check large topoi using standard model
checkers.
While
SPIN checks that \eq{a} holds over  \fig{prom1} in less than a
second, it can fail
to terminate for larger systems models.
In  one  study, we offered 40 properties of the form of \eq{a} to SPIN along
with \fig{s89} expressed in the same format as \fig{prom1}.
Given 100MB of maximum RAM, SPIN ran out of memory for most of the properties.
We suspected that the search space was too big. \fig{s89} contains 80 variables,
each of which has at least the values $up, down, steady, undef$; i.e. total space
of options at least of size ($4^{80} \approx 10^{48})$. In a second study,
we reduced the size of the system by removing the $steady$ values. This shrank the
options to ($3^{80} \approx 10^{38})$. However, even in this reduced system,
SPIN ran out of memory and  failed to return anything
for  29 of the 40 properties~\cite{powell99}.

In summary, even though topoi can can be processed by
standard model checkers, in practice, this may not be
feasible. Fundamentally, this is due to the  NP-hard nature
of topoi inference\footnote{NP-hard problems belong to a
class of problems with no known polynomial upper-bound on
their solution time; i.e. it may not be possible to scale
NP-hard tasks to large problems.}.  To show that topic
processing in NP-hard, consider the graph generated by
applying \eq{+}, \eq{-} to (e.g.) \fig{egs}.i. This   graph
contains {\em impossible pairs}; i.e. we could construct a
pathway from certain inputs to the impossible pair of
\mbox{{\em flexibility}$\uparrow$} and \mbox{{\em
flexibility}$\downarrow$}. To avoid this contradiction, a
topoi inference engine must take care to build consistent
pathways across a topoi. Gabow et.~al.~\cite{gabow76}
showed that building consistent pathways across graphs with
impossible pairs is a problem that can be reduced to 3SAT.
As such it is NP-hard for all but the simplest graphs (in
this context, a topoi is very simple if it is a tree, or
has an out-degree $\leq 1$).

\section{RAPTURE and SP2}

While general topoi defeat general-purpose model checkers,
specialized search engines can quickly check the temporal
properties of a special class of topoi called {\em
twinned topoi}. A  twinned topoi
graph $G(V,E)$ has three  features of interest.
Firstly, a temporal property can be demonstrated
by checking for set membership within a {\em time
series}\footnote{MIKE: a plea for less ink: time series, not temporal
sequence} (defined below) of
nodes reachable from inputs $I$ ($I \subseteq V$).
For example, to generate a counter-example to  {\em
always X},
it would be sufficient to find a time series containing
$\neg X$ (i.e. $\lozenge \neg X$ is a counter-example to $\square X$).
Secondly,
this time series can be generated
in near-linear time using the RAPTURE/SP2 algorithms described below.
Thirdly,
if that that series does not contain some
desired property, it can be incrementally
 {\em coaxed} towards a series with a higher likelihood
 of containing  the property.
That is, our proposal is to replace an exponential time algorithm with the
repeated application of a linear time algorithm.

Previously we have argued for the first feature~\cite{me00q}.
The second and third feature are the novel contribution of this paper
and we  demonstrate them below.

\subsection{Twinned Topoi}

A twinned topoi is a graph $G(V,E)$
of the following form.
For every
node $V_i$, there exists  a {\em twin} $\bar{V_i}$.
For example,
 $performance\uparrow$ (up) has the twin
 $performance\downarrow$ (down).
Twins are incompatible; e.g. we can't believe that
$performance$ is both $\uparrow$ (up) and $\downarrow$ (down) simultaneously.
The twin of a twin is itself; i.e.
$\bar{\bar{V_i}}= V_i$. This lets us represent (e.g.)
negation where $x$ and $\bar{x}$ represents $x$ and
$\neg{x}$ (respectively); and $\bar{\bar{x}}=x$ is analogous
to $\neg\neg{x}=x$.

In a twinned topoi,
edges have a numeric weight $\lambda$.  Nodes and their
twins are connected by edges with the same weight; i.e.
$E(V_i,V_j)=\lambda_k$ and
$E(\bar{V_i},\bar{V_j})=\lambda_k$.

SP2 is a variant of Dijkstra’s shortest paths tree algorithm, described in the appendix,
 that generates an acyclic directed graph $R$
that holds the nodes that are {\em reachable} from certain inputs
$I$ ($I\subseteq V$).
This tree divides into  subsets $R_0, R_1$
where the inputs are the roots of $R_0$.
For all $i$,
nodes in
$R_{i+1}$ are descendants of $R_i$.
Also,
each subset $R_i$ is
 {\em consistent}; i.e. a node and its twin
do not appear in the same subset ($\forall V_i \in R_i,
\bar{V_i} \not\in R_i$).






\begin{figure}
{\footnotesize {\sf
\begin{tabbing}
\setuptabs
\> {\bf function} rapture(inputs: I; topoi: T; properties: P): $S$\\
\>1.       \>  $G \leftarrow twin(T)$\\
\>2.        \>  {\bf repeat} maxCoaxes {\bf times do} \\
\>2a.\>        \> $R \leftarrow \emptyset$\\
\>2b.\>      \> $<R_0,R_1> \;\leftarrow\;$ SP2 \{SP2 is defined in the appendix\}\\
\>2c.\>       \>  $N_0 \leftarrow \{\forall V_i \in R_0 | (V_j \in $ after$(V_i)) \bigwedge (V_j \in R_0) \bigwedge (\bar{V_j} \in R_1)\}$\\
\>2d.\>     \>   $L_0 \leftarrow R_0 - N_0$\\
\>2e.\>    \> $i \leftarrow 1$ \\
\>2f.\>   \> {\bf while} $\neg$ ($R_{i-2} = R_{i}$ {\bf or} $R_{i} = \emptyset$)\\
\>2f1.\>    \>    \> $i \leftarrow i+1$\\
\>2f2.\>    \>    \> $R_i \leftarrow \emptyset$\\
\>2f3.\>    \>    \> {\bf if} i=useful {\bf then}\\
\>2f3a.\>    \>    \> \> {\bf for} $V_i \in L_0$ {\bf do} \\
\>    \>    \>    \>  \>  \> $R_i\leftarrow R_i \cup V_i$\\
\>    \>    \>    \>  \>  \> $V_i.demote  \leftarrow\;$ avoid($V_i$)\\
\>    \>    \>    \>  \>  \> $V_i.promote  \leftarrow\;$ want($V_i$)\\
\>    \>    \>    \> \> {\bf end for}\\
\>2f3b.\>   \>   \> {\bf else}  \> {\bf for} ($V_i \in\;$ SP($R_{i-1}$) $\bigwedge (V_i \in R_{i-2})$ {\bf do} \\
\>     \>   \>     \> \>\> \{SP is Dijstra's shortest paths trees algorithm\}\\
\>     \>   \>     \>  \> \>$R_i\leftarrow R_i \cup V_i$\\
\>     \>   \>      \>  \>\> $V_i.demote  \leftarrow\;$ avoid($V_i$)\\
\>\>    \>    \>    \> \>$V_i.promote  \leftarrow\;$ want($V_i$)\\
\>      \>    \>     \> \>{\bf end for}\\
\>      \>    \>    \> {\bf end if}\\
\>\>    \>    {\bf end while}\\
\>2g.\>    \>{\bf for} $p \in P$ {\bf do} \\
\>\>    \>\> $how \leftarrow$ DFS($p$) \{depth first search across $R$ to inputs $I$\}\\
\>\>    \> \> $bad \leftarrow$  HIGHEST\_BAD($how$)\\
\>\>    \> {\bf end for}\\
\>2h.\>    \> $G \leftarrow\;$ COAX($bad$);\\
\>\>    {\bf end repeat}\\
\> 3.   \> $S_0 \leftarrow I$\\
\> 4.   \> $S_1 \leftarrow N_0$;\\
\> 5.   \> {\bf for} $(R_i \in R) \bigwedge (i > 1)$ {\bf do} $S_{i+1} \leftarrow R_i$ {\bf end for}\\
\> 6. \>  {\bf return} $S$\\
\>  {\bf end} rapture
\end{tabbing}}}
\caption{The RAPTURE algorithm.}\label{fig:rapture}
\end{figure}
Note that we do not require analysts to write
twinned topoi. Rather, analysts generate topoi
such as \fig{topoi} and \fig{egs}. Then,
an automatic process ``twins'' that topoi by
adding in the required twinned nodes and twinned edges
(see Step 1 of \fig{rapture}).
For example, if analysts generated \fig{teg}.A, then
we would auto-generate \fig{teg}.B.

\begin{figure}
{\footnotesize
\begin{tabular}{p{1.8in}p{1.5in}}
\includegraphics[width=2in]{model.eps}&\includegraphics[width=1.5in]{later.eps}\\
\fig{teg}.A: analyst logic &\fig{teg}.B: a twinned topoi (edge wieghts not shown).
\end{tabular}}
\caption{Auto-generation of a twinned topoi from
an analyst's logic.}\label{fig:teg}
\end{figure}

We use SP2 to generate  $R_0, R_1$ for two reasons.
Firstly, if the nodes reachable from the inputs across a twinned
topoi can't be divided
into $R_0, R_1$, then there exists a shorter path
to those nodes (this is proved in the appendix).
Since  Dijkstra's
algorithm, and SP2, ensures shortest paths then
it must be possible to generate $R_0, R_1$ in the
$O(|V|+|E|*log(|V|))$ time of a shortest paths tree
traversal.
Secondly,
just like Dijkstra's shortest paths tree algorithm,
SP2 will generate the ``shrotest'' paths to properties
(where ``shortest'' is defined as the sum of the weights
of the used edges). This
greatly improves the
comprehensibility of our approach.

\subsection{Generating  a Time Series}

A time series is the set of realizable
scenarios of the form $inputs,S_0,S_1,... S_i$.
Each $S_i$ is a consistent set of state changes occurring
at time step $i$.

$S_i$  can be found using
the RAPTURE algorithm of \fig{rapture}. In summary,
SP2 is used to find $S_i$ ($i<2$) and another technique
is used to find $S_i$ ($i \ge 2$).
The core of the process is Step 2f3b of \fig{rapture}.
$R_i$ contains the nodes reachable from
$R_{i-1}$ that appeared two time ticks ago
(within $R_i$). Note that
\begin{equation}\label{eq:even}
R_0 \subseteq R_2 \subseteq R_4 \subseteq ..
\end{equation}
and
\begin{equation}\label{eq:odd}
R_1 \subseteq R_3 \subseteq R_5 \subseteq ..
\end{equation}
Since any subset of a consistent set is also consistent, then this process is
guaranteed  to generate consistent time series.

It is easy to show that RAPTURE  terminates in near-linear time\footnote{Mike: i've never written a section
like this before. please feel free to edit it heavily}.
Its  sub-routines are all linear or nearly-linear.
SP2 and SP (called at Steps 2b and 2f3b) run in $O(|V|+|E|*log(|V|))$ time (see above).
The COAX and AFTER sub-routines are described below and, worst
case, are  $O(|V|+|E|)$.
We can show that these sub-routines are called a
finite number of times;
i.e. RAPTURE termiantes in near-linear time.
Firstly, $maxCoaxes$ (at Step 2)
is typically small ($< 50$).
Secondly,  Step 2f  terminates in a fnite number of steps.
\eq{even} and \eq{odd} show that $R_i$ will never be larger than $R_{i-2}$.
Hence, there will occur two cases
when we can terminate: \be
\item
$R_i$ is identical to $R_{i-2}$;
\item
$R_i$ has shrunk away to the empty set.
\ee

We use $I_{max}$ to denote the $i$ value where we terminate Step 2f.

\subsubsection{Now and Later}

While proving temporal
properties, it is convenient to know what nodes
can appear at any point in the series.
To find  such a set,  we first find $N_0$: the nodes that are both reachable
from inputs in $R_0$ and which have incompatiable twins in $R_1$.
The set $L_0$ is $R_0 - N_0$; i.e.
the nodes that are reachable from inputs, but whose
incompatiable twin cannot be reached in $R_1$  (see
Step 2d of \fig{rapture}- the function LATER($V_i$)
is a $O(|V|)$
depth-first-search that finds all descendant nodes of $V_i$ within  $R_0$ and $R_1$).
For example, \fig{later} shows  $N_0$ (the {\em now} set) and $L_0$ (the {\em later} set)
generated from \fig{teg}; i.e. $L_0=\{v,w\}$\footnote{mike- this is the example you passed me over the phone
but is there an error here? does $in$ connect to (a)~just
$x$ or (b)~both $x$ and $\bar{x}$? Option (a) violates twining but option(b) would make
$\bar{x}, \bar{v}$ and $\bar{w}$ reachable in $R_1$, therefore not part of $L_0$.
What I think is that a better definition of $L_0$ is  as follows and includes the inputs
as
a special case (and contrast this
with Step 2c in \fig{rapture}):
\(N_0 \leftarrow
\{\forall V_i \in R_0 | (
    (V_j \in R_1) \bigwedge
        (V_i \in R_0  \cap before(V_j)) - input \bigwedge
            (\bar{V_i} \in R_1)\}\)
and, as before, $L_0 \leftarrow R_0 - N_0$.
In this example, this would lead to $L_0=\{v,w\}$}.

\begin{figure}
\begin{center}
\includegraphics[width=1.5in]{later1.eps}
\end{center}
\caption{$L_0$ and $N_0$ from \fig{teg}.}\label{fig:later}
\end{figure}

RAPTURE ensures that all even-numbered time steps are consistent and
that all odd-numbered time steps are consistent.
Hence, if we place $N_0$ at $S_0$ (Step 4 of \fig{rapture}),
then we cannot reach anything inconsistent with $L_0$
at $R_0$ or $R_1$ or at {\em any time point in the future}.
Further, since $L_0 \subseteq R_0$, it $L_0$
is both reachable
and consistent at any time step. Therefore, we are free to place $L_0$
at any {\em
useful} location (see
Step 2f3a in \fig{rapture}).



\subsection{Testing Properties }

In  certain  cases, testing for properties in   a time series is very simple.
For example:
\begin{eqnarray}\label{eq:eventually}
\lozenge x & = & R_i \in R \wedge x \in R_i
\end{eqnarray}

Note that model checkers like SPIN don't prove properties. Rather, they seek counter-examples; i.e.
specific situations where a property fails.  We do the same.
Generating certain counter examples is very simple:
\begin{eqnarray}\nonumber
\neg(\square x)&=& \lozenge \bar{x}\\\label{eq:always}
&=& R_i \in R \wedge \bar{x} \in R_i \;\mbox{(by \eq{eventually})}
\end{eqnarray}
Generating a counter example for $\neg(\lozenge x)$ is a special case where the property is demonstrated
by failure to ever find it\footnote{not sure of this one- nervous about testing for non-membership
of $R$ but it seems justified in this case. we can even do it before trying coaxing!}:
\begin{eqnarray}
\neg(\lozenge x)&=& \neg(R_i \in R \wedge x \in R_i)
\end{eqnarray}
Generating counter examples for other properties requires a little more machinery.
In our notation, a property is true at some time in a series if
 \[x \sqsubset R_i\]
This test is implemented as follows.
We adopt the assumption
that a variable's value
remains unchanged until
we see  evidence to
the contrary. For example,
suppose $x$ was false
at $R_{i-1}$. This boolean could
became true at time $i$
iff $x\in R_i$.
Also, if (e.g.) $x$ was false at time $i-1$, then
$x$ remains false    at
time $i$ iff
$\bar{x}\in R_i$ or
$\bar{x}\not\in R_i \wedge
x\not\in R_i$.

Hence, $x \sqsubset R_i$  is true if evidence for $x$ can be found up to, and including,
$R_i$ and no counter evidence against $x$ can be found afterwards; i.e.
\[
x \sqsubset R_i = \left(j < k <= i <= I_{max}\right) \bigwedge \left(x \in R_j\right)  \bigwedge
\left(\neg(\bar{x} \in R_k)\right)\]
A counter-example to   $x \sqsubset R_i$ is denoted as
$x \not\sqsubset R_i$. Such a counter example can be generated as follows: \[
x \not\sqsubset R_i = \left(j < k <= i <= I_{max}\right) \bigwedge
\left( \bar{x} \in R_j \right) \bigwedge \left( \neg(x \in R_k\right)) \]
$x \not\sqsubset R_i$ is defined only for atomic expressions of
$x$ and $\bar{x}$. Hence, non-atomic expressions must be
rewritten to isolate the primitive test for $x \not\sqsubset R_i$.
These rewritten expressions are tested over
time steps
$front=R_i$, $next=R_{i+1}$ and $behind=R_{j > i }$ for $i=0..I_{max}$
(see \fig{ce})\footnote{eeek- is there a better way?}.



\begin{figure}
{\small
\begin{center}
\begin{tabular}{|p{3.5in}|}\hline
next:
\begin{eqnarray}\nonumber
\bigcirc x & = & x \sqsubset next\\
\therefore \neg(\bigcirc x) & = & x \not\sqsubset next
\end{eqnarray}
eventually:
\begin{eqnarray}\nonumber
\lozenge x & = & x \sqsubset front \vee x \sqsubset behind \\\nonumber
\therefore \neg(\lozenge x) & = &\neg(x \sqsubset front \vee x \sqsubset behind)\\\nonumber
&=& \neg(x \sqsubset front) \wedge \neg(x \sqsubset behind)\\
&=& x \not\sqsubset front \wedge x \not\sqsubset behind
\end{eqnarray}
until:
\begin{eqnarray}\nonumber
x \cup y & = & y \sqsubset front \vee (x \sqsubset front \wedge y \sqsubset behind)\\\nonumber
\therefore \neg(x \cup y) & = &
\neg(y \sqsubset front \vee (x \sqsubset front \wedge y \sqsubset behind))\\\nonumber
&=& \neg(y \sqsubset front) \wedge \neg(x \sqsubset front \wedge y \sqsubset behind)\\\nonumber
&=& \neg(y \sqsubset front) \wedge (\neg(x \sqsubset front) \vee \neg(y \sqsubset behind))\\\label{eq:until}
&=&y \not\sqsubset front \wedge (x \not\sqsubset front \vee y \not\sqsubset behind)
\end{eqnarray}
weak until:
\begin{eqnarray}\nonumber
x \emph{W} y & = & (x \cup y) \vee \square x\\\nonumber
\therefore \neg(x \emph{W} y) & = & \neg((x \cup y) \vee \square x)\\\nonumber
& = & \neg(x \cup y) \wedge \neg\square x\\
& = & \eq{until} \wedge \eq{always}
\end{eqnarray}\\\hline
\end{tabular}
\end{center}}
\caption{Generating counter examples}\label{fig:ce}
\end{figure}

Note that the generation of counter example requires moving
nodes backwards and forwards in the time series.
The functions {\em want} and {\em avoid} return true
if we want to promote or demote (respectively) the location of nodes in $R$
(see Step 2f3 of \fig{rapture}). The COAX function (described below)
use this information
to nudge nodes backwards and forwards in a time series.

For complex properties, there may exist
an infinite set of possible $i,j$ values
for $front,next,behind$. To make our search tractable, we apply two natural
constraints. Firstly, $j \le I_max$.  Secondly, at least one of $front,next,behind$ must be
from a time step we can directly control. Those directly controllable
time steps are $L_0$ (which we can place anywhere)
and $N_0,R_1$ (which we can coax via SP2).


\subsection{Coaxing}

The above discussion of RAPTURE/SP2 describes how to generate a single time series. This section
describes how to incrementally patch a time series in order to increase the chances that   nodes
appearing at certain time steps. As discussed above,
one patching method is to place $L_0$
at some location that most increases the number of covered counter-examples.
This section discusses another patching method.


Recall that,
in our framework, we first build the first  two  steps in a time series ($R_0$ and $R_1$).
These initial two steps are the seeds for the rest of the series.
Altering the initial two steps therefore has a major
impact on the position of nodes in the rest of the series. Recall also that we use a shortest
paths tree algorithm to find those initial two steps where ``shortest'' is defined in terms of the
sum of the $\lambda$ weight values on the edges used to reach nodes. Clearly, by adjusting
$\lambda$, and rerunning
SP2, nodes will change position in the time series.

There are two cases where we might want to to adjust the lambda weight values. Firstly, as
discussed in the last section, when seeking particular counter examples, it may be required
to coax nodes into
particular time steps. Secondly, while the twinning process guarantees a  $O(|V|+|E|*log(|V|))$
runtime for SP2, it may result in certain unusable
nodes appearing within $R$ (the reasons for this are discussed in \fig{ands}).
If
we  {\em demoted} these unusable nodes in the time series, then  it is possible to reach
nodes in a counter example {\em before} using the problematic nodes.



\begin{figure}
{\small
\begin{center}
\begin{tabular}{|p{3in}|}\hline
Consider
the following topoi:
\[\usability\stackrel{-}{\rightarrow}\flexibility \stackrel{-}{\leftarrow}\performance\]
\eq{0} says that the conjunction of competing upstream influence can
result in a steady value in a downstream variable; i.e.
\begin{eqnarray}
\usability\uparrow &\rightarrow& \andone\nonumber\\
\performance\downarrow &\rightarrow& \andone\nonumber\\
\andone&\rightarrow&\flexibility=\steady\label{eq:xpander}
\end{eqnarray}
where $\andone$ is an and-node especially created for this conjunction.
SP2 has no special knowledge of and-nodes so, conceivably, it can place some conjunction
pre-conditions {\em after} the post-condition; e.g.  \mbox{$\flexibility=\steady \in R_0$},
$\mbox{\usability$\uparrow$} \in R_1$ and $\mbox{\performance$\downarrow$} \in R_1$.
Coaxing is required to nudge the pre-conditions  back in time.

The rules of twinned topoi
also require that if we create the edges shown in
\eq{xpander},
then we must also create the following complementary rules:
\begin{eqnarray}
\usability\downarrow &\rightarrow& \bar{\andone}\nonumber\\
\performance\uparrow &\rightarrow& \bar{\andone}\nonumber\\
\bar{\andone}&\rightarrow&\bar{\flexibility=\steady}\label{eq:xpander1}
\end{eqnarray}
where ${\bar X}$ is an invented node representing ``all the other values
of $X$''.
$\bar{\andone}$ and $\bar{\flexibility=\steady}$ are  nonsense symbols required
to maintain the twinning condition, but should never appear in
counter-example. Coaxing is required to nudge these nonsense symbols till
{\em after} all the nodes required in counter-examples.
\\\hline
\end{tabular}
\end{center}}
\caption{Situations causing coaxing}\label{fig:ands}
\end{figure}


Whatever the motivation for coaxing, the   method is the same.  When generating $R$, it is possible
to identify nodes we want to {\em avoid} and nodes we {\em want} on the pathways to nodes
in counter-examples (see Step 2f3a and 2f3b within \fig{rapture}).
Adjusting the $\lambda$ of certain edges
will throw nodes back and forwards across $R$.
The adjustments must be made with care. Firstly, when changing $\lambda$, the twinning properties must be maintained. That is,
if we change $E(V_i,V_j)=\lambda_k + \delta$, then we must
also add $\delta$ to
$E(\bar{V_i},\bar{V_j})$.
Secondly, there is little point in coaxing nodes that are dependent on
other nodes that are being coaxed. Instead, given a set of nodes to be coaxed,
it is best to just coax the nodes that are most upstream;
i.e. dependent on no other node to be coaxed (see
Step 2h in \fig{rapture}).
Thirdly, there may exist a large number of edges between initial conditions and the node
to be coaxed. Ideally, we should only adjust weights on the least number of
{\em most influencial edge}
that leads to that node. The appendix of this paper discusses heuristics for selecting such
{\em most influencial edges}.







%\>2c.\>       \>  $N_0 \leftarrow \{\forall V_i \in R_0 | V_j \in after(V_i) \wedge V_j \in R_0 \wedge \bar{V_j} \in R_1\}$\\
%\>2d.\>     \>   $L_0 \leftarrow R_0 - N_0$\\



\subsection{Experiments with SP2}\label{sec:j}

\subsubsection{Experiments with Coaxing}

A major pre-experimental concern was that the nearly linear-time
processing of RAPTURE/SP2 could be followed by an indefinitely long coaxing
process. After much experimentation, we can report that we
have never seen this
worst-case behavior in practice.
For example, in the large
experimental studies  described in~\cite{powell99}, randomly generated
topoi graphs were probed for randomly selected properties.
In those experiments:
\bi
\item
The topoi size was fixed to 10,000
nodes;
\item
The topoi fanout was varied from 2 to 6 edges per node;
\item
The frequency of conjunctions
was varied from 5\% to 75\% of the total number of nodes;
\item
The results after 10 coaxes were
compared to the results after 100 coaxes.
\ei
In all cases, the coverage of the goals reached a plateau after at most five
iterations of SP2 plus coaxing. Also, the plateau reached after 10 coaxes
differed little from that reached after up to 100 coaxes.
Further, SP2 never used more than
1MB of memory  or one minute of runtime.
Our conclusion from
these experiments is that the need for heuristic coaxing does
not diminish the time and space efficiency of SP2.

\subsubsection{Comparisons with SPIN}

\fig{presults} shows a comparison of SPIN vs SP2 using properties
of the form of \eq{eventually} and the systems model of \fig{s89}.
Of the 40 properties which were analyzed by both SPIN and
SP2, SPIN was able to return a verification result in only
11 out of 40 cases ($27.5\%$) before running out of memory.  In
every case where SPIN did return a verification result,
SP2's result was in agreement.

\begin{figure}[!t]
\begin{center}
{\footnotesize
~\\
\begin{tabular}{|c|c|c|c|} \cline{2-4}
\multicolumn{1}{c|}{} &  SPIN & SP2    & Number of Cases \\ \cline{2-4}\cline{2-4}
\multicolumn{1}{c|}{} &  ??       & found  & 21 \\ \cline{2-4}
 \multicolumn{1}{c|}{} & ??       & not found & 8 \\ \cline{2-4}
\multicolumn{1}{c|}{} & found   & found           & 11 \\ \cline{2-4}
\multicolumn{1}{c|}{}  &  not found & not found         & 0 \\ \cline{2-4}
 \multicolumn{1}{c|}{}  &found   & not found         & 0 \\ \cline{2-4}
\multicolumn{1}{c|}{}  &  not found & found          & 0 \\ \hline
RAM used (max) & 100MB & $<1$MB & \multicolumn{1}{c}{}\\\cline{1-3}
\end{tabular}
}
\end{center}
\caption{Finding properties of \protect\fig{s89}
using  SPIN and SP2. ``??''
denotes that SPIN did not terminate in 100MB of RAM.}\label{fig:presults}
\end{figure}

Regarding computer resources, SP2 used less than 1\% of the RAM required
by SPIN.
Also, in the case of the  properties that were not found,
SP2 terminated in less than a second CPU time while
SPIN took much longer.

We mentioned earlier that one  pre-experimental concern
with informal topoi
is that they are so under-defined that we could use them to infer
any set of properties at all.
\fig{presults} shows that this is not always true.
In the case of 8 of the 40 properties, SP2 could not find them across
the large under-defined topoi of \fig{s89}.

%Because the memory
%requirements for SP2 does not vary over different
%properties to being verified, it also returned a definitive result
%for all 40 properties.  As a reasonablity check, it should be
%noted that SP2 did make a distinction between properties
%that did and did not exist, returning a result of \emph{false} for
%$20\%$ (8 of 40) of the properties and \emph{true} for the
%remaining $80\%$.  Therefore, according to these experiments with
%the chosen SPIN benchmark,  the effectiveness of SP2's
%ability to return valid results seems very high.


\section{Related Work}

\subsection{History}

Historically,
this work is based on Feldman \& Compton's study of the
validation of topoi~\cite{fecosm89b} (which they called
qualitative compartmental models).  Menzies concluded that this
inference procedure was NP-hard, and tried to
optimize that validation process. The resulting algorithm, HT4,
ran orders of magnitude faster than the
validation engine built by Feldman \& Compton. However, HT4 still suffered
from  exponential
runtimes~\cite{me96a,me96b,me95}.

That prior work also made the restrictive assumption
that topoi were processed as   propositional theories, i.e. each
variable receiving a single assignment. This assumption was made
after observing that   experts only ever used topoi to generate
 acyclic explanations.
Cyclic explanations introduce a temporal aspect to variable assignment;
i.e. if variables can't be assignment contradictory values, then
the explanation
\[a\uparrow \rightarrow b\uparrow \rightarrow a\downarrow\]
is only sensible  when $\{a\uparrow, a\downarrow\}$ occur
 at different times. Cyclic explanations
 are required when adding temporal simulation properties
 to qualitative compartmental models.
Assuming a certain
restriction on topoi edge types, Cohen, Menzies, Waugh and
Goss showed that the cost of checking temporal properties
of topoi-based simulation is a function of the number of
time-ticks in the query~\cite{me97m}.

At ICSE 2001, we presented
an earlier version of the SP2 algorithm that extended
the Cohen, Menzies, Waugh and
Goss to twinned topoi.
The ICSE 2001  version of SP2 only handled  two
time ticks but found that
an interesting  set of temporal
properties that could still
be useful explored, even in such a
restricted space~\cite{me00q}.
This paper removes the temporal restriction
of the ICSE 2001 paper since now we can
generate in near-linear
time consistent
temporal sequences of arbitrary length.

\subsection{Lightweight Formal Reasoning for Requirements}

We are hardly the first to explore formal methods for
requirements engineering. For example,
in the KAOS system~\cite{lam98}, analysts generate a
properties model by incrementally augmenting object-oriented scenario
diagrams with temporal logic statements.
Potentially, this research reduces the costs of testing requirements
 by
integrating the generation of the properties model into the rest of
the system development.  Our reading of the KAOS work is that
while the resulting model may be more formal, the level of skill
required to write the temporal logic can significantly increase the personnel
cost. Further, the extra time required for the augmentation could
increase the effect of the development brake.

In other work,
Schneider
et.al.~\cite{schnieder98} explored reducing the manual modeling
costs using
{\em lightweight formal methods}. In the lightweight approach, only partial
descriptions of the systems and properties models were constructed
using the SPIN formal analysis tool~\cite{holzmann97}.  Despite their
incomplete nature, Schneider et.al. found that such partial models
could still detect significant systems errors.  While exciting research,
this approach still
incurs the personnel cost since scarce expertise is required to drive
tools like SPIN.

\subsection{Representing Temporal Options}

In our research, we explore  the temporal properties of
a topi graph $G^t=<E^t,V^t>$.  In our approach,
graphs contain and-nodes and
or-nodes; i.e.
$V^t=V^T_{and}\cup V^t_{or}$.
$V^t_{or}$
contains single assignments to variables. and an or-node
can be reached
if any of its parents can be reached. $V^t_{and}$
models conjunctions and these
can be reached if all its parents can be reached. Edges are of two
types:  explicit $E^t_{yes}$ edges that
model valid connections between variables; and
implicit $E^t_{no}$ edges connecting   incompatiable nodes.
This paper has argued that when $E^t_{no}$ is binary (i.e. only between
$V^t_i$ and $\bar{V^t_i}$), then   twinning enables a near-liner time
generation of a consistent time series.

Two alternate representations for temporal properties
are a   {\em flow-graph} $G^f$ and a Clarke-style {\em state space} $G^s$.
These alternative methods are discussed below.

\subsubsection{Flowgraphs}\label{sec:fg}

In a flow graph $G^f=<V^f,E^f>$,
values at a node $V_i \in V^f$ are the result
of some transform performed during the traversal of an edge
upstream from that node. Our (non-twinned)
topoi graphs reduce to simple flowgraphs in the
case of
$V_{and}=\emptyset$ and $E_{no}=\emptyset$.
Methods for exploring the temporal properties of flowgraphs
have been extensively explored.
For example, Olender and Osterweil's CECIL
system~\cite{olender92} uses Tarjan's path solving
algorithms~\cite{tarjan81} to condense the flowgraph to a regular
expression summarizing the whole graph. This reduced space is then
explored for violations to system constraints.


For another example of flowgraph-based work,
Corbett~\cite{corbet94}
mapped finite state automoma to a flowgraph from
some start state to some final state where
the flow through some arc $i$
is represented by an integer variable $x_i$.
Assuming conversation of mass, flow equations
can be generated by assuming that  in-flows
to a state must equal the out-flows from that state.
As shown by Corbett,
such a system of flow equations can be solved via linear programming (LP)
methods.

RAPTURE/SP2 does not use Tarjan methods since we can
exploit certain special properties of twinned topoi (e.g. near-linear
time generation of time series).
Also, RAPATURE/SP2 does not use linear programming since our experience has been
that integer programming combined with conjunction constraints requires
heuristics for carefully relaxing some of the conjunctions. The more we explored the heuristics
we required, the closer we got to the coaxing methods described in this paper. That is,
if we elected
to explore LP, we still would require  much of our machinery.



\subsubsection{State-space Search}


In state space $G^s=<V^s,E^s>$,
each $V_i \in V^s$ contains
consistent value assignments to all program variables
and each $E_j \in E^s$ is a state change condoned by the program. Clarke's classic
model checker (MC) performs a linear-time search across a state
space  to find a set of states that lead to a violation of some
desired temporal property~\cite{clarke86}. If the MC search
terminates, then the search path is a counter-example showing how
that program can fail. While this search takes linear-time,
the size of state space is exponential on the number of assignments
per variable.  Elaborate techniques have been developed to
tame the state space explosion problem. A sample of these
techniques are described below.

{\em Abstraction or partial
ordering:} only use the part of the  space required for a
particular counter-example. Implementations exploiting this
technique can restrain how the space is
traversed~\cite{god97}, or constructed in the first
place~\cite{schnieder98}.

{\em Clustering:} divide the
systems model into  sub-systems which can be reasoned about
separately~\cite{clarke89a}.

{\em Meta-knowledge:} avoid
studying the entire space. Instead,  study only succinct
meta-knowledge of the space. One example used an
eigenvector analysis of the long-term properties of the
 systems model under study~\cite{ishida89}.


{\em Exploit symmetry:} Find properties in some part of
the systems model, then reuse those counter-examples if
ever those parts are found elsewhere in  the systems
model~\cite{clarke93}.

{\em Semantic minimization:} Replace
the space with some smaller, equivalent space. For example,
the BANDERA system~\cite{corbet00} reduces both the systems
modeling cost and the execution cost via automatically
extracting (slicing) the minimum portions of a JAVA
program's bytecodes which are relevant to particular
properties models.


While the above techniques have
all been useful in their  test domains,
they may not be universally applicable.
Certain optimizations  require
expensive pre-processing, such as \cite{ishida89}.
Also,
these methods may rely on
certain topological features of the system
being studied. Exploiting symmetry
is only useful if the system under study is highly
symmetric.
Clustering generally fails for tightly connected models.
Further, for requirements engineering,
systems like BANDERA are not suitable.
BANDERA only works on implemented
systems; that is, not until long
after the requirements phase has ended.

Hence, in the general case, only small models can be tested.
Further, these models must be precisely specified. In contrast, this
work describes methods for quickly finding properties in large models
that have been hastily sketched.

\section{Conclusion}

We need better formal testing for our requirements. Applying
formal methods can lead to an unacceptable brake on the development process.
Cost-effective formal methods have to reduce the cost and skill involved in
modeling systems and their properties. The cost
of properties modeling can be reduced via temporal logic patterns. However,
the execution cost of the resulting properties model may require expensive
rework of the properties generated from the patterns.

In the specific case of requirements that can be mapped into twinned topoi,
we have shown that the systems modeling cost is reduced (since the
topoi can be sketched quickly). For such twinned topoi,
we can  reduce the execution
cost for finding formal properties
to time that is nearly linear on the number of edges and nodes
in the topoi.

The combination of easy specification of properties and systems models implies
that the personnel cost of formal modeling is reduced. This
cost-reduction can only be achieved in domains where the systems model
can be expressed as topoi and the properties model refers more to
temporal occurrence properties than temporal ordering properties.
We have argued that requirements engineering is one such domain.


While on results to date are promising,
an open issue with this technique is its scalability to other models
with more complex
temporal properties. While our theoretical results encourage our belief
in the scalability of RAPTURE, such a belief must be tested.
Currently, we are working with our industrial partners to
explore a wider range of models and a wider range of temporal properties.




\section*{Acknowledgements}

This paper benefitted greatly
from the insightful comments of our  anonymous reviewers.

\bibliographystyle{IEEEbib}
\bibliography{../../refs}

\appendix

\section{Proof of Correctness for Algorithm SP2}

\subsection{Main Result}

Consider a path $\pi=(p_0,p_1,\ldots,p_m)$ in G-space compliant
graph $G\langle V,E\rangle$, originating at
$p_0\in V$ and terminating at $p_m\in V$. The length of $\pi$,
denoted $\wt{\pi}$, is the sum of the lengths of its edges,
$\sum_i^m \wt{(p_{i-1},p_i)}$. If $m=0$, the length of the path
shall be deemed to be zero. We will restrict our attention to
paths which are {\em simple}; that is, those in which no node
appears more than once.

Any path $\pi$ achieving the minimum length over all paths from
$p_0$ to $p_m$ shall be called a {\em shortest path} from $p_0$ to
$p_m$ in $G$; alternatively, the {\em distance} from $p_0$ to
$p_m$ is the length of any shortest path between them.  This
terminology can be extended to sets of nodes in the following
manner: if $S$ and $T$ are sets of nodes, then a path $\pi$ is a
shortest path from $S$ to $T$ if $p_0\in S$, $p_m\in T$, and $\pi$
has length no greater than any other path originating at a node in
$S$ and terminating at a node in $T$.  Shortest paths from sets to
a single node, and from a single node to a set, can be defined
analogously.

Path $\pi$ may or may not be consistent. If not, then there exists
a value $k$ between 1 and the number of edges of the path such
that the deletion of $k$ edges of $\pi$ yields $k+1$ consistent
subpaths.  If $k$ is the minimum such value, we say that the path
is {\em $k$-inconsistent}.  A consistent path will sometimes be
said to be {\em 0-inconsistent}. The set of $k$ edges deleted
shall be referred to as a {\em cut set} of the path, each edge of
which will be called a {\em cut edge}.

We will show in this section that:

\begin{theorem}
\label{T:main} Let $G\langle V,E\rangle$ be a G-space compliant
graph, and let $S$
be a consistent subset of $V$.  Let $V'$ be the set of all nodes
of $V$ reachable from some node of $S$ in $G$. Then there exists a
subgraph $G'\langle V',E'\rangle$ of $G$ such that:
\begin{enumerate}
\item
For every $v\in V'$, exactly one shortest path $\sigma(v)$ from
$S$ to $v$ in $G$ is also contained in $G'$.
\item
$G'$ is the union of the paths $\sigma(v)$ taken over all $v\in
V'$.
\item
Every path $\sigma(v)$ is either consistent or 1-inconsistent.
\item
There exists a set of cut edges resolving all 1-inconsistent paths
$\sigma(v)$, such that no shortest path $\sigma(v)$ contains more
than one cut edge.
\item
The cut edges define a partition of $V'$ into two disjoint node
sets $S'$ and $T'$ such that
\begin{itemize}
\item
$S\subseteq S'$,
\item
$S'$ and $T'$ are both consistent, and
\item
edge $(u,v)$ is a cut edge if and only if $u\in S'$ and $v\in T'$.
\end{itemize}
\end{enumerate}
\end{theorem}

A subgraph $G'$ satisfying the conditions of the theorem shall be
referred to as a {\em reachability\/} graph for $S$ in $G$.  We shall
also show that reachability graphs can be computed in $O(|V| + |E|\log
|V|)$ time in general, and in $O(|V| + |E|)$ time when all edge
lengths are identical.


\subsection{Paths}

Each cut edge $e=(p_i,p_{i+1})$ can be associated with the node
pairs it separates.  If $p_a$ and $p_b$ are nodes of the path such
that $a\leq i$ and $b\geq i+1$ and $p_a=\bar{p_b}$, then the
deletion of any edge of $\pi$ on the path from $p_a$ to $p_b$
(including $e$) ensures that no subpath of $\pi$ contains both
$p_a$ and $p_b$. The edges on the path from $p_a$ to $p_b$ form a
{\em cut interval} associated with $e$.  The intersection of all
cut intervals associated with edge $e$ will be called the {\em cut
intersection} $\mincutint{e}$ of $e$.

Since the number of cut intersections is $k$, and cannot be
reduced, no two cut intersections may overlap (otherwise, deletion
of an edge in the overlap resolves all cut intervals of both cut
intersections, contradicting the minimality of $k$).

\begin{observation}
\label{O:nooverlap} Let $e$ and $f$ be distinct cut edges drawn
from the same cut set of path $\pi$ in $G$. Then their associated
cut intersections $\mincutint{e}$ and $\mincutint{f}$ must share
no edges.
\end{observation}

\begin{lemma}
\label{L:pathcomplement} Let $x$ and $y$ be nodes of $G$ such that
$y$ is reachable from $x$. Then
\begin{itemize}
\item
$\bar{y}$ is reachable from $\bar{x}$, and
\item
the distance from $x$ to $y$ is equal to the distance from
$\bar{x}$ to $\bar{y}$.
\end{itemize}
\end{lemma}

\begin{PROOF}
Let $\pi=(p_0,p_1,\ldots,p_m)$ be a shortest path from $p_0=x$ to
$p_m=y$.  Since the edge $(p_i,p_{i+1})$ is in $G$ for all $0\leq
i < m$, the edge $(\bar{p_i},\bar{p_{i+1}})$ must be in $G$ as
well.  This implies that the path
$\bar{\pi}=(\bar{p_0},\bar{p_1},\ldots,\bar{p_m})$ exists from
$\bar{p_0}=\bar{x}$ to $\bar{p_m}=\bar{y}$.

The paths $\pi$ and $\bar{\pi}$ are both of length $\wt{\pi}$.
$\bar{\pi}$ must be a shortest path from $\bar{x}$ to $\bar{y}$;
otherwise, if a shorter path existed from $\bar{x}$ to $\bar{y}$,
a path of the same length would exist from $x$ to $y$,
contradicting the assumption that $\pi$ was shortest.
\end{PROOF}

\begin{lemma}
\label{L:consistent} If $t$ is reachable from $s$ in $G$, then any
shortest path from $s$ to $t$ is either consistent or
1-inconsistent.
\end{lemma}

\begin{PROOF}
By contradiction: let us assume that every path from $s$ to $t$ is
neither consistent nor 1-inconsistent.  Then consider a shortest
path $\pi=(p_0,p_1,\ldots,p_m)$ from $p_0=s$ to $p_m=t$ in $G$.
Let $\lambda_i$ be the length of the subpath
$\pi_i=(p_0,\ldots,p_i)$ of $\pi$, for all $0\leq i\leq m$.

Path $\pi$ must be $k$-inconsistent, for some $k\geq 2$. Let
$I_1=(p_a,p_b)$ and $I_2=(p_c,p_d)$ be two cut intersections
associated with the cut set of $\pi$.  By
Observation~\ref{O:nooverlap}, $I_1$ and $I_2$ must be disjoint,
and thus without loss of generality we may assume that $0\leq
a<b\leq c<d\leq m$.

Since the endpoints of cut intersections derive from cut
intervals, $p_b$ must be separated from its negation
$p_{b'}=\bar{p_b}$ by $I_1$.  This implies that $b'\leq a<b$.
Similarly, node $p_c$ must be separated from $p_{c'}=\bar{p_d}$ by
$I_2$, where $c<d\leq c'$.

Lemma~\ref{L:pathcomplement} implies that the distance from
$p_{b'}$ to $p_{c'}$ is the same as the distance from $p_b$ to
$p_c$ --- that is, $\lambda_c-\lambda_b$. Since the path from
$p_0$ to $p_{b'}$ is of length $\lambda_{b'}$, and the path from
$p_{c'}$ to $p_m$ is of length $\lambda_m-\lambda_{c'}$, there
exists a path from $p_0$ to $p_m$ of length
\[
  \lambda_{b'}+(\lambda_c-\lambda_b)+(\lambda_m-\lambda_{c'}) =
  \lambda_m-(\lambda_{c'}-\lambda_c)-(\lambda_b-\lambda_{b'}) < \lambda_m.
\]
This contradicts the assumption that the distance from $s$ to $t$
was $\lambda_m$.
\end{PROOF}

\subsection{Shortest Path Trees}

The proof of the main theorem is by construction. Let $S$ be a
consistent subset of $V$.  Consider now an augmentation of the
graph $G(V,E)$ by two artificial nodes $r$ and $\bar{r}$, and a
pair of artificial edges $(r,s)$ and $(\bar{r},\bar{s})$ for each
$s\in S$.  The length of each artificial edge is deemed to be
$\varepsilon>0$, an arbitrary positive constant. The resultant
graph --- call it $G^*\langle V^*,E^*\rangle$ --- remains a
G-space compliant graph.

\begin{figure}
{\small {\sf
\begin{tabbing}
\setuptabs \> {\bf function} \sptree: \\ \>    \>\> tree $Z$, node
sets $S', T'$, edge set $C$ \\ \>1.  \> {\bf for} each $v\in V$
{\bf do} \\ \>    \>\> $D[v]\leftarrow \infty$ \ \{all nodes are
{\em unvisited\/}\} \\ \>    \>\> $C[v]\leftarrow \emptyset$ \
\{no node is below a cut edge\} \\ \>    \> {\bf end for} \\ \>2.
\> $\PQ \leftarrow Z\leftarrow \emptyset$ \\ \>    \> \{let $r$ be
an artificial node of $G$\} \\ \>3.  \> $S' \leftarrow \{r\}$ \\
\>4.  \> $T'\leftarrow \emptyset$ \\ \>5.  \> {\bf for} each
initial node $s\in S$ {\bf do} \\ \>    \>\> $\PQ \leftarrow \PQ
\cup \{(0,(r,s))\}$ \\ \>    \> {\bf end for} \\ \>6.  \> {\bf
while} $\PQ$ is not empty {\bf do} \\ \>6a. \>\> $(d,(u,v))
\leftarrow \deletemin{\PQ}$ \\ \>6b. \>\> {\bf if} $D[v] \neq
\infty$ {\bf then} \\ \>    \>\>\> go to next iteration of the
{\bf while} loop \\ \>    \>\> {\bf end if} \\ \>6c. \>\> {\bf if}
$d=D[\bar{v}]$ and $\bar{v}\in T'$ {\bf then} \\ \>    \>\>\>
\{let $\bar{x}$ be the parent of $\bar{v}$ in $Z$\} \\ \>
\>\>\> {\bf if} $u\neq x$ {\bf then} \\ \>    \>\>\>\> go to next
iteration of the {\bf while} loop \\ \>    \>\>\> {\bf end if} \\
\>    \>\> {\bf end if} \\ \>6d. \>\> $D[v] \leftarrow d$ \ \{$v$
becomes {\em visited\/}\}\\ \>6e1.\>\> {\bf if} $u\in S'$ {\bf
and} $\bar{v}\not\in S'$ {\bf then} \\ \>    \>\>\> $S' \leftarrow
S' \cup \{v\}$ \\ \>6e2.\>\> {\bf else } \\ \>    \>\>\> $T'
\leftarrow T' \cup \{v\}$ \\ \>    \>\>\> {\bf if} $u\in S'$ {\bf
then} \\ \>    \>\>\>\> $C[v] \leftarrow (u,v)$ \\ \>    \>\>\>
{\bf else} \\ \>    \>\>\>\> $C[v] \leftarrow C[u]$ \\ \>
\>\>\> {\bf end if} \\ \>    \>\> {\bf end if} \\ \>6f. \>\> $Z
\leftarrow Z \cup \{(u,v)\}$ \\ \>6g. \>\> {\bf for} each $w$ such
that $(v,w)\in E$ {\bf do} \\ \>    \>\>\> $\PQ \leftarrow \PQ
\cup \{(D[v]+\wt{(v,w)},(v,w))\}$ \\ \>    \> {\bf end while} \\
\>7.  \> $S' \leftarrow S' \setminus \{r\}$ \\ \>8.  \> {\bf
return} $Z$, $S'$, $T'$, $C$ \\ \> {\bf end} \sptree
\end{tabbing}
}}
\caption{The SP2 algorithm}\label{fig:sp}
\end{figure}
Within the graph $G^*$, a variant of Dijkstra's
single-source shortest path algorithm \cite{dijk59} is used to
construct a tree of shortest paths from $r$ to all nodes reachable
from $r$; a pseudocode description of the algorithm is shown
in \fig{sp}.
Since the only neighbours of $r$ are the nodes of $S$,
the tree would also contain shortest paths to all nodes reachable
from $S$. The shortest path tree will later be shown to contain as
a subgraph a reachability graph of $S$.

As with Dijkstra's original algorithm, \sptree\ grows the shortest
path tree $Z$ from the root in greedy fashion, ensuring that the
current tree is a shortest path tree over the nodes it spans.  A
priority queue $\PQ$ is used to keep track of candidate edges for
inclusion. Each entry in the queue consists of:
\begin{itemize}
\item
an edge $(u,v)$, where $v$ is the candidate node and $u$ is a node
already in the tree;
\item
a distance $d$, the length of the shortest path from the root to
$v$ passing through $u$.
\end{itemize}

The entries in the queue are prioritized according to their values
of $d$, with small values being given the highest priority.
Although not strictly necessary for Theorem~\ref{T:main} to hold,
we will later require $\PQ$ to be {\em stable}, in that two
entries having the same distance $d$ should emerge from $\PQ$ in
the same order in which they were inserted.  Once a node $v$ is
inserted into the tree, its distance $D[v]$ from $r$ will have
been calculated and stored.


As nodes are added to the shortest path tree, they are assigned to
one of the two sets $S'$ and $T'$.  Whenever possible, the new
node (call it $v$) is added to set $S'$.  Only in those situations
where an assignment to $S'$ would result in an inconsistency (that
is, when $\bar{v}$ already belongs to $S'$), or in a path with
more than one cut edge, is an assignment of $v$ to $T'$
considered.  If the edge $(u,v)$ is inserted, with $u\in S'$ and
$v\in T'$, the transition from $S'$ to $T'$ is noted as the cut
edge $C[v]$ above $v$.  All subsequent descendents $w$ below $v$
will also inherit $C[w]=(u,v)$ as the cut edge above it.

In certain conditions, \sptree\ will choose to defer the insertion
of node $v$ altogether. It shall be shown in
Lemma~\ref{L:consistency} that whenever the algorithm defers the
insertion (Step 6c of \fig{sp}), a path of equal length will eventually be
found to $v$ passing through another node. Step 6c is the only
point of difference in how Dijkstra's algorithm and Algorithm
\sptree\ handle the insertion of nodes into the shortest path
tree.



If $\PQ$ is implemented using a heap, the worst-case time of the
algorithm is in $O(|V|+|E|\log |V|)$.  As is the case with the
many variants of Dijkstra's algorithm, data structures such as
two-dimensional lookup tables or Fibonacci heaps can also be used
to organize the insertion of nodes into the tree, with varying
time complexities (see \cite{cormen90} for details). However, it
is worth mentioning that some distributions of edge length (such
as when all edges have identical length) allow for the use of an
ordinary FIFO (First-In-First-Out) queue, resulting in an overall
worst-case time in $O(|E|)$.

\begin{lemma}
\label{L:consistency} Given an augmented G-space compliant graph
$G^*(V^*,E^*)$ and its artificial root $r$:
\begin{enumerate}
\item
Algorithm \sptree\ correctly creates a shortest path tree $Z$ of
all nodes reachable from $r$ in $G^*$.
\item
$S'$ and $T'$ are both consistent.
\end{enumerate}
\end{lemma}

%\begin{PROOF}
%Omitted due to space limitations.  For full details, we refer the
%reader to the technical report \cite{techrept}.
%
%The only difference in the construction of the shortest path tree
%between Algorithm \sptree\ and Dijkstra's algorithm is in
%the rejection of certain edges that is carried out in Step 6c.
%Provided that the nodes are added to the tree in non-decreasing
%order of their distances from $r$, the arguments that show the
%correctness of Dijksta's algorithm apply to \sptree\ as
%well. In the full proof, it is shown that in the construction of
%the shortest path tree, whenever an edge $(u,v)$ is
%rejected at Step 6c, node $v$ will be attached by means of another
%edge without changing its distance from $r$.
%\end{PROOF}

\begin{PROOF}
The only difference in the construction of the shortest path tree
between Algorithm \sptree\ and Dijkstra's algorithm is in the
rejection of certain edges that is carried out in Step 6c.
Provided that the nodes are added to the tree in non-decreasing
order of their distances from $r$, the arguments that show the
correctness of Dijksta's algorithm apply to \sptree\ as well. To
show that Algorithm \sptree\ constructs a shortest path tree, one
need only show that whenever an edge $(u,v)$ is rejected at Step
6c, node $v$ will be attached by means of another edge without
changing its distance from $r$.

The argument that $S'$ and $T'$ are consistent is by induction: we
assume that after each of the previous insertions of a node $w$
into $Z$,
\begin{itemize}
\item
$Z$ was a correct shortest path tree for the nodes it spanned,
\item
all nodes having distances to $r$ strictly less than $D[w]$ have
been included in the tree.
\item
the current sets $S'$ and $T'$ were both consistent.
\end{itemize}
Initially, the tree consists of the single node $r\in S'$, for
which the lemma holds.

Assume now that the edge $(u,v)$ is considered for inclusion. If
$v$ is already reachable using $Z$, the edge will be discarded at Step 6b.
Otherwise, the execution continues at Step 6c.

If $\bar{v}$ is not already in the tree, then $v$ is added to the
tree in Steps 6d through 6f. Node $v$ is assigned to the same node
set ($S'$ or $T'$) as its parent $u$.

If $\bar{v}$ is already in the tree, then it must have been
assigned to either $S'$ or $T'$. If $\bar{v}\in S'$ , then $v$
will be correctly placed in $T'$ at Step 6e2, regardless of the
status of $u$.  If $\bar{v}\in T'$, then $v$ cannot be placed in
$T'$ without violating the consistency of $T'$.  Step 6e appears
to allow this to happen in the case where $\bar{v}\in T'$ and
$u\in T'$, and $D[\bar{v}]<D[v]$. If $D[\bar{v}]=D[v]$ instead,
then the edge is rejected at Step 6c unless $u=x$
--- control never reaches Step 6e for the edge $(u,v)$ unless
$(\bar{u},\bar{v})$ is in $T$. However, we will now show that the
former situation never arises, and that rejecting the edge in the
latter situation is always safe, whenever $\bar{v}\in T'$.

If $u\in T'$ as well as $\bar{v}\in T'$, then there must be a cut
edge $(\bar{p_{j-1}},\bar{p_j})$ along the path
$\sigma(\bar{v})=(\bar{p_0},\bar{p_1},\ldots,\bar{p_m})$, where
$\bar{p_0}=r$ and $\bar{p_m}=\bar{v}$. For
$(\bar{p_{j-1}},\bar{p_j})$ to be a cut edge, $p_j$ must have been
added to the shortest path tree before $\bar{p_j}$.  The induction
hypothesis therefore implies that $D[p_j]\leq D[\bar{p_j}]$. By
the properties of G-space compliant graphs, there must be a path from
$p_j$ to $v$ of the same length as that from $\bar{p_j}$ to
$\bar{v}$.  This would imply the existence of a path from $r$ to
$v$ of length no more than $D[\bar{v}]$.

If $D[\bar{v}]<D[v]$, we have a contradiction, as we have found a
path from $r$ to $v$ of length strictly less than $D[v]$.  It
remains to be shown that if $D[\bar{v}]=D[v]$, any rejection of
$(u,v)$ that occurs in Step 6c is safe.  We shall do this by
showing that at least one opportunity exists for connecting $v$
without violating the consistency of $S'$ and $T'$.  In
particular, we shall show that $v$ can be attached to $p_{m-1}=x$.

Consider now the path $\sigma'(v)$ formed by $\sigma(p_{m-1})$
followed by the edge $(p_{m-1},v)$.
\[
\begin{array}{l}
  D[\bar{p_{m-1}}] + \wt{(\bar{p_{m-1}},\bar{v})} = D[\bar{v}] = D[v] \\
  \mbox{\ \ \ \ }\leq \wt{\sigma'(v)} = D[p_{m-1}] + \wt{(p_{m-1},v)}
\end{array}
\]
Lemma~\ref{L:pathcomplement} implies that
$\wt{(\bar{p_{m-1}},\bar{v})} = \wt{(p_{m-1},v)}$, and therefore
$D[\bar{p_{m-1}}] \leq D[p_{m-1}]$. However, we have already shown
that $D[\bar{p_j}] \geq D[p_j]$, from which it follows that
\[
\begin{array}{l}
D[\bar{p_j}] + \wt{(\bar{p_j},\bar{p_{j+1}},\ldots,\bar{p_{m-1}})}
\\
  \mbox{\ \ \ \ \ \ \ \ \ }\geq D[p_j] + \wt{(p_j,p_{j+1},\ldots,p_{m-1})}
\end{array}
\]
and $D[\bar{p_{m-1}}] \geq D[p_{m-1}]$. We must therefore have
$D[\bar{p_{m-1}}] = D[p_{m-1}]$.

Since $D[v] = D[\bar{v}] > D[\bar{p_{m-1}}] = D[p_{m-1}]$, the
length of the path from $r$ to $v$ through $p_{m-1}$ is equal to
$D[v]$, the shortest path length from $r$ to $v$.  Also, since
$D[p_{m-1}] < D[v]$, $p_{m-1}$ must already have been added to the
tree by the time $v$ is considered. In this regard, $p_{m-1}=x$ is
a suitable candidate for attaching $v$ to.

The node $\bar{p_{m-1}}$ must be in $T'$.  Otherwise, if
$\bar{p_{m-1}}$ were in $S'$, $\bar{p_m}=\bar{v}$ would have been
added to $S'$ at Step 6e1 (as $v$ had not yet been encountered
when $\bar{v}$ was added to the tree).  The induction hypothesis
then implies that $p_{m-1}\in S'$. When attempting to attach $v$
to the shortest path tree via node $p_{m-1}$, $v$ would be
assigned to set $S'$ --- consistent with the previous assignment
of $\bar{v}$ to $T'$. We conclude that $p_{m-1}=x$ is a suitable
candidate at which to attach $v$.
\end{PROOF}

Once the shortest path tree $Z$ of the augmented graph $G^*$ has
been computed, we can obtain a subgraph $G'(V',E')$ of the
original graph $G$ by simply deleting $r$ and $\bar{r}$ together
with the edges leading from them.

We are now in a position to complete the proof of the main
theorem, by showing that $G'$ satisfies its conditions.

\bigskip

\begin{mainproof}
\begin{enumerate}
\item
{\em For every $v\in V'$, exactly one shortest path $\sigma(v)$
from $S$ to $v$ in $G$ is also contained in $G'$.}

This follows from the properties of the shortest path tree $Z$,
and Lemma~\ref{L:consistency}.  Note that every path in $Z$ from
$r$ to another node must pass through a node of $S$.
\item
{\em $G'$ is the union of the paths $\sigma(v)$ taken over all
$v\in V'$.}

This also follows from the properties of the shortest path tree.
\item
{\em Every path $\sigma(v)$ is either consistent or
1-inconsistent.}

Follows from Lemma~\ref{L:consistent}.
\item
{\em There exists a set of cut edges resolving all 1-inconsistent
paths $\sigma(v)$, such that no shortest path $\sigma(v)$ contains
more than one cut edge.}

By the construction of $Z$, no node $v$ can be assigned to $S'$ if
its predecessor $u$ in $Z$ has been assigned to $T'$.  Since the root
$r$ is assigned to $S'$, there can therefore be only at most one
alternation from $S'$ to $T'$ along any path.  As $(u,v)$ can be a
cut edge only if $u\in S'$ and $v\in T'$, this condition is
satisfied by $G'$.
\item
{\em The cut edges define a partition of $V'$ into two disjoint
node sets $S'$ and $T'$ such that
\begin{itemize}
\item
$S\subseteq S'$,
\item
$S'$ and $T'$ are both consistent, and
\item
edge $(u,v)$ is a cut edge if and only if $u\in S'$ and $v\in T'$.
\end{itemize}
}

The consistency of $S'$ and $T'$ follows from
Lemma~\ref{L:consistency}. The set of cut edges satisfies the
condition by construction.

To see that $S\subseteq S'$, consider the relationship of the
nodes of $S$ with $r$ in $G^*$.  Root $r$ is connected to all
nodes of $S$, and only the nodes of $S$.  Each node of $S$ is
strictly closer to $r$ than any other node of
$V^*\setminus(S\cup\{r\})$. This implies that the nodes of $S$
will be considered for insertion in $Z$ before any of the other
nodes.

Let $s$ be a node of $S$.  Since $\bar{s}\not\in S$, $s$ must be
considered for insertion before $\bar{s}$.  Since $s$ is
considered by means of the edge $(r,s)$, and since $r\in S'$,
therefore $s$ is assigned to $S'$ at Step 6e1.  This shows that
$S\subset S'$ as required.
\end{enumerate}
\end{mainproof}

Provided that every pair of edges $e$ and $\bar{e}$ satisfies
$\wt{e}=\wt{\bar{e}}$, Algorithm \sptree\ is guaranteed to produce
a consistent partition of $V$ into $S'$ and $T'$.  However, the
actual sets $S'$ and $T'$ produced depend greatly on the initial
choice of edge weights.  In the next section, we will see how the
freedom of choice of edge weights can be exploited when attempting
to generate partitions satisfying desired criteria.

%========================================

\subsection{Weight Adjustment Strategies}

Consider an edge $(u,v)$ in $G$ leading to some and-node $v$. If
as a result of the application of \sptree\ on $G$ the node $u$ was
assigned to $T'$ and the node $v$ was assigned to $S'$, the and-node
$v$ would appear to depend on an input node $u$ which assumed
its value at a later time step.  One approach to resolving this
problem is to adjust some of the edge weights of $G$ in order to
encourage the reassignment of $u$ to $S'$ in a second application
of \sptree; alternatively, the reassignment of $v$ to $T'$ may be
attempted. Another situation in which the adjustment of weights
can be beneficial is when searching for a collection of paths in
which no node depends on a particular node $w$.

In this section, we shall discuss strategies for adjusting weights
which encourage the migration of nodes in a manner which resolves
these situations.  The general principle is that by greatly
increasing the weight of an edge $(u,v)$ in the shortest path tree
$Z$, any subsequent application of \sptree\ is likely to find a
different shortest path to $v$, and to nodes in the subtree of $v$
in $Z$.  Throughout the discussion, we shall assume that \sptree\
uses a stable implementation of the priority queue $\PQ$, and that
the insertion of entries into $\PQ$ at Steps 5 and 6g is performed
in some fixed order.

\subsection{Preserving Paths While Adjusting Weights}

Although the goal of weight adjustment is to produce a change in
an existing shortest path tree, it is important to be able to do
so without changing certain desirable paths or subtrees.  We begin
our investigation by giving conditions in which a shortest path
remains unchanged after weight adjustment and a subsequent
application of \sptree.

Let $Z_1$ be the shortest path tree produced by an application of
\sptree\ on $G^*$, and $Z_2$ be the shortest path tree produced by
an application of \sptree\ on the same graph after its edge
weights have been adjusted. For any edge $e\in E^*$, its weight
before and after the adjustment shall be denoted $\wta{1}{e}$ and
$\wta{2}{e}$, respectively. We will consider only adjustments for
which $\wta{2}{e}=\wta{2}{\bar{e}}$ for all $e,\bar{e}\in E^*$.

Some points regarding the notation: as before, the notation for
edge weights can be extended to lengths of paths in $G^*$. Also,
when referring to shortest paths within the graph $G^*$, we will
use the notation $G^*_1(V^*,E^*_1)$ to refer to the graph before
the weight adjustment, and $G^*_2(V^*,E^*_2)$ after the
adjustment. The partitions of $V^*$ produced for $G^*_1$ and
$G^*_2$ shall be denoted $\{S'_1,T'_1\}$ and $\{S'_2,T'_2\}$,
respectively.

\begin{lemma}
\label{L:stable} Let $A$ be a collection of edge pairs whose
weights are to be increased between two applications of \sptree\
(the weights of all other edges are left unchanged). Let
$\Pi_1=(\pi^1_1,\pi^1_2,\ldots,\pi^1_k)$ be the sequence of
shortest paths to $v$ in $G^*_1$, in the order in which they
emerge from $\PQ$ at Step~6a of the first application of \sptree.
Similarly, let $\Pi_2=(\pi^2_1,\pi^2_2,\ldots,\pi^2_k)$ be the
sequence of shortest paths to $v$ in $G^*_2$, in the order in
which they emerge from $\PQ$. Let $\pi\in\Pi_1$ be the shortest
path to $v$ in $Z_1$. If $\pi$ contains no edge of $A$, then
$\Pi_2$ is a subsequence of $\Pi_1$. Furthermore, path $\pi$ is
also in $\Pi_2$.
\end{lemma}

\begin{PROOF}
Let $\rho$ be any path from $r$ to $v$ in $G^*_1$. Since no edge
of $E^*$ has had its weight reduced,
$\wta{2}{\rho}\geq\wta{1}{\rho}$.  As $\pi$ contains no edges of
$A$, $\wta{1}{\rho}\geq\wta{1}{\pi}=\wta{2}{\pi}$, and therefore
$\pi$ must also be a shortest path in $G^*_2$.

Let us now assume that $\rho'$ is also a shortest path of $G^*_2$.
Path $\rho'$ must not contain any edge of $A$; otherwise, we would
have $\wta{1}{\rho} < \wta{2}{\rho} = \wta{2}{\pi} =
\wta{1}{\pi}$, contradicting the assumption that $\pi$ was a
shortest path in $G^*_1$. $\rho'$ must therefore be a shortest
path of $G^*_1$ as well. This implies that $\Pi_2\subseteq\Pi_1$,
and therefore that no path of $\Pi_2$ contains an edge of $A$.

Two assumptions have been made on the use and operation of the
priority queue in Algorithm \sptree: that entries are inserted
into $\PQ$ in some canonical order (at Step~6g), and that $\PQ$ is
stable. Considering only those nodes appearing on paths in
$\Pi_2$, one can show by an inductive argument that the relative
order in which the nodes are inserted into $\PQ$ is the same in
both applications of {\sptree}, as no weight adjustment has
been performed on any edges of these paths. The stability of $\PQ$
in turn implies that the order in which the nodes emerge from
$\PQ$ (at Step~6a) is the also the same in both applications, and
the result follows.
\end{PROOF}

The previous lemma shows that the choice of a stable data
structure for the priority queue can help to maintain continuity
in some parts of the shortest path tree after a weight adjustment.
The extent to which portions of the tree are left unchanged is
made clear by the following lemma.

\begin{lemma}
\label{L:adjust} Let $A$ be a collection of edge pairs whose
weights are to be increased between two applications of \sptree\
(the weights of all other edges are left unchanged). Let $\pi$ be
the shortest path to a node $v$ in the tree $Z_1$.
\begin{enumerate}
\item
If $\bar{v}$ is not reachable from $r$ and $\pi$ contains no edge
of $A$, then $\pi$ also belongs to the tree $Z_2$. Moreover, all
nodes of $\pi$ belonging to $S'_2$ and $T'_2$ are exactly those
belonging to $S'_1$ and $T'_1$, respectively.
\item
If $\bar{v}$ is reachable from $r$, let $\pi'$ be the shortest
path to $\bar{v}$ in $Z_1$.  If both $\pi$ and $\pi'$ contain no
edge of $A$, then $\pi$ and $\pi'$ belong to $Z_2$ as well.
Moreover, all nodes of $\pi$ and $\pi'$ belonging to $S'_2$ and
$T'_2$ are exactly those belonging to $S'_1$ and $T'_1$,
respectively.
\end{enumerate}
\end{lemma}

\begin{PROOF}
Note that it suffices to show that $\pi$ belongs to $Z_2$ when the
conditions of the lemma are satisfied, due to the symmetry of the
conditions on $\pi$ and $\pi'$ in the case when both exist.  Note
that by Lemma~\ref{L:stable}, $\pi$ must be considered for
inclusion in $Z_2$ by the second application of \sptree.

The proof is by induction on the sequence of insertions of nodes
into $Z_1$.  If $v\in S$, the lemma clearly holds; we therefore
may assume that $v\not\in S$, that $v$ and $\bar{v}$ satisfy one
of the two sets of conditions of the lemma, and that the lemma
holds for all nodes already in $Z$ that satisfy the conditions.

When the path $\pi$ is considered by the first application of
\sptree\ at Step 6c (via the edge $(u,v)$), we have three cases:
\begin{itemize}
\item $d>D[\bar{v}]$.

In this case, \sptree\ attaches $v$ to $Z_1$ using the first entry
to emerge from $\PQ$.  Since $\pi$ is considered first among all
paths to $v$ in the first application of \sptree,
Lemma~\ref{L:stable} implies that $\pi$ is the first path to $v$
considered in the second application as well.  The assumption that
no edges of $A$ lie on the shortest path to $\bar{v}$ imply that
$d>D[\bar{v}]$ when $\pi$ is considered in the second application,
and therefore $\pi$ is inserted into $Z_2$.

Since $d>D[\bar{v}]$, $\bar{v}$ must already have been added to
$Z_1$, and is therefore reachable.  Step 6d must have been
executed, since $d\neq D[\bar{v}]$.  The inductive hypothesis
implies that the paths to $u$ and $\bar{v}$ in $Z_2$ are identical
to those in $Z_1$, and that the assignment of nodes $u$ and
$\bar{v}$ in the second application of \sptree\ matches that of
the first application. Node $v$ is therefore assigned to $S'_2$ if
$v\in S'_1$, and to $T'_2$ if $v\in T'_1$.  The lemma follows for
this case.

\item $d<D[\bar{v}]$.

For reasons similar to those of the previous case, $\pi$ is
inserted into $Z_2$ in this case as well.

Since $d<D[\bar{v}]$, $\bar{v}$ must not yet have been added to
$Z_1$; it may or may not be reachable.  In any event, it cannot
yet have been assigned to $S'_1$.  Step 6d must have been
executed, since $d\neq D[\bar{v}]$.  The inductive hypothesis
implies that the path to $u$ in $Z_2$ is identical to that in
$Z_1$, and that the assignment of node $u$ in the second
application of \sptree\ matches that of the first application.
Since $\bar{v}\not\in S'_1$, $v$ is therefore assigned to the same
set as $u$.  Since $v$ is assigned to the same set as $u$ in the
second application of \sptree\ as well, $v$ is assigned to $S'_2$
if $v\in S'_1$, and to $T'_2$ if $v\in T'_1$.

\item $d=D[\bar{v}]$.

In this case, if $\bar{v}\not\in T'_1$ when the first path to $v$
emerges from $\PQ$, then this path is used to attach $v$ to $Z_1$
--- that is, $\pi$. As in the previous cases, Lemma~\ref{L:stable}
implies that $\pi$ is the first path to $v$ considered in the
second application as well.  The assumption that no edges of $A$
lie on the shortest path to $\bar{v}$ imply that at the moment
when $\pi$ is considered in the second application, $\bar{v}$ is
in $S'_2$ if it is in $S'_1$, and unassigned otherwise. In either
case, $\pi$ is inserted into $Z_2$. Since $u$ satisfies the
conditions of the lemma, the inductive hypothesis implies that
$u\in S'_2$ if $u\in S'_1$, and $u\in T'_2$ if $u\in T'_1$.  Steps
6d to 6f then ensure that $v$ is assigned to the same sets as $u$
in both applications of \sptree.

If $\bar{v}\in T'_1$ when the first path to $v$ emerges from
$\PQ$, then the correctness of \sptree\ implies that when $v$ is
attached via $\pi$, that $(u,v)$ and $(\bar{u},\bar{v})$ both
appear in $Z_1$.  Steps 6d to 6f ensure that $u$ and $v$ are
assigned to $S'_1$, and $\bar{u}$ and $\bar{v}$ are assigned to
$T'_1$. Nodes $u$, $\bar{u}$, and $\bar{v}$ all satisfy the
conditions of the lemma, and therefore by the inductive hypothesis
we have $u\in S'_1$, $\bar{u}\in T'_2$, and $\bar{v}\in T'_2$.  As
a result, the only way $v$ can be attached to $Z_2$ is via $u$,
assigned to $S'_1$. This completes the proof of this case, and the
lemma.
\end{itemize}
\vspace{-0.7cm}
\end{PROOF}

\subsection{Heuristics for Node Migration}

Lemma~\ref{L:adjust} provides us an important guarantee regarding
the limitations of the effect of edge weight adjustments upon the
structure of the shortest path tree.  It tells us that the fewer
the edges whose weights are adjusted, the greater the portion of
the tree whose structure is undisturbed.  This is a particularly
important consideration when attempting to improve upon a shortest
path tree which already has many desirable characteristics.

Consider the effect of adjusting the weights $\wt{e}$ and $\wt{e}$
of edges $e=(u,v)$ and $\bar{e}=(\bar{u},\bar{v})$ by adding to
them the amount $\bigvalue$.  If $\bigvalue$ is chosen to be
larger than the sum of the original edge weights of $G$, on the
next application of \sptree, $e$ will not be inserted into the
shortest path tree unless no other path of unadjusted edges to $v$
exists. The following three heuristics all adjust the weights of
only a single pair of edges, by a constant amount $\bigvalue$.

\begin{enumerate}
\item {\em Given $u\in T'_1$ and $v\in S'_1$, we want $u\in S'_2$.}

This situation can arise when $v$ corresponds to an and-node in
$G$. Interpreting $S'_1$ and $T'_1$ as temporal divisions in which
$S'_1$ events occur before $T'_1$ events, the and-node $v$ from
the earlier division would appear to depend on another event
occurring at the later division. Moving $u$ to $S'_2$ in a second
application of \sptree\ would resolve this anomaly.

If the shortest path length to $\bar{u}$ is no more than that of
$u$, and if the parent $w_{\bar{u}}$ of $\bar{u}$ in $Z_1$ is not
paired with that of $u$, $\bar{u}$ can be coaxed away from $S_1$
and into $T_2$ by increasing the distance from $\bar{u}$ to
$w_{\bar{u}}$. This adjustment of the weights of
$(w_{\bar{u}},\bar{u})$ and its paired edge
$(\bar{w_{\bar{u}}},u)$ does not affect the distance from $r$ to
$u$, since $\bar{w_{\bar{u}}}$ is not the parent of $u$ in $Z_1$.

On the other hand, if $\bar{u}$ is unreachable from $r$, if the
shortest path length to $\bar{u}$ is already greater than that of
$u$, or if the parent of $\bar{u}$ in $Z_1$ is paired with that of
$u$, the weight adjustment described above will be ineffective.
In the first two cases, $u$ is attached to $Z_1$ before $\bar{u}$,
yet nevertheless was assigned to $T'_1$.  Increasing the distance
to $\bar{u}$ will not alter this assignment of $u$.  In the third
case, increasing the distance to $\bar{u}$ in this way increases
the distance to $u$ by the same amount.  Instead, one way in which
$u$ can be encouraged to join $S'_2$ is to increase the weight of
the unique cut edge $(a,b)$ in the shortest path leading to $u$ in
$Z_1$.  By adding $\bigvalue$ to the weight of $(a,b)$, the second
application of \sptree\ is guaranteed to find a different,
unadjusted path to $u$ if such a path exists.  This path, if
shorter than that to $\bar{u}$, may allow $u$ to be assigned to
$S'_2$ instead of $\bar{u}$. Note that the weight of
$(\bar{a},\bar{b})$ must be adjusted by the same amount.

\begin{heuristic}
Let $(u,v)$ be an edge of $E^*$ such that $u\in T'_1$ and $v\in
S'_1$. Let $(a,b)$ be the unique cut edge on the path to $u$ in
$Z_1$, and let $w_u$ and $w_{\bar{u}}$ be the parents of $u$ and
$\bar{u}$ in $Z_1$, respectively (let $w_{\bar{u}}=\emptyset$ if
$\bar{u}$ is not reachable from $r$). To encourage $u$ to be
assigned to $S'_2$ in the next application of \sptree, then:
\begin{itemize}
\item
If $D[\bar{u}]\leq D[u]$ and $\bar{w_u}\neq w_{\bar{u}}$ after the
execution of \sptree, adjust weights
$\wta{2}{(w_{\bar{u}},\bar{u})}\leftarrow\wta{2}{(\bar{w_{\bar{u}}},u)}
\leftarrow\wta{1}{(w_{\bar{u}},\bar{u})}+\bigvalue$.
\item
If $D[\bar{u}]>D[u]$ or $\bar{w_u}=w_{\bar{u}}$ after the
execution of \sptree, adjust weights
$\wta{2}{(\bar{a},\bar{b})}\leftarrow\wta{2}{(a,b)}
\leftarrow\wta{1}{(a,b)}+\bigvalue$.
\end{itemize}
\end{heuristic}

\item {\em Given $u\in T'_1$ and $v\in S'_1$, we want $v\in T'_2$.}

Another way of resolving the anomaly mentioned above is to coax
$v$ into entering $T'_2$.

If the shortest path length to $\bar{v}$ is no less than that of
$v$ (including the case where $\bar{v}$ is unreachable from $r$),
and if the parent $w_v$ of $v$ in $Z_1$ is not paired with that of
$\bar{v}$, $v$ can be coaxed away from $S_1$ and into $T_2$ by
increasing the distance from $w_v$ to $v$. This adjustment of the
weights of $(w_v,v)$ and its paired edge $(\bar{w_v},\bar{v})$
does not affect the distance from $r$ to $\bar{v}$, since
$\bar{w_v}$ is not the parent of $\bar{v}$ in $Z_1$.

On the other hand, if the shortest path length to $\bar{v}$ is
already less than that of $v$, or if the parent of $\bar{v}$ in
$Z_1$ is paired with that of $v$, the weight adjustment described
above will be ineffective.  In the former case, $\bar{v}$ is
attached to $Z_1$ before $v$, yet nevertheless was assigned to
$T'_1$.  Increasing the distance to $v$ will not alter this
assignment of $v$.  In the latter case, increasing the distance to
$v$ in this way increases the distance to $\bar{v}$ by the same
amount.  Instead, one way in which $v$ can be encouraged to join
$T'_2$ is to increase the weight of the unique cut edge
$(\bar{a},\bar{b})$ in the shortest path leading to $\bar{v}$ in
$Z_1$.  By adding $\bigvalue$ to the weight of
$(\bar{a},\bar{b})$, the second application of \sptree\ is
guaranteed to find a different, unadjusted path to $\bar{v}$ if
such a path exists.  This path, if shorter than that to $v$, may
allow $\bar{v}$ to be assigned to $S'_2$ instead of $v$. Note that
the weight of $(a,b)$ must be adjusted by the same amount.

\begin{heuristic}
Let $(u,v)$ be an edge of $E^*$ such that $u\in T'_1$ and $v\in
S'_1$. Let $(\bar{a},\bar{b})$ be the unique cut edge on the path
to $\bar{v}$ in $Z_1$, and let $w_v$ and $w_{\bar{v}}$ be the
parents of $v$ and $\bar{v}$ in $Z_1$, respectively (let
$w_{\bar{v}}=\emptyset$ if $\bar{v}$ is not reachable from $r$).
To encourage $v$ to be assigned to $T'_2$ in the next application
of \sptree, then:
\begin{itemize}
\item
If $D[\bar{v}]\geq D[v]$ and $\bar{w_v}\neq w_{\bar{v}}$ after the
execution of \sptree, adjust weights
$\wta{2}{(w_v,v)}\leftarrow\wta{2}{(\bar{w_v},\bar{v})}
\leftarrow\wta{1}{(w_v,v)}+\bigvalue$.
\item
If $D[\bar{v}]<D[v]$ or $\bar{w_v}=w_{\bar{v}}$ after the
execution of \sptree, adjust weights
$\wta{2}{(\bar{a},\bar{b})}\leftarrow\wta{2}{(a,b)}
\leftarrow\wta{1}{(a,b)}+\bigvalue$.
\end{itemize}
\end{heuristic}


\item {\em Given $(u,v)\in Z_1$, we want $(u,v)\not\in Z_2$.}

This situation can arise when $\bar{u}$ corresponds to an and-node
in $G$. Although $\bar{u}$ may have a valid interpretation within
the graph, the paired node $u$ generally will not.  If $u$
were a leaf of the shortest path tree $Z_2$, no other node of
$Z_2$ would depend from $u$, relieving the need to interpret $u$.
The action to be taken here is
straightforward: by increasing the weight of $(u,v)$ and its
paired edge $(\bar{u},\bar{v})$, $v$ will be connected to $Z_2$
through some unadjusted path whenever such a path exists.
Increasing the weights of all children of $u$ in $Z_1$ would
strongly encourage $u$ to become a leaf of $Z_2$.

\begin{heuristic}
Let $(u,v)$ be an edge of $E^*$. To discourage $v$ from being the
child of $u$ in $T'_2$ after the next application of \sptree, then
adjust weights $\wta{2}{(\bar{u},\bar{v})}\leftarrow\wta{2}{(u,v)}
\leftarrow\wta{1}{(u,v)}+\bigvalue$.
\end{heuristic}
\end{enumerate}

Each of the heuristics outlined above adjusts the edge weights of
a single pair (call it $(x,y)$ and $(\bar{x},\bar{y}))$.
Lemma~\ref{L:adjust} implies that this reweighting can affect only
the portion of $Z_1$ below $y$ and $\bar{y}$.  In particular, some
of the nodes in these portions of $Z_1$ may find themselves
migrating from $T'_1$ to $S'_2$ or from $S'_1$ to $T'_2$. Although
this migration may resolve anomalies of the kind discussed here,
one should be aware that it has the potential to create them as
well. For this reason, it is best to minimize the number of edge
weight adjustments.
\clearpage
\renewcommand\thepage{{\roman{page}}}
\setcounter{page}{1}
\section*{Changes since the ICSE 2001 Version}

Here, we describe how changed this paper in light of the comments of the ICSE 2001 reviewers.

The  major changes are:
\bi
\item This paper is twice the length of the ICSE 2001 version and contains a formal proof of
correctness for our algorithm
\item The ICSE 2001 version of this work had a "two time tick" restriction on the temporal queries.
This paper removes that restriction.
\item
The ICSE 2001's claim to generality was based on an analysis of coverage of the
Dwyer corpus of temporal logic patterns.
The removal of the "two time tick" restriction makes that analysis redundant.  Hence, it was removed.
\ei

This paper incorporates many of the changes proposed by the ICSE 2001 reviewers: see below.

\newcommand{\ro}{{\em Reviewer 1:~}}
\newcommand{\rt}{{\em Reviewer 2:~}}
\newcommand{\rth}{{\em Reviewer 3:~}}
\newcommand{\rf}{{\em Reviewer 4:~}}
\be
\item
\ro  made many positive comments and made some editing suggestions- which we applied.
\item
\rt ``How much of a system's requirements can be
expressed in topoi diagrams (clearly some of the requirements can
be)?''.

This is addressed in the introduction when we say:
\begin{quote}
Specifically,  the systems
model must be expressed as topoi diagrams. Topoi are not
very expressive, and exclude statements such as first-order
assertions, iterations, sub-routine calls, and assignments.
Due to these language limitations, our approach is not
suited to domains that need the excluded statements, such
as complex protocols seen in  concurrent processes.

These restrictions are not fatal to the modelling process,
at least at the requirements stage. We will show via
example that topoi diagrams are sufficient to represent a
wide range of diagrams seen in certain approaches to
requirements engineering and recording design rationales.
Hence, when we say that this approach is practical and
useful, we really mean {\em practical and useful for early
life cycle requirements discussions only}.
\end{quote}

\item
\rt ``What is the connection of this work to flow graph
analysis?''. This connection was unknown to us in the earlier version and is discussed in  \tion{fg}.

\item
\rth This  reviewer was concerned that the presentation of our techniques
was being over-sold, that we were claiming more than we should regarding the
power of our tools. We agree- the ICSE 2001
paper confused logical `proofs' with
`counter examples'. This draft removes that confusion.
\item
\rth The ICSE 2001 version argued for the generality of this technique
via a review of the Dwyer corpus of temporal logic patterns.
Reviewer 3 doubted this analysis but this
issue is now redundant.
The ICSE 2001's claim to generality was based on an analysis of coverage of the
Dwyer corpus of temporal logic patterns.
The removal of the `two time tick' restriction makes that analysis redundant.  Hence, it was removed.
\item
\rth ``Why would subroutine calls be of concern at the requirements stage?''
They should not- we only mention these to distinguish our topoi approach from
systems like SPIN which can handle sub-routines.
\item
\rth ``How is `rigorous requirements engineering'
related to 'formally
checking a system by formal first-order query'?''.  By rigorous RE, we mean that formal testing
is applied early in the lifecycle.
As to `formal first-order queries':
\bi
\item
Various researchers have
explored lightweight formal methods using temporal logic model checkers.
\item
Cost-benefit
studies of these approaches include Lowry et.al.~\cite{lowrey98} who argue that
a single test is like a ground propositional query  while a formal query is like
a first-order sentence with non-ground variables that can range over a larger
set of values.
\item
Hence, a single formal query can substitute for many tests and can increase
our rigor in RE
\ei
\item \rth ``Why is the freezing of requirements (applying the development brake)
a
result of costs? '' A full formal analysis is expensive and,
once completed, may be too costly to repeat. That is, any changes in the requirements
found {\em after} the formal analysis may be ignored (since to do otherwise can be too expensive).
\item
\rth
``these terms seem interchangeable:
testing requirements, formal requirements analysis,
rigorous
requirements engineering'' Yes. we have removed the repeated terms.


\item
\rth
``A reference to topoi diagrams would be useful.''.
The reference~\cite{dieng95} has been added to page one.

\item
\rth ``It sounds as if the topoi diagrams are used for both the properties
and
the systems model; and then later the two models seem to be mixed
up,
used interchangeably.'' Yes- the text now distinguishes between compiling
a system description into a topoi and compiling a temporal logic
properties model into set memberships of parts of a time series
generated from that topoi, see \fig{ce}.

\item
\rth ``is a query a property in the properties model''. No- a
query
is a test for the entire properties model\footnote{mike- and that means
we have to test for disjunctions, which means MULTIPLE calls to
our process}.

\item
\rth ``The claims about topoi graphs being quickly generated and systems
modelling costs being low is only justified based on the authors'
experience. It would at least be help to state their experience
doing
what, especially since this claim underlies the entire methods'
effectiveness.'' Relevant references (\cite{dieng95}
and Menzies~\cite{me95}) are offered in the introduction.

\item
\rth ``Where in the topoi
Figures are the strengths which are continuous numbers.''. In
all our topoi examples, the strengths default to 1 for each
edge. The repeated assignment of 1 to each edge is not shown since
this would confuse the reader.

\item
\rth
``\fig{s89} is totally unreadable''. Yes- and that is our point.
Real world topoi such as \fig{s89}
soon become too complicated to read manually. Automatic tools
are required to implement this process.

\item
\rth
``The authors had a pre-experimental concern that informal topoi are
so
under-defined that anything could be inferred; they state that this
turns out not to always be the case therefore implying that
sometimes
it is the case. How good is this?'' The experience of \cite{me95}
is that, often, it is good enough. A similar belief that they
are good enough (i.e.
under-defined models can still be used to make
interesting conclusions)
is the base premise of the qualitative reasoning
community~\cite{iwasaki89,simon86,iwasaki88,kuipers86}.
A similar endorsement of under-defined theories is offered by
researchers discussing  the merits of lightweight notations
for testing software  (e.g.~\cite[chp 18]{leven95}
\cite{schnieder98}).

\item
\rth
``Are vertices equivalent to variables since they can be assigned
values?'' No- if a variable can be assigned N distinct values, then that would
imply N vertices

\item
\rth
``Who does the coaxing by applying edge weights to a topoi? This
seems
extremely burdensome.'' The appendix and the source code of RAPTURE (in \fig{rapture})
makes it clear that it is an automatic process.


\item
\rth
``It's not clear what the plateau reached after 10 coaxes barely
changed
in up to 100 coaxes means; isn't a plateau usually set and
processing
stops when it is reached?'' That is the strategy that should be applied
at runtime. However, to test if coaxing is missing anything, what we did here
is   to compare the goals found after a small number of coaxes to the
the goals found after a very very large number of coaxes.

\item
\rth
``Is it possible to tell in advance whether requirements can be mapped
into symmetric topoi?'' Yes- if the model can be abstracted to a propositional
theory (i.e. two assignments per variable).


\item
\rf ``Most of the technical meat of the paper is glossed
over.
The SP2 algorithm is summarized, but relatively easy to follow. The details are
apparently
presented in a technical report and another seemingly unpublished
report,
rather than presented in this paper.'' The SP2 algorithm is presented in full
in this paper.


\item
\rf
``One has to question whether a topoi whose analysis needs to be
coaxed
is cost effective. Automated analysis works best on models that
are difficult to reason about manually (e.g., model checking a
concurrent
models, where it is difficult for a human to reason about the global
state of the system). Topoi diagrams are a global model of simple
relations. While I can see the benefit of having an automated
analyzer
push a flow through the graph, this benefit deteriorates if the
human
analyzer has to play with assigning weights to edges in order to
force
the analyzer to consider feasible paths. Wouldn't it be easier,
more
cost effective, and no less error-prone to have the human analyzer
inspect the Topoi?'' Two comments here:
\bi
\item
Coaxing is an automatic process- this was NOT clear in the ICSE2001 paper but is here
\item
As to manually inspecting the topoi, this reviewer is invited to inspect \fig{s89} to
identify the goals and outputs NOT supported by this theory. Good luck!
\ei

\item
\rf
``The paper should reference the work of Jim Corbett, who models
requirements as flow graphs (not unlike Topoi graphs), but
transforms
the graph and the property into a set of equations and inequalities
and
looks for an integer solution (if there is none, then the system
never
violates the property).'' Done- see \tion{fg}.

\ee



\end{document}
