summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2006-07-23 23:48:50 +0000
committerKarl Berry <karl@freefriends.org>2006-07-23 23:48:50 +0000
commit68b95e72d5ea1fe8fa89e11bc896a33ce8c42cc5 (patch)
treeb7166d594b0610a6a6b8ac9fc3e7d05119aa8892 /Master/texmf-dist/doc
parent40017fc23f5df1b885094287255acd2138fe727e (diff)
new (latex) package lsc (23feb06)
git-svn-id: svn://tug.org/texlive/trunk@1908 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc')
-rw-r--r--Master/texmf-dist/doc/latex/lsc/README13
-rw-r--r--Master/texmf-dist/doc/latex/lsc/lsc.pdfbin0 -> 196507 bytes
-rw-r--r--Master/texmf-dist/doc/latex/lsc/lsc.tex3956
3 files changed, 3969 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/lsc/README b/Master/texmf-dist/doc/latex/lsc/README
new file mode 100644
index 00000000000..ae5f6fad9c0
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/README
@@ -0,0 +1,13 @@
+
+This package is similar to the 'msc' package in that it provides
+macros for typesetting a variant of sequence diagrams, in this
+case the Live Sequence Charts of Damm and Harel.
+
+It supports the full LSC language of the original LSC paper, the
+Klose-extensions for formal verification and some of the Harel-
+extensions for the Play-In/Play-Out approach (cf. the manual).
+
+This material is subject to the LaTeX Project Public License. See
+http://www.ctan.org/tex-archive/help/Catalogue/licenses.lppl.html
+for the details of that license.
+
diff --git a/Master/texmf-dist/doc/latex/lsc/lsc.pdf b/Master/texmf-dist/doc/latex/lsc/lsc.pdf
new file mode 100644
index 00000000000..a1643042fdb
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/lsc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/lsc/lsc.tex b/Master/texmf-dist/doc/latex/lsc/lsc.tex
new file mode 100644
index 00000000000..d4c9d8837b1
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/lsc.tex
@@ -0,0 +1,3956 @@
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+% $Id: lsc.tex,v 1.17 2006/02/23 12:57:15 berndw Exp $
+%
+% User's manual for lsc.sty.
+%
+% Author: Bernd Westphal <westphal@informatik.uni-oldenburg.de>
+%
+% Copyright (c) 2005-2006 Bernd Westphal. All rights reserved.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+%
+% This work may be distributed and/or modified under the conditions of
+% the LaTeX Project Public License, either version 1.3 of this license
+% or (at your option) any later version.
+% The latest version of this license is in
+% http://www.latex-project.org/lppl.txt
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is the copyright holder.
+%
+% This work consists of the files README, lsc.sty, lsc.tex, lsc.bib.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+\documentclass{article}
+
+\usepackage{makeidx}
+\usepackage{lsc}
+
+\title{\texttt{lsc.sty} -- Typesetting Live Sequence Charts}
+\author{Bernd Westphal}
+
+\newsavebox{\bsbox}%<@<
+\newcommand{\bs}{\usebox{\bsbox}}
+\newsavebox{\lcbbox}
+\newcommand{\lcb}{\usebox{\lcbbox}}
+\newsavebox{\rcbbox}
+\newcommand{\rcb}{\usebox{\rcbbox}}
+\newsavebox{\lbbox}
+\newcommand{\lb}{\usebox{\lbbox}}
+\newsavebox{\rbbox}
+\newcommand{\rb}{\usebox{\rbbox}}
+%
+\newcommand{\AT}{@}
+%
+\newcommand{\env}[1]{\texttt{#1}}
+\newcommand{\cmd}[1]{\bs\texttt{#1}}
+\newcommand{\con}[1]{%
+ \ifmmode{\texttt{#1}}\else{`\texttt{#1}'}\fi}
+\newcommand{\sty}[1]{\texttt{#1.sty}}
+%
+\newcommand{\lscsty}{\sty{lsc}}
+%
+%
+\newcommand{\mbegin}[1]{\bs\texttt{begin}\lcb\texttt{#1}\rcb}
+\newcommand{\mend}[1]{\bs\texttt{end}\lcb\texttt{#1}\rcb}
+%
+\newcommand{\mlscActor}{\cmd{lscActor}}
+\newcommand{\mlscAct}{\cmd{lscAct}}
+\newcommand{\mlscAsynRcv}{\cmd{lscAsynRcv}}
+\newcommand{\mlscAsynSnd}{\cmd{lscAsynSnd}}
+\newcommand{\mlscAsyn}{\cmd{lscAsyn}}
+\newcommand{\mlscAtom}{\cmd{lscAtom}}
+\newcommand{\mlscBalloon}{\cmd{lscBalloon}}
+\newcommand{\mlscClock}{\cmd{lscClock}}
+\newcommand{\mlscCond}{\cmd{lscCond}}
+\newcommand{\mlscCreate}{\cmd{lscCreate}}
+\newcommand{\mlscCut}{\cmd{lscCut}}
+\newcommand{\mlscEnvLine}{\cmd{lscEnvLine}}
+\newcommand{\mlscEnv}{\cmd{lscEnv}}
+\newcommand{\mlscFooterHeightFactor}{\cmd{lscFooterHeightFactor}}
+\newcommand{\mlscInstRcv}{\cmd{lscInstRcv}}
+\newcommand{\mlscInstSnd}{\cmd{lscInstSnd}}
+\newcommand{\mlscInst}{\cmd{lscInst}}
+\newcommand{\mlscKill}{\cmd{lscKill}}
+\newcommand{\mlscLabelAtomAt}{\cmd{lscLabelAtomAt}}
+\newcommand{\mlscLabelAtom}{\cmd{lscLabelAtom}}
+\newcommand{\mlscLine}{\cmd{lscLine}}
+\newcommand{\mlscLocationHeight}{\cmd{lscLocationHeight}}
+\newcommand{\mlscLocationWidth}{\cmd{lscLocationWidth}}
+\newcommand{\mlscLocinvBegin}{\cmd{lscLocinvBegin}}
+\newcommand{\mlscLocinvEnd}{\cmd{lscLocinvEnd}}
+\newcommand{\mlscLocinvOffset}{\cmd{lscLocinvOffset}}
+\newcommand{\mlscLocinvStart}{\cmd{lscLocinvStart}}
+\newcommand{\mlscLocinv}{\cmd{lscLocinv}}
+\newcommand{\mlscNamedCut}{\cmd{lscNamedCut}}
+\newcommand{\mlscPut}{\cmd{lscPut}}
+\newcommand{\mlscSetCutColour}{\cmd{lscSetCutColour}}
+\newcommand{\mlscSetCutLinestyle}{\cmd{lscSetCutLinestyle}}
+\newcommand{\mlscSetCutWidth}{\cmd{lscSetCutWidth}}
+\newcommand{\mlscSetNamedCutColour}{\cmd{lscSetNamedCutColour}}
+\newcommand{\mlscSetNamedCutLinestyle}{\cmd{lscSetNamedCutLinestyle}}
+\newcommand{\mlscSetNamedCutWidth}{\cmd{lscSetNamedCutWidth}}
+\newcommand{\mlscTimeout}{\cmd{lscTimeout}}
+\newcommand{\mlscTimerReset}{\cmd{lscTimerReset}}
+\newcommand{\mlscTimerSet}{\cmd{lscTimerSet}}
+\newcommand{\mlscWidecondOff}{\cmd{lscWidecondOff}}
+\newcommand{\mlscWidecondOn}{\cmd{lscWidecondOn}}
+\newcommand{\mlscWidecond}{\cmd{lscWidecond}}
+%
+\newcommand{\mFullLsc}{\env{FullLsc}}
+\newcommand{\mLsc}{\env{Lsc}}
+\newcommand{\mcoregion}{\env{coregion}}
+\newcommand{\mlsccreateinst}{\env{lsccreateinst}}
+\newcommand{\mlscinst}{\env{lscinst}}
+\newcommand{\msimregion}{\env{simregion}}
+%
+\newcommand{\mhot}{\con{hot}}%
+\newcommand{\mcold}{\con{cold}}%
+%
+\newcommand{\ml}{\con{l}}%
+\newcommand{\mr}{\con{r}}%
+%
+\newcommand{\mra}{\con{ra}}%
+\newcommand{\mrb}{\con{rb}}%
+\newcommand{\mla}{\con{la}}%
+\newcommand{\mlb}{\con{lb}}%
+%
+\newcommand{\mb}{\con{b}}%
+\newcommand{\mf}{\con{f}}%
+%
+\newcommand{\mincl}{\con{incl}}%
+\newcommand{\mexcl}{\con{excl}}%
+%
+\newcommand{\mnoboxSD}{\con{noboxSD}}%
+\newcommand{\mSD}{\con{SD}}%
+\newcommand{\mMSC}{\con{MSC}}%
+\newcommand{\mesymSD}{\con{esymSD}}%
+\newcommand{\mesymMSC}{\con{esymMSC}}%
+%
+\newcommand{\muniversal}{\con{universal}}%
+\newcommand{\mexistential}{\con{existential}}%
+\newcommand{\mnone}{\con{none}}%
+%
+\newcommand{\mempty}{\con{}}%
+\newcommand{\mweak}{\con{weak}}%
+\newcommand{\mpermissive}{\con{permissive}}%
+\newcommand{\mstrict}{\con{strict}}%
+%
+\newcommand{\minitial}{\con{initial}}%
+\newcommand{\minvariant}{\con{invariant}}%
+\newcommand{\miterative}{\con{iterative}}%
+%
+%
+\newcommand{\pstricks}{\texttt{pstricks}}
+%
+\newcommand{\optparam}[1]{\lb{#1}\rb}
+\newcommand{\param}[1]{\lcb{#1}\rcb}
+\newcommand{\var}[1]{\textit{#1}}
+\newcommand{\this}[1]{\texttt{#1}}
+\newcommand{\orthat}[1]{$\,\mid\,$\texttt{#1}}%>@>
+
+\makeindex
+
+\begin{document}
+
+\maketitle
+
+\tableofcontents
+
+\begin{lrbox}{\bsbox}\verb"\"\end{lrbox}%<@<
+\begin{lrbox}{\lcbbox}\verb"{"\end{lrbox}
+\begin{lrbox}{\rcbbox}\verb"}"\end{lrbox}
+\begin{lrbox}{\lbbox}\verb"["\end{lrbox}
+\begin{lrbox}{\rbbox}\verb"]"\end{lrbox}%>@>
+
+\section{Introduction}
+\label{sec:intro}
+
+%<@<
+The \lscsty{} package provides means to typeset
+ \index{Live Sequence Charts}%
+Live Sequence Charts.
+%
+The Live Sequence Charts (LSC) language is a variant of
+ \index{Message Sequence Charts|see{MSC}}%
+ \index{MSC}%
+Message Sequence Charts (MSC)~\cite{ITU-T1993}.
+%
+It's intended use is as a language to formalise requirements on the
+communication in a (software or hardware) system under design.
+%
+The basic difference to MSCs is the addition of modalities to the elements of
+a chart to distinguish
+ \index{mandatory}%
+\emph{mandatory} from
+ \index{possible}%
+\emph{possible} behaviour.
+%
+For example, locations on instance lines can be
+ \index{hot}%
+\emph{hot} to indicate that
+ \index{progress}%
+progress is required to satisfy the LSC
+ \index{liveness}%
+(liveness) or
+ \index{cold}%
+\emph{cold} to indicate that behaviour without progress is acceptable.
+%
+This is where the LSC language gets its name from.
+%>@>
+
+\subsection{Supported LSC Language}
+
+%<@<
+For further information on the original syntax, semantics, and pragmatics of
+the LSC language see:
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{DammHarel2001}]
+ Werner Damm and David Harel,
+ \emph{{LSC}s: Breathing Life into Message Sequence Charts},
+ Formal Methods in System Design, 19(1):45--80, July 2001.
+\end{description}
+\end{quote}
+%
+The LSC language presented in this publication is (up to minor deviations in
+ \index{style}%
+style) fully supported by \lscsty{}.
+
+\medskip
+
+From the original language, two
+ \index{dialects}%
+ \index{LSC dialects}%
+dialects emerged, each of them tailored for a
+particular use of an LSC specification, i.e. a collection of single charts.
+%
+The dialect presented in
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{Klose2003}]
+ Jochen Klose,
+ \emph{Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behaviour},
+ PhD thesis, {Carl von Ossietzky Universit\"{a}t Oldenburg}, 2003.
+\end{description}
+\end{quote}
+%
+considers LSCs as the requirements specification language in a classical
+ \index{development process}%
+development process where the system implementation is finally tested to
+satisfy the requirements or, possibly better, a system \emph{model} is
+ \index{formal verification}%
+formally verified to satisfy the requirements.
+
+To this end, the author added
+ \index{timer}%
+timers and
+ \index{timing interval}%
+timing intervals (also taken from MSCs),
+ \index{local invariant}%
+local invariants to state requirements on spans of time in contrast to
+conditions which apply only to single points of time, three
+ \index{activation mode}%
+activation modes, and two
+ \index{interpretation}%
+interpretations, but doesn't support
+ \index{scope}%
+scopes.
+%
+The articles
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{KloseWestphal2002}]
+ Jochen Klose and Bernd Westphal,
+ \emph{Relating {LSC} Specifications to {UML} Models},
+ In: Hartmut Ehrig and Martin Gro\ss{}e-Rhode (Eds.),
+ Proceedings of the Workshop Integration of Software Specification Techniques (INT'02),
+ pages 130--137, April 2002.
+\item[\cite{DammWestphal2005}]
+ Werner Damm and Bernd Westphal,
+ \emph{Live and Let Die: {LSC}-based Verification of {UML}-Models},
+ Science of of Computer Programming,
+ 55(1--3):117--159, March 2005.
+\end{description}
+\end{quote}
+%
+provide a further extension to so called
+ \index{dynamic binding}%
+dynamic binding instance lines.
+
+The LSC language presented in these publications is (up to minor deviations in
+ \index{style}%
+style) fully supported by \lscsty{}.
+
+\medskip
+
+
+
+The dialect presented in
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{HarelMarelly2003}]
+ David Harel and Rami Marelly,
+ \emph{Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine},
+ Springer-Verlag, 2003.
+\end{description}
+\end{quote}
+%
+is tailored for an approach called
+ \index{play-out}%
+play-out\emph{play-out}.
+%
+In this approach, the LSC specification \emph{is} the implementation. A tool
+called
+ \index{play-engine}%
+play-engine interprets an LSC specification that has to be related to a
+GUI. If the GUI is operated by a user, then the play-engine looks up its
+collection of LSCs and operates the GUI accordingly, thus interacts with a
+user.
+
+To this end, they added, for example,
+ \index{actor instance line}%
+actor instance lines,
+ \index{action}%
+actions to modify the system state and extended
+ \index{scope}%
+scopes to
+ \index{loop}%
+loops.
+%
+They independently also added
+ \index{symbolic instances}%
+symbolic instances, means to handle
+ \index{time}%
+time and to
+ \index{exclude observations}%
+exclude observations by
+ \index{forbidden elements}%
+forbidden elements, and two
+ \index{interpretations}%
+interpretations.
+
+The LSC language presented in~\cite{HarelMarelly2003} is not fully supported
+by \lscsty, and if supported, features are rendered in the
+ \index{style}%
+style and terminology of~\cite{Klose2003}.
+%
+Section~\ref{sec:pipo} discusses how \emph{some} constructs of this LSC
+dialect can although be typeset with some
+ \index{manual intervention}%
+manual intervention using some special features \lscsty.
+%>@>
+
+\subsection{Typesetting MSCs and Sequence Diagrams}
+
+%<@<
+As LSCs are a derivative of MSCs as are
+ \index{UML}%
+UML's
+ \index{Sequence Diagram|see{SD}}%
+ \index{SD}%
+Sequence Diagrams (SDs), there is a
+ \index{common sublanguage}%
+common sublanguage and MSCs or SDs from the common sublanguage may well be
+typeset using \lscsty.
+
+But note that there are no plans to extend \lscsty{} to full support of
+either language.
+%
+For MSCs, for example, there is an own \LaTeX{} style and SDs may finally be
+supported by styles for typesetting UML diagrams.
+%>@>
+
+\subsection{Related Styles}
+
+%<@<
+As soon as \lscsty{} reached some usable state -- of course -- it
+turned out that there exist \LaTeX{} packages for typesetting variants of
+sequence diagrams from which \lscsty{} could have been derived from.
+
+We briefly list and discuss the styles we're aware of in the following
+sections.
+
+\subsubsection{MSC}
+
+ \index{MSC}%
+Version 1.13 of the
+ \index{msc@\sty{msc}}%
+msc\sty{msc} package%
+\footnote{
+ \small{\tt http://www.win.tue.nl/~sjouke/misc/mscpackage}
+}
+by
+ \index{Mauw@Mauw, S.}%
+S. Mauw and
+ \index{Bos@Bos, V.}%
+V. Bos~\cite{MauwBos2001} claims to support the full
+ \index{MSC2000}%
+MSC2000 language.
+
+The most obvious difference is that \sty{msc} seems to be able to compute a
+ \index{layout}%
+layout on its own, i.e. it only takes a description of the dependencies in the
+LSC, i.e. the user needn't give precise positioning commands while
+ \index{manual intervention}%
+manual intervention is still possible.
+
+In contrast, \lscsty{} is more low level as it expects \emph{all} layout to be
+given by the user.
+
+\subsubsection{UML}
+
+ \index{UML}%
+ \index{SD}%
+For example, the
+ \index{pst-uml@\sty{pst-uml}}%
+\sty{pst-uml} package%
+\footnote{
+ \small{\tt http://www.ensta.fr/~diam/latex/pst-uml/index.html}
+}
+by
+ \index{Diamantini@Diamantini, M.}%
+M. Diamantini provides rudimentary support for UML sequence diagrams.
+%>@>
+
+
+\section{Preliminaries}
+\label{sec:pre}
+
+%<@<
+The macros provided by \lscsty{} can be divided into three
+ \index{categories}%
+categories:
+%
+\begin{description}
+\item[Environments.]
+ \index{environment}%
+ The \mFullLsc{} and \mLsc{} environments draw LSC charts with and without
+ header, the \mlscinst{} and \mlsccreateinst{} environments draw instances
+ within LSCs, and the \mcoregion{} and \msimregion{} environments mark
+ coregions and simultaneous regions within instances.
+\item[Atomic Commands.]
+ \index{atomic command}%
+ \index{command!atomic}%
+ An atomic command directly draws an LSC element, instance line segment, or
+ annotation that is related to only a single location.
+ %
+ Examples are instance line segments, action boxes, or timer set/reset and
+ timeout.
+\item[Composite Commands.]
+ \index{composite command}%
+ \index{command!composite}%
+ Composite commands draw LSC elements that are related to more than one
+ location. There are typically macros to set the locations which are used
+ within an instance line environment and one macro which finally draws the
+ element based on the set locations.
+ %
+ A typical example are the macros for messages which comprise one macro for
+ setting the sending location, one macro for setting the reception location,
+ and a macro which draws the message arrow.
+\end{description}
+
+\begin{figure}%<@< \label{fig:expl}
+\begin{center}
+\begin{minipage}{0.225\textwidth}
+ \makeatletter
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{5.25}
+ \begin{lscinst}{\textit{Inst}}
+ \lscPut{\pnode(1.4,0.3){ibAA}}
+ \psaddtolength{\lsc@Y}{-0.25}
+ \lscLine{hot}{1.0}
+ \lscPut{\pnode(0.2,0.5){laAA}}
+ \psaddtolength{\lsc@Y}{-0.25}
+ \lscCond{hot}{\textit{Cond}}
+ \lscPut{\pnode(0.9,-0.25){cAA}}
+ \lscLine{cold}{0}
+ \psaddtolength{\lsc@Y}{-0.75}
+ \lscLine{cold}{2.0}
+ \lscPut{\pnode(0.2,0.5){lbAA}}
+ \psaddtolength{\lsc@Y}{-0.75}
+ \lscPut{\pnode(1.4,0.3){ieAA}}
+ \end{lscinst}
+ \end{Lsc}}
+ \makeatother%
+\end{minipage}%
+%
+\hfill%
+%
+\begin{minipage}{0.225\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{{\it Inst}}
+ \lscPut{\pnode(-1.4,0.3){ibAB}}
+ \lscPut{\pnode(1.4,0.3){ibBA}}
+ \lscLine{hot}{1}
+ \lscPut{\pnode(-0.2,0.5){laAB}}
+ \lscPut{\pnode(0.2,0.5){laBA}}
+ \lscCond{hot}{{\it Cond}}
+ \lscPut{\pnode(-0.9,-0.25){cAB}}
+ \lscPut{\pnode(0.9,-0.25){cBA}}
+ \lscLine{cold}{2}
+ \lscPut{\pnode(-0.2,1){lbAB}}
+ \lscPut{\pnode(0.2,1){lbBA}}
+ \lscPut{\pnode(-1.4,0.3){ieAB}}
+ \lscPut{\pnode(1.4,0.3){ieBA}}
+ \end{lscinst}
+ \end{Lsc}}%
+\end{minipage}%
+%
+\hfill%
+%
+{%
+\pnode(0.25,0.85){ibBB}% before the minipage as it seems to add height
+\pnode(0.25,-0.75){ieBB}%
+\pnode(0.55,0.50){laBB}%
+\pnode(0.55,-0.35){lbBB}%
+\pnode(0.55,0.075){cBB}%
+%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{\it Inst}
+ \lscLine{hot}{1}
+ \lscCond{hot}{\it Cond}
+ \lscLine{cold}{2}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}
+\end{minipage}}%
+%
+\psset{linewidth=0.5pt,linestyle=dotted}%
+\ncline{ibAA}{ibAB}\ncline{ibBA}{ibBB}%
+\ncline{ieAA}{ieAB}\ncline{ieBA}{ieBB}%
+\ncline{laAA}{laAB}\ncline{laBA}{laBB}%
+\ncline{lbAA}{lbAB}\ncline{lbBA}{lbBB}%
+\ncline{cAA}{cAB}\ncline{cBA}{cBB}%
+\end{center}
+\caption{\small%
+ \index{exploded view}%
+ {\bf Exploded view} of a simple LSC.}
+\label{fig:expl}
+\end{figure}%>@>
+
+Figure~\ref{fig:expl} illustrates the drawing principle.
+%
+The LSC in the middle is the result of the source on the right.
+%
+To pinpoint the relation between commands and graphics, we provide an
+ \index{exploded view}%
+exploded view on the left and connect graphics and text by dotted lines.
+
+In the example, the
+ \index{Lsc@$\mLsc{}$}%
+\mLsc{} environment draws nothing as we use the
+ \index{none}%
+quantification
+ \index{none@$\mnone{}$}%
+\mnone{} (which is special to \lscsty{} and not part of any LSC dialect) and
+have no prechart.
+%
+If we used
+ \index{universal@$\muniversal{}$}%
+\muniversal{} or
+ \index{existential@$\mexistential{}$}%
+\mexistential{}, then the \mLsc{} would draw the solid or dashed frame around
+the body and if we had a prechart, \mLsc{} would draw the large dashed
+ \index{kandis}%
+kandis.%
+\footnote{
+ A \emph{kandis} is a giant sugar crystal which plays a role in East Frisian
+ tea ceremonies (first the kandis, then the tea, and then slowly and
+ carefully some cream).
+ %
+ From the side a kandis typically looks like a hexagon, i.e. like the shape
+ used for rendering conditions and pre-charts.
+ %
+ Throughout this text, we use kandis to denote the hexagon shape.
+}
+But although it doesn't draw something, it defines the \env{pspicture}
+environment enclosing the LSC and thereby defines the
+ \index{box boundary}%
+box boundary.
+%
+The size of the box is determined by the number of instance lines (1 in the
+example) and their height (3
+ \index{pstricks units@\pstricks{} units}%
+\pstricks{} units in the example).
+
+Within the \mLsc{} environment, there is a single
+ \index{lscinst@$\mlscinst{}$}%
+\mlscinst{} environment.
+%
+It takes one required argument, the instance name, and is responsible for
+drawing the instance head and footer.
+%
+A possible parameter controls the shape of the head and the footer (cf.
+Section~\ref{sec:inst}).
+
+Within the \mlscinst{} environment, there are only atomic commands in the
+example.
+%
+The
+ \index{lscLine@$\mlscLine{}$}%
+\mlscLine{} command draws an instance line segment and advances vertical
+position by the segment length.
+%
+The first parameter is either
+ \index{hot@$\mhot{}$}%
+\mhot{},
+ \index{cold@$\mcold{}$}%
+\mcold{},
+or
+ \index{none@$\mnone{}$}%
+\mnone{} and gives the temperature (or mode) of the location at the beginning
+of the instance line segment (cf. Section~\ref{sec:line} for the pseudo-mode
+`\mnone{}').
+%
+The second parameter is the instance line segment length. In the example, we
+use \pstricks{} units, but any length understood by \pstricks{} will do
+%
+(cf. Section~\ref{sec:line} for a discussion of environment instance line
+segments and their optional parameter for timing intervals).
+
+The
+ \index{lscCond@$\mlscCond$}%
+\mlscCond{} command draws a condition restricted to a single instance line,
+also called
+ \index{narrow condition}%
+ \index{condition!narrow condition}%
+narrow condition (cf. Section~\ref{sec:cond} for a discussion of narrow vs.
+wide conditions).
+%
+The first parameter is either
+ \index{hot@$\mhot{}$}%
+\mhot{} or
+ \index{cold@$\mcold{}$}%
+\mcold{} and gives the mode, the second parameter is the condition expression.
+%
+The \mlscCond{} command doesn't advance the vertical position, that is, all
+atomic commands different from instance line segments which are given between
+two instance line segments are drawn at the same position and implicitly form
+a
+ \index{simultaneous region}%
+simultaneous region.
+%
+The
+ \index{simregion@$\msimregion{}$}%
+\msimregion{} environment can be used to make this explicit by drawing a
+large dot at the shared location (cf. Section~\ref{sec:simreg}).
+
+Note that the instance line segments in the LSC in the middle of
+Figure~\ref{fig:expl} are of different length according to the source on the
+right but appear to be of roughly the same length.
+%
+The reason for using different lengths is that the first instance line segment
+spans from the bottom line of the instance header frame to the top line of the
+condition kandis.
+%
+The second instance line segment spans from the top (!) line of the condition
+kandis to the bottom (!) line of the footer, i.e. the beginning is hidden by
+the condition and the end is hidden by the footer.
+%
+The former hiding takes place because only after drawing an instance line
+segment, all elements in the simultaneous region \emph{before} it are
+ \index{flush}%
+``flushed''.
+%
+The footer is drawn after the last instance line segment has been drawn but it
+is the only element whose bottom line is positioned at the current position.
+%
+Conditions, for example, are placed such that the top line lies at the current
+position.
+%>@>
+
+\section{LSC Environments}
+\label{sec:lsc}
+
+The \lscsty{} package provides two environments for LSCs, one for complete LSC
+specifications and one omitting the header, in particular to typeset LSC
+bodies only without enclosing frame.
+
+\subsection{Full LSCs}
+\label{sec:lsc:fulllsc}
+
+%<@<
+ \index{FullLsc@$\mFullLsc$}%
+\begin{center}\fbox{\parbox{0.86\textwidth}{%
+\mbegin{FullLsc}%
+ \optparam{\var{prechartloc}}%
+ \param{\var{name}}%
+ \param{\var{ac}}%
+ \newline%
+ \hspace*{8em}%
+ \param{\this{$\minvariant$}\orthat{$\minitial$}\orthat{$\miterative$}}%
+ \newline%
+ \hspace*{8em}%
+ \param{\this{$\mstrict$}\orthat{$\mweak$}\orthat{$\mpermissive$}\orthat{}}%
+ \newline%
+ \hspace*{8em}%
+ \param{\this{$\mexistential$}\orthat{$\muniversal$}}%
+ \param{\var{nrinsts}}%
+ \param{\var{nrlocs}}
+\newline
+\dots
+\newline
+\mend{FullLsc}
+}}\end{center}
+
+The \mLsc{} environment typesets full LSCs, i.e. LSC with a header giving the
+name \var{name}, the activation condition \var{ac}, the activation mode
+(one of
+\\
+\minvariant{}, \minitial{}, or \miterative{}), the interpretation,
+(one of \mstrict{},
+\mweak{}, \mpermissive{}, or empty), and the quantification (either
+\muniversal{} or \mexistential{}).
+
+The optional first parameter gives the height of the pre-chart, \var{nrinsts}
+is the (strictly positive) number of instances, and \var{nrlocs} the height of
+instance lines.
+
+\newcommand{\verbunskip}{\vspace*{-1.85\baselineskip}}%
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{FullLsc}{Name}{ActCond}{invariant}{weak}{existential}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{FullLsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{FullLsc}%
+ {Name}{ActCond}%
+ {invariant}{weak}%
+ {existential}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{FullLsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+
+Note that the
+ \index{interpretation}%
+interpretation
+ \index{weak@$\mweak{}$}%
+\mweak{} maps to the unified name permissive in the LSC header.
+%
+If no interpretation is given, the corresponding field is not present in the
+LSC header at all.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{FullLsc}[1.5]{Name}{ActCond}{iterative}{}{universal}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{FullLsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{FullLsc}[1.5]%
+ {Name}{ActCond}%
+ {iterative}{}%
+ {universal}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{FullLsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{LSCs without Header}
+\label{sec:lsc:lsc}
+
+%<@<
+ \index{Lsc@$\mLsc$}%
+\begin{center}\fbox{\parbox{0.85\textwidth}{%
+\mbegin{Lsc}%
+ \optparam{\var{prechartloc}}%
+ \newline%
+ \hspace*{6em}%
+ \param{\this{$\mexistential$}\orthat{$\muniversal$}\orthat{$\mnone$}}%
+ \param{\var{nrinsts}}%
+ \param{\var{nrlocs}}
+\newline
+\dots
+\newline
+\mend{Lsc}
+}}\end{center}
+
+The \mLsc{} environment is provided to typeset LSCs without header and LSCs
+without surrounding frame indicating the quantification.
+%
+With the special quantification \mnone{}, the frame is omitted and thus only
+the LSC body drawn.
+%
+This is useful in publications on LSCs which discuss, for example, the
+compilation of LSC bodies to automata.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Instance Lines}
+\label{sec:inst}
+
+There are two flavours of instance line environment, ordinary and creation
+instance lines.
+%
+Creation instance lines are used to indicate that an object is created during
+a scenario.
+%
+To this end the instance head can be placed some offset below the regular
+position of instance heads and it defines a hook for the composite
+\mlscCreate{} command which draws the creation arrow.
+
+\subsection{Ordinary Instance Lines}
+\label{sec:inst:ord}
+
+%<@<
+ \index{lscinst@$\mlscinst$}%
+\begin{center}\fbox{\parbox{0.8\textwidth}{
+\mbegin{lscinst}%
+ \optparam{\underline{\this{$\mMSC$}}\orthat{$\mSD$}\orthat{$\mnoboxSD$}\orthat{$\mesymMSC$}\orthat{$\mesymSD$}}%
+ \param{\var{name}}
+\newline
+\dots
+\newline
+\mend{lscinst}
+}}\end{center}
+
+The \var{name} is set on top of the instance line segments.
+%
+The optional parameter controls the appearance of the instance header and
+footer according to the following table:
+
+ \index{MSC@$\mMSC$}%
+ \index{SD@$\mSD$}%
+ \index{noboxSD@$\mnoboxSD$}%
+ \index{esymMSC@$\mesymMSC$}%
+ \index{esymSD@$\mesymSD$}%
+\begin{center}
+\begin{tabular}{||l|c|c||}
+\hline
+ & framed header & footer \\
+\hline
+\mMSC{}
+(default) & solid & $\times$ \\
+\hline
+\mSD{} & solid & $-$ \\
+\hline
+\mnoboxSD{} & none & $-$ \\
+\hline
+\mesymMSC{} & dashed & $\times$ \\
+\hline
+\mesymSD{} & dashed & $-$ \\
+\hline
+\end{tabular}
+\end{center}
+
+There is no kind for the fourth possible combination -- nobody wants the
+combination of no frame but a footer.
+
+\begin{center}%<@<
+\begin{minipage}{0.625\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{3}{3}
+ \begin{lscinst}{MSC}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}[SD]{SD}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}[noboxSD]{noboxSD}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \begin{lscinst}{MSC}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}[SD]{SD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}[noboxSD]%
+ {noboxSD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lscinst}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+See Section~\ref{sec:pipo:inst} for examples of existential symbolic instances.
+%>@>
+
+\subsection{Creation Instance Lines}
+\label{sec:inst:cre}
+
+%<@<
+ \index{lsccreateinst@$\mlsccreateinst$}%
+\begin{center}\fbox{\parbox{0.775\textwidth}{%
+\mbegin{lsccreateinst}%
+ \optparam{\underline{\this{$\mMSC$}}\orthat{$\mSD$}\orthat{$\mnoboxSD$}\orthat{$\mesymMSC$}\orthat{$\mesymSD$}}%
+\newline
+\hspace*{3.75cm}
+ \param{\var{offset}}%
+ \param{\var{id}}%
+ \param{\var{name}}%
+\newline
+\dots
+\newline
+\mend{lsccreateinst}
+}}\end{center}
+
+The optional parameter \mlsccreateinst{} and the \var{name} work just like in
+the \mlscinst{} environment.
+%
+The additional parameter \var{offset} gives the offset of the instance header
+relative to the headers of ordinary instance lines.
+%
+That is, it is exactly equivalent to \mlscinst{} if the \var{offset} is 0 and
+the corresponding \lscCreate{} command is omitted.
+
+ \index{lscCreate@$\mlscCreate$}%
+\begin{center}\fbox{
+\mlscCreate%
+ \param{\var{id}}%
+}\end{center}
+
+The parameter \var{id} is a legal \LaTeX{} identifier which can be used in the
+\mlscCreate{} command to draw the create arrow.
+
+\begin{center}%<@<
+\begin{minipage}{0.435\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.7}
+ \lscCreate{cr}
+ \lscLine{hot}{2.3}
+ \end{lscinst}
+ \begin{lsccreateinst}{1}{cr}{Inst2}
+ \lscLine{hot}{2}
+ \end{lsccreateinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.7}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscCreate{cr}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2.3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \begin{lsccreateinst}{1}{cr}{Inst2}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lsccreateinst}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+\begin{center}%<@<
+\begin{minipage}{0.435\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lsccreateinst}[noboxSD]{1}{cr}{Inst1}
+ \lscLine{hot}{2}
+ \end{lsccreateinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.7}
+ \lscCreate{cr}
+ \lscLine{hot}{2.3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \begin{lsccreateinst}{1}{cr}{Inst2}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lsccreateinst}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.7}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscCreate{cr}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2.3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}%
+\end{minipage}
+\end{center}%>@>
+
+ \index{creation arrow}
+Note that the creation arrow ends at the border of the frame when the instance
+head has a frame and at the label if there is no frame.
+%
+Further note that the instance line end of the arrow is located 0.3 pstricks
+units above the bottom of the instance head such that the instance line
+segment lengths on the instance line with the \mlscCreate{} can easily be
+adjusted to obtain a vertical arrow.
+
+The creation arrow is drawn as soon as both ends, i.e. the \mlscCreate{}
+location and the creation instance, are given. The identifier is then
+undefined, i.e. the same identifier may legally occur in two
+\mlscCreate{}/\mlsccreateinst{} pairs in the same LSC -- but this is obviously
+bad style.
+%>@>
+
+\subsection{Instance Location and Footer Dimensions}
+\label{sec:inst:dim}
+
+%<@<
+ \index{lscLocationWidth@$\mlscLocationWidth$}%
+ \index{lscLocationHeight@$\mlscLocationHeight$}%
+\begin{center}\fbox{\parbox{12em}{%
+ \mlscLocationWidth
+ \newline
+ \mlscLocationHeight
+}}\end{center}
+
+\begin{figure}%<@< \label{fig:locdim}
+\begin{center}
+{\pssetlength{\lscLocationWidth}{4}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscPut{\pcline[linewidth=0.5pt]{|-|}%
+ (-0.5\lscLocationWidth,1)%
+ (0.5\lscLocationWidth,1)%
+ \lput*{0}{\mlscLocationWidth}}
+ \lscLine{hot}{1}
+ \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+ (-0.5\lscLocationWidth,\lscLocationHeight)%
+ (0.5\lscLocationWidth,0)}
+ \lscLine{hot}{1}
+ \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+ (-0.5\lscLocationWidth,\lscLocationHeight)%
+ (0.5\lscLocationWidth,0)}
+ \lscPut{\pcline[linewidth=0.5pt]{|-|}%
+ (0.6\lscLocationWidth,\lscLocationHeight)%
+ (0.6\lscLocationWidth,0)%
+ \lput*[l]{0}{\mlscLocationHeight}}
+ \lscLine{hot}{1}
+ \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+ (-0.5\lscLocationWidth,\lscLocationHeight)%
+ (0.5\lscLocationWidth,0)}
+ \end{lscinst}
+\end{Lsc}}
+\end{center}
+%
+\caption{\small%
+ {\bf Dimensions} of a location.}
+\label{fig:locdim}
+\end{figure}%>@>
+
+ \index{box boundary|textbf}%
+The LSC's box boundary is basically computed in terms of the width and height
+of a single location within an instance (cf. Figure~\ref{fig:locdim}) as
+defined by lengths \mlscLocationWidth{} (default: 3 pstricks units) and
+\mlscLocationHeight{} (default: 1 pstricks unit).
+%
+The width of the LSC body is computed as
+\[
+\textit{number of instances} * \mlscLocationWidth
+\]
+and the height of the LSC body is computed as
+\[
+\textit{number of locations} * \mlscLocationHeight.
+\]
+%
+Both lengths can be manipulated, for example, to obtain wider or narrower
+instances or to globally scale the length of instance line segments.
+
+To change the dimension for only a single LSC, one can exploit that curly
+braces in \LaTeX{} define scopes and that changes to lengths or commands are
+local to these scopes.
+%
+To this end we have enclosed the manipulation of the lengths and the \mLsc{}
+environment in curly braces.
+
+\begin{center}%<@<
+\begin{minipage}{0.275\textwidth}%
+ \scalebox{0.9}{%
+ \pssetlength{\lscLocationWidth}{5em}
+ \pssetlength{\lscLocationHeight}{1.5}
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{\parbox{4em}{Instance No. 1}}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.50\textwidth}%
+\small%
+\begin{verbatim}
+{\pssetlength{\lscLocationWidth}{5em}
+\pssetlength{\lscLocationHeight}{1.5}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{%
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \parbox{4em}{Instance No. 1}}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+Note that the height of the instance head frame depends on the height of its
+content, i.e. a \cmd{parbox} may be used to obtain multiline annotations in
+instance heads.
+
+ \index{lscFooterHeightFactor@$\mlscFooterHeightFactor$}%
+\begin{center}\fbox{%
+ \mlscFooterHeightFactor
+}\end{center}
+
+The command (!) \mlscFooterHeightFactor{} (default: 0.2) affects the
+appearance of instance footers.
+%
+It should be set to a positive real number, at best from the left-open
+interval $]0,0.2]$. The footer is basically a filled framebox around a
+\cmd{rule} of height
+%
+\[
+\mlscFooterHeightFactor * \mlscLocationHeight.
+\]
+
+\begin{center}%<@<
+\begin{minipage}{0.225\textwidth}%
+ \scalebox{0.9}{%
+ \renewcommand{\lscFooterHeightFactor}{0.05}
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.61\textwidth}%
+\small%
+\begin{verbatim}
+{\renewcommand{\lscFooterHeightFactor}{0.01}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Instance Line Segments}
+\label{sec:line}
+
+There are two flavours of instance line segments, ordinary and environment
+instance line segments.
+%
+Environment instance line segments are rendered like the ones of Sequence
+Diagrams.
+
+\subsection{Ordinary Instance Line Segments}
+\label{sec:line:ord}
+
+%<@<
+ \index{lscLine@$\mlscLine$}%
+\begin{center}\fbox{
+\mlscLine%
+ \optparam{\var{interval}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}\orthat{$\mnone$}}%
+ \param{\var{length}}%
+}\end{center}
+
+The \mlscLine{} command draws the elements belonging to the location where the
+line starts, draws the instance line segment of length \var{length}, and
+advances the vertical position by this amount.
+%
+The mode `\mnone{}' is not a valid mode of LSCs but only present to draw an
+invisible line segment to draw abstract LSCs, e.g. to explain LSC
+construction algorithms.
+
+The actual length of the line segment is computed as
+$\var{length} \cdot \mlscLocationHeight{}$.
+
+If the optional \var{interval} is given, it rendered to the right of the
+instance line segment. This may be any content, but it is typically used to
+place timing intervals.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.75}
+ \lscLine{none}{0.75}
+ \lscLine{cold}{1.5}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine[{$[1,2]$}]{cold}{1.25}
+ \lscLine[{$[3,17]$}]{hot}{1.75}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscLine{hot}{0.75}
+ \lscLine{none}{0.75}
+ \lscLine{cold}{1.5}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscLine[{$[1,2]$}]{cold}{1.25}
+ \lscLine[{$[3,17]$}]{hot}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that timing intervals are always vertically centred on the line and put
+to the right.
+%
+As this is already the optional parameter, there are no plans to support
+variable positioning of the timing interval but nobody keeps you from using
+\cmd{rput} should the need arise.
+
+\medskip
+
+The \mlscLine{} command doesn't set the line colour, thus one can obtain
+colourful LSCs using the \cmd{psset} command.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ {\psset{linecolor=green}
+ \lscLine{hot}{1.25}}
+ {\psset{linecolor=blue}
+ \lscLine{cold}{1.75}}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ {\psset{linecolor=green}
+ \lscLine{hot}{1.25}}
+ {\psset{linecolor=blue}
+ \lscLine{cold}{1.75}}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Environment Instance Line Segments}
+\label{sec:line:env}
+
+%<@<
+ \index{lscEnvLine@$\mlscEnvLine$}%
+\begin{center}\fbox{
+\mlscEnvLine%
+ \optparam{\var{interval}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{length}}%
+}\end{center}
+
+The \mlscEnvLine{} behaves just like \mlscLine{}, only the instance line
+segment is rendered differently, namely in
+ \index{Sequence Diagram}%
+Sequence Diagram style.
+%
+To indicate hot segments, a solid line is drawn on top of the environment
+line segment.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscEnvLine{hot}{1.25}
+ \lscEnvLine{cold}{1.75}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscEnvLine[{$[1,2]$}]{cold}{1.25}
+ \lscEnvLine[{$[3,17]$}]{hot}{1.75}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscEnvLine{hot}{1.25}
+ \lscEnvLine{cold}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \lscEnvLine[{$[1,2]$}]{cold}{1.25}
+ \lscEnvLine[{$[3,17]$}]{hot}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\section{Messages}
+\label{sec:msg}
+
+Both message kinds distinguished by~\cite{Klose2003} are supported by two sets
+of composite commands.
+%
+For each kind, there is one command to mark the sending location, one command
+to mark the reception location, and one command to finally draw the arrow.
+
+The difference between both is only the shape of the arrow, it is not enforced
+that instantaneous messages are drawn horizontally without slope.
+
+Both also don't define the line colour, i.e. one can obtain coloured arrows
+using \cmd{psset} (cf. Section~\ref{sec:line:ord}).
+
+Self messages are currently not supported.
+%
+If the sending and reception lie on the same instance line, then the arrow's
+line coincides with the instance line and only the arrow itself and the
+annotation will be visible.
+
+\subsection{Asynchronous Messages}
+\label{sec:msg:asyn}
+
+%<@<
+ \index{lscAsynSnd@$\mlscAsynSnd$}%
+ \index{lscAsynRcv@$\mlscAsynRcv$}%
+ \index{lscAsyn@$\mlscAsyn$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscAsynSnd%
+ \param{\var{id}}%
+\newline
+\mlscAsynRcv%
+ \param{\var{id}}%
+\newline
+\mlscAsyn%
+ \param{\var{id}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{label}}
+}}\end{center}
+
+If \mlscAsynSnd{} and \mlscAsynRcv{} occurred exactly once within an
+\mFullLsc{} or \mLsc{} environment, then a following \mlscAsyn{} command with
+the same \var{id} draws the arrow annotated with \var{label}.
+
+The \var{id} can be reused for another message within the same LSC after
+\mlscAsyn{} has been called, but this is not considered good style.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.5}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{1.5}%
+ \lscAsynRcv{f}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscAsynSnd{f}%
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \lscAsyn{f}{cold}{F}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynSnd{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynRcv{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynRcv{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynSnd{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsyn{e}{hot}{E}%
+ \lscAsyn{f}{cold}{F}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that the closing commands of composite commands, like \mlscAsyn{} in the
+example, are by
+ \index{convention}%
+convention collected below all instance environments.
+%
+It is by no means necessary, as explained above, but thereby one provides a
+common place to look for all definitions.
+%>@>
+
+\subsection{Instantaneous Messages}
+\label{sec:msg:inst}
+
+%<@<
+ \index{lscInstSnd@$\mlscInstSnd$}%
+ \index{lscInstRcv@$\mlscInstRcv$}%
+ \index{lscInst@$\mlscInst$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscInstSnd%
+ \param{\var{id}}%
+\newline
+\mlscInstRcv%
+ \param{\var{id}}%
+\newline
+\mlscInst%
+ \param{\var{id}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{label}}
+}}\end{center}
+
+The composite command for instantaneous messages is operated exactly like
+\mlscAsyn{} and friends (cf. Section~\ref{sec:msg:asyn}).
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscInstSnd{e}%
+ \lscLine{hot}{1}%
+ \lscInstRcv{f}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+ \lscInstRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscInstSnd{f}%
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ %
+ \lscInst{e}{hot}{E}%
+ \lscInst{f}{cold}{F}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstSnd{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstRcv{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstRcv{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstSnd{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInst{e}{hot}{E}%
+ \lscInst{f}{cold}{F}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Self Messages}
+\label{sec:msg:self}
+
+%<@<
+Self messages are not a third category but both asynchronous and instantaneous
+messages may well begin and end at the same instance line.
+
+\begin{center}%<@<
+\begin{minipage}{0.33\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.5}
+ \lscAsynSnd{e}
+ \lscLine{hot}{1}
+ \lscAsynRcv{e}
+ \lscLine{hot}{0.5}
+ \lscInstSnd{f}
+ \lscLine{hot}{1}
+ \lscInstRcv{f}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscAsyn{e}{hot}{E}
+ \lscInst{f}{hot}{F}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynSnd{e}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsynRcv{e}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstSnd{f}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscInstRcv{f}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAsyn{e}{hot}{E}
+ \lscInst{f}{hot}{F}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Currently, the shape is fixed, i.e. the arrow extends to the right of the
+instance line and has ``armlength'' 0.5 pstricks units.
+%>@>
+
+
+\section{Conditions}
+\label{sec:cond}
+
+Conditions can be rendered using an atomic command and a composite command.
+%
+The former command is provided for convenience for the frequent case that a
+condition spans only a single instance line
+ \index{narrow condition}%
+(narrow condition).
+%
+In this case, all information, i.e. the location, the temperature, and the
+label, can be given immediately.
+
+A wide condition may also span only one instance line but it may also cover
+more.
+
+\subsection{Narrow Conditions}
+\label{sec:cond:narrow}
+
+%<@<
+ \index{lscCond@$\mlscCond$}%
+\begin{center}\fbox{%
+\mlscCond%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{label}}
+}\end{center}
+
+The \mlscCond{} command renders a condition kandis at the current position.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscCond{hot}{$x = a$}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.5}%
+ \lscCond{cold}{\parbox{4em}{\centering$y = 0$ $\vee\ z = 0$}}%
+ \lscLine{hot}{2.5}%
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.47\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscCond{hot}{$x = a$}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscCond{cold}{%
+ \parbox{4em}{\centering%
+ $y=0$ $\vee\ z=0$}}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2.5}%
+ \end{lscinst}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The size of the kandis scales with the size of \var{label}'s box.
+%
+This has the effect that it is rather low if \var{label} has neither over- nor
+underlength and it scales unproportionally if \var{label} has multiple lines.
+%
+The former issue can be addressed using \cmd{rule} or \cmd{phantom}, the
+latter will have to be addressed by a smarter kandis drawing macro within
+\lscsty{}.
+
+\subsection{Wide Conditions}
+\label{sec:cond:wide}
+
+%<@<
+ \index{lscWidecondOn@$\mlscWidecondOn$}%
+ \index{lscWidecondOff@$\mlscWidecondOff$}%
+ \index{lscWidecond@$\mlscWidecond$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscWidecondOn%
+ \param{\var{id}}%
+\newline
+\mlscWidecondOff%
+ \param{\var{id}}%
+\newline
+\mlscWidecond%
+ \param{\var{id}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{label}}
+}}\end{center}
+
+The \mlscWidecondOn{} and \mlscWidecondOff{} commands add locations to a wide
+condition.
+%
+They have to occur on exactly the same height and consecutively.
+%
+Use \mlscWidecondOn{} for those instances to which the condition applies and
+\mlscWidecondOff{} otherwise.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+ \pssetlength{\lscLocationWidth}{2.5}%
+ \begin{Lsc}{none}{3}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}
+ \lscWidecondOn{wc}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}
+ \lscWidecondOff{wc}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \begin{lscinst}{Inst3}
+ \lscLine{hot}{1}
+ \lscWidecondOn{wc}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \lscWidecond{wc}{hot}{$\qquad\quad x = 0$}
+ \end{Lsc}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.39\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\pssetlength%
+ {\lscLocationWidth}{2.5}%
+\begin{Lsc}{none}{3}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscWidecondOn{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscWidecondOff{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \begin{lscinst}{Inst3}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscWidecondOn{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscWidecond{wc}{hot}%
+ {$\qquad\quad x = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The \var{label} is set in the centre of the kandis. If the condition doesn't
+apply to the central location, one may need to add some offset like in the
+example above to avoid the instance line segment running through the label.
+
+Note that the size of wide conditions is fixed, i.e. it does in particular not
+scale with the height of \var{label}'s box.
+%
+As a consequence, \var{label} should fit onto a single line.
+%>@>
+
+\subsection{Colourful Conditions}
+\label{sec:cond:colour}
+
+The appearance of
+ \index{narrow condition}%
+ \index{condition!narrow}%
+narrow conditions, and in particular the colour of its outline, cannot be
+easily manipulated because narrow conditions are ``scheduled'' and drawn when
+the next instance line segment is drawn (cf. Section~\ref{sec:simreg}).
+%
+Thus changing the colour of the outline applies to all elements which are
+drawn together with the instance line segment, in particular the instance line
+itself.
+
+If
+ \index{wide condition}%
+ \index{condition!wide}%
+wide conditions are sufficient (cf. Section~\ref{sec:cond:wide}), their colour
+can be modified as shown in the following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.25\textwidth}%
+ \scalebox{0.9}{%
+ \let\lscWidecondOooginool\lscWidecond%
+ \renewcommand{\lscWidecond}[3]{{%
+ \ifthenelse{\equal{#2}{hot}}{%
+ \psset{linecolor=red}}{%
+ \psset{linecolor=blue}}%
+ \lscWidecondOooginool{#1}{#2}{#3}}}
+ \begin{Lsc}{none}{1}{4.5}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}%
+ \lscWidecondOn{c}%
+ \lscLine{hot}{1.5}%
+ \lscWidecondOn{d}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \lscWidecond{c}{hot}{$f = g$}%
+ \lscWidecond{d}{cold}{$g = f$}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.575\textwidth}%
+\small%
+{\begin{verbatim}
+\let\lscWidecondOooginool\lscWidecond%
+\renewcommand{\lscWidecond}[3]{{%
+ \ifthenelse{\equal{#2}{hot}}{%
+ \psset{linecolor=red}}{%
+ \psset{linecolor=blue}}%
+ \lscWidecondOooginool{#1}{#2}{#3}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4.5}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}%
+ \lscWidecondOn{c}%
+ \lscLine{hot}{1.5}%
+ \lscWidecondOn{d}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \lscWidecond{c}{hot}{$f = g$}%
+ \lscWidecond{d}{cold}{$g = f$}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Local Invariants}
+\label{sec:locinv}
+
+%<@<
+ \index{lscLocinvStart@$\mlscLocinvStart$}%
+ \index{lscLocinvBegin@$\mlscLocinvBegin$}%
+ \index{lscLocinvEnd@$\mlscLocinvEnd$}%
+ \index{lscLocinv@$\mlscLocinv$}%
+\begin{center}\fbox{\parbox{0.875\textwidth}{
+\mlscLocinvStart%
+ \param{\var{id}}%
+\newline
+\mlscLocinvBegin%
+ \param{\var{id}}%
+\newline
+\mlscLocinvEnd%
+ \param{\var{id}}%
+\newline
+\mlscLocinv%
+ \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+ \param{\var{id}}%
+ \param{\this{$\mincl$}\orthat{$\mexcl$}}%
+ \param{\this{$\mincl$}\orthat{$\mexcl$}}%
+ \param{\this{$\mhot$}\orthat{$\mcold$}}%
+ \param{\var{label}}
+}}\end{center}
+
+The commands \mlscLocinvBegin{} (or, synonymously, \mlscLocinvStart{}) and
+\mlscLocinvEnd{} mark the beginning and end position of local invariant
+\var{id}.
+
+The \mlscLocinv{} command renders the local invariant \var{id}.
+%
+The position of the vertical line to which the kandis is connected can be
+controlled by the optional parameter (default: \mr{} (to the right)).
+
+The third and fourth parameters select whether the ends are inclusive (\mincl)
+or exclusive (\mexcl).
+%
+Inclusive ends are rendered with a filled circle and exclusive ends with a
+non-filled circle (just like jumps are indicated in function graphs).
+%
+This is different from~\cite{Klose2003} where the kandis is rotated by 90
+degrees and inclusive ends are indicated by having the kandis end in a
+rectangular shape instead of triangular.
+%
+The drawback is that a both-inclusive local invariant looks like a rotated
+action box and doesn't resemble conditions at all.%
+\footnote{%
+ And -- first of all -- it seemed easier to render the shape we chose.
+}
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLocinvBegin{li}
+ \lscLine{hot}{1}
+ \begin{simregion}
+ \lscLocinvStart{lj}
+ \end{simregion}
+ \lscLine{hot}{1}
+ \lscLocinvEnd{li}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}
+ \lscLocinvEnd{lj}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscLocinv[l]{li}{incl}{excl}{hot}{$x = 0$}
+ \lscLocinv{lj}{excl}{incl}{cold}{$y = 0$}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvBegin{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvStart{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{simregion}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvEnd{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvEnd{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinv[l]{li}%
+ {incl}{excl}{hot}{$x = 0$}
+ \lscLocinv{lj}%
+ {excl}{incl}{cold}{$y = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+In the example above, we used a simregion (cf. Section~\ref{sec:simreg}) to
+highlight the point where the local invariant connects to the instance line in
+lack of other elements.
+%
+Local invariants in the wild typically end at simultaneous regions with other
+elements as the LSC's automaton becomes non-deterministic otherwise.
+
+Note that the local invariant kandis behaves like that of narrow conditions.
+%
+That is, it looks too low if \var{label} has no over- or underlength and it
+scales unproportionally with multiline \var{label}s (cf.
+Section~\ref{sec:cond:narrow}).
+
+Further note that the
+ \index{box boundary}%
+box boundary of the LSC doesn't consider the amounts by which local invariants
+kandis stand out to the left or the right.
+%
+One has to explicitly treat kandis overlapping other text by adding vertical
+space to the left or the right.%
+\footnote{%
+ Technically the problem is that the box boundary is determined when the
+ \mLsc{} environment is opened. At this point in time the extension of local
+ invariants is not yet known. And the dimension cannot be changed afterwards
+ (as far as the author knows).
+}
+
+ \index{lscLocinvOffset@$\mlscLocinvOffset$}%
+\begin{center}\fbox{
+ \mlscLocinvOffset
+}\end{center}
+
+The length \mlscLocinvOffset{} (default: 0) is added to the horizontal
+distance between instance line and local invariant.
+%
+To move the local invariant further outwards, set it to a positive number
+and to move it further inwards, set it to a negative number.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLocinvBegin{li}
+ \lscLine{hot}{1}
+ \begin{simregion}
+ \lscLocinvStart{lj}
+ \end{simregion}
+ \lscLine{hot}{1}
+ \lscLocinvEnd{li}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}
+ \lscLocinvEnd{lj}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \pssetlength{\lscLocinvOffset}{0.5}
+ \lscLocinv[l]{li}{incl}{excl}{hot}{$x = 0$}
+ \pssetlength{\lscLocinvOffset}{-0.5}
+ \lscLocinv{lj}{excl}{incl}{cold}{$y = 0$}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.52\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvBegin{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvStart{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{simregion}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvEnd{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLocinvEnd{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \pssetlength{\lscLocinvOffset}{0.5}
+ \lscLocinv[l]{li}%
+ {incl}{excl}{hot}{$x = 0$}
+ \pssetlength{\lscLocinvOffset}{-0.5}
+ \lscLocinv{lj}%
+ {excl}{incl}{cold}{$y = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The vertical position of the kandis is fixed. It is always drawn centred
+between the beginning and end point.
+%>@>
+
+
+\section{Timer Sets, Timer Resets, and Timeouts}
+\label{sec:tset}
+\label{sec:treset}
+\label{sec:tout}
+
+%<@<
+ \index{lscTimerSet@$\mlscTimerSet$}%
+ \index{lscTimerReset@$\mlscTimerReset$}%
+ \index{lscTimeout@$\mlscTimeout$}%
+\begin{center}\fbox{\parbox{0.875\textwidth}{
+\mlscTimerSet%
+ \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+ \param{\var{label}}%
+ \param{\var{duration}}%
+\newline
+\mlscTimerReset%
+ \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+ \param{\var{label}}%
+\newline
+\mlscTimeout%
+ \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+ \param{\var{label}}%
+}}\end{center}
+
+The atomic commands \mlscTimerSet{}, \mlscTimerReset{}, and \mlscTimeout{}
+render the timer symbols.
+%
+The position of the hourglass symbols can be controlled by the optional
+parameter (default: \mr{} (to the right)).
+
+The parameter \var{label} is not an identifier as used with composite commands
+but arbitrary text. To connect, e.g., timer setting and timeout they should
+obtain the same \var{label}.
+
+A timer type is currently not explicitly supported. It may be written as part
+of the \var{label}.
+
+\begin{center}%<@<
+\begin{minipage}{0.4\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.75}
+ \lscTimerSet{$t$ : superstep}{3}
+ \lscLine{hot}{1}
+ \lscTimerReset[l]{$t$}
+ \lscLine{hot}{1}
+ \lscTimeout{$t$}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.5\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.75}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscTimerSet{$t$ : superstep}{3}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscTimerReset[l]{$t$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscTimeout{$t$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Actions}
+\label{sec:act}
+
+%<@<
+ \index{lscAct@$\mlscAct$}%
+\begin{center}\fbox{
+\mlscAct%
+ \param{\var{label}}%
+}\end{center}
+
+The \lscAct{} atomic command draws a rectangular action symbol annotated with
+\var{label}.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}
+ \lscAct{Aaand -- action!}
+ \lscLine{hot}{2}
+ \end{lscinst}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.40\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAct{Aaand -- action!}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{2}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Self Destructions}
+\label{sec:kill}
+
+%<@<
+ \index{lscKill@$\mlscKill$}%
+\begin{center}\fbox{
+\mlscKill%
+}\end{center}
+
+The atomic \mlscKill{} command draws a cross at the current position to
+indicate
+ \index{termination}%
+termination of the instance.
+%
+It is typically not followed by any more \mlscLine{} commands.
+
+There is no explicit
+ \index{deletion arrow}%
+deletion arrow (like there is a creation arrow) since instantaneous messages
+may be used for this purpose.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}[SD]{Inst1}
+ \lscLine{hot}{1.5}
+ \lscInstSnd{rip}
+ \lscLine{hot}{1}
+ \lscKill
+ \end{lscinst}
+ \begin{lscinst}[SD]{Inst2}
+ \lscLine{hot}{1.5}
+ \lscInstRcv{rip}
+ \lscKill
+ \end{lscinst}
+ \lscInst{rip}{hot}{RIP}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.39\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}[SD]{Inst1}
+ \lscLine{hot}{1.5}
+ \lscInstSnd{rip}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscKill
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}[SD]{Inst2}
+ \lscLine{hot}{1.5}
+ \lscInstRcv{rip}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscKill
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \end{lscinst}
+ \lscInst{rip}{hot}{RIP}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Coregions}
+\label{sec:coreg}
+
+%<@<
+ \index{coregion@$\mcoregion$}%
+\begin{center}\fbox{%
+\mbegin{coregion}%
+ \optparam{\underline{\this{$\ml$}}\orthat{$\mr$}}%
+\dots
+\mend{coregion}
+}\end{center}
+
+The elements and instance line segments enclosed in a \mcoregion{} environment
+are marked with a parallel dotted line to indicate that they form a
+ \index{coregion}%
+coregion.
+%
+The optional parameter controls whether the line appears to the left (\ml{},
+the default) or to the right (\mr) of the instance line.
+%
+\mcoregion{} environments shall not be nested.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscInstSnd{e}%
+ \lscLine{hot}{1}%
+ \lscInstRcv{f}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+ \begin{coregion}[r]
+ \lscInstRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscInstSnd{f}%
+ \psset{linecolor=red}
+ \end{coregion}
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ %
+ \lscInst{e}{hot}{E}%
+ \lscInst{f}{cold}{F}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.49\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}\lscInstSnd{e}%
+ \lscLine{hot}{1}\lscInstRcv{f}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{coregion}[r]
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscInstRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscInstSnd{f}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \psset{linecolor=red}
+ \end{coregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ \lscInst{e}{hot}{E}%
+ \lscInst{f}{cold}{F}%
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The \mcoregion{} environment doesn't set the line's colour so it can be
+manipulated using \cmd{psset}.
+%
+But it does set the width to ensure that the dotted line is noticeable. To
+change the width one may temporary redefine the internal length
+ \index{lsccoregwidth@$\cmd{lsc\AT{}coregwidth}$}%
+\cmd{lsc@coregwidth}.
+
+The coregion line is drawn when the environment is closed. This has the
+(not so nice) effect that the line lies above condition kandis, action boxes
+etc. So currently coregions look best when applied to message ends.
+%>@>
+
+
+\section{Simultaneous Regions}
+\label{sec:simreg}
+
+%<@<
+ \index{simregion@$\msimregion$}%
+\begin{center}\fbox{%
+\mbegin{simregion}%
+ \optparam{\underline{\this{$\mb$}}\orthat{$\mf$}}%
+\dots
+\mend{simregion}
+}\end{center}
+
+The elements enclosed in a \msimregion{} environment are marked with a large
+dot to explicitly indicate that they lie in a
+ \index{simultaneous region}%
+simultaneous region.
+%
+ \index{b@$\mb$}%
+The optional parameter controls whether the dot appears behind (\mb{}, the
+ \index{f@$\mf$}%
+default) or in front of (\mf) the elements.
+%
+\msimregion{} environments shall not be nested and shall not comprise instance
+line segments.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.75}
+ \lscInstSnd{e}
+ \lscLine{hot}{1}
+ \begin{simregion}
+ \lscInstRcv{f}
+ \lscCond{hot}{$x=0$}
+ \end{simregion}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.75}
+ \begin{simregion}[f]
+ \lscCond{hot}{$y=0$}
+ \lscInstRcv{e}
+ \end{simregion}
+ \lscLine{hot}{1}
+ \lscInstSnd{f}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}
+ \lscInst{f}{hot}{F}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.36\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{0.75}
+ \lscInstSnd{e}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscInstRcv{f}
+ \lscCond{hot}{$x=0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.75}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{simregion}[f]
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscInstRcv{e}
+ \lscCond{hot}{$y=0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLine{hot}{1}
+ \lscInstSnd{f}
+ \lscLine{hot}{1.25}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}
+ \lscInst{f}{hot}{F}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that the order of elements (except for cuts) of different kinds in a
+simultaneous region is not significant.
+%
+The
+ \index{drawing order}%
+drawing order is (from bottom to top):
+%
+\begin{enumerate}
+\item
+ \index{simultaneous region}%
+ simultaneous region dot, if it should go into the background
+\item
+ white background of
+ \index{wide condition}%
+ wide condition behind the instance line
+ (\mlscWidecondOn{})
+\item
+ white background of
+ \index{wide condition}%
+ wide condition in front of the instance line
+ (\mlscWidecondOff{})
+\item
+ \index{action}%
+ action or
+ \index{narrow condition}%
+ narrow condition
+\item
+ \index{timer set}%
+ timer set,
+ \index{timer reset}%
+ reset, or
+ \index{timeout}%
+ timeout
+\item
+ \index{atom}%
+ atom (cf. Section~\ref{sec:tech:atom})
+\item
+ \index{simultaneous region}%
+ simultaneous region dot, if it should go into the foreground
+\end{enumerate}
+
+Per simregion, at most one action or narrow condition can be drawn. If one
+really needs to put one above the other (typically sacrificing readability)
+one may use instance line segments of length 0. Two actions or narrow
+conditions can also be stacked one above the other using a manually tailored
+instance line segment in between and a foreground simregion circle like in the
+following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}
+ \lscCond{hot}{x=0}
+ \lscLine{hot}{0.5}
+ \begin{simregion}[f]
+ \lscCond{hot}{y=0}
+ \end{simregion}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.36\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscCond{hot}{x=0}
+ \lscLine{hot}{0.5}
+ \begin{simregion}[f]
+ \lscCond{hot}{y=0}
+ \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The order of the finalising commands of composite commands and cuts \emph{is}
+significant. They are drawn immediately, the one occurring first is drawn
+first.
+%>@>
+
+
+\section{Technicalities}
+\label{sec:tech}
+
+The \lscsty{} package is in particular used to describe the semantics of LSCs
+which depends on the notion of atoms and cuts, i.e. sets of atoms.
+%
+There commands introduced in this section are mainly intended to be able to
+illustrate such descriptions. For example, to show the position of a cut.
+
+\subsection{Atoms}
+\label{sec:tech:atom}
+
+%<@<
+ \index{lscAtom@$\mlscAtom$}%
+ \index{lscLabelAtom@$\mlscLabelAtom$}%
+ \index{lscLabelAtomAt@$\mlscLabelAtomAt$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscAtom%
+ \param{\var{id}}%
+\newline
+\mlscLabelAtomAt%
+ \param{\var{angle}}%
+ \param{\var{id}}%
+ \param{\var{label}}%
+\newline
+\mlscLabelAtom%
+ \optparam{\underline{\this{$\mra$}}\orthat{$\mrb$}\orthat{$\mla$}\orthat{$\mlb$}}%
+ \param{\var{id}}%
+ \param{\var{label}}%
+}}\end{center}
+
+The \mlscAtom{} command marks the (atom(s) at the) current location with a
+dashed circle and equips it with an identity \var{id}.
+%
+This identity may then be used to label the
+ \index{atom mark}%
+atom mark.
+
+The command \mlscLabelAtomAt{} puts the \var{label} at position \var{angle}
+relative to the atom mark with identity \var{id}.
+
+The command \mlscLabelAtom{} is a shortcut for the most common angles.
+%
+ \index{ra@$\mra$}
+The default is $-45$ degrees (\mra{} (right above)), the other options are
+ \index{rb@$\mrb$}
+ \index{la@$\mla$}
+$-135$ degrees (\mrb{} (right below)), $45$ degrees (\mla{} (left above)), and
+ \index{lb@$\mlb$}
+$135$ degrees (\mlb{} (left below)).
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.5}
+ \lscAtom{aa}
+ \lscLine{hot}{1.5}
+ \lscAtom{ab}
+ \lscLine{hot}{1}
+ \lscAtom{ac}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscLabelAtom{ab}{right above}
+ \lscLabelAtomAt{93}{ac}{other}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{4}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAtom{aa}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAtom{ab}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscAtom{ac}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscLabelAtom{ab}{right above}
+ \lscLabelAtomAt{93}{ac}{other}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Cuts}
+\label{sec:tech:cut}
+
+%<@<
+ \index{lscCut@$\mlscCut$}%
+ \index{lscSetCutColour@$\mlscSetCutColour$}%
+ \index{lscSetCutLinestyle@$\mlscSetCutLinestyle$}%
+ \index{lscSetCutWidth@$\mlscSetCutWidth$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscCut%
+\newline
+\mlscSetCutColour%
+ \param{\var{colour}}%
+\newline
+\mlscSetCutLinestyle%
+ \param{\var{linestyle}}%
+\newline
+\mlscSetCutWidth%
+ \param{\var{length}}%
+}}\end{center}
+
+The \mlscCut{} atomic command draws a vertical line at the current position
+indicating the location of the
+ \index{cut}%
+cut on the current instance line. The line is connected to the last existing
+cut on the left.
+%
+There shall not be more than one \mlscCut{} command per instance line.
+
+The command \mlscSetCutColour{} sets the colour to the colour name
+\var{colour} (default: red), \mlscSetCutLinestyle{} sets the line style to
+\var{linestyle} (default: solid), and \mlscSetCutWidth{} sets the width to
+\var{length} (default: 3pt).
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscAsynSnd{e}%
+ \lscCut%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscCut%
+ \lscLine{hot}{2}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.49\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscCut%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscAsynSnd{e}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscCut%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}%
+ \lscAsynRcv{e}%
+ \psset{linecolor=red}
+ \end{coregion}
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ \lscAsyn{e}{hot}{E}%
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+ \index{lscNamedCut@$\mlscNamedCut$}%
+ \index{lscSetNamedCutColour@$\mlscSetNamedCutColour$}%
+ \index{lscSetNamedCutLinestyle@$\mlscSetNamedCutLinestyle$}%
+ \index{lscSetNamedCutWidth@$\mlscSetNamedCutWidth$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscNamedCut%
+ \param{\var{id}}%
+\newline
+\mlscSetNamedCutColour%
+ \param{\var{id}}%
+ \param{\var{colour}}%
+\newline
+\mlscSetNamedCutLinestyle%
+ \param{\var{id}}%
+ \param{\var{linestyle}}%
+\newline
+\mlscSetNamedCutWidth%
+ \param{\var{id}}%
+ \param{\var{length}}%
+}}\end{center}
+
+To allow
+ \index{cut!multiple}%
+multiple cuts in a single LSC, there is a corresponding set of commands for
+ \index{cut!named}%
+named cuts.
+%
+They take an \var{id} as first parameter.
+
+If not set explicitly, the colour, line style, and width of named cuts is
+inherited from the general cut colour, line style, and width as set by
+\mlscSetCutColour{}, \mlscSetCutLinestyle{}, and \mlscSetCutWidth{}.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \lscSetCutColour{lightgray}
+ \lscSetNamedCutWidth{Xb}{1.5pt}
+ \lscSetNamedCutColour{Xc}{green}
+ \lscSetNamedCutColour{Xb}{blue}
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscNamedCut{Xa}%
+ \lscLine{hot}{0.95}%
+ \lscNamedCut{Xb}%
+ \lscLine{hot}{0.05}
+ \lscAsynSnd{e}%
+ \lscLine{hot}{0.05}
+ \lscNamedCut{Xc}%
+ \lscLine{hot}{1.45}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscNamedCut{Xa}%
+ \lscLine{hot}{0.05}%
+ \lscNamedCut{Xb}%
+ \lscLine{hot}{1.95}%
+ \lscNamedCut{Xc}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\begin{verbatim}
+\lscSetCutColour{lightgray}
+\lscSetNamedCutWidth{Xb}{1.5pt}
+\lscSetNamedCutColour{Xc}{green}
+\lscSetNamedCutColour{Xb}{blue}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xa}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.95}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xb}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.05}
+ \lscAsynSnd{e}%
+ \lscLine{hot}{0.05}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xc}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.45}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xd}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xa}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.05}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xb}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.95}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xc}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscAsynRcv{e}%
+ \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscNamedCut{Xd}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ \lscAsyn{e}{hot}{E}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+To avoid cuts to hide each other, one will typically add very short instance
+line segments in between as shown in the example above.
+
+\medskip
+
+Using line style `none' one can easily obtain an animation effect as shown in
+the following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.35\textwidth}
+ \newcommand{\lscanim}[1]{%
+ \lscSetCutLinestyle{none}%
+ \lscSetNamedCutLinestyle{#1}{solid}%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscNamedCut{Xa}%
+ \lscLine{hot}{1}%
+ \lscNamedCut{Xb}%
+ \lscNamedCut{Xc}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{1.5}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscNamedCut{Xa}%
+ \lscNamedCut{Xb}%
+ \lscLine{hot}{2}%
+ \lscNamedCut{Xc}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \end{Lsc}}
+ %
+ \scalebox{0.7}{\lscanim{Xa}}
+ \\[\bigskipamount]
+ \scalebox{0.7}{\lscanim{Xb}}
+ \\[\bigskipamount]
+ \scalebox{0.7}{\lscanim{Xc}}
+ \\[\bigskipamount]
+ \scalebox{0.7}{\lscanim{Xd}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\begin{verbatim}
+\newcommand{\lscanim}[1]{%
+ \lscSetCutLinestyle{none}%
+ \lscSetNamedCutLinestyle{#1}{solid}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscNamedCut{Xa}%
+ \lscLine{hot}{1}%
+ \lscNamedCut{Xb}%
+ \lscNamedCut{Xc}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{1.5}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscNamedCut{Xa}%
+ \lscNamedCut{Xb}%
+ \lscLine{hot}{2}%
+ \lscNamedCut{Xc}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{0.5}%
+ \lscNamedCut{Xd}%
+ \lscLine{hot}{0.5}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \end{Lsc}}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\lscanim{Xa}\lscanim{Xb}
+\lscanim{Xc}\lscanim{Xd}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Putting Stuff at the Current Location}
+\label{sec:tech:put}
+
+%<@<
+ \index{lscPut@$\mlscPut$}%
+\begin{center}\fbox{
+\mlscPut%
+ \param{\var{stuff}}%
+}\end{center}
+
+The \mlscPut{} command typesets \var{stuff} at the current location.
+%
+This is useful to put additional labels or elements for which there is no
+explicit support.
+
+We use \mlscPut{}, for example, to draw the dashed frames indicating the
+location dimensions in Figure~\ref{fig:locdim}.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1.5}
+ \lscPut{%
+ \psline{<-}(0.5,0.5)%
+ \rput[lb](0.5,0.5){You are here.}}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.575\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+ \begin{lscinst}{Inst}
+ \lscLine{hot}{1.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscPut{%
+ \psline{<-}(0.5,0.5)%
+ \rput[lb](0.5,0.5){You are here.}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Typesetting Play-Engine LSCs}
+\label{sec:pipo}
+
+As mentioned in the introduction, \lscsty{} in general renders LSC in the
+ \index{style}%
+style of \cite{Klose2003}.
+%
+But it provides a couple of commands which support the typesetting of LSCs in
+the
+ \index{style!play-engine}%
+play-engine style.
+
+In cases where the play-engine style is not supported, it may be sufficient to
+modify the existing elements, for example, by manually adding an hourglass to
+an action box to represent the saving of a timer.
+
+\subsection{Actors, Clocks, and Environments}
+\label{sec:pipo:actor}
+\label{sec:pipo:clock}
+\label{sec:pipo:env}
+
+%<@<
+ \index{lscActor@$\mlscActor$}%
+ \index{lscClock@$\mlscClock$}%
+ \index{lscEnv@$\mlscEnv$}%
+\begin{center}\fbox{\parbox{5em}{%
+\mlscActor%
+\newline
+\mlscClock%
+\newline
+\mlscEnv%
+}}\end{center}
+
+The \mlscActor{}, \mlscClock{}, and \mlscEnv{} draw the symbols which are used
+to mark the
+ \index{instance line!actor}%
+ \index{actor}%
+actor,
+ \index{instance line!clock}%
+ \index{clock}%
+clock, and
+ \index{instance line!environment}%
+ \index{environment}%
+environment instance line.
+%
+They are best used as the label of a \mnoboxSD{} instance.
+
+\begin{center}%<@<
+\begin{minipage}{0.4\textwidth}
+ \scalebox{0.9}{%
+ \pssetlength{\lscLocationWidth}{1.75}%
+ \begin{Lsc}{none}{3}{3}
+ \begin{lscinst}[noboxSD]{\lscActor}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}[noboxSD]{\lscClock}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}[noboxSD]{\lscEnv}
+ \lscEnvLine{cold}{3}
+ \end{lscinst}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{3}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{lscinst}[noboxSD]{\lscActor}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{lscinst}[noboxSD]{\lscClock}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+ \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \begin{lscinst}[noboxSD]{\lscEnv}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscEnvLine{cold}{3}
+ \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Existential Symbolic Instances}
+\label{sec:pipo:inst}
+
+%<@<
+ \index{lscBalloon@$\mlscBalloon$}%
+\begin{center}\fbox{%
+\mlscBalloon%
+ \param{\this{$\mexistential$}\orthat{$\muniversal$}}%
+ \param{\var{stuff}}%
+}\end{center}
+
+The \mlscBalloon{} command draws
+ \index{balloon}%
+ \index{think balloon}%
+think balloons that are used to provide
+ \index{binding expression}%
+binding expressions of
+ \index{symbolic instance}%
+symbolic instances.
+
+They have to be explicitly positioned using, e.g., \cmd{lscPut} and one has to
+care for vertical space before the LSC as they are not considered in the
+computation of the boundary box.
+%
+That is, symbolic instances can at best be called semi-supported.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}[esymMSC]{esymMSC}
+ \lscPut{%
+ \rput(0,0.9){\lscBalloon{existential}{.ID$=$ID}}}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \begin{lscinst}[esymSD]{esymSD}
+ \lscPut{%
+ \rput(0,0.9){\lscBalloon{universal}{.Alloc$> 0$}}}
+ \lscLine{hot}{3}
+ \end{lscinst}
+ \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.5\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \begin{lscinst}[esymMSC]{esymMSC}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscPut{\rput(0,0.9){%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscBalloon%
+ {existential}{.ID$=$ID}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lscinst}
+ \begin{lscinst}[esymSD]{esymSD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscPut{\rput(0,0.9){%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscBalloon%
+ {universal}{.Alloc$> 0$}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+ \end{lscinst}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+The combination on the right above is not a well-formed LSC instance. It is
+only used to demonstrate both kinds of loops in the same figure.
+%>@>
+
+\subsection{Branching, Subcharts, and Loops}
+\label{sec:pipo:scopes}
+
+%<@<
+Both
+ \index{branch}%
+branching and
+ \index{loop}%
+loops are based on
+ \index{subchart}%
+subcharts.
+%
+Subcharts are not directly supported but can be simulated by putting frames
+using \mlscPut{}.
+
+\begin{center}%<@<
+\pssetlength{\lscLocationWidth}{2}%
+\begin{minipage}{0.30\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{3}{4}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1.5}
+ \lscInstSnd{e}
+ \lscLine{hot}{1}
+ \lscInstSnd{f}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.5}
+ \lscCond{hot}{$j = 0$}
+ \lscLine{hot}{1}
+ \lscInstRcv{e}
+ \lscLine{hot}{0.5}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (0.5\lscLocationWidth,1.5\lscLocationHeight)}
+ \lscLine{hot}{0.5}
+ \lscInstRcv{f}
+ \lscLine{hot}{0.5}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (0.5\lscLocationWidth,1\lscLocationHeight)}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}
+ \lscInst{f}{hot}{F}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.685\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{4}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1.5}\lscInstSnd{e}
+ \lscLine{hot}{1}\lscInstSnd{f}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{0.5}
+ \lscCond{hot}{$j = 0$}
+ \lscLine{hot}{1}\lscInstRcv{e}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (0.5\lscLocationWidth,1.5\lscLocationHeight)}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{0.5}\lscInstRcv{f}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (0.5\lscLocationWidth,1\lscLocationHeight)}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}\lscInst{f}{hot}{F}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+\begin{center}%<@<
+\pssetlength{\lscLocationWidth}{2}%
+\begin{minipage}{0.30\textwidth}
+ \scalebox{0.9}{%
+ \begin{Lsc}{none}{3}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1.5}
+ \lscInstSnd{e}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1.5}
+ \lscInstRcv{e}
+ \lscLine{hot}{0.5}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (0.5\lscLocationWidth,1.5\lscLocationHeight)%
+ \rput[lt](-1.5\lscLocationWidth,%
+ 1.5\lscLocationHeight){%
+ \rput(0.3,-0.3){\textbf{3}}}}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}
+ \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.685\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1.5}\lscInstSnd{e}
+ \lscLine{hot}{1.5}
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{1.5}\lscInstRcv{e}
+ \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+ \lscPut{\psframe[dimen=inner]%
+ (-1.5\lscLocationWidth,0)%
+ (.5\lscLocationWidth,1.5\lscLocationHeight)
+ \rput[lt](-1.5\lscLocationWidth,%
+ 1.5\lscLocationHeight){%
+ \rput(0.3,-0.3){\textbf{3}}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+ \lscLine{hot}{1}
+ \end{lscinst}
+ \lscInst{e}{hot}{E}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Tricks and Tweaks}
+\label{sec:tricks}
+
+\subsection{Linewidth}
+\label{sec:tricks:lines}
+
+%<@<
+All parts of the LSC (except for cuts) are rendered with the current
+\pstricks{}
+ \index{linewidth}%
+linewidth.
+%
+That it, if the lines appear too
+ \index{fat}%
+fat they can be globally be changed using
+\cmd{psset}.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}
+ \scalebox{0.9}{%
+ \psset{linewidth=0.25pt}
+ \begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ %
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ %
+ \lscAsyn{e}{hot}{E}%
+ \end{Lsc}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.35\textwidth}%
+\small%
+{\begin{verbatim}
+\psset{linewidth=0.25pt}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+ \begin{lscinst}{Inst1}
+ \lscLine{hot}{1}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{2}%
+ \end{lscinst}
+ \begin{lscinst}{Inst2}
+ \lscLine{hot}{2}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{1}%
+ \end{lscinst}
+ \lscAsyn{e}{hot}{E}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Scaling}
+\label{sec:tricks:scaling}
+
+%<@<
+LSCs can be
+ \index{scale}%
+scaled by changing the width and height of locations (cf.
+Section~\ref{sec:inst:dim}) keeping the size of text.
+%
+To scale the LSC including all annotations, the \mFullLsc{} and \mLsc{}
+environments can be passed to a
+ \index{scalebox}%
+\cmd{scalebox} command.
+
+\begin{center}%<@<
+\begin{minipage}{0.35\textwidth}
+ \centering
+ \newcommand{\scalex}{%
+ \begin{Lsc}{none}{2}{3.5}
+ \begin{lscinst}{$i_1$}
+ \lscLine{hot}{1}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{2.5}%
+ \end{lscinst}
+ \begin{lscinst}{$i_2$}
+ \lscLine{hot}{2}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ \lscAsyn{e}{hot}{$E$}%
+ \end{Lsc}
+ }
+
+ {\pssetlength{\lscLocationWidth}{2}
+ \pssetlength{\lscLocationHeight}{0.666}
+ \scalex}%
+
+ \bigskip
+ {\pssetlength{\lscLocationWidth}{1.5}
+ \pssetlength{\lscLocationHeight}{0.5}
+ \scalex}%
+
+ \bigskip
+ {\pssetlength{\lscLocationWidth}{1}
+ \pssetlength{\lscLocationHeight}{0.333}
+ \scalex}%
+
+ \bigskip
+ \scalebox{0.5}{\scalex}
+\end{minipage}
+\hfill
+\begin{minipage}{0.535\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\newcommand{\scalex}{%
+ \begin{Lsc}{none}{2}{3.5}
+ \begin{lscinst}{$i_1$}
+ \lscLine{hot}{1}%
+ \lscAsynSnd{e}%
+ \lscLine{hot}{2.5}%
+ \end{lscinst}
+ \begin{lscinst}{$i_2$}
+ \lscLine{hot}{2}%
+ \lscAsynRcv{e}%
+ \lscLine{hot}{1.5}%
+ \end{lscinst}
+ \lscAsyn{e}{hot}{$E$}%
+ \end{Lsc}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+
+{\pssetlength{\lscLocationWidth}{2}
+\pssetlength{\lscLocationHeight}{0.666}
+\scalex}%
+
+{\pssetlength{\lscLocationWidth}{1.5}
+\pssetlength{\lscLocationHeight}{0.5}
+\scalex}%
+
+{\pssetlength{\lscLocationWidth}{1}
+\pssetlength{\lscLocationHeight}{0.333}
+\scalex}%
+
+\scalebox{0.5}{\scalex}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\printindex
+
+\bibliographystyle{alpha}
+\bibliography{lsc}
+
+\clearpage
+\appendix
+\section*{License}
+
+This work may be distributed and/or modified under the conditions of the
+\LaTeX{} Project Public License, either version 1.3 of this license or (at
+your option) any later version.
+
+The latest version of this license is in
+%
+\begin{quote}
+\tt http://www.latex-project.org/lppl.txt
+\end{quote}
+%
+and version 1.3 or later is part of all distributions of \LaTeX{} version
+2005/12/01 or later.
+%
+This work has the LPPL maintenance status `maintained'.
+
+The Current Maintainer of this work is the copyright holder.
+%
+This work consists of the files README, lsc.sty, lsc.tex, lsc.bib.
+
+\medskip
+
+In addition, all examples from this manual may of course be freely used,
+modified, copied, and distributed in whole or partly.
+
+\end{document}
+vim:foldmethod=marker commentstring=%%s foldmarker=<@<,>@>