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