% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
% $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=<@<,>@>