diff options
author | Karl Berry <karl@freefriends.org> | 2006-07-23 23:48:50 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2006-07-23 23:48:50 +0000 |
commit | 68b95e72d5ea1fe8fa89e11bc896a33ce8c42cc5 (patch) | |
tree | b7166d594b0610a6a6b8ac9fc3e7d05119aa8892 /Master/texmf-dist/doc/latex/lsc | |
parent | 40017fc23f5df1b885094287255acd2138fe727e (diff) |
new (latex) package lsc (23feb06)
git-svn-id: svn://tug.org/texlive/trunk@1908 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/lsc')
-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 |
3 files changed, 3969 insertions, 0 deletions
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=<@<,>@> |