% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % $Id: lsc.tex,v 1.17 2006/02/23 12:57:15 berndw Exp $ % % User's manual for lsc.sty. % % Author: Bernd Westphal % % 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=<@<,>@>