new (latex) package lsc (23feb06)

git-svn-id: svn://tug.org/texlive/trunk@1908 c570f23f-e606-0410-a88d-b1316a301751

9 files changed, 6082 insertions, 1 deletions

diff --git a/Build/tools/tpm-ctan-check b/Build/tools/tpm-ctan-check
index 077777b48b8..9fc6132fbc5 100755
--- a/Build/tools/tpm-ctan-check
+++ b/Build/tools/tpm-ctan-check
@@ -54,7 +54,7 @@ sub main
        jneurosci juramisc
        koma-script
        l2picfaq l2tabu-english
-         labelcas ledmac lewis lfb lh linearA lineno listings
+         labelcas ledmac lewis lfb lh linearA lineno listings lsc
          lshort-bulgarian lshort-dutch lshort-english
          lshort-finnish lshort-french  lshort-german 
          lshort-italian lshort-japanese lshort-korean 
diff --git a/Master/texmf-dist/bibtex/bib/lsc/lsc.bib b/Master/texmf-dist/bibtex/bib/lsc/lsc.bib
new file mode 100644
index 00000000000..355652be760
--- /dev/null
+++ b/Master/texmf-dist/bibtex/bib/lsc/lsc.bib
@@ -0,0 +1,108 @@
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+% $Id: lsc.bib,v 1.2 2006/02/23 12:57:15 berndw Exp $
+%
+% Bibliography to the lsc.sty manual.
+% 
+% Author: Bernd Westphal <westphal at 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.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+@article{DammHarel2001,
+  author       = "Werner Damm and David Harel",
+  title        = "{LSC}s: Breathing Life into Message Sequence Charts",
+  year         = "2001",
+  month        = jul,
+  journal      = "Formal Methods in System Design",
+  volume       = 19,
+  number       = 1,
+  pages        = "45--80",
+  x-topics     = "lsc"
+}
+
+@book{ITU-T1993,
+  author       = {ITU-T},
+  title        = {{ITU-T R}ecommendation {Z}.120: {M}essage {S}equence {C}hart ({MSC})},
+  year         = "1999",
+  url          = "-",
+  publisher    = {ITU-T},
+  x-topics     = "msc standard"
+}
+
+@phdthesis{Klose2003,
+  author       = "Jochen Klose",
+  title        = "Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior",
+  year         = "2003",
+  school       = {Carl von Ossietzky Universit\"{a}t Oldenburg},
+  x-topics     = "lsc spec diss"
+}
+
+@book{HarelMarelly2003,
+  author       = "David Harel and Rami Marelly",
+  title        = "Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine",
+  year         = "2003",
+  url          = "-",
+  publisher    = "Springer-Verlag",
+  x-topics     = "lsc playinplayout"
+}
+
+@inproceedings{KloseWestphal2002,
+  author       = "Jochen Klose and Bernd Westphal",
+  title        = "Relating {LSC} Specifications to {UML} Models",
+  year         = "2002",
+  pages        = "130--137",
+  url          = "-",
+  crossref     = "ProcINT2002",
+  x-topics     = "lsc"
+}
+
+@proceedings{ProcINT2002,
+  editor       = {Hartmut Ehrig and Martin Grosse-Rhode},
+  booktitle    = "Proceedings of the Workshop Integration of Software Specification Techniques, INT'02",
+  month        = apr,
+  year         = 2002
+}
+
+@article{DammWestphal2005,
+  author       = "Werner Damm and Bernd Westphal",
+  title        = {Live and Let Die: {LSC}-based Verification of {UML}-Models},
+  year         = "2005",
+  journal      = "Science of of Computer Programming",
+  volume       = "55",
+  number       = "1--3",
+  month        = mar,
+  pages        = "117--159",
+  x-topics     = "umlverif sym lsc"
+}
+
+@article{MauwBos2001,
+  author       = "Sjouke Mauw and Victor Bos",
+  title        = {Drawing {M}essage {S}equence {C}harts with {\LaTeX}},
+  year         = "2001",
+  url          = "ftp://ftp.win.tue.nl/pub/techreports/sjouke/tbmsc.ps.Z",
+  journal      = {TUGBoat},
+  volume       = 22,
+  number       = {1-2},
+  pages        = {87--92},
+  month        = {March/June},
+  x-pardate    = "Wed Dec 28 18:50:28 MET 2005",
+  x-topics     = "msc latex"
+}
+
diff --git a/Master/texmf-dist/doc/latex/lsc/README b/Master/texmf-dist/doc/latex/lsc/README
new file mode 100644
index 00000000000..ae5f6fad9c0
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/README
@@ -0,0 +1,13 @@
+
+This package is similar to the 'msc' package in that it provides
+macros for typesetting a variant of sequence diagrams, in this
+case the Live Sequence Charts of Damm and Harel.
+
+It supports the full LSC language of the original LSC paper, the
+Klose-extensions for formal verification and some of the Harel-
+extensions for the Play-In/Play-Out approach (cf. the manual).
+
+This material is subject to the LaTeX Project Public License. See
+http://www.ctan.org/tex-archive/help/Catalogue/licenses.lppl.html
+for the details of that license.
+
diff --git a/Master/texmf-dist/doc/latex/lsc/lsc.pdf b/Master/texmf-dist/doc/latex/lsc/lsc.pdf
new file mode 100644
index 00000000000..a1643042fdb
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/lsc.pdf
diff --git a/Master/texmf-dist/doc/latex/lsc/lsc.tex b/Master/texmf-dist/doc/latex/lsc/lsc.tex
new file mode 100644
index 00000000000..d4c9d8837b1
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lsc/lsc.tex
@@ -0,0 +1,3956 @@
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+% $Id: lsc.tex,v 1.17 2006/02/23 12:57:15 berndw Exp $
+%
+% User's manual for lsc.sty.
+% 
+% Author: Bernd Westphal <westphal@informatik.uni-oldenburg.de> 
+% 
+% Copyright (c) 2005-2006 Bernd Westphal.  All rights reserved.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+%
+% This work may be distributed and/or modified under the conditions of
+% the LaTeX Project Public License, either version 1.3 of this license
+% or (at your option) any later version.
+% The latest version of this license is in
+%   http://www.latex-project.org/lppl.txt
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+% 
+% The Current Maintainer of this work is the copyright holder.
+%
+% This work consists of the files README, lsc.sty, lsc.tex, lsc.bib.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+\documentclass{article}
+
+\usepackage{makeidx}
+\usepackage{lsc}
+
+\title{\texttt{lsc.sty} -- Typesetting Live Sequence Charts}
+\author{Bernd Westphal}
+
+\newsavebox{\bsbox}%<@<
+\newcommand{\bs}{\usebox{\bsbox}}
+\newsavebox{\lcbbox}
+\newcommand{\lcb}{\usebox{\lcbbox}}
+\newsavebox{\rcbbox}
+\newcommand{\rcb}{\usebox{\rcbbox}}
+\newsavebox{\lbbox}
+\newcommand{\lb}{\usebox{\lbbox}}
+\newsavebox{\rbbox}
+\newcommand{\rb}{\usebox{\rbbox}}
+%
+\newcommand{\AT}{@}
+%
+\newcommand{\env}[1]{\texttt{#1}}
+\newcommand{\cmd}[1]{\bs\texttt{#1}}
+\newcommand{\con}[1]{%
+  \ifmmode{\texttt{#1}}\else{`\texttt{#1}'}\fi}
+\newcommand{\sty}[1]{\texttt{#1.sty}}
+%
+\newcommand{\lscsty}{\sty{lsc}}
+%
+%
+\newcommand{\mbegin}[1]{\bs\texttt{begin}\lcb\texttt{#1}\rcb}
+\newcommand{\mend}[1]{\bs\texttt{end}\lcb\texttt{#1}\rcb}
+%
+\newcommand{\mlscActor}{\cmd{lscActor}}
+\newcommand{\mlscAct}{\cmd{lscAct}}
+\newcommand{\mlscAsynRcv}{\cmd{lscAsynRcv}}
+\newcommand{\mlscAsynSnd}{\cmd{lscAsynSnd}}
+\newcommand{\mlscAsyn}{\cmd{lscAsyn}}
+\newcommand{\mlscAtom}{\cmd{lscAtom}}
+\newcommand{\mlscBalloon}{\cmd{lscBalloon}}
+\newcommand{\mlscClock}{\cmd{lscClock}}
+\newcommand{\mlscCond}{\cmd{lscCond}}
+\newcommand{\mlscCreate}{\cmd{lscCreate}}
+\newcommand{\mlscCut}{\cmd{lscCut}}
+\newcommand{\mlscEnvLine}{\cmd{lscEnvLine}}
+\newcommand{\mlscEnv}{\cmd{lscEnv}}
+\newcommand{\mlscFooterHeightFactor}{\cmd{lscFooterHeightFactor}}
+\newcommand{\mlscInstRcv}{\cmd{lscInstRcv}}
+\newcommand{\mlscInstSnd}{\cmd{lscInstSnd}}
+\newcommand{\mlscInst}{\cmd{lscInst}}
+\newcommand{\mlscKill}{\cmd{lscKill}}
+\newcommand{\mlscLabelAtomAt}{\cmd{lscLabelAtomAt}}
+\newcommand{\mlscLabelAtom}{\cmd{lscLabelAtom}}
+\newcommand{\mlscLine}{\cmd{lscLine}}
+\newcommand{\mlscLocationHeight}{\cmd{lscLocationHeight}}
+\newcommand{\mlscLocationWidth}{\cmd{lscLocationWidth}}
+\newcommand{\mlscLocinvBegin}{\cmd{lscLocinvBegin}}
+\newcommand{\mlscLocinvEnd}{\cmd{lscLocinvEnd}}
+\newcommand{\mlscLocinvOffset}{\cmd{lscLocinvOffset}}
+\newcommand{\mlscLocinvStart}{\cmd{lscLocinvStart}}
+\newcommand{\mlscLocinv}{\cmd{lscLocinv}}
+\newcommand{\mlscNamedCut}{\cmd{lscNamedCut}}
+\newcommand{\mlscPut}{\cmd{lscPut}}
+\newcommand{\mlscSetCutColour}{\cmd{lscSetCutColour}}
+\newcommand{\mlscSetCutLinestyle}{\cmd{lscSetCutLinestyle}}
+\newcommand{\mlscSetCutWidth}{\cmd{lscSetCutWidth}}
+\newcommand{\mlscSetNamedCutColour}{\cmd{lscSetNamedCutColour}}
+\newcommand{\mlscSetNamedCutLinestyle}{\cmd{lscSetNamedCutLinestyle}}
+\newcommand{\mlscSetNamedCutWidth}{\cmd{lscSetNamedCutWidth}}
+\newcommand{\mlscTimeout}{\cmd{lscTimeout}}
+\newcommand{\mlscTimerReset}{\cmd{lscTimerReset}}
+\newcommand{\mlscTimerSet}{\cmd{lscTimerSet}}
+\newcommand{\mlscWidecondOff}{\cmd{lscWidecondOff}}
+\newcommand{\mlscWidecondOn}{\cmd{lscWidecondOn}}
+\newcommand{\mlscWidecond}{\cmd{lscWidecond}}
+%
+\newcommand{\mFullLsc}{\env{FullLsc}}
+\newcommand{\mLsc}{\env{Lsc}}
+\newcommand{\mcoregion}{\env{coregion}}
+\newcommand{\mlsccreateinst}{\env{lsccreateinst}}
+\newcommand{\mlscinst}{\env{lscinst}}
+\newcommand{\msimregion}{\env{simregion}}
+%
+\newcommand{\mhot}{\con{hot}}%
+\newcommand{\mcold}{\con{cold}}%
+%
+\newcommand{\ml}{\con{l}}%
+\newcommand{\mr}{\con{r}}%
+%
+\newcommand{\mra}{\con{ra}}%
+\newcommand{\mrb}{\con{rb}}%
+\newcommand{\mla}{\con{la}}%
+\newcommand{\mlb}{\con{lb}}%
+%
+\newcommand{\mb}{\con{b}}%
+\newcommand{\mf}{\con{f}}%
+%
+\newcommand{\mincl}{\con{incl}}%
+\newcommand{\mexcl}{\con{excl}}%
+%
+\newcommand{\mnoboxSD}{\con{noboxSD}}%
+\newcommand{\mSD}{\con{SD}}%
+\newcommand{\mMSC}{\con{MSC}}%
+\newcommand{\mesymSD}{\con{esymSD}}%
+\newcommand{\mesymMSC}{\con{esymMSC}}%
+%
+\newcommand{\muniversal}{\con{universal}}%
+\newcommand{\mexistential}{\con{existential}}%
+\newcommand{\mnone}{\con{none}}%
+%
+\newcommand{\mempty}{\con{}}%
+\newcommand{\mweak}{\con{weak}}%
+\newcommand{\mpermissive}{\con{permissive}}%
+\newcommand{\mstrict}{\con{strict}}%
+%
+\newcommand{\minitial}{\con{initial}}%
+\newcommand{\minvariant}{\con{invariant}}%
+\newcommand{\miterative}{\con{iterative}}%
+%
+%
+\newcommand{\pstricks}{\texttt{pstricks}}
+%
+\newcommand{\optparam}[1]{\lb{#1}\rb}
+\newcommand{\param}[1]{\lcb{#1}\rcb}
+\newcommand{\var}[1]{\textit{#1}}
+\newcommand{\this}[1]{\texttt{#1}}
+\newcommand{\orthat}[1]{$\,\mid\,$\texttt{#1}}%>@>
+
+\makeindex
+
+\begin{document}
+
+\maketitle
+
+\tableofcontents
+
+\begin{lrbox}{\bsbox}\verb"\"\end{lrbox}%<@<
+\begin{lrbox}{\lcbbox}\verb"{"\end{lrbox}
+\begin{lrbox}{\rcbbox}\verb"}"\end{lrbox}
+\begin{lrbox}{\lbbox}\verb"["\end{lrbox}
+\begin{lrbox}{\rbbox}\verb"]"\end{lrbox}%>@>
+
+\section{Introduction}
+\label{sec:intro}
+
+%<@<
+The \lscsty{} package provides means to typeset 
+  \index{Live Sequence Charts}%
+Live Sequence Charts.
+%
+The Live Sequence Charts (LSC) language is a variant of 
+  \index{Message Sequence Charts|see{MSC}}%
+  \index{MSC}%
+Message Sequence Charts (MSC)~\cite{ITU-T1993}.
+%
+It's intended use is as a language to formalise requirements on the
+communication in a (software or hardware) system under design.
+%
+The basic difference to MSCs is the addition of modalities to the elements of
+a chart to distinguish
+  \index{mandatory}%
+\emph{mandatory} from
+  \index{possible}%
+\emph{possible} behaviour.
+%
+For example, locations on instance lines can be
+  \index{hot}%
+\emph{hot} to indicate that 
+  \index{progress}%
+progress is required to satisfy the LSC 
+  \index{liveness}%
+(liveness) or 
+  \index{cold}%
+\emph{cold} to indicate that behaviour without progress is acceptable.
+%
+This is where the LSC language gets its name from.
+%>@>
+
+\subsection{Supported LSC Language}
+
+%<@<
+For further information on the original syntax, semantics, and pragmatics of
+the LSC language see:
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{DammHarel2001}]
+  Werner Damm and David Harel,
+  \emph{{LSC}s: Breathing Life into Message Sequence Charts},
+  Formal Methods in System Design, 19(1):45--80, July 2001.
+\end{description}
+\end{quote}
+%
+The LSC language presented in this publication is (up to minor deviations in
+  \index{style}%
+style) fully supported by \lscsty{}.
+
+\medskip
+
+From the original language, two 
+  \index{dialects}%
+  \index{LSC dialects}%
+dialects emerged, each of them tailored for a
+particular use of an LSC specification, i.e. a collection of single charts.
+%
+The dialect presented in
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{Klose2003}]
+  Jochen Klose,
+  \emph{Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behaviour},
+  PhD thesis, {Carl von Ossietzky Universit\"{a}t Oldenburg}, 2003.
+\end{description}
+\end{quote}
+%
+considers LSCs as the requirements specification language in a classical
+  \index{development process}%
+development process where the system implementation is finally tested to
+satisfy the requirements or, possibly better, a system \emph{model} is
+  \index{formal verification}%
+formally verified to satisfy the requirements.
+
+To this end, the author added 
+  \index{timer}%
+timers and 
+  \index{timing interval}%
+timing intervals (also taken from MSCs), 
+  \index{local invariant}%
+local invariants to state requirements on spans of time in contrast to
+conditions which apply only to single points of time, three 
+  \index{activation mode}%
+activation modes, and two 
+  \index{interpretation}%
+interpretations, but doesn't support 
+  \index{scope}%
+scopes.
+%
+The articles
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{KloseWestphal2002}]
+  Jochen Klose and Bernd Westphal,
+  \emph{Relating {LSC} Specifications to {UML} Models},
+  In: Hartmut Ehrig and Martin Gro\ss{}e-Rhode (Eds.),
+  Proceedings of the Workshop Integration of Software Specification Techniques (INT'02),
+  pages 130--137, April 2002.
+\item[\cite{DammWestphal2005}]
+  Werner Damm and Bernd Westphal,
+  \emph{Live and Let Die: {LSC}-based Verification of {UML}-Models},
+  Science of of Computer Programming,
+  55(1--3):117--159, March 2005.
+\end{description}
+\end{quote}
+%
+provide a further extension to so called 
+  \index{dynamic binding}%
+dynamic binding instance lines.
+
+The LSC language presented in these publications is (up to minor deviations in
+  \index{style}%
+style) fully supported by \lscsty{}.
+
+\medskip
+
+
+
+The dialect presented in
+%
+\begin{quote}
+\small
+\begin{description}
+\item[\cite{HarelMarelly2003}]
+  David Harel and Rami Marelly,
+  \emph{Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine},
+  Springer-Verlag, 2003.
+\end{description}
+\end{quote}
+%
+is tailored for an approach called 
+  \index{play-out}%
+play-out\emph{play-out}. 
+%
+In this approach, the LSC specification \emph{is} the implementation.  A tool
+called 
+  \index{play-engine}%
+play-engine interprets an LSC specification that has to be related to a
+GUI.  If the GUI is operated by a user, then the play-engine looks up its
+collection of LSCs and operates the GUI accordingly, thus interacts with a
+user.
+
+To this end, they added, for example, 
+  \index{actor instance line}%
+actor instance lines, 
+  \index{action}%
+actions to modify the system state and extended 
+  \index{scope}%
+scopes to 
+  \index{loop}%
+loops.
+%
+They independently also added 
+  \index{symbolic instances}%
+symbolic instances, means to handle 
+  \index{time}%
+time and to 
+  \index{exclude observations}%
+exclude observations by 
+  \index{forbidden elements}%
+forbidden elements, and two 
+  \index{interpretations}%
+interpretations.
+
+The LSC language presented in~\cite{HarelMarelly2003} is not fully supported
+by \lscsty, and if supported, features are rendered in the 
+  \index{style}%
+style and terminology of~\cite{Klose2003}.
+%
+Section~\ref{sec:pipo} discusses how \emph{some} constructs of this LSC
+dialect can although be typeset with some 
+  \index{manual intervention}%
+manual intervention using some special features \lscsty.
+%>@>
+
+\subsection{Typesetting MSCs and Sequence Diagrams}
+
+%<@<
+As LSCs are a derivative of MSCs as are 
+  \index{UML}%
+UML's 
+  \index{Sequence Diagram|see{SD}}%
+  \index{SD}%
+Sequence Diagrams (SDs), there is a 
+  \index{common sublanguage}%
+common sublanguage and MSCs or SDs from the common sublanguage may well be
+typeset using \lscsty.
+
+But note that there are no plans to extend \lscsty{} to full support of
+either language.
+%
+For MSCs, for example, there is an own \LaTeX{} style and SDs may finally be
+supported by styles for typesetting UML diagrams.
+%>@>
+
+\subsection{Related Styles}
+
+%<@<
+As soon as \lscsty{} reached some usable state -- of course -- it
+turned out that there exist \LaTeX{} packages for typesetting variants of
+sequence diagrams from which \lscsty{} could have been derived from.
+
+We briefly list and discuss the styles we're aware of in the following
+sections.
+
+\subsubsection{MSC}
+
+  \index{MSC}%
+Version 1.13 of the 
+  \index{msc@\sty{msc}}%
+msc\sty{msc} package%
+\footnote{
+  \small{\tt http://www.win.tue.nl/~sjouke/misc/mscpackage}
+}
+by
+  \index{Mauw@Mauw, S.}%
+S.  Mauw and 
+  \index{Bos@Bos, V.}%
+V. Bos~\cite{MauwBos2001} claims to support the full 
+  \index{MSC2000}%
+MSC2000 language.
+
+The most obvious difference is that \sty{msc} seems to be able to compute a 
+  \index{layout}%
+layout on its own, i.e. it only takes a description of the dependencies in the
+LSC, i.e. the user needn't give precise positioning commands while 
+  \index{manual intervention}%
+manual intervention is still possible.
+
+In contrast, \lscsty{} is more low level as it expects \emph{all} layout to be
+given by the user.
+
+\subsubsection{UML}
+
+  \index{UML}%
+  \index{SD}%
+For example, the 
+  \index{pst-uml@\sty{pst-uml}}%
+\sty{pst-uml} package%
+\footnote{
+  \small{\tt http://www.ensta.fr/~diam/latex/pst-uml/index.html}
+}
+by 
+  \index{Diamantini@Diamantini, M.}%
+M. Diamantini provides rudimentary support for UML sequence diagrams.
+%>@>
+
+
+\section{Preliminaries}
+\label{sec:pre}
+
+%<@<
+The macros provided by \lscsty{} can be divided into three 
+  \index{categories}%
+categories:
+%
+\begin{description}
+\item[Environments.]
+    \index{environment}%
+  The \mFullLsc{} and \mLsc{} environments draw LSC charts with and without
+  header, the \mlscinst{} and \mlsccreateinst{} environments draw instances
+  within LSCs, and the \mcoregion{} and \msimregion{} environments mark
+  coregions and simultaneous regions within instances.
+\item[Atomic Commands.]
+  \index{atomic command}%
+  \index{command!atomic}%
+  An atomic command directly draws an LSC element, instance line segment, or
+  annotation that is related to only a single location.
+  %
+  Examples are instance line segments, action boxes, or timer set/reset and
+  timeout.
+\item[Composite Commands.]
+  \index{composite command}%
+  \index{command!composite}%
+  Composite commands draw LSC elements that are related to more than one
+  location.  There are typically macros to set the locations which are used
+  within an instance line environment and one macro which finally draws the
+  element based on the set locations.
+  %
+  A typical example are the macros for messages which comprise one macro for
+  setting the sending location, one macro for setting the reception location,
+  and a macro which draws the message arrow.
+\end{description}
+
+\begin{figure}%<@< \label{fig:expl}
+\begin{center}
+\begin{minipage}{0.225\textwidth}
+  \makeatletter
+  \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{5.25}
+    \begin{lscinst}{\textit{Inst}}
+      \lscPut{\pnode(1.4,0.3){ibAA}}
+      \psaddtolength{\lsc@Y}{-0.25}
+      \lscLine{hot}{1.0}
+      \lscPut{\pnode(0.2,0.5){laAA}}
+      \psaddtolength{\lsc@Y}{-0.25}
+      \lscCond{hot}{\textit{Cond}}
+      \lscPut{\pnode(0.9,-0.25){cAA}}
+      \lscLine{cold}{0}
+      \psaddtolength{\lsc@Y}{-0.75}
+      \lscLine{cold}{2.0}
+      \lscPut{\pnode(0.2,0.5){lbAA}}
+      \psaddtolength{\lsc@Y}{-0.75}
+      \lscPut{\pnode(1.4,0.3){ieAA}}
+    \end{lscinst}
+  \end{Lsc}}
+  \makeatother%
+\end{minipage}%
+%
+\hfill%
+%
+\begin{minipage}{0.225\textwidth}
+  \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{{\it Inst}}
+      \lscPut{\pnode(-1.4,0.3){ibAB}}
+      \lscPut{\pnode(1.4,0.3){ibBA}}
+      \lscLine{hot}{1}
+      \lscPut{\pnode(-0.2,0.5){laAB}}
+      \lscPut{\pnode(0.2,0.5){laBA}}
+      \lscCond{hot}{{\it Cond}}
+      \lscPut{\pnode(-0.9,-0.25){cAB}}
+      \lscPut{\pnode(0.9,-0.25){cBA}}
+      \lscLine{cold}{2}
+      \lscPut{\pnode(-0.2,1){lbAB}}
+      \lscPut{\pnode(0.2,1){lbBA}}
+      \lscPut{\pnode(-1.4,0.3){ieAB}}
+      \lscPut{\pnode(1.4,0.3){ieBA}}
+    \end{lscinst}
+  \end{Lsc}}%
+\end{minipage}%
+%
+\hfill%
+%
+{%
+\pnode(0.25,0.85){ibBB}% before the minipage as it seems to add height
+\pnode(0.25,-0.75){ieBB}%
+\pnode(0.55,0.50){laBB}%
+\pnode(0.55,-0.35){lbBB}%
+\pnode(0.55,0.075){cBB}%
+%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{\it Inst}
+    \lscLine{hot}{1}
+    \lscCond{hot}{\it Cond}
+    \lscLine{cold}{2}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}
+\end{minipage}}%
+%
+\psset{linewidth=0.5pt,linestyle=dotted}%
+\ncline{ibAA}{ibAB}\ncline{ibBA}{ibBB}%
+\ncline{ieAA}{ieAB}\ncline{ieBA}{ieBB}%
+\ncline{laAA}{laAB}\ncline{laBA}{laBB}%
+\ncline{lbAA}{lbAB}\ncline{lbBA}{lbBB}%
+\ncline{cAA}{cAB}\ncline{cBA}{cBB}%
+\end{center}
+\caption{\small%
+  \index{exploded view}%
+  {\bf Exploded view} of a simple LSC.}
+\label{fig:expl}
+\end{figure}%>@>
+
+Figure~\ref{fig:expl} illustrates the drawing principle.
+%
+The LSC in the middle is the result of the source on the right.
+%
+To pinpoint the relation between commands and graphics, we provide an 
+  \index{exploded view}%
+exploded view on the left and connect graphics and text by dotted lines.
+
+In the example, the 
+  \index{Lsc@$\mLsc{}$}%
+\mLsc{} environment draws nothing as we use the
+  \index{none}%
+quantification 
+  \index{none@$\mnone{}$}%
+\mnone{} (which is special to \lscsty{} and not part of any LSC dialect) and
+have no prechart.
+%
+If we used 
+  \index{universal@$\muniversal{}$}%
+\muniversal{} or 
+  \index{existential@$\mexistential{}$}%
+\mexistential{}, then the \mLsc{} would draw the solid or dashed frame around
+the body and if we had a prechart, \mLsc{} would draw the large dashed 
+  \index{kandis}%
+kandis.%
+\footnote{
+  A \emph{kandis} is a giant sugar crystal which plays a role in East Frisian
+  tea ceremonies (first the kandis, then the tea, and then slowly and
+  carefully some cream).
+  %
+  From the side a kandis typically looks like a hexagon, i.e. like the shape
+  used for rendering conditions and pre-charts. 
+  %
+  Throughout this text, we use kandis to denote the hexagon shape.
+}
+But although it doesn't draw something, it defines the \env{pspicture}
+environment enclosing the LSC and thereby defines the 
+  \index{box boundary}%
+box boundary.
+%
+The size of the box is determined by the number of instance lines (1 in the
+example) and their height (3 
+  \index{pstricks units@\pstricks{} units}%
+\pstricks{} units in the example).
+
+Within the \mLsc{} environment, there is a single 
+  \index{lscinst@$\mlscinst{}$}%
+\mlscinst{} environment.
+%
+It takes one required argument, the instance name, and is responsible for
+drawing the instance head and footer.
+%
+A possible parameter controls the shape of the head and the footer (cf.
+Section~\ref{sec:inst}).
+
+Within the \mlscinst{} environment, there are only atomic commands in the
+example.
+%
+The 
+  \index{lscLine@$\mlscLine{}$}%
+\mlscLine{} command draws an instance line segment and advances vertical
+position by the segment length.
+%
+The first parameter is either 
+  \index{hot@$\mhot{}$}%
+\mhot{},
+  \index{cold@$\mcold{}$}%
+\mcold{},
+or 
+  \index{none@$\mnone{}$}%
+\mnone{} and gives the temperature (or mode) of the location at the beginning
+of the instance line segment (cf. Section~\ref{sec:line} for the pseudo-mode
+`\mnone{}').
+%
+The second parameter is the instance line segment length.  In the example, we
+use \pstricks{} units, but any length understood by \pstricks{} will do
+%
+(cf. Section~\ref{sec:line} for a discussion of environment instance line
+segments and their optional parameter for timing intervals).
+
+The 
+  \index{lscCond@$\mlscCond$}%
+\mlscCond{} command draws a condition restricted to a single instance line,
+also called 
+  \index{narrow condition}%
+  \index{condition!narrow condition}%
+narrow condition (cf. Section~\ref{sec:cond} for a discussion of narrow vs.
+wide conditions).
+%
+The first parameter is either 
+  \index{hot@$\mhot{}$}%
+\mhot{} or 
+  \index{cold@$\mcold{}$}%
+\mcold{} and gives the mode, the second parameter is the condition expression.
+%
+The \mlscCond{} command doesn't advance the vertical position, that is, all
+atomic commands different from instance line segments which are given between
+two instance line segments are drawn at the same position and implicitly form
+a 
+  \index{simultaneous region}%
+simultaneous region.
+%
+The 
+  \index{simregion@$\msimregion{}$}%
+\msimregion{} environment can be used to make this explicit by drawing a
+large dot at the shared location (cf. Section~\ref{sec:simreg}).
+
+Note that the instance line segments in the LSC in the middle of
+Figure~\ref{fig:expl} are of different length according to the source on the
+right but appear to be of roughly the same length.
+%
+The reason for using different lengths is that the first instance line segment
+spans from the bottom line of the instance header frame to the top line of the
+condition kandis.
+%
+The second instance line segment spans from the top (!) line of the condition
+kandis to the bottom (!) line of the footer, i.e. the beginning is hidden by
+the condition and the end is hidden by the footer.
+%
+The former hiding takes place because only after drawing an instance line
+segment, all elements in the simultaneous region \emph{before} it are
+  \index{flush}%
+``flushed''.
+%
+The footer is drawn after the last instance line segment has been drawn but it
+is the only element whose bottom line is positioned at the current position.
+%
+Conditions, for example, are placed such that the top line lies at the current
+position.
+%>@>
+
+\section{LSC Environments}
+\label{sec:lsc}
+
+The \lscsty{} package provides two environments for LSCs, one for complete LSC
+specifications and one omitting the header, in particular to typeset LSC
+bodies only without enclosing frame.
+
+\subsection{Full LSCs}
+\label{sec:lsc:fulllsc}
+
+%<@<
+  \index{FullLsc@$\mFullLsc$}%
+\begin{center}\fbox{\parbox{0.86\textwidth}{%
+\mbegin{FullLsc}%
+  \optparam{\var{prechartloc}}%
+  \param{\var{name}}%
+  \param{\var{ac}}%
+  \newline%
+  \hspace*{8em}%
+  \param{\this{$\minvariant$}\orthat{$\minitial$}\orthat{$\miterative$}}%
+  \newline%
+  \hspace*{8em}%
+  \param{\this{$\mstrict$}\orthat{$\mweak$}\orthat{$\mpermissive$}\orthat{}}%
+  \newline%
+  \hspace*{8em}%
+  \param{\this{$\mexistential$}\orthat{$\muniversal$}}%
+  \param{\var{nrinsts}}%
+  \param{\var{nrlocs}}
+\newline
+\dots
+\newline
+\mend{FullLsc}
+}}\end{center}
+
+The \mLsc{} environment typesets full LSCs, i.e. LSC with a header giving the
+name \var{name}, the activation condition \var{ac}, the activation mode
+(one of 
+\\
+\minvariant{}, \minitial{}, or \miterative{}), the interpretation,
+(one of \mstrict{},
+\mweak{}, \mpermissive{}, or empty), and the quantification (either
+\muniversal{} or \mexistential{}).
+
+The optional first parameter gives the height of the pre-chart, \var{nrinsts}
+is the (strictly positive) number of instances, and \var{nrlocs} the height of
+instance lines.
+
+\newcommand{\verbunskip}{\vspace*{-1.85\baselineskip}}%
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{FullLsc}{Name}{ActCond}{invariant}{weak}{existential}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{FullLsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{FullLsc}%
+        {Name}{ActCond}%
+        {invariant}{weak}%
+        {existential}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{3}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{FullLsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+
+Note that the 
+  \index{interpretation}%
+interpretation 
+  \index{weak@$\mweak{}$}%
+\mweak{} maps to the unified name permissive in the LSC header.
+%
+If no interpretation is given, the corresponding field is not present in the
+LSC header at all.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{FullLsc}[1.5]{Name}{ActCond}{iterative}{}{universal}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{FullLsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{FullLsc}[1.5]%
+        {Name}{ActCond}%
+        {iterative}{}%
+        {universal}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{3}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{FullLsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{LSCs without Header}
+\label{sec:lsc:lsc}
+
+%<@<
+  \index{Lsc@$\mLsc$}%
+\begin{center}\fbox{\parbox{0.85\textwidth}{%
+\mbegin{Lsc}%
+  \optparam{\var{prechartloc}}%
+  \newline%
+  \hspace*{6em}%
+  \param{\this{$\mexistential$}\orthat{$\muniversal$}\orthat{$\mnone$}}%
+  \param{\var{nrinsts}}%
+  \param{\var{nrlocs}}
+\newline
+\dots
+\newline
+\mend{Lsc}
+}}\end{center}
+
+The \mLsc{} environment is provided to typeset LSCs without header and LSCs
+without surrounding frame indicating the quantification.
+%
+With the special quantification \mnone{}, the frame is omitted and thus only
+the LSC body drawn.
+%
+This is useful in publications on LSCs which discuss, for example, the
+compilation of LSC bodies to automata.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{3}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Instance Lines}
+\label{sec:inst}
+
+There are two flavours of instance line environment, ordinary and creation
+instance lines.
+%
+Creation instance lines are used to indicate that an object is created during
+a scenario.
+%
+To this end the instance head can be placed some offset below the regular
+position of instance heads and it defines a hook for the composite
+\mlscCreate{} command which draws the creation arrow.
+
+\subsection{Ordinary Instance Lines}
+\label{sec:inst:ord}
+
+%<@<
+  \index{lscinst@$\mlscinst$}%
+\begin{center}\fbox{\parbox{0.8\textwidth}{
+\mbegin{lscinst}%
+  \optparam{\underline{\this{$\mMSC$}}\orthat{$\mSD$}\orthat{$\mnoboxSD$}\orthat{$\mesymMSC$}\orthat{$\mesymSD$}}%
+  \param{\var{name}}
+\newline
+\dots
+\newline
+\mend{lscinst}
+}}\end{center}
+
+The \var{name} is set on top of the instance line segments.
+%
+The optional parameter controls the appearance of the instance header and
+footer according to the following table:
+
+  \index{MSC@$\mMSC$}%
+  \index{SD@$\mSD$}%
+  \index{noboxSD@$\mnoboxSD$}%
+  \index{esymMSC@$\mesymMSC$}%
+  \index{esymSD@$\mesymSD$}%
+\begin{center}
+\begin{tabular}{||l|c|c||}
+\hline
+            & framed header & footer \\
+\hline
+\mMSC{}
+(default)   & solid         & $\times$ \\
+\hline
+\mSD{}      & solid         & $-$ \\
+\hline
+\mnoboxSD{} & none          & $-$ \\
+\hline
+\mesymMSC{} & dashed        & $\times$ \\
+\hline
+\mesymSD{}  & dashed        & $-$ \\
+\hline
+\end{tabular}
+\end{center} 
+
+There is no kind for the fourth possible combination -- nobody wants the
+combination of no frame but a footer.
+
+\begin{center}%<@<
+\begin{minipage}{0.625\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{3}{3}
+    \begin{lscinst}{MSC}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}[SD]{SD}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}[noboxSD]{noboxSD}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.375\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \begin{lscinst}{MSC}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}[SD]{SD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}[noboxSD]%
+                 {noboxSD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lscinst}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+See Section~\ref{sec:pipo:inst} for examples of existential symbolic instances.
+%>@>
+
+\subsection{Creation Instance Lines}
+\label{sec:inst:cre}
+
+%<@<
+  \index{lsccreateinst@$\mlsccreateinst$}%
+\begin{center}\fbox{\parbox{0.775\textwidth}{%
+\mbegin{lsccreateinst}%
+  \optparam{\underline{\this{$\mMSC$}}\orthat{$\mSD$}\orthat{$\mnoboxSD$}\orthat{$\mesymMSC$}\orthat{$\mesymSD$}}%
+\newline
+\hspace*{3.75cm}
+  \param{\var{offset}}%
+  \param{\var{id}}%
+  \param{\var{name}}%
+\newline
+\dots
+\newline
+\mend{lsccreateinst}
+}}\end{center}
+
+The optional parameter \mlsccreateinst{} and the \var{name} work just like in
+the \mlscinst{} environment.
+%
+The additional parameter \var{offset} gives the offset of the instance header
+relative to the headers of ordinary instance lines.
+%
+That is, it is exactly equivalent to \mlscinst{} if the \var{offset} is 0 and
+the corresponding \lscCreate{} command is omitted.
+
+  \index{lscCreate@$\mlscCreate$}%
+\begin{center}\fbox{
+\mlscCreate%
+  \param{\var{id}}%
+}\end{center}
+
+The parameter \var{id} is a legal \LaTeX{} identifier which can be used in the
+\mlscCreate{} command to draw the create arrow.
+
+\begin{center}%<@<
+\begin{minipage}{0.435\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{0.7}
+      \lscCreate{cr}
+      \lscLine{hot}{2.3}
+    \end{lscinst}
+    \begin{lsccreateinst}{1}{cr}{Inst2}
+      \lscLine{hot}{2}
+    \end{lsccreateinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{0.7}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscCreate{cr}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2.3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \begin{lsccreateinst}{1}{cr}{Inst2}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lsccreateinst}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+\begin{center}%<@<
+\begin{minipage}{0.435\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lsccreateinst}[noboxSD]{1}{cr}{Inst1}
+      \lscLine{hot}{2}
+    \end{lsccreateinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{0.7}
+      \lscCreate{cr}
+      \lscLine{hot}{2.3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \begin{lsccreateinst}{1}{cr}{Inst2}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lsccreateinst}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{0.7}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscCreate{cr}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2.3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}%
+\end{minipage}
+\end{center}%>@>
+
+  \index{creation arrow}
+Note that the creation arrow ends at the border of the frame when the instance
+head has a frame and at the label if there is no frame.
+% 
+Further note that the instance line end of the arrow is located 0.3 pstricks
+units above the bottom of the instance head such that the instance line
+segment lengths on the instance line with the \mlscCreate{} can easily be
+adjusted to obtain a vertical arrow.
+
+The creation arrow is drawn as soon as both ends, i.e. the \mlscCreate{}
+location and the creation instance, are given.   The identifier is then
+undefined, i.e. the same identifier may legally occur in two
+\mlscCreate{}/\mlsccreateinst{} pairs in the same LSC -- but this is obviously
+bad style.
+%>@>
+
+\subsection{Instance Location and Footer Dimensions}
+\label{sec:inst:dim}
+
+%<@<
+  \index{lscLocationWidth@$\mlscLocationWidth$}%
+  \index{lscLocationHeight@$\mlscLocationHeight$}%
+\begin{center}\fbox{\parbox{12em}{%
+  \mlscLocationWidth
+  \newline
+  \mlscLocationHeight
+}}\end{center}
+
+\begin{figure}%<@< \label{fig:locdim}
+\begin{center}
+{\pssetlength{\lscLocationWidth}{4}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+    \lscPut{\pcline[linewidth=0.5pt]{|-|}%
+                   (-0.5\lscLocationWidth,1)%
+                   (0.5\lscLocationWidth,1)%
+            \lput*{0}{\mlscLocationWidth}}
+    \lscLine{hot}{1}
+    \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+                    (-0.5\lscLocationWidth,\lscLocationHeight)%
+                    (0.5\lscLocationWidth,0)}
+    \lscLine{hot}{1}
+    \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+                    (-0.5\lscLocationWidth,\lscLocationHeight)%
+                    (0.5\lscLocationWidth,0)}
+    \lscPut{\pcline[linewidth=0.5pt]{|-|}%
+                   (0.6\lscLocationWidth,\lscLocationHeight)%
+                   (0.6\lscLocationWidth,0)%
+            \lput*[l]{0}{\mlscLocationHeight}}
+    \lscLine{hot}{1}
+    \lscPut{\psframe[linewidth=0.25pt,linestyle=dashed]%
+                    (-0.5\lscLocationWidth,\lscLocationHeight)%
+                    (0.5\lscLocationWidth,0)}
+  \end{lscinst}
+\end{Lsc}}
+\end{center}
+%
+\caption{\small%
+  {\bf Dimensions} of a location.}
+\label{fig:locdim}
+\end{figure}%>@>
+
+  \index{box boundary|textbf}%
+The LSC's box boundary is basically computed in terms of the width and height
+of a single location within an instance (cf. Figure~\ref{fig:locdim}) as
+defined by lengths \mlscLocationWidth{} (default: 3 pstricks units) and
+\mlscLocationHeight{} (default: 1 pstricks unit).
+%
+The width of the LSC body is computed as
+\[
+\textit{number of instances} * \mlscLocationWidth
+\]
+and the height of the LSC body is computed as
+\[
+\textit{number of locations} * \mlscLocationHeight.
+\]
+%
+Both lengths can be manipulated, for example, to obtain wider or narrower
+instances or to globally scale the length of instance line segments.
+
+To change the dimension for only a single LSC, one can exploit that curly
+braces in \LaTeX{} define scopes and that changes to lengths or commands are
+local to these scopes.
+%
+To this end we have enclosed the manipulation of the lengths and the \mLsc{}
+environment in curly braces.
+
+\begin{center}%<@<
+\begin{minipage}{0.275\textwidth}%
+ \scalebox{0.9}{%
+  \pssetlength{\lscLocationWidth}{5em}
+  \pssetlength{\lscLocationHeight}{1.5}
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{\parbox{4em}{Instance No. 1}}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.50\textwidth}%
+\small%
+\begin{verbatim}
+{\pssetlength{\lscLocationWidth}{5em}
+\pssetlength{\lscLocationHeight}{1.5}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{%
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+      \parbox{4em}{Instance No. 1}}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+Note that the height of the instance head frame depends on the height of its
+content, i.e. a \cmd{parbox} may be used to obtain multiline annotations in
+instance heads.
+
+  \index{lscFooterHeightFactor@$\mlscFooterHeightFactor$}%
+\begin{center}\fbox{%
+  \mlscFooterHeightFactor
+}\end{center}
+
+The command (!) \mlscFooterHeightFactor{} (default: 0.2) affects the
+appearance of instance footers.
+%
+It should be set to a positive real number, at best from the left-open
+interval $]0,0.2]$.  The footer is basically a filled framebox around a
+\cmd{rule} of height
+%
+\[
+\mlscFooterHeightFactor * \mlscLocationHeight.
+\]
+
+\begin{center}%<@<
+\begin{minipage}{0.225\textwidth}%
+ \scalebox{0.9}{%
+  \renewcommand{\lscFooterHeightFactor}{0.05}
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.61\textwidth}%
+\small%
+\begin{verbatim}
+{\renewcommand{\lscFooterHeightFactor}{0.01}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Instance Line Segments}
+\label{sec:line}
+
+There are two flavours of instance line segments, ordinary and environment
+instance line segments.
+%
+Environment instance line segments are rendered like the ones of Sequence
+Diagrams.
+
+\subsection{Ordinary Instance Line Segments}
+\label{sec:line:ord}
+
+%<@<
+  \index{lscLine@$\mlscLine$}%
+\begin{center}\fbox{
+\mlscLine%
+  \optparam{\var{interval}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}\orthat{$\mnone$}}%
+  \param{\var{length}}%
+}\end{center}
+
+The \mlscLine{} command draws the elements belonging to the location where the
+line starts, draws the instance line segment of length \var{length}, and
+advances the vertical position by this amount.
+%
+The mode `\mnone{}' is not a valid mode of LSCs but only present to draw an
+invisible line segment to draw  abstract LSCs, e.g. to explain LSC
+construction algorithms.
+
+The actual length of the line segment is computed as
+$\var{length} \cdot \mlscLocationHeight{}$.
+
+If the optional \var{interval} is given, it rendered to the right of the
+instance line segment.  This may be any content, but it is typically used to
+place timing intervals.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{0.75}
+      \lscLine{none}{0.75}
+      \lscLine{cold}{1.5}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine[{$[1,2]$}]{cold}{1.25}
+      \lscLine[{$[3,17]$}]{hot}{1.75}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscLine{hot}{0.75}
+    \lscLine{none}{0.75}
+    \lscLine{cold}{1.5}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscLine[{$[1,2]$}]{cold}{1.25}
+    \lscLine[{$[3,17]$}]{hot}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that timing intervals are always vertically centred on the line and put
+to the right.
+%
+As this is already the optional parameter, there are no plans to support
+variable positioning of the timing interval but nobody keeps you from using
+\cmd{rput} should the need arise.
+
+\medskip
+
+The \mlscLine{} command doesn't set the line colour, thus one can obtain
+colourful LSCs using the \cmd{psset} command.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{Inst}
+      {\psset{linecolor=green}
+      \lscLine{hot}{1.25}}
+      {\psset{linecolor=blue}
+      \lscLine{cold}{1.75}}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    {\psset{linecolor=green}
+    \lscLine{hot}{1.25}}
+    {\psset{linecolor=blue}
+    \lscLine{cold}{1.75}}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Environment Instance Line Segments}
+\label{sec:line:env}
+
+%<@<
+  \index{lscEnvLine@$\mlscEnvLine$}%
+\begin{center}\fbox{
+\mlscEnvLine%
+  \optparam{\var{interval}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{length}}%
+}\end{center}
+
+The \mlscEnvLine{} behaves just like \mlscLine{}, only the instance line
+segment is rendered differently, namely in 
+  \index{Sequence Diagram}%
+Sequence Diagram style.
+%
+To indicate hot segments, a solid line is drawn on top of the environment
+line segment.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscEnvLine{hot}{1.25}
+      \lscEnvLine{cold}{1.75}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscEnvLine[{$[1,2]$}]{cold}{1.25}
+      \lscEnvLine[{$[3,17]$}]{hot}{1.75}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.48\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscEnvLine{hot}{1.25}
+    \lscEnvLine{cold}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+    \lscEnvLine[{$[1,2]$}]{cold}{1.25}
+    \lscEnvLine[{$[3,17]$}]{hot}{1.75}
+\end{verbatim}
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\section{Messages}
+\label{sec:msg}
+
+Both message kinds distinguished by~\cite{Klose2003} are supported by two sets
+of composite commands.
+%
+For each kind, there is one command to mark the sending location, one command
+to mark the reception location, and one command to finally draw the arrow.
+
+The difference between both is only the shape of the arrow, it is not enforced
+that instantaneous messages are drawn horizontally without slope.
+
+Both also don't define the line colour, i.e. one can obtain coloured arrows
+using \cmd{psset} (cf. Section~\ref{sec:line:ord}).
+
+Self messages are currently not supported.
+%
+If the sending and reception lie on the same instance line, then the arrow's
+line coincides with the instance line and only the arrow itself and the
+annotation will be visible.
+
+\subsection{Asynchronous Messages}
+\label{sec:msg:asyn}
+
+%<@<
+  \index{lscAsynSnd@$\mlscAsynSnd$}%
+  \index{lscAsynRcv@$\mlscAsynRcv$}%
+  \index{lscAsyn@$\mlscAsyn$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscAsynSnd%
+  \param{\var{id}}%
+\newline
+\mlscAsynRcv%
+  \param{\var{id}}%
+\newline
+\mlscAsyn%
+  \param{\var{id}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{label}}
+}}\end{center}
+
+If \mlscAsynSnd{} and \mlscAsynRcv{} occurred exactly once within an
+\mFullLsc{} or \mLsc{} environment, then a following \mlscAsyn{} command with
+the same \var{id} draws the arrow annotated with \var{label}.
+
+The \var{id} can be reused for another message within the same LSC after
+\mlscAsyn{} has been called, but this is not considered good style.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{0.5}%
+      \lscAsynSnd{e}%
+      \lscLine{hot}{1.5}%
+      \lscAsynRcv{f}%
+      \lscLine{hot}{1}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{1}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{0.5}%
+      \lscAsynSnd{f}%
+      \lscLine{hot}{1.5}%
+    \end{lscinst}
+    %
+    \lscAsyn{e}{hot}{E}%
+    \lscAsyn{f}{cold}{F}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynSnd{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynRcv{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynRcv{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynSnd{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}%
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscAsyn{e}{hot}{E}%
+  \lscAsyn{f}{cold}{F}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that the closing commands of composite commands, like \mlscAsyn{} in the
+example, are by 
+  \index{convention}%
+convention collected below all instance environments. 
+%
+It is by no means necessary, as explained above, but thereby one provides a
+common place to look for all definitions.
+%>@>
+
+\subsection{Instantaneous Messages}
+\label{sec:msg:inst}
+
+%<@<
+  \index{lscInstSnd@$\mlscInstSnd$}%
+  \index{lscInstRcv@$\mlscInstRcv$}%
+  \index{lscInst@$\mlscInst$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscInstSnd%
+  \param{\var{id}}%
+\newline
+\mlscInstRcv%
+  \param{\var{id}}%
+\newline
+\mlscInst%
+  \param{\var{id}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{label}}
+}}\end{center}
+
+The composite command for instantaneous messages is operated exactly like
+\mlscAsyn{} and friends (cf. Section~\ref{sec:msg:asyn}).
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}%
+      \lscInstSnd{e}%
+      \lscLine{hot}{1}%
+      \lscInstRcv{f}%
+      \lscLine{hot}{1}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{1}%
+      \lscInstRcv{e}%
+      \lscLine{hot}{0.5}%
+      \lscInstSnd{f}%
+      \lscLine{hot}{1.5}%
+    \end{lscinst}
+    %
+    \lscInst{e}{hot}{E}%
+    \lscInst{f}{cold}{F}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstSnd{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstRcv{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstRcv{e}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstSnd{f}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}%
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscInst{e}{hot}{E}%
+  \lscInst{f}{cold}{F}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Self Messages}
+\label{sec:msg:self}
+
+%<@<
+Self messages are not a third category but both asynchronous and instantaneous
+messages may well begin and end at the same instance line.
+
+\begin{center}%<@<
+\begin{minipage}{0.33\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{4}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{0.5}
+      \lscAsynSnd{e}
+      \lscLine{hot}{1}
+      \lscAsynRcv{e}
+      \lscLine{hot}{0.5}
+      \lscInstSnd{f}
+      \lscLine{hot}{1}
+      \lscInstRcv{f}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \lscAsyn{e}{hot}{E}
+    \lscInst{f}{hot}{F}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.33\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynSnd{e}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAsynRcv{e}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstSnd{f}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscInstRcv{f}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscAsyn{e}{hot}{E}
+  \lscInst{f}{hot}{F}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Currently, the shape is fixed, i.e. the arrow extends to the right of the
+instance line and has ``armlength'' 0.5 pstricks units.
+%>@>
+
+
+\section{Conditions}
+\label{sec:cond}
+
+Conditions can be rendered using an atomic command and a composite command.
+%
+The former command is provided for convenience for the frequent case that a
+condition spans only a single instance line
+  \index{narrow condition}%
+(narrow condition).
+%
+In this case, all information, i.e. the location, the temperature, and the
+label, can be given immediately.
+
+A wide condition may also span only one instance line but it may also cover
+more.
+
+\subsection{Narrow Conditions}
+\label{sec:cond:narrow}
+
+%<@<
+  \index{lscCond@$\mlscCond$}%
+\begin{center}\fbox{%
+\mlscCond%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{label}}
+}\end{center}
+
+The \mlscCond{} command renders a condition kandis at the current position.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}%
+      \lscCond{hot}{$x = a$}%
+      \lscLine{hot}{2}%
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{0.5}%
+      \lscCond{cold}{\parbox{4em}{\centering$y = 0$ $\vee\ z = 0$}}%
+      \lscLine{hot}{2.5}%
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.47\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscCond{hot}{$x = a$}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscCond{cold}{%
+      \parbox{4em}{\centering%
+        $y=0$ $\vee\ z=0$}}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2.5}%
+  \end{lscinst}
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The size of the kandis scales with the size of \var{label}'s box.
+%
+This has the effect that it is rather low if \var{label} has neither over- nor
+underlength and it scales unproportionally if \var{label} has multiple lines. 
+%
+The former issue can be addressed using \cmd{rule} or \cmd{phantom}, the
+latter will have to be addressed by a smarter kandis drawing macro within
+\lscsty{}.
+
+\subsection{Wide Conditions}
+\label{sec:cond:wide}
+
+%<@<
+  \index{lscWidecondOn@$\mlscWidecondOn$}%
+  \index{lscWidecondOff@$\mlscWidecondOff$}%
+  \index{lscWidecond@$\mlscWidecond$}%
+\begin{center}\fbox{\parbox{15em}{
+\mlscWidecondOn%
+  \param{\var{id}}%
+\newline
+\mlscWidecondOff%
+  \param{\var{id}}%
+\newline
+\mlscWidecond%
+  \param{\var{id}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{label}}
+}}\end{center}
+
+The \mlscWidecondOn{} and \mlscWidecondOff{} commands add locations to a wide
+condition.
+%
+They have to occur on exactly the same height and consecutively.
+%
+Use \mlscWidecondOn{} for those instances to which the condition applies and
+\mlscWidecondOff{} otherwise.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+  \pssetlength{\lscLocationWidth}{2.5}%
+  \begin{Lsc}{none}{3}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}
+      \lscWidecondOn{wc}
+      \lscLine{hot}{2}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{1}
+      \lscWidecondOff{wc}
+      \lscLine{hot}{2}
+    \end{lscinst}
+    \begin{lscinst}{Inst3}
+      \lscLine{hot}{1}
+      \lscWidecondOn{wc}
+      \lscLine{hot}{2}
+    \end{lscinst}
+    \lscWidecond{wc}{hot}{$\qquad\quad x = 0$}
+  \end{Lsc}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.39\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\pssetlength%
+  {\lscLocationWidth}{2.5}%
+\begin{Lsc}{none}{3}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscWidecondOn{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscWidecondOff{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+  \end{lscinst}
+  \begin{lscinst}{Inst3}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscWidecondOn{wc}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscWidecond{wc}{hot}%
+    {$\qquad\quad x = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The \var{label} is set in the centre of the kandis.  If the condition doesn't
+apply to the central location, one may need to add some offset like in the
+example above to avoid the instance line segment running through the label.  
+
+Note that the size of wide conditions is fixed, i.e. it does in particular not
+scale with the height of \var{label}'s box.
+%
+As a consequence, \var{label} should fit onto a single line.
+%>@>
+
+\subsection{Colourful Conditions}
+\label{sec:cond:colour}
+
+The appearance of 
+  \index{narrow condition}%
+  \index{condition!narrow}%
+narrow conditions, and in particular the colour of its outline, cannot be
+easily manipulated because narrow conditions are ``scheduled'' and drawn when
+the next instance line segment is drawn (cf.  Section~\ref{sec:simreg}).
+%
+Thus changing the colour of the outline applies to all elements which are
+drawn together with the instance line segment, in particular the instance line
+itself.
+
+If 
+  \index{wide condition}%
+  \index{condition!wide}%
+wide conditions are sufficient (cf. Section~\ref{sec:cond:wide}), their colour
+can be modified as shown in the following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.25\textwidth}%
+ \scalebox{0.9}{%
+  \let\lscWidecondOooginool\lscWidecond%
+  \renewcommand{\lscWidecond}[3]{{%
+    \ifthenelse{\equal{#2}{hot}}{%
+      \psset{linecolor=red}}{%
+      \psset{linecolor=blue}}%
+    \lscWidecondOooginool{#1}{#2}{#3}}}
+  \begin{Lsc}{none}{1}{4.5}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{1}%
+      \lscWidecondOn{c}%
+      \lscLine{hot}{1.5}%
+      \lscWidecondOn{d}%
+      \lscLine{hot}{2}%
+    \end{lscinst}
+    \lscWidecond{c}{hot}{$f = g$}%
+    \lscWidecond{d}{cold}{$g = f$}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.575\textwidth}%
+\small%
+{\begin{verbatim}
+\let\lscWidecondOooginool\lscWidecond%
+\renewcommand{\lscWidecond}[3]{{%
+  \ifthenelse{\equal{#2}{hot}}{%
+    \psset{linecolor=red}}{%
+    \psset{linecolor=blue}}%
+  \lscWidecondOooginool{#1}{#2}{#3}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4.5}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{1}%
+    \lscWidecondOn{c}%
+    \lscLine{hot}{1.5}%
+    \lscWidecondOn{d}%
+    \lscLine{hot}{2}%
+  \end{lscinst}
+  \lscWidecond{c}{hot}{$f = g$}%
+  \lscWidecond{d}{cold}{$g = f$}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Local Invariants}
+\label{sec:locinv}
+
+%<@<
+  \index{lscLocinvStart@$\mlscLocinvStart$}%
+  \index{lscLocinvBegin@$\mlscLocinvBegin$}%
+  \index{lscLocinvEnd@$\mlscLocinvEnd$}%
+  \index{lscLocinv@$\mlscLocinv$}%
+\begin{center}\fbox{\parbox{0.875\textwidth}{
+\mlscLocinvStart%
+  \param{\var{id}}%
+\newline
+\mlscLocinvBegin%
+  \param{\var{id}}%
+\newline
+\mlscLocinvEnd%
+  \param{\var{id}}%
+\newline
+\mlscLocinv%
+  \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+  \param{\var{id}}%
+  \param{\this{$\mincl$}\orthat{$\mexcl$}}%
+  \param{\this{$\mincl$}\orthat{$\mexcl$}}%
+  \param{\this{$\mhot$}\orthat{$\mcold$}}%
+  \param{\var{label}}
+}}\end{center}
+
+The commands \mlscLocinvBegin{} (or, synonymously, \mlscLocinvStart{}) and
+\mlscLocinvEnd{} mark the beginning and end position of local invariant
+\var{id}.
+
+The \mlscLocinv{} command renders the local invariant \var{id}.
+%
+The position of the vertical line to which the kandis is connected can be
+controlled by the optional parameter (default: \mr{} (to the right)).
+
+The third and fourth parameters select whether the ends are inclusive (\mincl)
+or exclusive (\mexcl).
+%
+Inclusive ends are rendered with a filled circle and exclusive ends with a
+non-filled circle (just like jumps are indicated in function graphs).
+%
+This is different from~\cite{Klose2003} where the kandis is rotated by 90
+degrees and inclusive ends are indicated by having the kandis end in a
+rectangular shape instead of triangular.
+%
+The drawback is that a both-inclusive local invariant looks like a rotated
+action box and doesn't resemble conditions at all.%
+\footnote{%
+  And -- first of all -- it seemed easier to render the shape we chose.
+}
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLocinvBegin{li}
+      \lscLine{hot}{1}
+      \begin{simregion}
+        \lscLocinvStart{lj}
+      \end{simregion}
+      \lscLine{hot}{1}
+      \lscLocinvEnd{li}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{2}
+      \lscLocinvEnd{lj}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \lscLocinv[l]{li}{incl}{excl}{hot}{$x = 0$}
+    \lscLocinv{lj}{excl}{incl}{cold}{$y = 0$}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvBegin{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+    \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+      \lscLocinvStart{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \end{simregion}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvEnd{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvEnd{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscLocinv[l]{li}%
+    {incl}{excl}{hot}{$x = 0$}
+  \lscLocinv{lj}%
+    {excl}{incl}{cold}{$y = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+In the example above, we used a simregion (cf. Section~\ref{sec:simreg}) to
+highlight the point where the local invariant connects to the instance line in
+lack of other elements.
+%
+Local invariants in the wild typically end at simultaneous regions with other
+elements as the LSC's automaton becomes non-deterministic otherwise.
+
+Note that the local invariant kandis behaves like that of narrow conditions.
+%
+That is, it looks too low if \var{label} has no over- or underlength and it
+scales unproportionally with multiline \var{label}s (cf.
+Section~\ref{sec:cond:narrow}).
+
+Further note that the
+  \index{box boundary}%
+box boundary of the LSC doesn't consider the amounts by which local invariants
+kandis stand out to the left or the right.
+%
+One has to explicitly treat kandis overlapping other text by adding vertical
+space to the left or the right.%
+\footnote{%
+  Technically the problem is that the box boundary is determined when the
+  \mLsc{} environment is opened.  At this point in time the extension of local
+  invariants is not yet known.  And the dimension cannot be changed afterwards
+  (as far as the author knows).
+}
+
+  \index{lscLocinvOffset@$\mlscLocinvOffset$}%
+\begin{center}\fbox{
+  \mlscLocinvOffset
+}\end{center}
+
+The length \mlscLocinvOffset{} (default: 0) is added to the horizontal
+distance between instance line and local invariant.
+%
+To move the local invariant further outwards, set it to a positive number
+and to move it further inwards, set it to a negative number.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLocinvBegin{li}
+      \lscLine{hot}{1}
+      \begin{simregion}
+        \lscLocinvStart{lj}
+      \end{simregion}
+      \lscLine{hot}{1}
+      \lscLocinvEnd{li}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{2}
+      \lscLocinvEnd{lj}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \pssetlength{\lscLocinvOffset}{0.5}
+    \lscLocinv[l]{li}{incl}{excl}{hot}{$x = 0$}
+    \pssetlength{\lscLocinvOffset}{-0.5}
+    \lscLocinv{lj}{excl}{incl}{cold}{$y = 0$}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.52\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvBegin{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+    \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+      \lscLocinvStart{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \end{simregion}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvEnd{li}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLocinvEnd{lj}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \pssetlength{\lscLocinvOffset}{0.5}
+  \lscLocinv[l]{li}%
+    {incl}{excl}{hot}{$x = 0$}
+  \pssetlength{\lscLocinvOffset}{-0.5}
+  \lscLocinv{lj}%
+    {excl}{incl}{cold}{$y = 0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The vertical position of the kandis is fixed.  It is always drawn centred
+between the beginning and end point.
+%>@>
+
+
+\section{Timer Sets, Timer Resets, and Timeouts}
+\label{sec:tset}
+\label{sec:treset}
+\label{sec:tout}
+
+%<@<
+  \index{lscTimerSet@$\mlscTimerSet$}%
+  \index{lscTimerReset@$\mlscTimerReset$}%
+  \index{lscTimeout@$\mlscTimeout$}%
+\begin{center}\fbox{\parbox{0.875\textwidth}{
+\mlscTimerSet%
+  \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+  \param{\var{label}}%
+  \param{\var{duration}}%
+\newline
+\mlscTimerReset%
+  \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+  \param{\var{label}}%
+\newline
+\mlscTimeout%
+  \optparam{\underline{\this{$\mr$}}\orthat{$\ml$}}%
+  \param{\var{label}}%
+}}\end{center}
+
+The atomic commands \mlscTimerSet{}, \mlscTimerReset{}, and \mlscTimeout{}
+render the timer symbols.
+%
+The position of the hourglass symbols can be controlled by the optional
+parameter (default: \mr{} (to the right)).
+
+The parameter \var{label} is not an identifier as used with composite commands
+but arbitrary text.  To connect, e.g., timer setting and timeout they should
+obtain the same \var{label}.
+
+A timer type is currently not explicitly supported.  It may be written as part
+of the \var{label}.
+
+\begin{center}%<@<
+\begin{minipage}{0.4\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{4}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{0.75}
+      \lscTimerSet{$t$ : superstep}{3}
+      \lscLine{hot}{1}
+      \lscTimerReset[l]{$t$}
+      \lscLine{hot}{1}
+      \lscTimeout{$t$}
+      \lscLine{hot}{1.25}
+    \end{lscinst}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.5\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{4}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{0.75}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscTimerSet{$t$ : superstep}{3}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscTimerReset[l]{$t$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscTimeout{$t$}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.25}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Actions}
+\label{sec:act}
+
+%<@<
+  \index{lscAct@$\mlscAct$}%
+\begin{center}\fbox{
+\mlscAct%
+  \param{\var{label}}%
+}\end{center}
+
+The \lscAct{} atomic command draws a rectangular action symbol annotated with
+\var{label}.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{1}
+      \lscAct{Aaand -- action!}
+      \lscLine{hot}{2}
+    \end{lscinst}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.40\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAct{Aaand -- action!}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{2}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Self Destructions}
+\label{sec:kill}
+
+%<@<
+  \index{lscKill@$\mlscKill$}%
+\begin{center}\fbox{
+\mlscKill%
+}\end{center}
+
+The atomic \mlscKill{} command draws a cross at the current position to
+indicate 
+  \index{termination}%
+termination of the instance.
+%
+It is typically not followed by any more \mlscLine{} commands.
+
+There is no explicit 
+  \index{deletion arrow}%
+deletion arrow (like there is a creation arrow) since instantaneous messages
+may be used for this purpose.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}[SD]{Inst1}
+      \lscLine{hot}{1.5}
+      \lscInstSnd{rip}
+      \lscLine{hot}{1}
+      \lscKill
+    \end{lscinst}
+    \begin{lscinst}[SD]{Inst2}
+      \lscLine{hot}{1.5}
+      \lscInstRcv{rip}
+      \lscKill
+    \end{lscinst}
+    \lscInst{rip}{hot}{RIP}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.39\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}[SD]{Inst1}
+    \lscLine{hot}{1.5}
+    \lscInstSnd{rip}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscKill
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}[SD]{Inst2}
+    \lscLine{hot}{1.5}
+    \lscInstRcv{rip}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscKill
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+  \end{lscinst}
+  \lscInst{rip}{hot}{RIP}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Coregions}
+\label{sec:coreg}
+
+%<@<
+  \index{coregion@$\mcoregion$}%
+\begin{center}\fbox{%
+\mbegin{coregion}%
+  \optparam{\underline{\this{$\ml$}}\orthat{$\mr$}}%
+\dots
+\mend{coregion}
+}\end{center}
+
+The elements and instance line segments enclosed in a \mcoregion{} environment
+are marked with a parallel dotted line to indicate that they form a 
+  \index{coregion}%
+coregion.
+%
+The optional parameter controls whether the line appears to the left (\ml{},
+the default) or to the right (\mr) of the instance line.
+%
+\mcoregion{} environments shall not be nested.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}%
+      \lscInstSnd{e}%
+      \lscLine{hot}{1}%
+      \lscInstRcv{f}%
+      \lscLine{hot}{1}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{1}%
+      \begin{coregion}[r]
+        \lscInstRcv{e}%
+        \lscLine{hot}{0.5}%
+        \lscInstSnd{f}%
+      \psset{linecolor=red}
+      \end{coregion}
+      \lscLine{hot}{1.5}%
+    \end{lscinst}
+    %
+    \lscInst{e}{hot}{E}%
+    \lscInst{f}{cold}{F}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.49\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}\lscInstSnd{e}%
+    \lscLine{hot}{1}\lscInstRcv{f}%
+    \lscLine{hot}{1}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \begin{coregion}[r]
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+      \lscInstRcv{e}%
+      \lscLine{hot}{0.5}%
+      \lscInstSnd{f}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+      \psset{linecolor=red}
+    \end{coregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}%
+  \end{lscinst}
+  \lscInst{e}{hot}{E}%
+  \lscInst{f}{cold}{F}%
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The \mcoregion{} environment doesn't set the line's colour so it can be
+manipulated using \cmd{psset}.
+%
+But it does set the width to ensure that the dotted line is noticeable.  To
+change the width one may temporary redefine the internal length
+  \index{lsccoregwidth@$\cmd{lsc\AT{}coregwidth}$}%
+\cmd{lsc@coregwidth}.
+
+The coregion line is drawn when the environment is closed.  This has the
+(not so nice) effect that the line lies above condition kandis, action boxes
+etc.  So currently coregions look best when applied to message ends.
+%>@>
+
+
+\section{Simultaneous Regions}
+\label{sec:simreg}
+
+%<@<
+  \index{simregion@$\msimregion$}%
+\begin{center}\fbox{%
+\mbegin{simregion}%
+  \optparam{\underline{\this{$\mb$}}\orthat{$\mf$}}%
+\dots
+\mend{simregion}
+}\end{center}
+
+The elements enclosed in a \msimregion{} environment are marked with a large
+dot to explicitly indicate that they lie in a 
+  \index{simultaneous region}%
+simultaneous region.
+%
+  \index{b@$\mb$}%
+The optional parameter controls whether the dot appears behind (\mb{}, the
+  \index{f@$\mf$}%
+default) or in front of (\mf) the elements.
+%
+\msimregion{} environments shall not be nested and shall not comprise instance
+line segments.
+
+\begin{center}%<@<
+\begin{minipage}{0.5\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{0.75}
+      \lscInstSnd{e}
+      \lscLine{hot}{1}
+      \begin{simregion}
+        \lscInstRcv{f}
+        \lscCond{hot}{$x=0$}
+      \end{simregion}
+      \lscLine{hot}{1.25}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{0.75}
+      \begin{simregion}[f]
+        \lscCond{hot}{$y=0$}
+        \lscInstRcv{e}
+      \end{simregion}
+      \lscLine{hot}{1}
+      \lscInstSnd{f}
+      \lscLine{hot}{1.25}
+    \end{lscinst}
+    \lscInst{e}{hot}{E}
+    \lscInst{f}{hot}{F}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.36\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{0.75}
+    \lscInstSnd{e}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \begin{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+      \lscInstRcv{f}
+      \lscCond{hot}{$x=0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.25}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{0.75}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \begin{simregion}[f]
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+      \lscInstRcv{e}
+      \lscCond{hot}{$y=0$}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscLine{hot}{1}
+    \lscInstSnd{f}
+    \lscLine{hot}{1.25}
+  \end{lscinst}
+  \lscInst{e}{hot}{E}
+  \lscInst{f}{hot}{F}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+Note that the order of elements (except for cuts) of different kinds in a
+simultaneous region is not significant.
+%
+The 
+  \index{drawing order}%
+drawing order is (from bottom to top):
+%
+\begin{enumerate}
+\item
+    \index{simultaneous region}%
+  simultaneous region dot, if it should go into the background
+\item
+  white background of 
+    \index{wide condition}%
+  wide condition behind the instance line
+  (\mlscWidecondOn{})
+\item
+  white background of 
+    \index{wide condition}%
+  wide condition in front of the instance line
+  (\mlscWidecondOff{})
+\item
+    \index{action}%
+  action or 
+    \index{narrow condition}%
+  narrow condition
+\item
+    \index{timer set}%
+  timer set, 
+    \index{timer reset}%
+  reset, or 
+    \index{timeout}%
+  timeout
+\item
+    \index{atom}%
+  atom (cf. Section~\ref{sec:tech:atom})
+\item
+    \index{simultaneous region}%
+  simultaneous region dot, if it should go into the foreground
+\end{enumerate}
+
+Per simregion, at most one action or narrow condition can be drawn.  If one
+really needs to put one above the other (typically sacrificing readability)
+one may use instance line segments of length 0.  Two actions or narrow
+conditions can also be stacked one above the other using a manually tailored
+instance line segment in between and a foreground simregion circle like in the
+following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{1}
+      \lscCond{hot}{x=0}
+      \lscLine{hot}{0.5}
+      \begin{simregion}[f]
+        \lscCond{hot}{y=0}
+      \end{simregion}
+      \lscLine{hot}{1.5}
+    \end{lscinst}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.36\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscCond{hot}{x=0}
+    \lscLine{hot}{0.5}
+    \begin{simregion}[f]
+      \lscCond{hot}{y=0}
+    \end{simregion}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+The order of the finalising commands of composite commands and cuts \emph{is}
+significant.  They are drawn immediately, the one occurring first is drawn
+first.
+%>@>
+
+
+\section{Technicalities}
+\label{sec:tech}
+
+The \lscsty{} package is in particular used to describe the semantics of LSCs
+which depends on the notion of atoms and cuts, i.e. sets of atoms.
+%
+There commands introduced in this section are mainly intended to be able to
+illustrate such descriptions.  For example, to show the position of a cut.
+
+\subsection{Atoms}
+\label{sec:tech:atom}
+
+%<@<
+  \index{lscAtom@$\mlscAtom$}%
+  \index{lscLabelAtom@$\mlscLabelAtom$}%
+  \index{lscLabelAtomAt@$\mlscLabelAtomAt$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscAtom%
+  \param{\var{id}}%
+\newline
+\mlscLabelAtomAt%
+  \param{\var{angle}}%
+  \param{\var{id}}%
+  \param{\var{label}}%
+\newline
+\mlscLabelAtom%
+  \optparam{\underline{\this{$\mra$}}\orthat{$\mrb$}\orthat{$\mla$}\orthat{$\mlb$}}%
+  \param{\var{id}}%
+  \param{\var{label}}%
+}}\end{center}
+
+The \mlscAtom{} command marks the (atom(s) at the) current location with a
+dashed circle and equips it with an identity \var{id}.
+%
+This identity may then be used to label the 
+  \index{atom mark}%
+atom mark. 
+
+The command \mlscLabelAtomAt{} puts the \var{label} at position \var{angle}
+relative to the atom mark with identity \var{id}.
+
+The command \mlscLabelAtom{} is a shortcut for the most common angles.
+%
+  \index{ra@$\mra$}
+The default is $-45$ degrees (\mra{} (right above)), the other options are
+  \index{rb@$\mrb$}
+  \index{la@$\mla$}
+$-135$ degrees (\mrb{} (right below)), $45$ degrees (\mla{} (left above)), and
+  \index{lb@$\mlb$}
+$135$ degrees (\mlb{} (left below)).
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{4}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{0.5}
+      \lscAtom{aa}
+      \lscLine{hot}{1.5}
+      \lscAtom{ab}
+      \lscLine{hot}{1}
+      \lscAtom{ac}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \lscLabelAtom{ab}{right above}
+    \lscLabelAtomAt{93}{ac}{other}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{4}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAtom{aa}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAtom{ab}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscAtom{ac}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \lscLabelAtom{ab}{right above}
+  \lscLabelAtomAt{93}{ac}{other}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Cuts}
+\label{sec:tech:cut}
+
+%<@<
+  \index{lscCut@$\mlscCut$}%
+  \index{lscSetCutColour@$\mlscSetCutColour$}%
+  \index{lscSetCutLinestyle@$\mlscSetCutLinestyle$}%
+  \index{lscSetCutWidth@$\mlscSetCutWidth$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscCut%
+\newline
+\mlscSetCutColour%
+  \param{\var{colour}}%
+\newline
+\mlscSetCutLinestyle%
+  \param{\var{linestyle}}%
+\newline
+\mlscSetCutWidth%
+  \param{\var{length}}%
+}}\end{center}
+
+The \mlscCut{} atomic command draws a vertical line at the current position
+indicating the location of the 
+  \index{cut}%
+cut on the current instance line.  The line is connected to the last existing
+cut on the left. 
+%
+There shall not be more than one \mlscCut{} command per instance line.
+
+The command \mlscSetCutColour{} sets the colour to the colour name
+\var{colour} (default: red), \mlscSetCutLinestyle{} sets the line style to
+\var{linestyle} (default: solid), and \mlscSetCutWidth{} sets the width to
+\var{length} (default: 3pt).
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}%
+      \lscAsynSnd{e}%
+      \lscCut%
+      \lscLine{hot}{2}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscCut%
+      \lscLine{hot}{2}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{1}%
+    \end{lscinst}
+    %
+    \lscAsyn{e}{hot}{E}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.49\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscCut%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscAsynSnd{e}%
+    \lscLine{hot}{2}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscCut%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}%
+    \lscAsynRcv{e}%
+      \psset{linecolor=red}
+    \end{coregion}
+    \lscLine{hot}{1.5}%
+  \end{lscinst}
+  \lscAsyn{e}{hot}{E}%
+\end{Lsc}}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+  \index{lscNamedCut@$\mlscNamedCut$}%
+  \index{lscSetNamedCutColour@$\mlscSetNamedCutColour$}%
+  \index{lscSetNamedCutLinestyle@$\mlscSetNamedCutLinestyle$}%
+  \index{lscSetNamedCutWidth@$\mlscSetNamedCutWidth$}%
+\begin{center}\fbox{\parbox{0.55\textwidth}{%
+\mlscNamedCut%
+  \param{\var{id}}%
+\newline
+\mlscSetNamedCutColour%
+  \param{\var{id}}%
+  \param{\var{colour}}%
+\newline
+\mlscSetNamedCutLinestyle%
+  \param{\var{id}}%
+  \param{\var{linestyle}}%
+\newline
+\mlscSetNamedCutWidth%
+  \param{\var{id}}%
+  \param{\var{length}}%
+}}\end{center}
+
+To allow 
+  \index{cut!multiple}%
+multiple cuts in a single LSC, there is a corresponding set of commands for
+  \index{cut!named}%
+named cuts.
+%
+They take an \var{id} as first parameter.
+
+If not set explicitly, the colour, line style, and width of named cuts is
+inherited from the general cut colour, line style, and width as set by
+\mlscSetCutColour{}, \mlscSetCutLinestyle{}, and \mlscSetCutWidth{}.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \lscSetCutColour{lightgray}
+  \lscSetNamedCutWidth{Xb}{1.5pt}
+  \lscSetNamedCutColour{Xc}{green}
+  \lscSetNamedCutColour{Xb}{blue}
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscNamedCut{Xa}%
+      \lscLine{hot}{0.95}%
+      \lscNamedCut{Xb}%
+      \lscLine{hot}{0.05}
+      \lscAsynSnd{e}%
+      \lscLine{hot}{0.05}
+      \lscNamedCut{Xc}%
+      \lscLine{hot}{1.45}%
+      \lscNamedCut{Xd}%
+      \lscLine{hot}{0.5}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscNamedCut{Xa}%
+      \lscLine{hot}{0.05}%
+      \lscNamedCut{Xb}%
+      \lscLine{hot}{1.95}%
+      \lscNamedCut{Xc}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{0.5}%
+      \lscNamedCut{Xd}%
+      \lscLine{hot}{0.5}%
+    \end{lscinst}
+    %
+    \lscAsyn{e}{hot}{E}%
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.45\textwidth}%
+\small%
+{\begin{verbatim}
+\lscSetCutColour{lightgray}
+\lscSetNamedCutWidth{Xb}{1.5pt}
+\lscSetNamedCutColour{Xc}{green}
+\lscSetNamedCutColour{Xb}{blue}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xa}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.95}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xb}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.05}
+    \lscAsynSnd{e}%
+    \lscLine{hot}{0.05}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xc}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.45}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xd}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xa}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.05}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xb}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.95}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xc}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscAsynRcv{e}%
+    \lscLine{hot}{0.5}%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscNamedCut{Xd}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}%
+  \end{lscinst}
+  \lscAsyn{e}{hot}{E}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+To avoid cuts to hide each other, one will typically add very short instance
+line segments in between as shown in the example above.
+
+\medskip
+
+Using line style `none' one can easily obtain an animation effect as shown in
+the following example.
+
+\begin{center}%<@<
+\begin{minipage}{0.35\textwidth}
+  \newcommand{\lscanim}[1]{%
+    \lscSetCutLinestyle{none}%
+    \lscSetNamedCutLinestyle{#1}{solid}%
+    \begin{Lsc}{none}{2}{3}
+      \begin{lscinst}{Inst1}
+        \lscNamedCut{Xa}%
+        \lscLine{hot}{1}%
+        \lscNamedCut{Xb}%
+        \lscNamedCut{Xc}%
+        \lscAsynSnd{e}%
+        \lscLine{hot}{1.5}%
+        \lscNamedCut{Xd}%
+        \lscLine{hot}{0.5}%
+      \end{lscinst}
+      %
+      \begin{lscinst}{Inst2}
+        \lscNamedCut{Xa}%
+        \lscNamedCut{Xb}%
+        \lscLine{hot}{2}%
+        \lscNamedCut{Xc}%
+        \lscAsynRcv{e}%
+        \lscLine{hot}{0.5}%
+        \lscNamedCut{Xd}%
+        \lscLine{hot}{0.5}%
+      \end{lscinst}
+      %
+      \lscAsyn{e}{hot}{E}%
+    \end{Lsc}}
+  %
+  \scalebox{0.7}{\lscanim{Xa}}
+  \\[\bigskipamount]
+  \scalebox{0.7}{\lscanim{Xb}}
+  \\[\bigskipamount]
+  \scalebox{0.7}{\lscanim{Xc}}
+  \\[\bigskipamount]
+  \scalebox{0.7}{\lscanim{Xd}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\begin{verbatim}
+\newcommand{\lscanim}[1]{%
+  \lscSetCutLinestyle{none}%
+  \lscSetNamedCutLinestyle{#1}{solid}%
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscNamedCut{Xa}%
+      \lscLine{hot}{1}%
+      \lscNamedCut{Xb}%
+      \lscNamedCut{Xc}%
+      \lscAsynSnd{e}%
+      \lscLine{hot}{1.5}%
+      \lscNamedCut{Xd}%
+      \lscLine{hot}{0.5}%
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscNamedCut{Xa}%
+      \lscNamedCut{Xb}%
+      \lscLine{hot}{2}%
+      \lscNamedCut{Xc}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{0.5}%
+      \lscNamedCut{Xd}%
+      \lscLine{hot}{0.5}%
+    \end{lscinst}
+    %
+    \lscAsyn{e}{hot}{E}%
+  \end{Lsc}}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+\lscanim{Xa}\lscanim{Xb}
+\lscanim{Xc}\lscanim{Xd}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Putting Stuff at the Current Location}
+\label{sec:tech:put}
+
+%<@<
+  \index{lscPut@$\mlscPut$}%
+\begin{center}\fbox{
+\mlscPut%
+  \param{\var{stuff}}%
+}\end{center}
+
+The \mlscPut{} command typesets \var{stuff} at the current location.
+%
+This is useful to put additional labels or elements for which there is no
+explicit support.
+
+We use \mlscPut{}, for example, to draw the dashed frames indicating the
+location dimensions in Figure~\ref{fig:locdim}.
+
+\begin{center}%<@<
+\begin{minipage}{0.3\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{1}{3}
+    \begin{lscinst}{Inst}
+      \lscLine{hot}{1.5}
+      \lscPut{%
+        \psline{<-}(0.5,0.5)%
+        \rput[lb](0.5,0.5){You are here.}}
+      \lscLine{hot}{1.5}
+    \end{lscinst}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.575\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{1}{3}
+  \begin{lscinst}{Inst}
+    \lscLine{hot}{1.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscPut{%
+      \psline{<-}(0.5,0.5)%
+      \rput[lb](0.5,0.5){You are here.}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1.5}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Typesetting Play-Engine LSCs}
+\label{sec:pipo}
+
+As mentioned in the introduction, \lscsty{} in general renders LSC in the 
+  \index{style}%
+style of \cite{Klose2003}.
+%
+But it provides a couple of commands which support the typesetting of LSCs in
+the 
+  \index{style!play-engine}%
+play-engine style.
+
+In cases where the play-engine style is not supported, it may be sufficient to
+modify the existing elements, for example, by manually adding an hourglass to
+an action box to represent the saving of a timer.
+
+\subsection{Actors, Clocks, and Environments}
+\label{sec:pipo:actor}
+\label{sec:pipo:clock}
+\label{sec:pipo:env}
+
+%<@<
+  \index{lscActor@$\mlscActor$}%
+  \index{lscClock@$\mlscClock$}%
+  \index{lscEnv@$\mlscEnv$}%
+\begin{center}\fbox{\parbox{5em}{%
+\mlscActor%
+\newline
+\mlscClock%
+\newline
+\mlscEnv%
+}}\end{center}
+
+The \mlscActor{}, \mlscClock{}, and \mlscEnv{} draw the symbols which are used
+to mark the 
+  \index{instance line!actor}%
+  \index{actor}%
+actor, 
+  \index{instance line!clock}%
+  \index{clock}%
+clock, and 
+  \index{instance line!environment}%
+  \index{environment}%
+environment instance line.
+%
+They are best used as the label of a \mnoboxSD{} instance.
+
+\begin{center}%<@<
+\begin{minipage}{0.4\textwidth}
+ \scalebox{0.9}{%
+  \pssetlength{\lscLocationWidth}{1.75}%
+  \begin{Lsc}{none}{3}{3}
+    \begin{lscinst}[noboxSD]{\lscActor}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}[noboxSD]{\lscClock}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}[noboxSD]{\lscEnv}
+      \lscEnvLine{cold}{3}
+    \end{lscinst}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.525\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{3}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \begin{lscinst}[noboxSD]{\lscActor}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \begin{lscinst}[noboxSD]{\lscClock}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+  \end{lscinst}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+  \begin{lscinst}[noboxSD]{\lscEnv}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscEnvLine{cold}{3}
+  \end{lscinst}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Existential Symbolic Instances}
+\label{sec:pipo:inst}
+
+%<@<
+  \index{lscBalloon@$\mlscBalloon$}%
+\begin{center}\fbox{%
+\mlscBalloon%
+  \param{\this{$\mexistential$}\orthat{$\muniversal$}}%
+  \param{\var{stuff}}%
+}\end{center}
+
+The \mlscBalloon{} command draws 
+  \index{balloon}%
+  \index{think balloon}%
+think balloons that are used to provide 
+  \index{binding expression}%
+binding expressions of 
+  \index{symbolic instance}%
+symbolic instances.
+
+They have to be explicitly positioned using, e.g., \cmd{lscPut} and one has to
+care for vertical space before the LSC as they are not considered in the
+computation of the boundary box.
+%
+That is, symbolic instances can at best be called semi-supported.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}%
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}[esymMSC]{esymMSC}
+      \lscPut{%
+        \rput(0,0.9){\lscBalloon{existential}{.ID$=$ID}}}
+      \lscLine{hot}{3}
+    \end{lscinst}
+    \begin{lscinst}[esymSD]{esymSD}
+      \lscPut{%
+        \rput(0,0.9){\lscBalloon{universal}{.Alloc$> 0$}}}
+      \lscLine{hot}{3}
+    \end{lscinst}
+  \end{Lsc}}
+\end{minipage}%
+\hfill%
+\begin{minipage}{0.5\textwidth}%
+\small%
+{\gray%
+\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \begin{lscinst}[esymMSC]{esymMSC}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscPut{\rput(0,0.9){%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+      \lscBalloon%
+        {existential}{.ID$=$ID}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lscinst}
+  \begin{lscinst}[esymSD]{esymSD}
+\end{verbatim}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscPut{\rput(0,0.9){%
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+      \lscBalloon%
+        {universal}{.Alloc$> 0$}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{3}
+\end{verbatim}}%
+\verbunskip%
+\begin{verbatim}
+  \end{lscinst}
+\end{verbatim}%
+\verbunskip%
+{\gray%
+\begin{verbatim}
+\end{Lsc}
+\end{verbatim}}
+\end{minipage}
+\end{center}%>@>
+
+The combination on the right above is not a well-formed LSC instance.  It is
+only used to demonstrate both kinds of loops in the same figure.
+%>@>
+
+\subsection{Branching, Subcharts, and Loops}
+\label{sec:pipo:scopes}
+
+%<@<
+Both 
+  \index{branch}%
+branching and 
+  \index{loop}%
+loops are based on 
+  \index{subchart}%
+subcharts.
+%
+Subcharts are not directly supported but can be simulated by putting frames
+using \mlscPut{}.
+
+\begin{center}%<@<
+\pssetlength{\lscLocationWidth}{2}%
+\begin{minipage}{0.30\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{3}{4}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1.5}
+      \lscInstSnd{e}
+      \lscLine{hot}{1}
+      \lscInstSnd{f}
+      \lscLine{hot}{1.5}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{0.5}
+      \lscCond{hot}{$j = 0$}
+      \lscLine{hot}{1}
+      \lscInstRcv{e}
+      \lscLine{hot}{0.5}
+      \lscPut{\psframe[dimen=inner]%
+        (-1.5\lscLocationWidth,0)%
+        (0.5\lscLocationWidth,1.5\lscLocationHeight)}
+      \lscLine{hot}{0.5}
+      \lscInstRcv{f}
+      \lscLine{hot}{0.5}
+      \lscPut{\psframe[dimen=inner]%
+        (-1.5\lscLocationWidth,0)%
+        (0.5\lscLocationWidth,1\lscLocationHeight)}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \lscInst{e}{hot}{E}
+    \lscInst{f}{hot}{F}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.685\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{4}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1.5}\lscInstSnd{e}
+    \lscLine{hot}{1}\lscInstSnd{f}
+    \lscLine{hot}{1.5}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{0.5}
+    \lscCond{hot}{$j = 0$}
+    \lscLine{hot}{1}\lscInstRcv{e}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscPut{\psframe[dimen=inner]%
+     (-1.5\lscLocationWidth,0)%
+     (0.5\lscLocationWidth,1.5\lscLocationHeight)}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{0.5}\lscInstRcv{f}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscPut{\psframe[dimen=inner]%
+     (-1.5\lscLocationWidth,0)%
+     (0.5\lscLocationWidth,1\lscLocationHeight)}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+  \lscInst{e}{hot}{E}\lscInst{f}{hot}{F}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+
+\begin{center}%<@<
+\pssetlength{\lscLocationWidth}{2}%
+\begin{minipage}{0.30\textwidth}
+ \scalebox{0.9}{%
+  \begin{Lsc}{none}{3}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1.5}
+      \lscInstSnd{e}
+      \lscLine{hot}{1.5}
+    \end{lscinst}
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{1.5}
+      \lscInstRcv{e}
+      \lscLine{hot}{0.5}
+      \lscPut{\psframe[dimen=inner]%
+          (-1.5\lscLocationWidth,0)%
+          (0.5\lscLocationWidth,1.5\lscLocationHeight)%
+        \rput[lt](-1.5\lscLocationWidth,%
+          1.5\lscLocationHeight){%
+           \rput(0.3,-0.3){\textbf{3}}}}
+      \lscLine{hot}{1}
+    \end{lscinst}
+    \lscInst{e}{hot}{E}
+  \end{Lsc}
+ }%
+\end{minipage}
+\hfill
+\begin{minipage}{0.685\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{3}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1.5}\lscInstSnd{e}
+    \lscLine{hot}{1.5}
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{1.5}\lscInstRcv{e}
+    \lscLine{hot}{0.5}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+    \lscPut{\psframe[dimen=inner]%
+       (-1.5\lscLocationWidth,0)%
+       (.5\lscLocationWidth,1.5\lscLocationHeight)
+      \rput[lt](-1.5\lscLocationWidth,%
+       1.5\lscLocationHeight){%
+         \rput(0.3,-0.3){\textbf{3}}}}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+    \lscLine{hot}{1}
+  \end{lscinst}
+  \lscInst{e}{hot}{E}
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+
+\section{Tricks and Tweaks}
+\label{sec:tricks}
+
+\subsection{Linewidth}
+\label{sec:tricks:lines}
+
+%<@<
+All parts of the LSC (except for cuts) are rendered with the current
+\pstricks{} 
+  \index{linewidth}%
+linewidth.
+%
+That it, if the lines appear too 
+  \index{fat}%
+fat they can be globally be changed using
+\cmd{psset}.
+
+\begin{center}%<@<
+\begin{minipage}{0.45\textwidth}
+ \scalebox{0.9}{%
+  \psset{linewidth=0.25pt}
+  \begin{Lsc}{none}{2}{3}
+    \begin{lscinst}{Inst1}
+      \lscLine{hot}{1}%
+      \lscAsynSnd{e}%
+      \lscLine{hot}{2}%
+    \end{lscinst}
+    %
+    \begin{lscinst}{Inst2}
+      \lscLine{hot}{2}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{1}%
+    \end{lscinst}
+    %
+    \lscAsyn{e}{hot}{E}%
+  \end{Lsc}}
+\end{minipage}
+\hfill
+\begin{minipage}{0.35\textwidth}%
+\small%
+{\begin{verbatim}
+\psset{linewidth=0.25pt}
+\end{verbatim}}%
+\verbunskip%
+{\gray\begin{verbatim}
+\begin{Lsc}{none}{2}{3}
+  \begin{lscinst}{Inst1}
+    \lscLine{hot}{1}%
+    \lscAsynSnd{e}%
+    \lscLine{hot}{2}%
+  \end{lscinst}
+  \begin{lscinst}{Inst2}
+    \lscLine{hot}{2}%
+    \lscAsynRcv{e}%
+    \lscLine{hot}{1}%
+  \end{lscinst}
+  \lscAsyn{e}{hot}{E}%
+\end{Lsc}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\subsection{Scaling}
+\label{sec:tricks:scaling}
+
+%<@<
+LSCs can be 
+  \index{scale}%
+scaled by changing the width and height of locations (cf.
+Section~\ref{sec:inst:dim}) keeping the size of text.
+%
+To scale the LSC including all annotations, the \mFullLsc{} and \mLsc{}
+environments can be passed to a 
+  \index{scalebox}%
+\cmd{scalebox} command.
+
+\begin{center}%<@<
+\begin{minipage}{0.35\textwidth}
+  \centering
+  \newcommand{\scalex}{%
+    \begin{Lsc}{none}{2}{3.5}
+      \begin{lscinst}{$i_1$}
+        \lscLine{hot}{1}%
+        \lscAsynSnd{e}%
+        \lscLine{hot}{2.5}%
+      \end{lscinst}
+      \begin{lscinst}{$i_2$}
+        \lscLine{hot}{2}%
+        \lscAsynRcv{e}%
+        \lscLine{hot}{1.5}%
+      \end{lscinst}
+      \lscAsyn{e}{hot}{$E$}%
+    \end{Lsc}
+  }
+
+  {\pssetlength{\lscLocationWidth}{2}
+  \pssetlength{\lscLocationHeight}{0.666}
+  \scalex}%
+
+  \bigskip
+  {\pssetlength{\lscLocationWidth}{1.5}
+  \pssetlength{\lscLocationHeight}{0.5}
+  \scalex}%
+
+  \bigskip
+  {\pssetlength{\lscLocationWidth}{1}
+  \pssetlength{\lscLocationHeight}{0.333}
+  \scalex}%
+
+  \bigskip
+  \scalebox{0.5}{\scalex}
+\end{minipage}
+\hfill
+\begin{minipage}{0.535\textwidth}%
+\small%
+{\gray\begin{verbatim}
+\newcommand{\scalex}{%
+  \begin{Lsc}{none}{2}{3.5}
+    \begin{lscinst}{$i_1$}
+      \lscLine{hot}{1}%
+      \lscAsynSnd{e}%
+      \lscLine{hot}{2.5}%
+    \end{lscinst}
+    \begin{lscinst}{$i_2$}
+      \lscLine{hot}{2}%
+      \lscAsynRcv{e}%
+      \lscLine{hot}{1.5}%
+    \end{lscinst}
+    \lscAsyn{e}{hot}{$E$}%
+  \end{Lsc}
+\end{verbatim}}%
+\verbunskip%
+{\begin{verbatim}
+
+{\pssetlength{\lscLocationWidth}{2}
+\pssetlength{\lscLocationHeight}{0.666}
+\scalex}%
+
+{\pssetlength{\lscLocationWidth}{1.5}
+\pssetlength{\lscLocationHeight}{0.5}
+\scalex}%
+
+{\pssetlength{\lscLocationWidth}{1}
+\pssetlength{\lscLocationHeight}{0.333}
+\scalex}%
+
+\scalebox{0.5}{\scalex}
+\end{verbatim}}%
+\end{minipage}
+\end{center}%>@>
+%>@>
+
+\printindex
+
+\bibliographystyle{alpha}
+\bibliography{lsc}
+
+\clearpage
+\appendix
+\section*{License}
+
+This work may be distributed and/or modified under the conditions of the
+\LaTeX{} Project Public License, either version 1.3 of this license or (at
+your option) any later version.
+
+The latest version of this license is in
+%
+\begin{quote}
+\tt http://www.latex-project.org/lppl.txt
+\end{quote}
+%
+and version 1.3 or later is part of all distributions of \LaTeX{} version
+2005/12/01 or later.
+%
+This work has the LPPL maintenance status `maintained'.
+
+The Current Maintainer of this work is the copyright holder.
+%
+This work consists of the files README, lsc.sty, lsc.tex, lsc.bib.
+
+\medskip
+
+In addition, all examples from this manual may of course be freely used,
+modified, copied, and distributed in whole or partly.
+
+\end{document}
+vim:foldmethod=marker commentstring=%%s foldmarker=<@<,>@>
diff --git a/Master/texmf-dist/tex/latex/lsc/lsc.sty b/Master/texmf-dist/tex/latex/lsc/lsc.sty
new file mode 100644
index 00000000000..81077b7f20a
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/lsc/lsc.sty
@@ -0,0 +1,1967 @@
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+% $Id: lsc.sty,v 1.34 2006/02/23 12:57:15 berndw Exp $
+%
+% LSC -- A LaTeX style for typesetting Live Sequence Charts
+% 
+% 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.
+%
+% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{lsc}[2005/12/30 Typesetting LSCs]
+
+\RequirePackage{ifthen,pstricks,pst-node}
+
+% Structure:
+%
+% - global constants:
+%
+%   Commands and lengths that parameterise the appearance of LSCs in general.
+%   If one knows what one is doing, one may redefine them, e.g. to obtain
+%   smaller or wider instance line boxes. 
+%
+% - constant within lsc environment:
+%
+%   Commands and lengths that are set anew in each Lsc/FullLsc environment and
+%   remain constant within this environment, e.g. the total width and height
+%   of the pspicture environment.  There's typically no sense in changing any
+%   of these.
+%
+% - constant within instance:
+%
+%   Commands and lengths that are set anew in each lscinst/lsccreateinst
+%   environment and remain constant within this environment, e.g. whether this
+%   instance line needs a footer or not.  There's typically no sense in
+%   changing any of these.
+%
+% - global variables
+%
+%   Commands and lengths that are redefined during construction of the Lsc.
+%   Currently only the current X and Y drawing position.
+%
+% - "local" variables
+%
+%   Commands and lengths that are used by single commands, e.g. to compute the
+%   dimension of pre-chart kandisses or timer hourglasses.
+%
+% - helper macros
+%
+%   Many exported commands are actually only checking parameters for well-
+%   formedness and then call helper macros which do the work.  Some work
+%   macros even have own helper macros to factor out common code.
+%   There's typically no sense in calling any of these from user code.
+%
+% - exported interface
+%
+%   The commands and environments that are provided to the user.
+%
+% Notes:
+%
+% - things with multiple ends, like message arrows, local invariants, wide
+%   conditions etc. share the following philosophy:
+%
+%    - they get an ID by the user and internally define macros whose name
+%      comprises the ID and which typically capture the corresponding X and Y
+%      coordinates
+%
+%    - when the element is drawn, these macros are used and afterwards cleared
+
+% % globally constant: % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+\newcommand{\lsc@true}{true}
+\newcommand{\lsc@false}{false}
+
+%% width for a single instance line and height of a single location
+%
+\newlength{\lscLocationWidth}
+\pssetlength{\lscLocationWidth}{3}
+\newlength{\lscLocationHeight}
+\pssetlength{\lscLocationHeight}{1}
+
+%% the height of the black footer boxes in MSC-mode is determined by a \rule
+%  of height \lscFooterHeightFactor * \lscLocationHeight
+%
+%  Note: this is a command, not a length, hence it is set by, e.g.,
+%  \renewcommand{\lscFooterHeightFactor}{0.10}
+%
+\newcommand{\lscFooterHeightFactor}{0.20}
+
+%% half width of the square around the kill symbol 'X'
+%
+\newlength{\lscKillLength}
+\pssetlength{\lscKillLength}{0.33}
+
+%% position of local invariants to the left of the LSC
+%
+\newlength{\lsc@liL}
+\pssetlength{\lsc@liL}{0.2\lscLocationWidth}
+
+%% offset of the dotted line indicating coregion and width of the coregion
+%  line
+%
+\newlength{\lsc@coregoffset}
+\pssetlength{\lsc@coregoffset}{0.15}
+%
+\newlength{\lsc@coregwidth}
+\pssetlength{\lsc@coregwidth}{1pt}
+
+%% offset of message labels from the message arrows
+%
+\newlength{\lsc@labelsep}
+\pssetlength{\lsc@labelsep}{1.5pt}
+
+%% radius of dots used to indicate exclusive/inclusive beginning and ending
+%  of local invariants
+%
+\newlength{\lsc@dotradius}
+\pssetlength{\lsc@dotradius}{0.1}
+
+%% radius of circles used to mark atoms
+%
+\newlength{\lsc@atomradius}
+\pssetlength{\lsc@atomradius}{0.35}
+
+%% radius of circles used to mark simultaneous regions
+%
+\newlength{\lsc@simregradius}
+\pssetlength{\lsc@simregradius}{0.125}
+
+%% vertical distance between baseline of the label text and the create arrow
+%
+\newlength{\lsc@createoffset}
+\pssetlength{\lsc@createoffset}{0.3}
+\newlength{\lsc@instheadframesep}
+\pssetlength{\lsc@instheadframesep}{2pt}
+
+%% parameters of the hourglass used for timers:
+%
+%  I         _______
+%  I         \     /
+%  I          \   /
+%  I           \ /
+%  I<-----------X    -
+%  I           / \   |
+%  I          /   \  | hgheight
+%  I         /_____\ _
+%  I        |-w-|
+%  |--hgoffset--|
+%
+\newlength{\lsc@hgwidth}
+\pssetlength{\lsc@hgwidth}{0.125}
+\newlength{\lsc@hgheight}
+\pssetlength{\lsc@hgheight}{1.5\lsc@hgwidth}
+\newlength{\lsc@hgoffset}
+\pssetlength{\lsc@hgoffset}{4\lsc@hgwidth}
+
+%% parameters of the instance head boxes and precharts:
+%  a \rule of depth \lsc@instheadruledepth and height \lsc@instheadruleheight
+%  defines the shape of the instance head box, the \lsc@pccorrection is the
+%  length _above_ 0 (this is the bottom end of the instance head boxes) that
+%  the upper line of the prechart or universal/existential box should lie s.t.
+%  it comprises the instance head nicely.
+%  \lsc@pccorrection could have been defined as follows (and is not for
+%  historical reasons):
+%
+%     -\lsc@instheadruledepth
+%     + \lsc@instheadruleheight
+%     + \lsc@distancebetweeninstanceheadbox and prechart
+%
+\newlength{\lsc@instheadruledepth}
+\pssetlength{\lsc@instheadruledepth}{-0.8ex}
+\newlength{\lsc@instheadruleheight}
+\pssetlength{\lsc@instheadruleheight}{3ex}
+\newlength{\lsc@pccorrection}
+\pssetlength{\lsc@pccorrection}{5.55ex}
+
+%% half width of environment instance line
+%
+\newlength{\lsc@envlinewidth}
+\pssetlength{\lsc@envlinewidth}{0.1}
+
+%% baselineskip correction within the name/ac/am/i box
+%
+\newlength{\lsc@acamboxblskipcorrection}
+\setlength{\lsc@acamboxblskipcorrection}{-1.00\smallskipamount}
+
+%% width, colour, and linestyle of the line used to draw cuts
+%
+\newlength{\lscCutWidth}
+\setlength{\lscCutWidth}{3pt}
+%
+\newcommand{\lscCutColour}{red}
+%
+\newcommand{\lscCutLinestyle}{solid}
+
+%% strings for comparison in \if\else\fi
+%
+\def\lsc@hot{hot}%
+\def\lsc@cold{cold}%
+%
+\def\lsc@l{l}%
+\def\lsc@r{r}%
+%
+\def\lsc@ra{ra}%
+\def\lsc@rb{rb}%
+\def\lsc@la{la}%
+\def\lsc@lb{lb}%
+%
+\def\lsc@b{b}%
+\def\lsc@f{f}%
+%
+\def\lsc@incl{incl}%
+\def\lsc@excl{excl}%
+%
+\def\lsc@noboxSD{noboxSD}%
+\def\lsc@SD{SD}%
+\def\lsc@MSC{MSC}%
+\def\lsc@esymSD{esymSD}%
+\def\lsc@esymMSC{esymMSC}%
+%
+\def\lsc@universal{universal}%
+\def\lsc@existential{existential}%
+\def\lsc@none{none}%
+%
+\def\lsc@empty{}%
+\def\lsc@weak{weak}%
+\def\lsc@permissive{permissive}%
+\def\lsc@strict{strict}%
+%
+\def\lsc@initial{initial}%
+\def\lsc@invariant{invariant}%
+\def\lsc@iterative{iterative}%
+
+
+% % constant within lsc environment: % % % % % % % % % % % % % % % % % % % % %
+
+%% position of local invariants to the right of the LSC
+%
+\newlength{\lsc@liR}
+
+%% width of all instance lines within current pspicture (the pspicture may be
+%  wider if there is a prechart)
+%
+\newlength{\lsc@width}
+
+%% boundaries of current lsc's pspicture coordinate system
+%
+\newlength{\lsc@ulX}
+\newlength{\lsc@ulY}
+\newlength{\lsc@lrX}
+\newlength{\lsc@lrY}
+
+
+% % constant within instance:  % % % % % % % % % % % % % % % % % % % % % % % %
+
+%% true if the instance should be drawn in MSC, false if SD style requested
+%
+\newboolean{lsc@MSC}
+
+
+% % global variables:  % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+%% current x/y position in the pspicture set up by the lsc environment
+%  (variables)
+%
+\newlength{\lsc@X}
+\newlength{\lsc@Y}
+
+
+% % "local" variables: % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+%% used by many macros that draw condtion "kandises":
+%
+%    _________________________
+%   /                         \
+%  /                           \ _
+%  \                           / | kheight
+%   \_________________________/  _
+%   |   kwidth   |
+%  |   kxwidth   |
+%
+%  _______________
+%  \
+%   \
+%   /
+%  /______________
+%  |  kxxwidth   |
+%   |  kxwidth   |
+%
+%
+% kdepth is only a helper to compute the kheight, kxxwidth is only use by the
+% puzzle pieces for wide conditions.
+%
+\newsavebox{\lsc@kbox}
+\newlength{\lsc@kdepth}
+\newlength{\lsc@kwidth}
+\newlength{\lsc@kheight}
+\newlength{\lsc@kxwidth}
+\newlength{\lsc@kxxwidth}
+
+%% used for the computation of boundaries in FullLsc 
+%
+\newsavebox{\lsc@acambox}
+\newlength{\lsc@acamheight}
+
+%% used by the macro drawing local invariants
+%
+\newlength{\lsc@liX}
+\newlength{\lsc@licondY}
+
+%% used by the macro drawing the surrounding frame
+%
+\newlength{\lsc@frameheight}
+\newlength{\lsc@frametop}
+
+%% used for positioning the destination end of create arrows 
+%
+\newlength{\lsc@createinstX}
+\newlength{\lsc@createinstY}
+\newlength{\lsc@createinstW}
+
+%% used in \lsc@namedCut to compute the vertical difference between last and
+%  current cut (if this is small, don't draw the vertical line)
+%
+\newlength{\lsc@cutvdiff}
+
+%% used by the macro drawing coregions
+%
+\newlength{\lsc@crX}
+
+
+% % helper macros: % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+%% define height and depth of instance head boxes
+%
+\newcommand{\lsc@instheadrule}%
+  {\rule[\lsc@instheadruledepth]{0ex}{\lsc@instheadruleheight}}
+
+%% draw the "kandis" for conditions -- used for single-instance conditions and
+%  local invariants, not for conditions spanning multiple instance lines;
+%  drawback: the angle of vertexes is kept constant, this causes the "kandis"
+%  to grow wider with higher content
+%
+% \lsc@kandis[<psset-commands>]{<content>}
+%
+\newcommand{\lsc@kandis}[2][]{%
+  \sbox{\lsc@kbox}{#2}%
+  \settowidth{\lsc@kwidth}{\usebox{\lsc@kbox}}%
+  \setlength{\lsc@kwidth}{.5\lsc@kwidth}%
+% \addtolength{\lsc@kwidth}{\fboxsep}%
+  \settoheight{\lsc@kheight}{\usebox{\lsc@kbox}}%
+  \settodepth{\lsc@kdepth}{\usebox{\lsc@kbox}}%
+  \addtolength{\lsc@kheight}{\lsc@kdepth}%
+% \addtolength{\lsc@kheight}{\fboxsep}%
+  \setlength{\lsc@kxwidth}{\lsc@kwidth}%
+  \addtolength{\lsc@kxwidth}{\lsc@kheight}%
+  \begin{pspicture}(-\lsc@kxwidth,\lsc@kheight)(\lsc@kxwidth,-\lsc@kheight)%
+  \pspolygon[#1](-\lsc@kxwidth,0)%
+                (-\lsc@kwidth,\lsc@kheight)%
+                (\lsc@kwidth,\lsc@kheight)%
+                (\lsc@kxwidth,0)%
+                (\lsc@kwidth,-\lsc@kheight)%
+                (-\lsc@kwidth,-\lsc@kheight)%
+  \rput(0,0){\usebox{\lsc@kbox}}%
+  \end{pspicture}%
+}
+%
+\newcommand{\lsc@hotkandis}[1]{%
+  \lsc@kandis[fillstyle=solid,linestyle=solid]{#1}}
+%
+\newcommand{\lsc@coldkandis}[1]{%
+  \lsc@kandis[fillstyle=solid,linestyle=dashed]{#1}}
+
+%% save coordinates of message sending and reception (values are accessed by
+%  _name_ later)
+%
+%  The easy solution consisting of just placing nodes and later connecting
+%  them by lines does not work since then label end up positioned upside-down
+%  below arrows for those messages going from right to left.  Hence we need to
+%  have both coordinates to draw the line the right way.
+%
+% \lsc@msg{a|i}{snd|rcv}{id}
+%
+\newcommand{\lsc@msg}[3]{%
+  \expandafter\ifx\csname lsc@#1msg#3#2X\endcsname\relax%
+    \expandafter\xdef\csname lsc@#1msg#3#2X\endcsname{\the\lsc@X}%
+    \expandafter\xdef\csname lsc@#1msg#3#2Y\endcsname{\the\lsc@Y}%
+  \else%
+    \errmessage{LSC error: #3: message location already defined!}%
+  \fi%
+}
+%
+%  remove all helper definitions again to be able to detect errors with later
+%  messages who use the same name
+%
+% \lsc@clearmsg{a|i}{id}
+%
+\newcommand{\lsc@clearmsg}[2]{%
+  \global\expandafter\let\csname lsc@#1msg#2sndX\endcsname\relax%
+  \global\expandafter\let\csname lsc@#1msg#2sndY\endcsname\relax%
+  \global\expandafter\let\csname lsc@#1msg#2rcvX\endcsname\relax%
+  \global\expandafter\let\csname lsc@#1msg#2rcvY\endcsname\relax%
+}
+
+%% draw a simultaneous-region "kuller" (circle) -- whether it goes to front or
+%  back is determined by the hook that is defined to be this command
+%
+\newcommand{\lsc@simregionkuller}{%
+  \rput(\lsc@X,\lsc@Y){%
+    \pscircle*{\lsc@simregradius}}}
+
+%% save coordinates of conditions spanning multiple instance lines; if first
+%  called for a name, the coordinates of the leftmost end are stored, the
+%  coordinates of the rightmost end are overwritten each time, leaving the
+%  actual rightmost values in the end; the Y-coordinate is only stored on the
+%  first call (values are accessed by _name_ later)
+%
+% \lsc@widecondloc{<id>}
+%
+\newcommand{\lsc@widecondloc}[1]{%
+  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
+    \expandafter\xdef\csname lsc@wc#1leftmostX\endcsname{\the\lsc@X}%
+    \expandafter\xdef\csname lsc@wc#1Y\endcsname{\the\lsc@Y}%
+  \fi%
+  \expandafter\xdef\csname lsc@wc#1rightmostX\endcsname{\the\lsc@X}}%
+
+%% write a white block as part of the background of a condition spanning
+%  multiple instance lines; in other words, the background of these conditions
+%  is not drawn at once but separately on each instance line
+%
+%  The trick for getting the outline right is to draw "puzzles": on the
+%  leftmost instance, a
+%       _______
+%      /   |   \
+%      \___|___/
+%
+%  piece is drawn and on all other instances a
+%     _________
+%     \    |   \
+%     /____|___/
+%
+%  pieces.  This even gets wide conditions covering only a single instance
+%  line right.
+%
+% \lsc@lscfirstblock
+%
+\newcommand{\lsc@firstblock}{%
+  \pssetlength{\lsc@kxwidth}{0.5\lscLocationWidth}%
+  \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
+  \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
+  \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
+  \rput(\lsc@X,\lsc@Y){%
+    \pspolygon*[linecolor=white]%
+      (-\lsc@kxwidth,-0.5\lsc@kheight)%
+      (-\lsc@kwidth,0)%
+      (\lsc@kwidth,0)%
+      (\lsc@kxwidth,-0.5\lsc@kheight)%
+      (\lsc@kwidth,-\lsc@kheight)%
+      (-\lsc@kwidth,-\lsc@kheight)}}%
+
+% \lsc@lscotherblock
+%
+\newcommand{\lsc@otherblock}{%
+  \pssetlength{\lsc@kxwidth}{0.5\lscLocationWidth}%
+  \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
+  \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
+  \pssetlength{\lsc@kxxwidth}{\lsc@kxwidth}%
+  \psaddtolength{\lsc@kxxwidth}{0.35\lscLocationHeight}%
+  \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
+  \rput(\lsc@X,\lsc@Y){%
+    \pspolygon*[linecolor=white]%
+      (-\lsc@kxwidth,-0.5\lsc@kheight)%
+      (-\lsc@kxxwidth,0)%
+      (\lsc@kwidth,0)%
+      (\lsc@kxwidth,-0.5\lsc@kheight)%
+      (\lsc@kwidth,-\lsc@kheight)%
+      (-\lsc@kxxwidth,-\lsc@kheight)}}%
+
+%% set cut colour and width of a named cut and draw a named cut -- explicitly
+%  named cuts get names of the form 'lsc@cutnamed...Y', the unnamed cut has
+%  names of the form 'lsc@cutinternalY' 
+%
+% \lsc@setCutColour{<id>}{<colourname>}
+%
+\newcommand{\lsc@setCutColour}[2]{%
+  \expandafter\def\csname lsc@cut#1Colour\endcsname{#2}}
+
+% \lsc@setCutWidth{<id>}{<length>}
+%
+\newcommand{\lsc@setCutWidth}[2]{%
+  \expandafter\def\csname lsc@cut#1Width\endcsname{#2}}
+
+% \lsc@setCutLinestyle{<id>}{<linestyle>}
+%
+\newcommand{\lsc@setCutLinestyle}[2]{%
+  \expandafter\def\csname lsc@cut#1Linestyle\endcsname{#2}}
+
+%% drawing a cut with name <id> comprises drawing a line in colour
+%  \lsc@cut<id>Colour with width \lsc@cut<id>Width at the current Y location
+%  over the full location width.   If we are _not_ on the first instance,
+%  then firstly a line at the leftmost boundary of the current location is
+%  drawn from \lsc@cut<id>Y, the vertical position of the last cut segment, to
+%  the current Y location.
+%
+% \lsc@namedCut{<id>}
+%
+\newcommand{\lsc@namedCut}[1]{%
+  %
+  % if the linestyle is 'none', explicitly don't do anything -- otherwise the
+  % 'c-c' line ends are drawn anyway...
+  %
+  \ifthenelse{\equal{\csname lsc@cut#1Linestyle\endcsname}{none}}{%
+    \relax%
+  }{{%
+    \psset{linecolor=\csname lsc@cut#1Colour\endcsname,%
+           linewidth=\csname lsc@cut#1Width\endcsname,%
+           linestyle=\csname lsc@cut#1Linestyle\endcsname,%
+           arrows=c-c}%
+    %
+    % if we are not on the first instance, consider to draw a vertical line
+    %
+    \ifthenelse{\equal{\lsc@firstinst}{\lsc@false}}{%
+      %
+      % it's not sufficient to check the last and the current Y position for
+      % equality since minimal deviations have the effect that the vertical line
+      % is drawn (and consequently creates the ugly artefact)
+      %
+      \ifthenelse{\lengthtest{\csname lsc@cut#1Y\endcsname > \lsc@Y}}{%
+        \pssetlength{\lsc@cutvdiff}{\csname lsc@cut#1Y\endcsname}
+        \addtolength{\lsc@cutvdiff}{-\lsc@Y}
+      }{%
+        \pssetlength{\lsc@cutvdiff}{\lsc@Y}
+        \addtolength{\lsc@cutvdiff}{-\csname lsc@cut#1Y\endcsname}
+      }%
+       \ifthenelse{\lengthtest{\lsc@cutvdiff < \csname lsc@cut#1Width\endcsname}}{%
+         % skip: don't draw vertical line when at (roughly) same height
+       }{%
+         \rput(-0.5\lscLocationWidth,0){%
+           \psline(\lsc@X,\csname lsc@cut#1Y\endcsname)(\lsc@X,\lsc@Y)}%
+       }%
+    }{}%
+    %
+    % draw horizontal line
+    %
+    \rput(\lsc@X,\lsc@Y){%
+      \psline(-0.5\lscLocationWidth,0)(0.5\lscLocationWidth,0)}%
+    \expandafter\xdef\csname lsc@cut#1Y\endcsname{\the\lsc@Y}%
+  }}%
+}
+
+%% helper macros for scheduling, drawing, and clearing hooks
+%
+\newcommand{\lsc@schedhook}[2]{%
+  \global\expandafter\def\csname lsc@draw#1hook\endcsname{#2}%
+}
+%
+\newcommand{\lsc@clearhook}[1]{%
+  \global\expandafter\let\csname lsc@draw#1hook\endcsname\relax}%
+%
+\newcommand{\lsc@clearhooks}{%
+ \lsc@clearhook{actcond}%
+ \lsc@clearhook{atom}%
+ \lsc@clearhook{bgblock}%
+ \lsc@clearhook{bgsimreg}%
+ \lsc@clearhook{fgblock}%
+ \lsc@clearhook{fgsimreg}%
+ \lsc@clearhook{timer}%
+}
+%
+\newcommand{\lsc@flushhook}[1]{%
+  \csname lsc@draw#1hook\endcsname%
+  \lsc@clearhook{#1}%
+}
+
+%% do the things that have to be done before the instance line is drawn,
+%  currently this comprises only the drawing of a multi-instance line
+%  condition background if one is scheduled for drawing and a simregion
+%  kuller.  Used by ordinary and environment instance lines.
+%  ('Scheduling' is done by defining macros.)
+%
+\newcommand{\lsc@linePrelude}{%
+  \lsc@flushhook{bgsimreg}%
+  \lsc@flushhook{bgblock}}%
+
+%% do the things that have to be done after the instance line is drawn,
+%  currently drawing the following things given in order from back to front
+%  (if scheduled):
+%   - background of multi-instance line conditions
+%   - condition or action (implies that there can be either a condition or an
+%     action at a location)
+%   - timer
+%   - atom circle
+%
+%  Used by ordinary and environment instance lines.
+%
+\newcommand{\lsc@linePostlude}[1]{%
+  \lsc@flushhook{fgblock}%
+  \lsc@flushhook{actcond}%
+  \lsc@flushhook{timer}%
+  \lsc@flushhook{atom}%
+  \lsc@flushhook{fgsimreg}%
+  \global\advance\lsc@Y by-#1\lscLocationHeight}%
+
+%% macros to draw instance lines, ordinary and environment
+%
+% \lsc@line{<timinginterval>}{solid|dashed}{<length>}
+%
+\newcommand{\lsc@line}[3]{%
+  \lsc@linePrelude%
+  \rput(\lsc@X,\lsc@Y){%
+    %
+    % use \pcline only if really needed -- it make small dvi files
+    % significantly larger (adds about 0.5k per small LSC)
+    %
+    \psset{linestyle=#2}%
+    \ifthenelse{\equal{#1}{}}{%
+      \psline(0,-#3\lscLocationHeight)%
+    }{%
+      \pcline(0,0)(0,-#3\lscLocationHeight)%
+      \lput[l]{0}{\ {#1}}%
+    }%
+  }
+  \lsc@linePostlude{#3}%
+}
+%
+% \lsc@envline{<timinginterval>}{solid|none}{<length>}
+%
+\newcommand{\lsc@envline}[3]{%
+  \lsc@linePrelude%
+  \rput(\lsc@X,\lsc@Y){%
+    %
+    % if there is a timing interval, position it to the right of the rightmost
+    % edge of the box
+    %
+    \ifthenelse{\equal{#1}{}}{%
+    }{%
+      \rput(\lsc@envlinewidth,0){%
+        \pcline[linestyle=none](0,0)(0,-#3\lscLocationHeight)}%
+      \lput[l]{0}{\ {#1}}%
+    }%
+    %
+    % the instance line itself as a criss-cross filled box 
+    %
+    \pspolygon[linestyle=none,fillstyle=hlines]%
+      (-\lsc@envlinewidth,0)%
+      (\lsc@envlinewidth,0)%
+      (\lsc@envlinewidth,-#3\lscLocationHeight)%
+      (-\lsc@envlinewidth,-#3\lscLocationHeight)%
+    %
+    % if it's hot, add a solid line over the middle of the box
+    %
+    \psline[linestyle=#2](0,-#3\lscLocationHeight)%
+  }%
+  \lsc@linePostlude{#3}%
+}
+
+%% see whether the labels for both ends of the create arrow have been defined
+%  and if so draw the arrow.  Used by the lscCreate command and the
+%  lsccreateinst instance line.
+%
+% \lsc@createarrow{<id>}
+%
+\newcommand{\lsc@createarrow}[1]{%
+  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
+    \relax%
+  \else\expandafter\ifx\csname lsc@createdest#1\endcsname\relax%
+    \relax%
+  \else%
+      \ncline{->}{\csname lsc@createsrc#1node\endcsname}{\csname lsc@createdest#1node\endcsname}%
+      \global\expandafter\let\csname lsc@createsrc#1\endcsname\relax%
+      \global\expandafter\let\csname lsc@createdest#1\endcsname\relax%
+  \fi\fi%
+}
+
+%% the first two macros only draw the hourglass and hour-X of timer set/reset
+%  and timeout, the third macro constructs a timer symbol with label and the
+%  latter three macros are actually used by the exported macros. 
+%
+\newcommand{\lsc@hourglass}{%
+  \pspolygon[fillstyle=solid]%
+            (-\lsc@hgwidth,\lsc@hgheight)%
+            (\lsc@hgwidth,\lsc@hgheight)%
+            (-\lsc@hgwidth,-\lsc@hgheight)%
+            (\lsc@hgwidth,-\lsc@hgheight)}%
+%
+\newcommand{\lsc@hourx}{%
+  \psline(-\lsc@hgwidth,\lsc@hgheight)%
+         (\lsc@hgwidth,-\lsc@hgheight)%
+  \psline(-\lsc@hgwidth,-\lsc@hgheight)%
+         (\lsc@hgwidth,\lsc@hgheight)}%
+%
+% \lsc@timer{<xposition>}{<arrows>}{<symbol>}{<text>}
+%
+% The label <text> is placed to the left of the symbol if <xposition> is
+% negative and to the right otherwise.
+%
+% For <xposition>, currently only \lsc@hgoffset or -\lsc@hgoffset are used,
+% for <arrows> only '-' or '<-' and for <symbol> \lsc@hourglass or \lsc@hourx.
+%
+\newcommand{\lsc@timer}[4]{%
+  \rput(\lsc@X,\lsc@Y){%
+    \rput(#1,0){%
+      {#3}%
+      \ifthenelse{\lengthtest{#1 < 0pt}}{%
+        \rput[r](-1.5\lsc@hgwidth,0){{#4}}%
+      }{%
+        \rput[l](1.5\lsc@hgwidth,0){{#4}}%
+      }}%
+    \psline{#2}(0,0)(#1,0)}}%
+%
+\newcommand{\lsc@timerset}[3]{%
+  \lsc@timer{#1}{-}{\lsc@hourglass}{{#2}({#3})}}
+%
+\newcommand{\lsc@timerreset}[2]{%
+  \lsc@timer{#1}{-}{\lsc@hourx}{{#2}}}
+%
+\newcommand{\lsc@timeout}[2]{%
+  \lsc@timer{#1}{<-}{\lsc@hourglass}{{#2}}}
+
+%% draw hot and cold single-instance condition
+%
+\newcommand{\lsc@cond}[1]{%
+  \rput[t](\lsc@X,\lsc@Y){#1}}
+%
+\newcommand{\lsc@hotcond}[1]{%
+  \lsc@cond{\lsc@hotkandis{#1}}}%
+%
+\newcommand{\lsc@coldcond}[1]{%
+  \lsc@cond{\lsc@coldkandis{#1}}}%
+
+%% macros to draw the message arrow -- checks whether both ends are defined
+%
+%  \lsc@msgarrow{a|i}{<linestyle>}{<id>}{<label>}
+%
+% The arrow shape is controlled by \psset{} in wrapping macros.
+%
+\newcommand{\lsc@msgarrow}[4]{{%
+  \expandafter\ifx\csname lsc@#1msg#3sndX\endcsname\relax%
+    \errmessage{LSC error: #3: send location not defined?}%
+  \else\expandafter\ifx\csname lsc@#1msg#3sndY\endcsname\relax%
+    \errmessage{LSC error: #3: send location not defined?}%
+  \else\expandafter\ifx\csname lsc@#1msg#3rcvX\endcsname\relax%
+    \errmessage{LSC error: #3: receive location not defined?}%
+  \else\expandafter\ifx\csname lsc@#1msg#3rcvY\endcsname\relax%
+    \errmessage{LSC error: #3: receive location not defined?}%
+  \else
+    \psset{linestyle=#2}%
+    \ifthenelse{\lengthtest{\csname lsc@#1msg#3sndX\endcsname < \csname lsc@#1msg#3rcvX\endcsname}}{%
+      \pcline{->}%
+        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
+        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
+    }{%
+    \ifthenelse{\lengthtest{\csname lsc@#1msg#3sndX\endcsname > \csname lsc@#1msg#3rcvX\endcsname}}{%
+      \pcline{<-}%
+        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
+        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
+    }{%
+      \pcbar[arm=0.5]{->}%
+        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
+        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
+    }}%
+    \aput[\lsc@labelsep]{:U}{#4}%
+  \fi\fi\fi\fi%
+}}
+%
+% \lsc@asynarrow{solid|dashed}{<id>}{<label>}
+%
+\newcommand{\lsc@asynarrow}[3]{{%
+  \psset{arrowsize=2pt 3,arrowlength=3,arrowinset=0.80,linestyle=#1}%
+  \lsc@msgarrow{a}{#1}{#2}{#3}}}
+%
+%  \lsc@hotasynarrow{<id>}{<label>}
+%
+\newcommand{\lsc@hotasynarrow}[2]{%
+  \lsc@asynarrow{solid}{#1}{#2}}%
+%
+%  \lsc@coldasynarrow{<id>}{<label>}
+%
+\newcommand{\lsc@coldasynarrow}[2]{%
+  \lsc@asynarrow{dashed}{#1}{#2}}%
+%
+\newcommand{\lsc@instarrow}[3]{{%
+  \psset{arrowsize=2pt 3,arrowlength=2,arrowinset=0,linestyle=#1}%
+  \lsc@msgarrow{i}{#1}{#2}{#3}}}
+%
+%  \lsc@hotinstarrow{<id>}{<label>}
+%
+\newcommand{\lsc@hotinstarrow}[2]{%
+  \lsc@instarrow{solid}{#1}{#2}}%
+%
+%  \lsc@coldinstarrow{<id>}{<label>}
+%
+\newcommand{\lsc@coldinstarrow}[2]{%
+  \lsc@instarrow{dashed}{#1}{#2}}%
+
+%% macros to draw a local invariant
+%
+% \lsc@likuller{<yfactor>}{<ypos>}
+%
+% <yfactor> is '-0.5' for start and '0.5' for end kuller; this provides a
+% small "inwards" offset to the kuller s.t. subsequent local invariants remain
+% readable. <ypos> is the y-position.
+% Filling of the kuller is controlled by \psset{} in calling wrapper macros.
+%
+\newcommand{\lsc@likuller}[2]{%
+  \rput(\lsc@liX,#2){%
+    \pscircle[fillstyle=solid](0,#1\lsc@dotradius){\lsc@dotradius}}%
+}
+%
+% \lsc@incllikuller{<yfactor>}{<ypos>}
+%
+\newcommand{\lsc@incllikuller}[2]{{%
+  \psset{fillcolor=black}%
+  \lsc@likuller{#1}{#2}%
+}}
+%
+% \lsc@excllikuller{<yfactor>}{<ypos>}
+%
+\newcommand{\lsc@excllikuller}[2]{{%
+  \lsc@likuller{#1}{#2}%
+}}
+%
+% \lsc@inclstartkuller{<id>}
+%
+\newcommand{\lsc@inclstartkuller}[1]{%
+  \lsc@incllikuller{-0.5}{\csname lsc@li#1startY\endcsname}}%
+%
+% \lsc@exclstartkuller{<id>}
+%
+\newcommand{\lsc@exclstartkuller}[1]{%
+  \lsc@excllikuller{-0.5}{\csname lsc@li#1startY\endcsname}}%
+%
+% \lsc@inclendkuller{<id>}
+%
+\newcommand{\lsc@inclendkuller}[1]{%
+  \lsc@incllikuller{0.5}{\csname lsc@li#1endY\endcsname}}%
+%
+% \lsc@exclendkuller{<id>}
+%
+\newcommand{\lsc@exclendkuller}[1]{%
+  \lsc@excllikuller{0.5}{\csname lsc@li#1endY\endcsname}}%
+%
+% \lsc@locinv{r|l}{<id>}{incl|excl}{incl|excl}{<kandis>}%
+%
+% Assumes that the first parameter is 'r' or 'l' (should've been checked
+% before) but checks itself for 'incl' and 'excl'.  <kandis> should be the
+% stuff to be put next to the vertical line, it is typically a hot or cold
+% \lsc@kandis, i.e. temperature has to be handled in the calling macro.
+%
+\newcommand{\lsc@locinv}[5]{%
+  \expandafter\ifx\csname lsc@li#2startX\endcsname\relax%
+    \errmessage{LSC error: #2: local invariant begin not defined?}%
+  \else\expandafter\ifx\csname lsc@li#2startY\endcsname\relax%
+    \errmessage{LSC error: #2: local invariant begin not defined?}%
+  \else\expandafter\ifx\csname lsc@li#2endX\endcsname\relax%
+    \errmessage{LSC error: #2: local invariant end not defined?}%
+  \else\expandafter\ifx\csname lsc@li#2endY\endcsname\relax%
+    \errmessage{LSC error: #2: local invariant end not defined?}%
+  \else
+    %
+    % draw the connections to the locations on the instance lines
+    %
+    \psline[linestyle=dotted,dotsep=1pt]%
+      (\csname lsc@li#2startX\endcsname,\csname lsc@li#2startY\endcsname)%
+      (\lsc@liX,\csname lsc@li#2startY\endcsname)%
+    \psline%
+      (\lsc@liX,\csname lsc@li#2startY\endcsname)%
+      (\lsc@liX,\csname lsc@li#2endY\endcsname)%
+    \psline[linestyle=dotted,dotsep=1pt]%
+      (\lsc@liX,\csname lsc@li#2endY\endcsname)%
+      (\csname lsc@li#2endX\endcsname,\csname lsc@li#2endY\endcsname)%
+    %
+    % draw the "kandis"
+    %
+    \pssetlength{\lsc@licondY}{\csname lsc@li#2endY\endcsname}%
+    \psaddtolength{\lsc@licondY}{\csname lsc@li#2startY\endcsname}%
+    \pssetlength{\lsc@licondY}{0.5\lsc@licondY}%
+    \rput[#1](\lsc@liX,\lsc@licondY){#5}%
+    %
+    % put the inclusive/exclusive markers
+    %
+    \def\lsc@arg{#3}%
+    \ifx\lsc@arg\lsc@incl%
+      \lsc@inclstartkuller{#2}%
+    \else\ifx\lsc@arg\lsc@excl%
+      \lsc@exclstartkuller{#2}%
+    \else%
+      \errmessage{LSC error: \lsc@arg: Local invariant start must be "incl" or "excl"!}%
+    \fi\fi%
+    %
+    \def\lsc@arg{#4}%
+    \ifx\lsc@arg\lsc@incl%
+      \lsc@inclendkuller{#2}%
+    \else\ifx\lsc@arg\lsc@excl%
+      \lsc@exclendkuller{#2}%
+    \else%
+      \errmessage{LSC error: \lsc@arg: Local invariant end must be "incl" or "excl"!}%
+    \fi\fi%
+  \fi\fi\fi\fi%
+}
+
+%% macros to position the instance lines end of creation arrows
+%
+% \lsc@createdest{<id>}
+%
+% Puts the pnode for the creation arrow.  Communicates with calling macros by
+% the shared lengths \lsc@createinstX, \lsc@createinstY and the X-offset
+% \lsc@createinstW.
+%
+\newcommand{\lsc@setcreatedest}[1]{%
+  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
+    %
+    % if the src of the creation arrow doesn't exist already, then it will end
+    % up to the right of us thus place the node to the right of the box (!)...
+    %
+    \addtolength{\lsc@createinstX}{\lsc@createinstW}%
+  \else%
+    %
+    % ...otherwise put it to the left
+    %
+    \addtolength{\lsc@createinstX}{-\lsc@createinstW}%
+  \fi%
+  %
+  \pnode(\lsc@createinstX,\lsc@createinstY){\csname lsc@createdest#1node\endcsname}%
+  %
+  \expandafter\xdef\csname lsc@createdest#1\endcsname{\lsc@true}%
+  %
+  \lsc@createarrow{#1}%
+}
+%
+% \lsc@createboxdest{<id>}
+%
+\newcommand{\lsc@setcreateboxdest}[1]{%
+  %
+  % for boxed create instance heads, the arrow should end on the line of the
+  % box
+  %
+  \setlength{\lsc@createinstW}{0.4\lscLocationWidth}%
+  \addtolength{\lsc@createinstW}{\lsc@instheadframesep}%
+  %
+  \lsc@setcreatedest{#1}%
+}
+%
+% \lsc@createnoboxdest{<id>}{<label>}
+%
+\newcommand{\lsc@setcreatenoboxdest}[2]{%
+  %
+  % for non-boxed create instance heads, the arrow should end a little bit to
+  % the left or right of the label (!)
+  %
+  \settowidth{\lsc@createinstW}{#2}%
+  \setlength{\lsc@createinstW}{0.5\lsc@createinstW}%
+  \psaddtolength{\lsc@createinstW}{0.1em}%
+  \psaddtolength{\lsc@createinstW}{\lsc@instheadframesep}%
+  %
+  \lsc@setcreatedest{#1}%
+}
+
+%% macros to draw an instance head
+%
+% \lsc@insthead[<Y>]{solid|dashed|none}{true|false}{<label>}
+%
+% The boolean 'lsc@MSC', which indicates whether we are in an MSC instance
+% line or not, i.e. whether a footer has to be drawn or not, is set to the
+% second parameter.
+%
+\newcommand{\lsc@insthead}[4][0]{%
+   \rput[b](\lsc@X,#1){\psframebox[fillstyle=solid,framesep=\lsc@instheadframesep,linestyle=#2]{%
+     \makebox[0.80\lscLocationWidth]{#4\lsc@instheadrule}}}%
+   \setboolean{lsc@MSC}{#3}}%
+%
+% \lsc@instheadbox[<Y>]{solid|dashed}{true|false}{<label>}
+%
+\newcommand{\lsc@instheadbox}[4][0]{%
+  \lsc@insthead[#1]{#2}{#3}{#4}}
+%
+% \lsc@instheadnobox[<Y>]{true|false}{<label>}
+%
+\newcommand{\lsc@instheadnobox}[3][0]{%
+  \lsc@insthead[#1]{none}{#2}{#3}}
+%
+% \lsc@instheadnoboxSD[<Y>]{<label>}
+%
+\newcommand{\lsc@instheadnoboxSD}[2][0]{%
+  \lsc@instheadnobox[#1]{false}{#2}}
+%
+% \lsc@instheadSD[<Y>]{<label>}
+%
+\newcommand{\lsc@instheadSD}[3][0]{%
+  \lsc@instheadbox[#1]{#2}{false}{#3}}
+%
+% \lsc@instheadMSC[<Y>]{<label>}
+%
+\newcommand{\lsc@instheadMSC}[3][0]{%
+  \lsc@instheadbox[#1]{#2}{true}{#3}}
+
+%% macros to draw an instance foot
+%
+% \lsc@instend
+%
+% If drawn, the instance end (footer) goes to the current location, not the
+% bottom of the LSC picture environment.
+%
+\newcommand{\lsc@instend}{%
+  % put the end if in MSC mode
+  %
+  \ifthenelse{\boolean{lsc@MSC}}{%
+     \rput[b](\lsc@X,\lsc@Y){%
+       \psframebox[fillstyle=solid,fillcolor=black]{%
+         \makebox[0.80\lscLocationWidth]{%
+           \rule{0mm}{\lscFooterHeightFactor\lscLocationHeight}}}}%
+  }{%
+  }%
+  %
+  % if we are at the end of an instance line, then the next one is not a
+  % first instance line -- unless the next one occurs in a new 'Lsc'
+  % environment
+  %
+  \xdef\lsc@firstinst{\lsc@false}%
+  %
+  % advance X position for the next instance line
+  %
+  \global\advance\lsc@X by\lscLocationWidth%
+}
+
+%% helper macros for symbolic instance balloons
+%
+% \lsc@balloon{solid|dashed}{<stuff>}
+%
+\newcommand{\lsc@balloon}[2]{%
+  \pscircle(0.1,0){0.09}%
+  \pscircle(0.3,0.2){0.13}%
+  \rput[b](0.5,0.4){%
+    \psovalbox[fillstyle=solid,linestyle=#1]{#2}}}%
+
+%% draw multi-instance line condition
+%
+% \lsc@widecond{<id>}{solid|dashed}{<label>}
+%
+\newcommand{\lsc@widecond}[3]{%
+  \expandafter\ifx\csname lsc@wc#1rightmostX\endcsname\relax%
+    \errmessage{LSC error: #1: no locations wide condition defined?}%
+  \else\expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
+    \errmessage{LSC error: #1: no locations wide condition defined?}%
+  \else\expandafter\ifx\csname lsc@wc#1Y\endcsname\relax%
+    \errmessage{LSC error: #1: no locations wide condition defined?}%
+  \else%
+    %
+    % compute the extension of the whole kandis from the saved information --
+    % forgot what the exact strategy was, the plan is to place the outline
+    % correctly of course...  
+    %
+    \pssetlength{\lsc@kxwidth}{\csname lsc@wc#1rightmostX\endcsname}%
+    \psaddtolength{\lsc@kxwidth}{-\csname lsc@wc#1leftmostX\endcsname}%
+    \psaddtolength{\lsc@kxwidth}{\lscLocationWidth}%
+    \pssetlength{\lsc@kxwidth}{0.5\lsc@kxwidth}%
+    \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
+    \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
+    \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
+    %
+    % draw the outline of the kandis, the background has been drawn by the 
+    % \lscWidecondOn/Off commands
+    %
+    \rput(\csname lsc@wc#1leftmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
+      \rput(\lsc@kxwidth,0){%
+        \rput(-0.5\lscLocationWidth,0){%
+          \pspolygon[linestyle=#2](-\lsc@kxwidth,-0.5\lsc@kheight)%
+                                     (-\lsc@kwidth,0)%
+                                     (\lsc@kwidth,0)%
+                                     (\lsc@kxwidth,-0.5\lsc@kheight)%
+                                     (\lsc@kwidth,-\lsc@kheight)%
+                                     (-\lsc@kwidth,-\lsc@kheight)}}}%
+    %
+    % position the label in the middle of the kandis using an \ncline between
+    % two helper named nodes and pstricks' labelling functions
+    %
+    \rput(\csname lsc@wc#1leftmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
+      \rput(0,-0.35\lscLocationHeight){%
+        \pnode{lscATwcL}}}%
+    \rput(\csname lsc@wc#1rightmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
+      \rput(0,-0.35\lscLocationHeight){%
+        \pnode{lscATwcR}}}%
+    \ncline[linestyle=none]{lscATwcL}{lscATwcR}%
+    \lput{0}{#3}%
+  \fi\fi\fi%
+  %
+  % clear definitions
+  %
+  \global\expandafter\let\csname lsc@wc#1rightmostX\endcsname\relax%
+  \global\expandafter\let\csname lsc@wc#1leftmostX\endcsname\relax%
+  \global\expandafter\let\csname lsc@wc#1Y\endcsname\relax}
+
+%% helper macros for the Lsc/FullLsc environment
+%
+% \lsc@init{<nrinsts>}{<nrlocs>}
+%
+\newcommand{\lsc@init}[2]{%
+  %
+  % reset X position (Y is reset in 'lscinst')
+  %
+  \pssetlength{\lsc@X}{0.5\lscLocationWidth}%
+  %
+  % compute horizontal position of right-bound local invariants (depends on
+  % width of current LSC of course)
+  %
+  \pssetlength{\lsc@liR}{#1\lscLocationWidth}%
+  \psaddtolength{\lsc@liR}{-0.2\lscLocationWidth}%
+  %
+  % the next 'lscinst' will be the first (-> \lscCut)
+  %
+  \def\lsc@firstinst{\lsc@true}%
+  %
+  % undefine all schedulings (-> \lscLine)
+  %
+  \lsc@clearhooks%
+  %
+  % compute extent of the image; considering pre-chart, universal/existential
+  % frame, and the name-ac-am box
+  %
+  \pssetlength{\lsc@width}{#1\lscLocationWidth}%
+  \pssetlength{\lsc@ulX}{0}%
+  \pssetlength{\lsc@ulY}{0}%
+  \pssetlength{\lsc@lrX}{\lsc@width}%
+  \pssetlength{\lsc@lrY}{-#2\lscLocationHeight}%
+}
+%
+% \lsc@addpcwidthcorrection
+%
+\newcommand{\lsc@addpcwidthcorrection}{%
+  \psaddtolength{\lsc@ulX}{-0.25\lscLocationWidth}%
+  \psaddtolength{\lsc@lrX}{0.25\lscLocationWidth}%
+}
+%
+% \lsc@addpccorrection
+%
+\newcommand{\lsc@addpccorrection}{%
+  \psaddtolength{\lsc@ulY}{\lsc@pccorrection}%
+}
+%
+% \lsc@addframecorrection
+%
+\newcommand{\lsc@addframecorrection}{%
+  \psaddtolength{\lsc@lrY}{-0.1\lscLocationHeight}%
+}
+%
+% \lsc@mkacambox{<name>}{<ac>}{invariant|initial|iterative}{strict|weak|}
+%
+\newcommand{\lsc@mkacambox}[4]{%
+  \def\lsc@arg{#4}%
+  \ifx\lsc@arg\lsc@empty%
+    \def\lsc@i{}%
+  \else\ifx\lsc@arg\lsc@weak%
+    \def\lsc@i{\lsc@permissive}%
+  \else\ifx\lsc@arg\lsc@permissive%
+    \def\lsc@i{\lsc@permissive}%
+  \else\ifx\lsc@arg\lsc@strict%
+    \def\lsc@i{\lsc@strict}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: FullLSC interpretation must be "", "permissive", "weak", or "strict"!}%
+    \def\lsc@i{???}%
+  \fi\fi\fi\fi%
+  %
+  \def\lsc@arg{#3}%
+  \ifx\lsc@arg\lsc@invariant%
+    \def\lsc@am{\lsc@invariant}%
+  \else\ifx\lsc@arg\lsc@initial%
+    \def\lsc@am{\lsc@initial}%
+  \else\ifx\lsc@arg\lsc@iterative%
+    \def\lsc@am{\lsc@iterative}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: FullLSC interpretation must be "invariant", "initial", or "iterative"!}%
+    \def\lsc@am{???}%
+  \fi\fi\fi%
+  %
+  \sbox{\lsc@acambox}{%
+    \psframebox[fillstyle=solid,framesep=0]{%
+      \small%
+      \begin{tabular}{ll}%
+        LSC:&{#1}\\[\lsc@acamboxblskipcorrection]%
+        AC:&{#2}\\[\lsc@acamboxblskipcorrection]%
+        AM:&{\lsc@am}{\ \hfill}%
+        \ifthenelse{\equal{\lsc@i}{}}{%
+        }{\begin{tabular}{ll}%
+           I:&{\lsc@i}%
+          \end{tabular}}%
+      \end{tabular}\hspace{.5em}}}%
+  %
+  \settoheight{\lsc@acamheight}{\usebox{\lsc@acambox}}%
+  \psaddtolength{\lsc@ulY}{\lsc@acamheight}%
+  \settodepth{\lsc@acamheight}{\usebox{\lsc@acambox}}%
+  \psaddtolength{\lsc@ulY}{\lsc@acamheight}%
+}
+%
+% \lsc@prechart{<prechartloc>}
+%
+\newcommand{\lsc@prechart}[1]{%
+  \pssetlength{\lsc@kwidth}{\lsc@width}%
+  \pssetlength{\lsc@kwidth}{.5\lsc@kwidth}%
+  \pssetlength{\lsc@kxwidth}{\lsc@kwidth}%
+  %
+  \pssetlength{\lsc@frametop}{\lsc@pccorrection}%
+  %
+  \ifthenelse{\equal{#1}{}}{%
+    %
+    % no pre-chart: just adjust length
+    %
+    \pssetlength{\lsc@kheight}{0}%
+  }{%
+    \psaddtolength{\lsc@kxwidth}{0.25\lscLocationWidth}%
+    %
+    % draw the pre-chart
+    %
+    \pssetlength{\lsc@kheight}{#1\lscLocationHeight}%
+    \psaddtolength{\lsc@kheight}{\lsc@pccorrection}%
+    %
+    \rput(0.5\lsc@width,\lsc@pccorrection){%
+      \pspolygon[linestyle=dashed](-\lsc@kxwidth,-0.5\lsc@kheight)%
+                                  (-\lsc@kwidth,0)%
+                                  (\lsc@kwidth,0)%
+                                  (\lsc@kxwidth,-0.5\lsc@kheight)%
+                                  (\lsc@kwidth,-\lsc@kheight)%
+                                  (-\lsc@kwidth,-\lsc@kheight)}%
+    %
+    \psaddtolength{\lsc@frametop}{-\lsc@kheight}%
+  }%
+}
+%
+% \lsc@frame{solid|dashed}
+%
+\newcommand{\lsc@frame}[1]{%
+   %
+   % draw the universal/existential box
+   %
+   \pssetlength{\lsc@frameheight}{\lsc@lrY}%
+   \psaddtolength{\lsc@frameheight}{\lsc@kheight}%
+   \psaddtolength{\lsc@frameheight}{-\lsc@pccorrection}%
+   %
+   \rput(0.5\lsc@width,\lsc@frametop){%
+     \psframe[linestyle=#1]%
+       (-\lsc@kxwidth,0)(\lsc@kxwidth,\lsc@frameheight)}%
+}
+
+
+% % exported interface:  % % % % % % % % % % % % % % % % % % % % % % % % % % %
+
+%% additional space between the instance line and the local invariant
+%  condition (in addition to the default space)
+%
+%      |....................................
+%      |                                   O ______
+%      |                                   |<_cond_>
+%      |...................................O
+%      |
+%
+%      |< basic offset >|< lscLocInvOffset >
+%
+\newlength{\lscLocinvOffset}
+\pssetlength{\lscLocinvOffset}{0}
+
+% \lscAsynSnd{<id>}
+%
+\newcommand{\lscAsynSnd}[1]{%
+  \lsc@msg{a}{snd}{#1}}
+
+% \lscAsynRcv{<id>}
+%
+\newcommand{\lscAsynRcv}[1]{%
+  \lsc@msg{a}{rcv}{#1}}
+
+% \lscInstSnd{<id>}
+%
+\newcommand{\lscInstSnd}[1]{%
+  \lsc@msg{i}{snd}{#1}}
+
+% \lscInstRcv{<id>}
+%
+\newcommand{\lscInstRcv}[1]{%
+  \lsc@msg{i}{rcv}{#1}}
+
+% \lscTimerSet[r|l]{<timername>}{<timerduration>}
+%
+\newcommand{\lscTimerSet}[3][r]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@r%
+    \lsc@schedhook{timer}{\lsc@timerset{\lsc@hgoffset}{#2}{#3}}%
+  \else\ifx\lsc@arg\lsc@l%
+    \lsc@schedhook{timer}{\lsc@timerset{-\lsc@hgoffset}{#2}{#3}}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: TimerSet position must be "l" (left) or "r" (right)!}%
+  \fi\fi%
+}
+
+% \lscTimerReset[r|l]{<timername>}
+%
+\newcommand{\lscTimerReset}[2][r]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@r%
+    \lsc@schedhook{timer}{\lsc@timerreset{\lsc@hgoffset}{#2}}%
+  \else\ifx\lsc@arg\lsc@l%
+    \lsc@schedhook{timer}{\lsc@timerreset{-\lsc@hgoffset}{#2}}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: TimerReset position must be "l" (left) or "r" (right)!}%
+  \fi\fi%
+}
+
+% \lscTimeout[r|l]{<timername>}
+%
+\newcommand{\lscTimeout}[2][r]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@r%
+    \lsc@schedhook{timer}{\lsc@timeout{\lsc@hgoffset}{#2}}%
+  \else\ifx\lsc@arg\lsc@l%
+    \lsc@schedhook{timer}{\lsc@timeout{-\lsc@hgoffset}{#2}}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Timeout position must be "l" (left) or "r" (right)!}%
+  \fi\fi%
+}
+
+
+% \lscAct{<content>}
+%
+\newcommand{\lscAct}[1]{%
+  \lsc@schedhook{actcond}{%
+    \rput[t](\lsc@X,\lsc@Y){%
+      \psframebox[fillstyle=solid]{#1}}}}
+
+% schedule a single instance line condition for drawing
+%
+% \lscCond{hot|cold}{<content>}
+%
+\newcommand{\lscCond}[2]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@schedhook{actcond}{\lsc@hotcond{#2}}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@schedhook{actcond}{\lsc@coldcond{#2}}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Condition temperature must be "hot" or "cold"!}%
+  \fi\fi%
+}
+
+% \lscKill
+%
+\newcommand{\lscKill}{%
+  \rput(\lsc@X,\lsc@Y){%
+    \psline(-\lscKillLength,\lscKillLength)(\lscKillLength,-\lscKillLength)%
+    \psline(-\lscKillLength,-\lscKillLength)(\lscKillLength,\lscKillLength)}}
+
+% \lscCreate{<id>}
+%
+\newcommand{\lscCreate}[1]{%
+  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
+    \rput[b](\lsc@X,\lsc@Y){%
+      \pnode{\csname lsc@createsrc#1node\endcsname}}%
+    %
+    \expandafter\xdef\csname lsc@createsrc#1\endcsname{\lsc@true}%
+    %
+    \lsc@createarrow{#1}%
+  \else%
+    \errmessage{LSC error: #1: Creation arrow source already defined!}%
+  \fi%
+}
+
+% draw the background of a multi-instance line condition for the current
+% instance; 'Off' means, the condition lies behind the current instance line,
+% i.e. the condition does not synchronise it
+%
+% \lscWidecondOff{<id>}
+%
+\newcommand{\lscWidecondOff}[1]{%
+  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
+    \lsc@schedhook{bgblock}{\lsc@firstblock}%
+  \else%
+    \lsc@schedhook{bgblock}{\lsc@otherblock}%
+  \fi%
+  \lsc@widecondloc{#1}}%
+
+% (see above) 'On' means, the condition lies before the current instance line,
+% i.e. the condition synchronises on it
+%
+% \lscWidecondOn{<id>}
+%
+\newcommand{\lscWidecondOn}[1]{%
+  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
+    \lsc@schedhook{fgblock}{\lsc@firstblock}%
+  \else%
+    \lsc@schedhook{fgblock}{\lsc@otherblock}%
+  \fi%
+  \lsc@widecondloc{#1}}%
+
+% mark the beginning/end of local invariant <id>.  It is actually drawn later,
+% using \lscLocinv after beginning and end have been marked, by convention
+% after all 'lscinst' environments.
+%
+% \lscLocinvStart{<id>}
+% \lscLocinvBegin{<id>}
+%
+\newcommand{\lscLocinvStart}[1]{%
+  \expandafter\ifx\csname lsc@li#1startX\endcsname\relax%
+    \expandafter\xdef\csname lsc@li#1startX\endcsname{\the\lsc@X}%
+    \expandafter\xdef\csname lsc@li#1startY\endcsname{\the\lsc@Y}%
+  \else%
+    \errmessage{LSC error: #1: local invariant begin already defined!}%
+  \fi%
+}
+\let\lscLocinvBegin\lscLocinvStart%
+
+% \lscLocinvEnd{<id>}
+%
+\newcommand{\lscLocinvEnd}[1]{%
+  \expandafter\ifx\csname lsc@li#1endX\endcsname\relax%
+    \expandafter\xdef\csname lsc@li#1endX\endcsname{\the\lsc@X}%
+    \expandafter\xdef\csname lsc@li#1endY\endcsname{\the\lsc@Y}%
+  \else%
+    \errmessage{LSC error: #1: local invariant end already defined!}%
+  \fi%
+}
+
+% draw an atom circle at the current location and label it with <id>.  Using
+% this ID, it can be labelled later. 
+%
+% \lscAtom{<id>}
+%
+\newcommand{\lscAtom}[1]{%
+  \lsc@schedhook{atom}{%
+    \rput(\lsc@X,\lsc@Y){%
+      \cnode[linestyle=dashed,dash=2pt 2pt]{\lsc@atomradius}{#1}}}}
+
+% label the atom <id> with <content>, positioning the label explicitly by
+% giving the angle.
+%
+% \lscLabelAtomAt{<angle}{<id>}{<content>}
+%
+\newcommand{\lscLabelAtomAt}[3]{%
+  \nccircle[linestyle=none,angleA=#1]{-}{#2}{0.175}%
+  \Bput{#3}}
+
+% a shortcut for the (anticipated) four most common angles to put an atom
+% label.
+%
+% \lscLabelAtom[ra|rb|la|lb]{<id>}{<content>}
+%
+\newcommand{\lscLabelAtom}[3][ra]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@ra%
+    \lscLabelAtomAt{-45}{#2}{#3}%
+  \else\ifx\lsc@arg\lsc@rb%
+    \lscLabelAtomAt{-135}{#2}{#3}%
+  \else\ifx\lsc@arg\lsc@la%
+    \lscLabelAtomAt{45}{#2}{#3}%
+  \else\ifx\lsc@arg\lsc@lb%
+    \lscLabelAtomAt{135}{#2}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Atom label position must be "ra", "rb", "la", or "lb"!}%
+  \fi\fi\fi\fi%
+}
+
+%% draw an instance line at the current location with all scheduled
+%  conditions, timers, simregion kullers, etc.
+%
+% \lscLine[<timinginterval>]{hot|cold|none}{<length>}
+%
+% 'none' is not a semantical concept of LSCs but may be used to draw
+% "pathological" or schematic LSCs needing vertical space
+%
+\newcommand{\lscLine}[3][]{%
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@line{#1}{solid}{#3}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@line{#1}{dashed}{#3}%
+  \else\ifx\lsc@arg\lsc@none%
+    \lsc@line{#1}{none}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Instance line temperature must be "hot", "cold", or none!}%
+  \fi\fi\fi%
+}
+
+%% draw an environment instance line in the Sequence Diagram style
+%  (cf. \lscLine)
+%
+% \lscEnvLine[<timinginterval>]{hot|cold}{<length>}
+%
+\newcommand{\lscEnvLine}[3][]{%
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@envline{#1}{solid}{#3}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@envline{#1}{none}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Environment instance line temperature must be "hot" or "cold"!}%
+  \fi\fi%
+}
+
+%% set the name/line width for the cut with ID <id>.
+%
+% \lscSetNamedCutColour{<id>}{<colourname>}
+%
+\newcommand{\lscSetNamedCutColour}[2]{%
+  \lsc@setCutColour{named#1}{#2}}
+
+% \lscSetNamedCutWidth{<id>}{<length>}
+%
+\newcommand{\lscSetNamedCutWidth}[2]{%
+  \lsc@setCutWidth{named#1}{#2}}
+
+% \lscSetNamedCutWidth{<id>}{<linestyle>}
+%
+\newcommand{\lscSetNamedCutLinestyle}[2]{%
+  \lsc@setCutLinestyle{named#1}{#2}}
+
+% \lscSetCutColour{<colourname>}
+%
+\newcommand{\lscSetCutColour}[1]{%
+  \def\lscCutColour{#1}}
+
+% \lscSetCutWidth{<length>}
+%
+\newcommand{\lscSetCutWidth}[1]{%
+  \setlength{\lscCutWidth}{#1}}
+
+% \lscSetCutLinestyle{<linestyle>}
+%
+\newcommand{\lscSetCutLinestyle}[1]{%
+  \def\lscCutLinestyle{#1}}
+
+%% draw a named cut.  Using different IDs one may draw multiple cuts into a
+%  single LSC -- whatever this might be good for one time.
+%
+% \lscNamedCut{<id>}
+%
+\newcommand{\lscNamedCut}[1]{%
+  \expandafter\ifx\csname lsc@cutnamed#1Colour\endcsname\relax%
+    \lscSetNamedCutColour{#1}{\lscCutColour}%
+  \fi%
+  \expandafter\ifx\csname lsc@cutnamed#1Width\endcsname\relax%
+    \lscSetNamedCutWidth{#1}{\lscCutWidth}%
+  \fi%
+  \expandafter\ifx\csname lsc@cutnamed#1Linestyle\endcsname\relax%
+    \lscSetNamedCutLinestyle{#1}{\lscCutLinestyle}%
+  \fi%
+  \lsc@namedCut{named#1}}
+
+%% draw the default cut through the current location.  The cut might come out
+%  corrupted if not all instance environments of the current Lsc comprise
+%  exactly one \lscCut.
+%
+% \lscCut
+%
+\newcommand{\lscCut}{%
+  \lsc@setCutColour{iNtErN@l}{\lscCutColour}%
+  \lsc@setCutWidth{iNtErN@l}{\lscCutWidth}%
+  \lsc@setCutLinestyle{iNtErN@l}{\lscCutLinestyle}%
+  \lsc@namedCut{iNtErN@l}}
+
+%% \rput <content> to the current drawing X/Y position in the LSC; a nested
+%  \rput places stuff relative to the current drawing position
+%
+% \lscPut{<content>}
+%
+\newcommand{\lscPut}[1]{%
+  \rput(\lsc@X,\lsc@Y){#1}}
+
+%% actually draw an asynchronous communication whose beginning and end have
+%  been set.
+%
+% \lscAsyn{<id>}{hot|cold}{<label>}
+%
+\newcommand{\lscAsyn}[3]{%
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@hotasynarrow{#1}{#3}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@coldasynarrow{#1}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Message temperature must be "hot" or "cold"!}%
+  \fi\fi%
+  \lsc@clearmsg{a}{#1}}
+
+%% actually draw an instantaneous communication whose beginning and end have
+%  been set.
+%
+% \lscInst{<id>}{hot|cold}{<label>}
+%
+\newcommand{\lscInst}[3]{%
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@hotinstarrow{#1}{#3}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@coldinstarrow{#1}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Message temperature must be "hot" or "cold"!}%
+  \fi\fi%
+  \lsc@clearmsg{i}{#1}}
+
+%% actually draw a multi-instance line condition whose locations have been
+%  set (consecutively).
+%
+% \lscWidecond{<id>}{hot|cold}{<label>}
+%
+\newcommand{\lscWidecond}[3]{%
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@hot%
+    \lsc@widecond{#1}{solid}{#3}%
+  \else\ifx\lsc@arg\lsc@cold%
+    \lsc@widecond{#1}{dashed}{#3}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Wide condition temperature must be "hot" or "cold"!}%
+  \fi\fi%
+}
+
+%% actually draw a local invariant whose beginning and end have been set.
+%  Local invariants always appear to the left or to the right of the _whole_
+%  LSC not somewhere in the middle (controlled by the optional parameter with
+%  legal values 'r' (default) or 'l').  Layouting has been considered to
+%  become too complicated otherwise.
+%
+% \lscLocinv[r|l]{<id>}{incl|excl}{incl|excl}{hot|cold}{<content>}
+%
+\newcommand{\lscLocinv}[6][r]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@r%
+    \pssetlength{\lsc@liX}{\lsc@liR}%
+    \psaddtolength{\lsc@liX}{\lscLocinvOffset}%
+    \def\lsc@lilr{l}%
+  \else\ifx\lsc@arg\lsc@l%
+    \pssetlength{\lsc@liX}{\lsc@liL}%
+    \psaddtolength{\lsc@liX}{-\lscLocinvOffset}%
+    \def\lsc@lilr{r}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Local invariant position must be "l" (left) or "r" (right)!}%
+    \def\lsc@lilr{x}%
+  \fi\fi%
+  %
+  \ifx\lsc@lilr{x}%
+    \relax% get here only if #1 was illegal by def. of \lsc@lilr
+  \else%
+    \def\lsc@arg{#5}%
+    \ifx\lsc@arg\lsc@hot%
+      \lsc@locinv{\lsc@lilr}{#2}{#3}{#4}{\lsc@hotkandis{#6}}%
+    \else\ifx\lsc@arg\lsc@cold%
+      \lsc@locinv{\lsc@lilr}{#2}{#3}{#4}{\lsc@coldkandis{#6}}%
+    \else%
+      \errmessage{LSC error: \lsc@arg: Local invariant temperature must be "hot" or "cold"!}%
+    \fi\fi%
+  \fi%
+  %
+  % undefine begin and end
+  %
+  \global\expandafter\let\csname lsc@li#2startX\endcsname\relax%
+  \global\expandafter\let\csname lsc@li#2startY\endcsname\relax%
+  \global\expandafter\let\csname lsc@li#2endX\endcsname\relax%
+  \global\expandafter\let\csname lsc@li#2endY\endcsname\relax}
+
+%% mark the locations within the 'coregion' environment as a coregion
+%
+% \begin{coregion}[r|l]
+% \end{coregion}
+%
+\newenvironment{coregion}[1][l]{%
+  % compute the X position of the line parallel to the instance line
+  %
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@l%
+    \pssetlength{\lsc@crX}{-\lsc@coregoffset}%
+  \else\ifx\lsc@arg\lsc@r%
+    \pssetlength{\lsc@crX}{\lsc@coregoffset}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Coregion position must be "l" (left) or "r" (right)!  Continuing as if "l" was given.}%
+    \pssetlength{\lsc@crX}{-\lsc@coregoffset}% use the default
+  \fi\fi%
+  %
+  \rput(\lsc@X,\lsc@Y){%
+    \rput(\lsc@crX,\lsc@coregoffset){%
+      \pnode{lsccoregbegin}}}%
+}{%
+  \rput(\lsc@X,\lsc@Y){%
+    \rput(\lsc@crX,-\lsc@coregoffset){%
+      \pnode{lsccoregend}}}%
+  \ncline[linestyle=dotted,dotsep=2pt,linewidth=\lsc@coregwidth]{lsccoregbegin}{lsccoregend}%
+}
+
+%% mark the elements within the 'simregion' environment by a dot
+%
+% \begin{simregion}[b|f]
+% \end{simregion}
+%
+\newenvironment{simregion}[1][b]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@b%
+    \lsc@schedhook{bgsimreg}{\lsc@simregionkuller}%
+  \else\ifx\lsc@arg\lsc@f%
+    \lsc@schedhook{fgsimreg}{\lsc@simregionkuller}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: Simregion position must be "b" (background) or "f" (foreground)!}%
+  \fi\fi%
+}{%
+}
+
+%% a regular instance line
+%
+% \begin{lscinst}[MSC|SD|noboxSD|esymMSC|esymSD]{<instancename>}
+% \end{lscinst}
+%
+\newenvironment{lscinst}[2][MSC]{%
+  % reset current Y position
+  %
+  \pssetlength{\lsc@Y}{0}%
+  %
+  % draw the head
+  %
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@noboxSD%
+    \lsc@instheadnoboxSD{#2}%
+  \else\ifx\lsc@arg\lsc@SD%
+    \lsc@instheadSD{solid}{#2}%
+  \else\ifx\lsc@arg\lsc@MSC%
+    \lsc@instheadMSC{solid}{#2}%
+  \else\ifx\lsc@arg\lsc@esymSD%
+    \lsc@instheadSD{dashed}{#2}%
+  \else\ifx\lsc@arg\lsc@esymMSC%
+    \lsc@instheadMSC{dashed}{#2}%
+  \else%
+    \errmessage{LSC error: #1: Instance kind must be "MSC", "SD", "noboxSD", "esymMSC", or "esymSD"!}%
+  \fi\fi\fi\fi\fi%
+}{%
+  % draw the foot (if necessary)
+  %
+  \lsc@instend%
+}
+
+%% an instance line with ingoing creation arrow
+%
+% \begin{lsccreateinst}[MSC|SD|noboxSD|esymMSC|esymSD]{<length>}{<id>}{<instancename>}
+% \end{lsccreateinst}
+%
+% <length> is the vertical offset from the regular location of instance
+% heads, i.e. with <length> = 0 the position of the instance head is the same
+% as with regular instance lines.
+% The <id> can be referenced in an lscCreate 
+%
+\newenvironment{lsccreateinst}[4][MSC]{%
+  %
+  % reset current Y position (always, to break the layout not completely)
+  %
+  \pssetlength{\lsc@Y}{0}%
+  \global\advance\lsc@Y by-#2\lscLocationHeight%
+  %
+  \expandafter\ifx\csname lsc@createdest#3\endcsname\relax%
+    %
+    % common setup for the createarrow pnode
+    %
+    \pssetlength{\lsc@createinstX}{\lsc@X}%
+    \pssetlength{\lsc@createinstY}{\lsc@Y}%
+    \psaddtolength{\lsc@createinstY}{\lsc@createoffset}%
+    %
+    % put the head and the endpoint for the create arrow
+    % (and remember whether we are in SD or MSC mode for the footer)
+    %
+    \def\lsc@arg{#1}%
+    \ifx\lsc@arg\lsc@noboxSD%
+      \lsc@instheadnoboxSD[\lsc@Y]{#4}%
+      \lsc@setcreatenoboxdest{#3}{#4}%
+    \else\ifx\lsc@arg\lsc@MSC%
+      \lsc@instheadMSC[\lsc@Y]{solid}{#4}%
+      \lsc@setcreateboxdest{#3}%
+    \else\ifx\lsc@arg\lsc@SD%
+      \lsc@instheadSD[\lsc@Y]{solid}{#4}%
+      \lsc@setcreateboxdest{#3}%
+    \else\ifx\lsc@arg\lsc@esymMSC%
+      \lsc@instheadMSC[\lsc@Y]{dashed}{#4}%
+      \lsc@setcreateboxdest{#3}%
+    \else\ifx\lsc@arg\lsc@esymSD%
+      \lsc@instheadSD[\lsc@Y]{dashed}{#4}%
+      \lsc@setcreateboxdest{#3}%
+    \else%
+      \errmessage{LSC error: \lsc@arg: Creation instance kind must be "MSC", "SD", "noboxSD", "esymMSC", or "esymSD"!}%
+    \fi\fi\fi\fi\fi%
+  \else%
+    \errmessage{LSC error: #3: Creation instance already defined!}%
+  \fi%
+}{%
+  \lsc@instend%
+}
+
+%% symbolic instance line balloon
+%
+% \lscBalloon{existential|universal}{<stuff>}
+%
+\newcommand{\lscBalloon}[2]{%
+  \def\lsc@arg{#1}%
+  \ifx\lsc@arg\lsc@existential%
+    \lsc@balloon{dashed}{#2}%
+  \else\ifx\lsc@arg\lsc@universal%
+    \lsc@balloon{solid}{#2}%
+  \else%
+    \errmessage{LSC error: #1: Balloon quantification must be "universal" or "existential"!}%
+  \fi\fi%
+}
+
+%% the actor symbol
+%
+% \lscActor
+%
+\newcommand{\lscActor}{%
+  \begin{pspicture}(-0.275,0.275)(0.275,-0.275)%
+    \psline(0,0.3)(0,-0.1)%
+    \psline(-0.15,0.05)(0.15,0.05)%
+    \psline(-0.1,-0.15)(-0.1,-0.275)%
+    \psline(0.1,-0.15)(0.1,-0.275)%
+    \pscircle[fillstyle=solid](0,0.2){0.1}%
+    \pspolygon[fillstyle=solid](0,0.0)(-0.15,-0.15)(0.15,-0.15)%
+  \end{pspicture}}
+
+%% the clock symbol
+%
+% \lscClock
+%
+\newcommand{\lscClock}{%
+  \begin{pspicture}(-0.275,0.275)(0.275,-0.275)%
+    \pscircle{0.275}%
+    \pscircle{0.225}%
+    \psline(0,0.225)(0,0)(0.225,0)%
+  \end{pspicture}}
+
+%% the environment symbol
+%
+% \lscEnv
+%
+\newcommand{\lscEnv}{%
+  \begin{pspicture}(-0.5,0.275)(0.5,-0.275)%
+    \psarc(-0.3,0.2){0.1}{0}{180}%
+    \psarc(-0.1,0.2){0.1}{0}{180}%
+    \psarc(0.1,0.2){0.1}{0}{180}%
+    \psarc(0.3,0.2){0.1}{0}{180}%
+    \psarc(-0.3,-0.2){0.1}{180}{0}%
+    \psarc(-0.1,-0.2){0.1}{180}{0}%
+    \psarc(0.1,-0.2){0.1}{180}{0}%
+    \psarc(0.3,-0.2){0.1}{180}{0}%
+    \psarc(-0.4,0.1){0.1}{90}{-90}%
+    \psarc(-0.4,-0.1){0.1}{90}{-90}%
+    \psarc(0.4,0.1){0.1}{-90}{90}%
+    \psarc(0.4,-0.1){0.1}{-90}{90}%
+    \rput(0,0){{\footnotesize ENV}}%
+  \end{pspicture}}
+
+% \begin{Lsc}[<prechartloc>]{existential|universal|none}{<nrinsts>}{<nrlocs>}
+% \end{Lsc}
+%
+\newenvironment{Lsc}[4][]{%
+  \lsc@init{#3}{#4}%
+  %
+  \ifthenelse{\equal{#1}{} \and \equal{#2}{none}}{%
+    %
+    % special case: no prechart, no frame
+    %
+    \psaddtolength{\lsc@ulY}{-\lsc@instheadruledepth}%
+    \psaddtolength{\lsc@ulY}{\lsc@instheadruleheight}%
+  }{%
+    % have prechart or frame: correct height
+    %
+    \lsc@addpccorrection%
+    %
+    \ifthenelse{\equal{#1}{}}{%
+    }{%
+      % have prechart: correct width
+      %
+      \lsc@addpcwidthcorrection%
+    }%
+  }%
+  %
+  % add height correction if we shall draw a frame 
+  %
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@none%
+    \relax%
+  \else\ifx\lsc@arg\lsc@existential%
+    \lsc@addframecorrection%
+  \else\ifx\lsc@arg\lsc@universal%
+    \lsc@addframecorrection%
+  \else%
+    \errmessage{LSC error: \lsc@arg: LSC kind must be "existential", "universal", or "none"!}%
+  \fi\fi\fi%
+  %
+  % start the picture
+  %
+  \begin{pspicture}(\lsc@ulX,\lsc@ulY)(\lsc@lrX,\lsc@lrY)%
+  %
+  % draw the prechart (also sets up some lengths for the frame)
+  %
+  \lsc@prechart{#1}%
+  %
+  % draw the universal/existential frame
+  %
+  \def\lsc@arg{#2}%
+  \ifx\lsc@arg\lsc@existential%
+    \lsc@frame{dashed}%
+  \else\ifx\lsc@arg\lsc@universal%
+    \lsc@frame{solid}%
+  \else\ifx\lsc@arg\lsc@none%
+    \relax%
+  \else%
+    \relax% error message is printed above 
+  \fi\fi\fi%
+}{%
+  \end{pspicture}%
+}%
+
+% \begin{FullLsc}[<prechartloc>]{<name>}{<ac>}{invariant|initial|iterative}{strict|weak|}{existential|universal}{<nrinsts>}{<nrlocs>}
+% \end{FullLsc}
+%
+\newenvironment{FullLsc}[8][]{%
+  \lsc@init{#7}{#8}%
+  %
+  \lsc@addpccorrection%
+  \lsc@addframecorrection%
+  %
+  \ifthenelse{\equal{#1}{}}{%
+  }{%
+    \lsc@addpcwidthcorrection%
+  }%
+  %
+  \lsc@mkacambox{#2}{#3}{#4}{#5}%
+  %
+  % start the picture
+  %
+  \begin{pspicture}(\lsc@ulX,\lsc@ulY)(\lsc@lrX,\lsc@lrY)%
+  %
+  % draw the prechart (also sets up some lengths for the frame)
+  %
+  \lsc@prechart{#1}%
+  %
+  % draw the universal/existential frame
+  %
+  \def\lsc@arg{#6}%
+  \ifx\lsc@arg\lsc@existential%
+    \lsc@frame{dashed}%
+  \else\ifx\lsc@arg\lsc@universal%
+    \lsc@frame{solid}%
+  \else%
+    \errmessage{LSC error: \lsc@arg: LSC quantification must be "existential" or "universal"!}%
+  \fi\fi%
+  %
+  \rput[lb](0,\lsc@pccorrection){%
+    \usebox{\lsc@acambox}}
+}{%
+  \end{pspicture}
+}%
+
+\endinput
diff --git a/Master/texmf-dist/tpm/lsc.tpm b/Master/texmf-dist/tpm/lsc.tpm
new file mode 100644
index 00000000000..251144e8901
--- /dev/null
+++ b/Master/texmf-dist/tpm/lsc.tpm
@@ -0,0 +1,27 @@
+<!DOCTYPE rdf:RDF SYSTEM "../../support/tpm.dtd">
+<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:TPM="http://texlive.dante.de/">
+  <rdf:Description about="http://texlive.dante.de/texlive/Package/lsc.zip">
+    <TPM:Name>lsc</TPM:Name>
+    <TPM:Type>Package</TPM:Type>
+    <TPM:Date>2006/02/23 12:57:00</TPM:Date>
+    <TPM:Version></TPM:Version>
+    <TPM:Creator>karl</TPM:Creator>
+    <TPM:Title>The lsc package.</TPM:Title>
+    <TPM:Description></TPM:Description>
+    <TPM:Author></TPM:Author>
+    <TPM:Size>356734</TPM:Size>
+    <TPM:Build/>
+    <TPM:RunFiles size="63581">
+texmf-dist/bibtex/bib/lsc/lsc.bib
+texmf-dist/tex/latex/lsc/lsc.sty
+texmf-dist/tpm/lsc.tpm
+    </TPM:RunFiles>
+    <TPM:DocFiles size="294065">
+texmf-dist/doc/latex/lsc/README
+texmf-dist/doc/latex/lsc/lsc.pdf
+texmf-dist/doc/latex/lsc/lsc.tex
+    </TPM:DocFiles>
+    <TPM:Provides>Package/lsc</TPM:Provides>
+  </rdf:Description>
+</rdf:RDF>
+
diff --git a/Master/texmf/lists/lsc b/Master/texmf/lists/lsc
new file mode 100644
index 00000000000..70a9d75c5cb
--- /dev/null
+++ b/Master/texmf/lists/lsc
@@ -0,0 +1,9 @@
+texmf-dist/doc/latex/lsc/README
+texmf-dist/doc/latex/lsc/lsc.pdf
+texmf-dist/doc/latex/lsc/lsc.tex
+
+texmf-dist/bibtex/bib/lsc/lsc.bib
+texmf-dist/tex/latex/lsc/lsc.sty
+texmf-dist/tpm/lsc.tpm
+
+texmf/lists/lsc
diff --git a/Master/texmf/tpm/collection-latexextra.tpm b/Master/texmf/tpm/collection-latexextra.tpm
index 010b3e49ad3..1858e703665 100644
--- a/Master/texmf/tpm/collection-latexextra.tpm
+++ b/Master/texmf/tpm/collection-latexextra.tpm
@@ -249,6 +249,7 @@ A large collection of add-on packages for LaTeX.
       <TPM:Package name="listofsymbols"/>
       <TPM:Package name="localloc"/>
       <TPM:Package name="logpap"/>
+      <TPM:Package name="msc"/>
       <TPM:Package name="ltablex"/>
       <TPM:Package name="ltabptch"/>
       <TPM:Package name="ltxindex"/>