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