% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
% $Id: lsc.sty,v 1.34 2006/02/23 12:57:15 berndw Exp $
%
% LSC -- A LaTeX style for typesetting Live Sequence Charts
% 
% Author: Bernd Westphal <westphal@informatik.uni-oldenburg.de> 
% 
% Copyright (c) 2005-2006 Bernd Westphal.  All rights reserved.
%
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%
% This work may be distributed and/or modified under the conditions of
% the LaTeX Project Public License, either version 1.3 of this license
% or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
% 
% The Current Maintainer of this work is the copyright holder.
%
% This work consists of the files README, lsc.sty, lsc.tex, lsc.bib.
%
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{lsc}[2005/12/30 Typesetting LSCs]

\RequirePackage{ifthen,pstricks,pst-node}

% Structure:
%
% - global constants:
%
%   Commands and lengths that parameterise the appearance of LSCs in general.
%   If one knows what one is doing, one may redefine them, e.g. to obtain
%   smaller or wider instance line boxes. 
%
% - constant within lsc environment:
%
%   Commands and lengths that are set anew in each Lsc/FullLsc environment and
%   remain constant within this environment, e.g. the total width and height
%   of the pspicture environment.  There's typically no sense in changing any
%   of these.
%
% - constant within instance:
%
%   Commands and lengths that are set anew in each lscinst/lsccreateinst
%   environment and remain constant within this environment, e.g. whether this
%   instance line needs a footer or not.  There's typically no sense in
%   changing any of these.
%
% - global variables
%
%   Commands and lengths that are redefined during construction of the Lsc.
%   Currently only the current X and Y drawing position.
%
% - "local" variables
%
%   Commands and lengths that are used by single commands, e.g. to compute the
%   dimension of pre-chart kandisses or timer hourglasses.
%
% - helper macros
%
%   Many exported commands are actually only checking parameters for well-
%   formedness and then call helper macros which do the work.  Some work
%   macros even have own helper macros to factor out common code.
%   There's typically no sense in calling any of these from user code.
%
% - exported interface
%
%   The commands and environments that are provided to the user.
%
% Notes:
%
% - things with multiple ends, like message arrows, local invariants, wide
%   conditions etc. share the following philosophy:
%
%    - they get an ID by the user and internally define macros whose name
%      comprises the ID and which typically capture the corresponding X and Y
%      coordinates
%
%    - when the element is drawn, these macros are used and afterwards cleared

% % globally constant: % % % % % % % % % % % % % % % % % % % % % % % % % % % %

\newcommand{\lsc@true}{true}
\newcommand{\lsc@false}{false}

%% width for a single instance line and height of a single location
%
\newlength{\lscLocationWidth}
\pssetlength{\lscLocationWidth}{3}
\newlength{\lscLocationHeight}
\pssetlength{\lscLocationHeight}{1}

%% the height of the black footer boxes in MSC-mode is determined by a \rule
%  of height \lscFooterHeightFactor * \lscLocationHeight
%
%  Note: this is a command, not a length, hence it is set by, e.g.,
%  \renewcommand{\lscFooterHeightFactor}{0.10}
%
\newcommand{\lscFooterHeightFactor}{0.20}

%% half width of the square around the kill symbol 'X'
%
\newlength{\lscKillLength}
\pssetlength{\lscKillLength}{0.33}

%% position of local invariants to the left of the LSC
%
\newlength{\lsc@liL}
\pssetlength{\lsc@liL}{0.2\lscLocationWidth}

%% offset of the dotted line indicating coregion and width of the coregion
%  line
%
\newlength{\lsc@coregoffset}
\pssetlength{\lsc@coregoffset}{0.15}
%
\newlength{\lsc@coregwidth}
\pssetlength{\lsc@coregwidth}{1pt}

%% offset of message labels from the message arrows
%
\newlength{\lsc@labelsep}
\pssetlength{\lsc@labelsep}{1.5pt}

%% radius of dots used to indicate exclusive/inclusive beginning and ending
%  of local invariants
%
\newlength{\lsc@dotradius}
\pssetlength{\lsc@dotradius}{0.1}

%% radius of circles used to mark atoms
%
\newlength{\lsc@atomradius}
\pssetlength{\lsc@atomradius}{0.35}

%% radius of circles used to mark simultaneous regions
%
\newlength{\lsc@simregradius}
\pssetlength{\lsc@simregradius}{0.125}

%% vertical distance between baseline of the label text and the create arrow
%
\newlength{\lsc@createoffset}
\pssetlength{\lsc@createoffset}{0.3}
\newlength{\lsc@instheadframesep}
\pssetlength{\lsc@instheadframesep}{2pt}

%% parameters of the hourglass used for timers:
%
%  I         _______
%  I         \     /
%  I          \   /
%  I           \ /
%  I<-----------X    -
%  I           / \   |
%  I          /   \  | hgheight
%  I         /_____\ _
%  I        |-w-|
%  |--hgoffset--|
%
\newlength{\lsc@hgwidth}
\pssetlength{\lsc@hgwidth}{0.125}
\newlength{\lsc@hgheight}
\pssetlength{\lsc@hgheight}{1.5\lsc@hgwidth}
\newlength{\lsc@hgoffset}
\pssetlength{\lsc@hgoffset}{4\lsc@hgwidth}

%% parameters of the instance head boxes and precharts:
%  a \rule of depth \lsc@instheadruledepth and height \lsc@instheadruleheight
%  defines the shape of the instance head box, the \lsc@pccorrection is the
%  length _above_ 0 (this is the bottom end of the instance head boxes) that
%  the upper line of the prechart or universal/existential box should lie s.t.
%  it comprises the instance head nicely.
%  \lsc@pccorrection could have been defined as follows (and is not for
%  historical reasons):
%
%     -\lsc@instheadruledepth
%     + \lsc@instheadruleheight
%     + \lsc@distancebetweeninstanceheadbox and prechart
%
\newlength{\lsc@instheadruledepth}
\pssetlength{\lsc@instheadruledepth}{-0.8ex}
\newlength{\lsc@instheadruleheight}
\pssetlength{\lsc@instheadruleheight}{3ex}
\newlength{\lsc@pccorrection}
\pssetlength{\lsc@pccorrection}{5.55ex}

%% half width of environment instance line
%
\newlength{\lsc@envlinewidth}
\pssetlength{\lsc@envlinewidth}{0.1}

%% baselineskip correction within the name/ac/am/i box
%
\newlength{\lsc@acamboxblskipcorrection}
\setlength{\lsc@acamboxblskipcorrection}{-1.00\smallskipamount}

%% width, colour, and linestyle of the line used to draw cuts
%
\newlength{\lscCutWidth}
\setlength{\lscCutWidth}{3pt}
%
\newcommand{\lscCutColour}{red}
%
\newcommand{\lscCutLinestyle}{solid}

%% strings for comparison in \if\else\fi
%
\def\lsc@hot{hot}%
\def\lsc@cold{cold}%
%
\def\lsc@l{l}%
\def\lsc@r{r}%
%
\def\lsc@ra{ra}%
\def\lsc@rb{rb}%
\def\lsc@la{la}%
\def\lsc@lb{lb}%
%
\def\lsc@b{b}%
\def\lsc@f{f}%
%
\def\lsc@incl{incl}%
\def\lsc@excl{excl}%
%
\def\lsc@noboxSD{noboxSD}%
\def\lsc@SD{SD}%
\def\lsc@MSC{MSC}%
\def\lsc@esymSD{esymSD}%
\def\lsc@esymMSC{esymMSC}%
%
\def\lsc@universal{universal}%
\def\lsc@existential{existential}%
\def\lsc@none{none}%
%
\def\lsc@empty{}%
\def\lsc@weak{weak}%
\def\lsc@permissive{permissive}%
\def\lsc@strict{strict}%
%
\def\lsc@initial{initial}%
\def\lsc@invariant{invariant}%
\def\lsc@iterative{iterative}%


% % constant within lsc environment: % % % % % % % % % % % % % % % % % % % % %

%% position of local invariants to the right of the LSC
%
\newlength{\lsc@liR}

%% width of all instance lines within current pspicture (the pspicture may be
%  wider if there is a prechart)
%
\newlength{\lsc@width}

%% boundaries of current lsc's pspicture coordinate system
%
\newlength{\lsc@ulX}
\newlength{\lsc@ulY}
\newlength{\lsc@lrX}
\newlength{\lsc@lrY}


% % constant within instance:  % % % % % % % % % % % % % % % % % % % % % % % %

%% true if the instance should be drawn in MSC, false if SD style requested
%
\newboolean{lsc@MSC}


% % global variables:  % % % % % % % % % % % % % % % % % % % % % % % % % % % %

%% current x/y position in the pspicture set up by the lsc environment
%  (variables)
%
\newlength{\lsc@X}
\newlength{\lsc@Y}


% % "local" variables: % % % % % % % % % % % % % % % % % % % % % % % % % % % %

%% used by many macros that draw condtion "kandises":
%
%    _________________________
%   /                         \
%  /                           \ _
%  \                           / | kheight
%   \_________________________/  _
%   |   kwidth   |
%  |   kxwidth   |
%
%  _______________
%  \
%   \
%   /
%  /______________
%  |  kxxwidth   |
%   |  kxwidth   |
%
%
% kdepth is only a helper to compute the kheight, kxxwidth is only use by the
% puzzle pieces for wide conditions.
%
\newsavebox{\lsc@kbox}
\newlength{\lsc@kdepth}
\newlength{\lsc@kwidth}
\newlength{\lsc@kheight}
\newlength{\lsc@kxwidth}
\newlength{\lsc@kxxwidth}

%% used for the computation of boundaries in FullLsc 
%
\newsavebox{\lsc@acambox}
\newlength{\lsc@acamheight}

%% used by the macro drawing local invariants
%
\newlength{\lsc@liX}
\newlength{\lsc@licondY}

%% used by the macro drawing the surrounding frame
%
\newlength{\lsc@frameheight}
\newlength{\lsc@frametop}

%% used for positioning the destination end of create arrows 
%
\newlength{\lsc@createinstX}
\newlength{\lsc@createinstY}
\newlength{\lsc@createinstW}

%% used in \lsc@namedCut to compute the vertical difference between last and
%  current cut (if this is small, don't draw the vertical line)
%
\newlength{\lsc@cutvdiff}

%% used by the macro drawing coregions
%
\newlength{\lsc@crX}


% % helper macros: % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

%% define height and depth of instance head boxes
%
\newcommand{\lsc@instheadrule}%
  {\rule[\lsc@instheadruledepth]{0ex}{\lsc@instheadruleheight}}

%% draw the "kandis" for conditions -- used for single-instance conditions and
%  local invariants, not for conditions spanning multiple instance lines;
%  drawback: the angle of vertexes is kept constant, this causes the "kandis"
%  to grow wider with higher content
%
% \lsc@kandis[<psset-commands>]{<content>}
%
\newcommand{\lsc@kandis}[2][]{%
  \sbox{\lsc@kbox}{#2}%
  \settowidth{\lsc@kwidth}{\usebox{\lsc@kbox}}%
  \setlength{\lsc@kwidth}{.5\lsc@kwidth}%
% \addtolength{\lsc@kwidth}{\fboxsep}%
  \settoheight{\lsc@kheight}{\usebox{\lsc@kbox}}%
  \settodepth{\lsc@kdepth}{\usebox{\lsc@kbox}}%
  \addtolength{\lsc@kheight}{\lsc@kdepth}%
% \addtolength{\lsc@kheight}{\fboxsep}%
  \setlength{\lsc@kxwidth}{\lsc@kwidth}%
  \addtolength{\lsc@kxwidth}{\lsc@kheight}%
  \begin{pspicture}(-\lsc@kxwidth,\lsc@kheight)(\lsc@kxwidth,-\lsc@kheight)%
  \pspolygon[#1](-\lsc@kxwidth,0)%
                (-\lsc@kwidth,\lsc@kheight)%
                (\lsc@kwidth,\lsc@kheight)%
                (\lsc@kxwidth,0)%
                (\lsc@kwidth,-\lsc@kheight)%
                (-\lsc@kwidth,-\lsc@kheight)%
  \rput(0,0){\usebox{\lsc@kbox}}%
  \end{pspicture}%
}
%
\newcommand{\lsc@hotkandis}[1]{%
  \lsc@kandis[fillstyle=solid,linestyle=solid]{#1}}
%
\newcommand{\lsc@coldkandis}[1]{%
  \lsc@kandis[fillstyle=solid,linestyle=dashed]{#1}}

%% save coordinates of message sending and reception (values are accessed by
%  _name_ later)
%
%  The easy solution consisting of just placing nodes and later connecting
%  them by lines does not work since then label end up positioned upside-down
%  below arrows for those messages going from right to left.  Hence we need to
%  have both coordinates to draw the line the right way.
%
% \lsc@msg{a|i}{snd|rcv}{id}
%
\newcommand{\lsc@msg}[3]{%
  \expandafter\ifx\csname lsc@#1msg#3#2X\endcsname\relax%
    \expandafter\xdef\csname lsc@#1msg#3#2X\endcsname{\the\lsc@X}%
    \expandafter\xdef\csname lsc@#1msg#3#2Y\endcsname{\the\lsc@Y}%
  \else%
    \errmessage{LSC error: #3: message location already defined!}%
  \fi%
}
%
%  remove all helper definitions again to be able to detect errors with later
%  messages who use the same name
%
% \lsc@clearmsg{a|i}{id}
%
\newcommand{\lsc@clearmsg}[2]{%
  \global\expandafter\let\csname lsc@#1msg#2sndX\endcsname\relax%
  \global\expandafter\let\csname lsc@#1msg#2sndY\endcsname\relax%
  \global\expandafter\let\csname lsc@#1msg#2rcvX\endcsname\relax%
  \global\expandafter\let\csname lsc@#1msg#2rcvY\endcsname\relax%
}

%% draw a simultaneous-region "kuller" (circle) -- whether it goes to front or
%  back is determined by the hook that is defined to be this command
%
\newcommand{\lsc@simregionkuller}{%
  \rput(\lsc@X,\lsc@Y){%
    \pscircle*{\lsc@simregradius}}}

%% save coordinates of conditions spanning multiple instance lines; if first
%  called for a name, the coordinates of the leftmost end are stored, the
%  coordinates of the rightmost end are overwritten each time, leaving the
%  actual rightmost values in the end; the Y-coordinate is only stored on the
%  first call (values are accessed by _name_ later)
%
% \lsc@widecondloc{<id>}
%
\newcommand{\lsc@widecondloc}[1]{%
  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
    \expandafter\xdef\csname lsc@wc#1leftmostX\endcsname{\the\lsc@X}%
    \expandafter\xdef\csname lsc@wc#1Y\endcsname{\the\lsc@Y}%
  \fi%
  \expandafter\xdef\csname lsc@wc#1rightmostX\endcsname{\the\lsc@X}}%

%% write a white block as part of the background of a condition spanning
%  multiple instance lines; in other words, the background of these conditions
%  is not drawn at once but separately on each instance line
%
%  The trick for getting the outline right is to draw "puzzles": on the
%  leftmost instance, a
%       _______
%      /   |   \
%      \___|___/
%
%  piece is drawn and on all other instances a
%     _________
%     \    |   \
%     /____|___/
%
%  pieces.  This even gets wide conditions covering only a single instance
%  line right.
%
% \lsc@lscfirstblock
%
\newcommand{\lsc@firstblock}{%
  \pssetlength{\lsc@kxwidth}{0.5\lscLocationWidth}%
  \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
  \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
  \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
  \rput(\lsc@X,\lsc@Y){%
    \pspolygon*[linecolor=white]%
      (-\lsc@kxwidth,-0.5\lsc@kheight)%
      (-\lsc@kwidth,0)%
      (\lsc@kwidth,0)%
      (\lsc@kxwidth,-0.5\lsc@kheight)%
      (\lsc@kwidth,-\lsc@kheight)%
      (-\lsc@kwidth,-\lsc@kheight)}}%

% \lsc@lscotherblock
%
\newcommand{\lsc@otherblock}{%
  \pssetlength{\lsc@kxwidth}{0.5\lscLocationWidth}%
  \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
  \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
  \pssetlength{\lsc@kxxwidth}{\lsc@kxwidth}%
  \psaddtolength{\lsc@kxxwidth}{0.35\lscLocationHeight}%
  \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
  \rput(\lsc@X,\lsc@Y){%
    \pspolygon*[linecolor=white]%
      (-\lsc@kxwidth,-0.5\lsc@kheight)%
      (-\lsc@kxxwidth,0)%
      (\lsc@kwidth,0)%
      (\lsc@kxwidth,-0.5\lsc@kheight)%
      (\lsc@kwidth,-\lsc@kheight)%
      (-\lsc@kxxwidth,-\lsc@kheight)}}%

%% set cut colour and width of a named cut and draw a named cut -- explicitly
%  named cuts get names of the form 'lsc@cutnamed...Y', the unnamed cut has
%  names of the form 'lsc@cutinternalY' 
%
% \lsc@setCutColour{<id>}{<colourname>}
%
\newcommand{\lsc@setCutColour}[2]{%
  \expandafter\def\csname lsc@cut#1Colour\endcsname{#2}}

% \lsc@setCutWidth{<id>}{<length>}
%
\newcommand{\lsc@setCutWidth}[2]{%
  \expandafter\def\csname lsc@cut#1Width\endcsname{#2}}

% \lsc@setCutLinestyle{<id>}{<linestyle>}
%
\newcommand{\lsc@setCutLinestyle}[2]{%
  \expandafter\def\csname lsc@cut#1Linestyle\endcsname{#2}}

%% drawing a cut with name <id> comprises drawing a line in colour
%  \lsc@cut<id>Colour with width \lsc@cut<id>Width at the current Y location
%  over the full location width.   If we are _not_ on the first instance,
%  then firstly a line at the leftmost boundary of the current location is
%  drawn from \lsc@cut<id>Y, the vertical position of the last cut segment, to
%  the current Y location.
%
% \lsc@namedCut{<id>}
%
\newcommand{\lsc@namedCut}[1]{%
  %
  % if the linestyle is 'none', explicitly don't do anything -- otherwise the
  % 'c-c' line ends are drawn anyway...
  %
  \ifthenelse{\equal{\csname lsc@cut#1Linestyle\endcsname}{none}}{%
    \relax%
  }{{%
    \psset{linecolor=\csname lsc@cut#1Colour\endcsname,%
           linewidth=\csname lsc@cut#1Width\endcsname,%
           linestyle=\csname lsc@cut#1Linestyle\endcsname,%
           arrows=c-c}%
    %
    % if we are not on the first instance, consider to draw a vertical line
    %
    \ifthenelse{\equal{\lsc@firstinst}{\lsc@false}}{%
      %
      % it's not sufficient to check the last and the current Y position for
      % equality since minimal deviations have the effect that the vertical line
      % is drawn (and consequently creates the ugly artefact)
      %
      \ifthenelse{\lengthtest{\csname lsc@cut#1Y\endcsname > \lsc@Y}}{%
        \pssetlength{\lsc@cutvdiff}{\csname lsc@cut#1Y\endcsname}
        \addtolength{\lsc@cutvdiff}{-\lsc@Y}
      }{%
        \pssetlength{\lsc@cutvdiff}{\lsc@Y}
        \addtolength{\lsc@cutvdiff}{-\csname lsc@cut#1Y\endcsname}
      }%
       \ifthenelse{\lengthtest{\lsc@cutvdiff < \csname lsc@cut#1Width\endcsname}}{%
         % skip: don't draw vertical line when at (roughly) same height
       }{%
         \rput(-0.5\lscLocationWidth,0){%
           \psline(\lsc@X,\csname lsc@cut#1Y\endcsname)(\lsc@X,\lsc@Y)}%
       }%
    }{}%
    %
    % draw horizontal line
    %
    \rput(\lsc@X,\lsc@Y){%
      \psline(-0.5\lscLocationWidth,0)(0.5\lscLocationWidth,0)}%
    \expandafter\xdef\csname lsc@cut#1Y\endcsname{\the\lsc@Y}%
  }}%
}

%% helper macros for scheduling, drawing, and clearing hooks
%
\newcommand{\lsc@schedhook}[2]{%
  \global\expandafter\def\csname lsc@draw#1hook\endcsname{#2}%
}
%
\newcommand{\lsc@clearhook}[1]{%
  \global\expandafter\let\csname lsc@draw#1hook\endcsname\relax}%
%
\newcommand{\lsc@clearhooks}{%
 \lsc@clearhook{actcond}%
 \lsc@clearhook{atom}%
 \lsc@clearhook{bgblock}%
 \lsc@clearhook{bgsimreg}%
 \lsc@clearhook{fgblock}%
 \lsc@clearhook{fgsimreg}%
 \lsc@clearhook{timer}%
}
%
\newcommand{\lsc@flushhook}[1]{%
  \csname lsc@draw#1hook\endcsname%
  \lsc@clearhook{#1}%
}

%% do the things that have to be done before the instance line is drawn,
%  currently this comprises only the drawing of a multi-instance line
%  condition background if one is scheduled for drawing and a simregion
%  kuller.  Used by ordinary and environment instance lines.
%  ('Scheduling' is done by defining macros.)
%
\newcommand{\lsc@linePrelude}{%
  \lsc@flushhook{bgsimreg}%
  \lsc@flushhook{bgblock}}%

%% do the things that have to be done after the instance line is drawn,
%  currently drawing the following things given in order from back to front
%  (if scheduled):
%   - background of multi-instance line conditions
%   - condition or action (implies that there can be either a condition or an
%     action at a location)
%   - timer
%   - atom circle
%
%  Used by ordinary and environment instance lines.
%
\newcommand{\lsc@linePostlude}[1]{%
  \lsc@flushhook{fgblock}%
  \lsc@flushhook{actcond}%
  \lsc@flushhook{timer}%
  \lsc@flushhook{atom}%
  \lsc@flushhook{fgsimreg}%
  \global\advance\lsc@Y by-#1\lscLocationHeight}%

%% macros to draw instance lines, ordinary and environment
%
% \lsc@line{<timinginterval>}{solid|dashed}{<length>}
%
\newcommand{\lsc@line}[3]{%
  \lsc@linePrelude%
  \rput(\lsc@X,\lsc@Y){%
    %
    % use \pcline only if really needed -- it make small dvi files
    % significantly larger (adds about 0.5k per small LSC)
    %
    \psset{linestyle=#2}%
    \ifthenelse{\equal{#1}{}}{%
      \psline(0,-#3\lscLocationHeight)%
    }{%
      \pcline(0,0)(0,-#3\lscLocationHeight)%
      \lput[l]{0}{\ {#1}}%
    }%
  }
  \lsc@linePostlude{#3}%
}
%
% \lsc@envline{<timinginterval>}{solid|none}{<length>}
%
\newcommand{\lsc@envline}[3]{%
  \lsc@linePrelude%
  \rput(\lsc@X,\lsc@Y){%
    %
    % if there is a timing interval, position it to the right of the rightmost
    % edge of the box
    %
    \ifthenelse{\equal{#1}{}}{%
    }{%
      \rput(\lsc@envlinewidth,0){%
        \pcline[linestyle=none](0,0)(0,-#3\lscLocationHeight)}%
      \lput[l]{0}{\ {#1}}%
    }%
    %
    % the instance line itself as a criss-cross filled box 
    %
    \pspolygon[linestyle=none,fillstyle=hlines]%
      (-\lsc@envlinewidth,0)%
      (\lsc@envlinewidth,0)%
      (\lsc@envlinewidth,-#3\lscLocationHeight)%
      (-\lsc@envlinewidth,-#3\lscLocationHeight)%
    %
    % if it's hot, add a solid line over the middle of the box
    %
    \psline[linestyle=#2](0,-#3\lscLocationHeight)%
  }%
  \lsc@linePostlude{#3}%
}

%% see whether the labels for both ends of the create arrow have been defined
%  and if so draw the arrow.  Used by the lscCreate command and the
%  lsccreateinst instance line.
%
% \lsc@createarrow{<id>}
%
\newcommand{\lsc@createarrow}[1]{%
  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
    \relax%
  \else\expandafter\ifx\csname lsc@createdest#1\endcsname\relax%
    \relax%
  \else%
      \ncline{->}{\csname lsc@createsrc#1node\endcsname}{\csname lsc@createdest#1node\endcsname}%
      \global\expandafter\let\csname lsc@createsrc#1\endcsname\relax%
      \global\expandafter\let\csname lsc@createdest#1\endcsname\relax%
  \fi\fi%
}

%% the first two macros only draw the hourglass and hour-X of timer set/reset
%  and timeout, the third macro constructs a timer symbol with label and the
%  latter three macros are actually used by the exported macros. 
%
\newcommand{\lsc@hourglass}{%
  \pspolygon[fillstyle=solid]%
            (-\lsc@hgwidth,\lsc@hgheight)%
            (\lsc@hgwidth,\lsc@hgheight)%
            (-\lsc@hgwidth,-\lsc@hgheight)%
            (\lsc@hgwidth,-\lsc@hgheight)}%
%
\newcommand{\lsc@hourx}{%
  \psline(-\lsc@hgwidth,\lsc@hgheight)%
         (\lsc@hgwidth,-\lsc@hgheight)%
  \psline(-\lsc@hgwidth,-\lsc@hgheight)%
         (\lsc@hgwidth,\lsc@hgheight)}%
%
% \lsc@timer{<xposition>}{<arrows>}{<symbol>}{<text>}
%
% The label <text> is placed to the left of the symbol if <xposition> is
% negative and to the right otherwise.
%
% For <xposition>, currently only \lsc@hgoffset or -\lsc@hgoffset are used,
% for <arrows> only '-' or '<-' and for <symbol> \lsc@hourglass or \lsc@hourx.
%
\newcommand{\lsc@timer}[4]{%
  \rput(\lsc@X,\lsc@Y){%
    \rput(#1,0){%
      {#3}%
      \ifthenelse{\lengthtest{#1 < 0pt}}{%
        \rput[r](-1.5\lsc@hgwidth,0){{#4}}%
      }{%
        \rput[l](1.5\lsc@hgwidth,0){{#4}}%
      }}%
    \psline{#2}(0,0)(#1,0)}}%
%
\newcommand{\lsc@timerset}[3]{%
  \lsc@timer{#1}{-}{\lsc@hourglass}{{#2}({#3})}}
%
\newcommand{\lsc@timerreset}[2]{%
  \lsc@timer{#1}{-}{\lsc@hourx}{{#2}}}
%
\newcommand{\lsc@timeout}[2]{%
  \lsc@timer{#1}{<-}{\lsc@hourglass}{{#2}}}

%% draw hot and cold single-instance condition
%
\newcommand{\lsc@cond}[1]{%
  \rput[t](\lsc@X,\lsc@Y){#1}}
%
\newcommand{\lsc@hotcond}[1]{%
  \lsc@cond{\lsc@hotkandis{#1}}}%
%
\newcommand{\lsc@coldcond}[1]{%
  \lsc@cond{\lsc@coldkandis{#1}}}%

%% macros to draw the message arrow -- checks whether both ends are defined
%
%  \lsc@msgarrow{a|i}{<linestyle>}{<id>}{<label>}
%
% The arrow shape is controlled by \psset{} in wrapping macros.
%
\newcommand{\lsc@msgarrow}[4]{{%
  \expandafter\ifx\csname lsc@#1msg#3sndX\endcsname\relax%
    \errmessage{LSC error: #3: send location not defined?}%
  \else\expandafter\ifx\csname lsc@#1msg#3sndY\endcsname\relax%
    \errmessage{LSC error: #3: send location not defined?}%
  \else\expandafter\ifx\csname lsc@#1msg#3rcvX\endcsname\relax%
    \errmessage{LSC error: #3: receive location not defined?}%
  \else\expandafter\ifx\csname lsc@#1msg#3rcvY\endcsname\relax%
    \errmessage{LSC error: #3: receive location not defined?}%
  \else
    \psset{linestyle=#2}%
    \ifthenelse{\lengthtest{\csname lsc@#1msg#3sndX\endcsname < \csname lsc@#1msg#3rcvX\endcsname}}{%
      \pcline{->}%
        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
    }{%
    \ifthenelse{\lengthtest{\csname lsc@#1msg#3sndX\endcsname > \csname lsc@#1msg#3rcvX\endcsname}}{%
      \pcline{<-}%
        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
    }{%
      \pcbar[arm=0.5]{->}%
        (\csname lsc@#1msg#3sndX\endcsname,\csname lsc@#1msg#3sndY\endcsname)%
        (\csname lsc@#1msg#3rcvX\endcsname,\csname lsc@#1msg#3rcvY\endcsname)%
    }}%
    \aput[\lsc@labelsep]{:U}{#4}%
  \fi\fi\fi\fi%
}}
%
% \lsc@asynarrow{solid|dashed}{<id>}{<label>}
%
\newcommand{\lsc@asynarrow}[3]{{%
  \psset{arrowsize=2pt 3,arrowlength=3,arrowinset=0.80,linestyle=#1}%
  \lsc@msgarrow{a}{#1}{#2}{#3}}}
%
%  \lsc@hotasynarrow{<id>}{<label>}
%
\newcommand{\lsc@hotasynarrow}[2]{%
  \lsc@asynarrow{solid}{#1}{#2}}%
%
%  \lsc@coldasynarrow{<id>}{<label>}
%
\newcommand{\lsc@coldasynarrow}[2]{%
  \lsc@asynarrow{dashed}{#1}{#2}}%
%
\newcommand{\lsc@instarrow}[3]{{%
  \psset{arrowsize=2pt 3,arrowlength=2,arrowinset=0,linestyle=#1}%
  \lsc@msgarrow{i}{#1}{#2}{#3}}}
%
%  \lsc@hotinstarrow{<id>}{<label>}
%
\newcommand{\lsc@hotinstarrow}[2]{%
  \lsc@instarrow{solid}{#1}{#2}}%
%
%  \lsc@coldinstarrow{<id>}{<label>}
%
\newcommand{\lsc@coldinstarrow}[2]{%
  \lsc@instarrow{dashed}{#1}{#2}}%

%% macros to draw a local invariant
%
% \lsc@likuller{<yfactor>}{<ypos>}
%
% <yfactor> is '-0.5' for start and '0.5' for end kuller; this provides a
% small "inwards" offset to the kuller s.t. subsequent local invariants remain
% readable. <ypos> is the y-position.
% Filling of the kuller is controlled by \psset{} in calling wrapper macros.
%
\newcommand{\lsc@likuller}[2]{%
  \rput(\lsc@liX,#2){%
    \pscircle[fillstyle=solid](0,#1\lsc@dotradius){\lsc@dotradius}}%
}
%
% \lsc@incllikuller{<yfactor>}{<ypos>}
%
\newcommand{\lsc@incllikuller}[2]{{%
  \psset{fillcolor=black}%
  \lsc@likuller{#1}{#2}%
}}
%
% \lsc@excllikuller{<yfactor>}{<ypos>}
%
\newcommand{\lsc@excllikuller}[2]{{%
  \lsc@likuller{#1}{#2}%
}}
%
% \lsc@inclstartkuller{<id>}
%
\newcommand{\lsc@inclstartkuller}[1]{%
  \lsc@incllikuller{-0.5}{\csname lsc@li#1startY\endcsname}}%
%
% \lsc@exclstartkuller{<id>}
%
\newcommand{\lsc@exclstartkuller}[1]{%
  \lsc@excllikuller{-0.5}{\csname lsc@li#1startY\endcsname}}%
%
% \lsc@inclendkuller{<id>}
%
\newcommand{\lsc@inclendkuller}[1]{%
  \lsc@incllikuller{0.5}{\csname lsc@li#1endY\endcsname}}%
%
% \lsc@exclendkuller{<id>}
%
\newcommand{\lsc@exclendkuller}[1]{%
  \lsc@excllikuller{0.5}{\csname lsc@li#1endY\endcsname}}%
%
% \lsc@locinv{r|l}{<id>}{incl|excl}{incl|excl}{<kandis>}%
%
% Assumes that the first parameter is 'r' or 'l' (should've been checked
% before) but checks itself for 'incl' and 'excl'.  <kandis> should be the
% stuff to be put next to the vertical line, it is typically a hot or cold
% \lsc@kandis, i.e. temperature has to be handled in the calling macro.
%
\newcommand{\lsc@locinv}[5]{%
  \expandafter\ifx\csname lsc@li#2startX\endcsname\relax%
    \errmessage{LSC error: #2: local invariant begin not defined?}%
  \else\expandafter\ifx\csname lsc@li#2startY\endcsname\relax%
    \errmessage{LSC error: #2: local invariant begin not defined?}%
  \else\expandafter\ifx\csname lsc@li#2endX\endcsname\relax%
    \errmessage{LSC error: #2: local invariant end not defined?}%
  \else\expandafter\ifx\csname lsc@li#2endY\endcsname\relax%
    \errmessage{LSC error: #2: local invariant end not defined?}%
  \else
    %
    % draw the connections to the locations on the instance lines
    %
    \psline[linestyle=dotted,dotsep=1pt]%
      (\csname lsc@li#2startX\endcsname,\csname lsc@li#2startY\endcsname)%
      (\lsc@liX,\csname lsc@li#2startY\endcsname)%
    \psline%
      (\lsc@liX,\csname lsc@li#2startY\endcsname)%
      (\lsc@liX,\csname lsc@li#2endY\endcsname)%
    \psline[linestyle=dotted,dotsep=1pt]%
      (\lsc@liX,\csname lsc@li#2endY\endcsname)%
      (\csname lsc@li#2endX\endcsname,\csname lsc@li#2endY\endcsname)%
    %
    % draw the "kandis"
    %
    \pssetlength{\lsc@licondY}{\csname lsc@li#2endY\endcsname}%
    \psaddtolength{\lsc@licondY}{\csname lsc@li#2startY\endcsname}%
    \pssetlength{\lsc@licondY}{0.5\lsc@licondY}%
    \rput[#1](\lsc@liX,\lsc@licondY){#5}%
    %
    % put the inclusive/exclusive markers
    %
    \def\lsc@arg{#3}%
    \ifx\lsc@arg\lsc@incl%
      \lsc@inclstartkuller{#2}%
    \else\ifx\lsc@arg\lsc@excl%
      \lsc@exclstartkuller{#2}%
    \else%
      \errmessage{LSC error: \lsc@arg: Local invariant start must be "incl" or "excl"!}%
    \fi\fi%
    %
    \def\lsc@arg{#4}%
    \ifx\lsc@arg\lsc@incl%
      \lsc@inclendkuller{#2}%
    \else\ifx\lsc@arg\lsc@excl%
      \lsc@exclendkuller{#2}%
    \else%
      \errmessage{LSC error: \lsc@arg: Local invariant end must be "incl" or "excl"!}%
    \fi\fi%
  \fi\fi\fi\fi%
}

%% macros to position the instance lines end of creation arrows
%
% \lsc@createdest{<id>}
%
% Puts the pnode for the creation arrow.  Communicates with calling macros by
% the shared lengths \lsc@createinstX, \lsc@createinstY and the X-offset
% \lsc@createinstW.
%
\newcommand{\lsc@setcreatedest}[1]{%
  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
    %
    % if the src of the creation arrow doesn't exist already, then it will end
    % up to the right of us thus place the node to the right of the box (!)...
    %
    \addtolength{\lsc@createinstX}{\lsc@createinstW}%
  \else%
    %
    % ...otherwise put it to the left
    %
    \addtolength{\lsc@createinstX}{-\lsc@createinstW}%
  \fi%
  %
  \pnode(\lsc@createinstX,\lsc@createinstY){\csname lsc@createdest#1node\endcsname}%
  %
  \expandafter\xdef\csname lsc@createdest#1\endcsname{\lsc@true}%
  %
  \lsc@createarrow{#1}%
}
%
% \lsc@createboxdest{<id>}
%
\newcommand{\lsc@setcreateboxdest}[1]{%
  %
  % for boxed create instance heads, the arrow should end on the line of the
  % box
  %
  \setlength{\lsc@createinstW}{0.4\lscLocationWidth}%
  \addtolength{\lsc@createinstW}{\lsc@instheadframesep}%
  %
  \lsc@setcreatedest{#1}%
}
%
% \lsc@createnoboxdest{<id>}{<label>}
%
\newcommand{\lsc@setcreatenoboxdest}[2]{%
  %
  % for non-boxed create instance heads, the arrow should end a little bit to
  % the left or right of the label (!)
  %
  \settowidth{\lsc@createinstW}{#2}%
  \setlength{\lsc@createinstW}{0.5\lsc@createinstW}%
  \psaddtolength{\lsc@createinstW}{0.1em}%
  \psaddtolength{\lsc@createinstW}{\lsc@instheadframesep}%
  %
  \lsc@setcreatedest{#1}%
}

%% macros to draw an instance head
%
% \lsc@insthead[<Y>]{solid|dashed|none}{true|false}{<label>}
%
% The boolean 'lsc@MSC', which indicates whether we are in an MSC instance
% line or not, i.e. whether a footer has to be drawn or not, is set to the
% second parameter.
%
\newcommand{\lsc@insthead}[4][0]{%
   \rput[b](\lsc@X,#1){\psframebox[fillstyle=solid,framesep=\lsc@instheadframesep,linestyle=#2]{%
     \makebox[0.80\lscLocationWidth]{#4\lsc@instheadrule}}}%
   \setboolean{lsc@MSC}{#3}}%
%
% \lsc@instheadbox[<Y>]{solid|dashed}{true|false}{<label>}
%
\newcommand{\lsc@instheadbox}[4][0]{%
  \lsc@insthead[#1]{#2}{#3}{#4}}
%
% \lsc@instheadnobox[<Y>]{true|false}{<label>}
%
\newcommand{\lsc@instheadnobox}[3][0]{%
  \lsc@insthead[#1]{none}{#2}{#3}}
%
% \lsc@instheadnoboxSD[<Y>]{<label>}
%
\newcommand{\lsc@instheadnoboxSD}[2][0]{%
  \lsc@instheadnobox[#1]{false}{#2}}
%
% \lsc@instheadSD[<Y>]{<label>}
%
\newcommand{\lsc@instheadSD}[3][0]{%
  \lsc@instheadbox[#1]{#2}{false}{#3}}
%
% \lsc@instheadMSC[<Y>]{<label>}
%
\newcommand{\lsc@instheadMSC}[3][0]{%
  \lsc@instheadbox[#1]{#2}{true}{#3}}

%% macros to draw an instance foot
%
% \lsc@instend
%
% If drawn, the instance end (footer) goes to the current location, not the
% bottom of the LSC picture environment.
%
\newcommand{\lsc@instend}{%
  % put the end if in MSC mode
  %
  \ifthenelse{\boolean{lsc@MSC}}{%
     \rput[b](\lsc@X,\lsc@Y){%
       \psframebox[fillstyle=solid,fillcolor=black]{%
         \makebox[0.80\lscLocationWidth]{%
           \rule{0mm}{\lscFooterHeightFactor\lscLocationHeight}}}}%
  }{%
  }%
  %
  % if we are at the end of an instance line, then the next one is not a
  % first instance line -- unless the next one occurs in a new 'Lsc'
  % environment
  %
  \xdef\lsc@firstinst{\lsc@false}%
  %
  % advance X position for the next instance line
  %
  \global\advance\lsc@X by\lscLocationWidth%
}

%% helper macros for symbolic instance balloons
%
% \lsc@balloon{solid|dashed}{<stuff>}
%
\newcommand{\lsc@balloon}[2]{%
  \pscircle(0.1,0){0.09}%
  \pscircle(0.3,0.2){0.13}%
  \rput[b](0.5,0.4){%
    \psovalbox[fillstyle=solid,linestyle=#1]{#2}}}%

%% draw multi-instance line condition
%
% \lsc@widecond{<id>}{solid|dashed}{<label>}
%
\newcommand{\lsc@widecond}[3]{%
  \expandafter\ifx\csname lsc@wc#1rightmostX\endcsname\relax%
    \errmessage{LSC error: #1: no locations wide condition defined?}%
  \else\expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
    \errmessage{LSC error: #1: no locations wide condition defined?}%
  \else\expandafter\ifx\csname lsc@wc#1Y\endcsname\relax%
    \errmessage{LSC error: #1: no locations wide condition defined?}%
  \else%
    %
    % compute the extension of the whole kandis from the saved information --
    % forgot what the exact strategy was, the plan is to place the outline
    % correctly of course...  
    %
    \pssetlength{\lsc@kxwidth}{\csname lsc@wc#1rightmostX\endcsname}%
    \psaddtolength{\lsc@kxwidth}{-\csname lsc@wc#1leftmostX\endcsname}%
    \psaddtolength{\lsc@kxwidth}{\lscLocationWidth}%
    \pssetlength{\lsc@kxwidth}{0.5\lsc@kxwidth}%
    \pssetlength{\lsc@kwidth}{\lsc@kxwidth}%
    \psaddtolength{\lsc@kwidth}{-0.35\lscLocationHeight}%
    \pssetlength{\lsc@kheight}{0.7\lscLocationHeight}%
    %
    % draw the outline of the kandis, the background has been drawn by the 
    % \lscWidecondOn/Off commands
    %
    \rput(\csname lsc@wc#1leftmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
      \rput(\lsc@kxwidth,0){%
        \rput(-0.5\lscLocationWidth,0){%
          \pspolygon[linestyle=#2](-\lsc@kxwidth,-0.5\lsc@kheight)%
                                     (-\lsc@kwidth,0)%
                                     (\lsc@kwidth,0)%
                                     (\lsc@kxwidth,-0.5\lsc@kheight)%
                                     (\lsc@kwidth,-\lsc@kheight)%
                                     (-\lsc@kwidth,-\lsc@kheight)}}}%
    %
    % position the label in the middle of the kandis using an \ncline between
    % two helper named nodes and pstricks' labelling functions
    %
    \rput(\csname lsc@wc#1leftmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
      \rput(0,-0.35\lscLocationHeight){%
        \pnode{lscATwcL}}}%
    \rput(\csname lsc@wc#1rightmostX\endcsname,\csname lsc@wc#1Y\endcsname){%
      \rput(0,-0.35\lscLocationHeight){%
        \pnode{lscATwcR}}}%
    \ncline[linestyle=none]{lscATwcL}{lscATwcR}%
    \lput{0}{#3}%
  \fi\fi\fi%
  %
  % clear definitions
  %
  \global\expandafter\let\csname lsc@wc#1rightmostX\endcsname\relax%
  \global\expandafter\let\csname lsc@wc#1leftmostX\endcsname\relax%
  \global\expandafter\let\csname lsc@wc#1Y\endcsname\relax}

%% helper macros for the Lsc/FullLsc environment
%
% \lsc@init{<nrinsts>}{<nrlocs>}
%
\newcommand{\lsc@init}[2]{%
  %
  % reset X position (Y is reset in 'lscinst')
  %
  \pssetlength{\lsc@X}{0.5\lscLocationWidth}%
  %
  % compute horizontal position of right-bound local invariants (depends on
  % width of current LSC of course)
  %
  \pssetlength{\lsc@liR}{#1\lscLocationWidth}%
  \psaddtolength{\lsc@liR}{-0.2\lscLocationWidth}%
  %
  % the next 'lscinst' will be the first (-> \lscCut)
  %
  \def\lsc@firstinst{\lsc@true}%
  %
  % undefine all schedulings (-> \lscLine)
  %
  \lsc@clearhooks%
  %
  % compute extent of the image; considering pre-chart, universal/existential
  % frame, and the name-ac-am box
  %
  \pssetlength{\lsc@width}{#1\lscLocationWidth}%
  \pssetlength{\lsc@ulX}{0}%
  \pssetlength{\lsc@ulY}{0}%
  \pssetlength{\lsc@lrX}{\lsc@width}%
  \pssetlength{\lsc@lrY}{-#2\lscLocationHeight}%
}
%
% \lsc@addpcwidthcorrection
%
\newcommand{\lsc@addpcwidthcorrection}{%
  \psaddtolength{\lsc@ulX}{-0.25\lscLocationWidth}%
  \psaddtolength{\lsc@lrX}{0.25\lscLocationWidth}%
}
%
% \lsc@addpccorrection
%
\newcommand{\lsc@addpccorrection}{%
  \psaddtolength{\lsc@ulY}{\lsc@pccorrection}%
}
%
% \lsc@addframecorrection
%
\newcommand{\lsc@addframecorrection}{%
  \psaddtolength{\lsc@lrY}{-0.1\lscLocationHeight}%
}
%
% \lsc@mkacambox{<name>}{<ac>}{invariant|initial|iterative}{strict|weak|}
%
\newcommand{\lsc@mkacambox}[4]{%
  \def\lsc@arg{#4}%
  \ifx\lsc@arg\lsc@empty%
    \def\lsc@i{}%
  \else\ifx\lsc@arg\lsc@weak%
    \def\lsc@i{\lsc@permissive}%
  \else\ifx\lsc@arg\lsc@permissive%
    \def\lsc@i{\lsc@permissive}%
  \else\ifx\lsc@arg\lsc@strict%
    \def\lsc@i{\lsc@strict}%
  \else%
    \errmessage{LSC error: \lsc@arg: FullLSC interpretation must be "", "permissive", "weak", or "strict"!}%
    \def\lsc@i{???}%
  \fi\fi\fi\fi%
  %
  \def\lsc@arg{#3}%
  \ifx\lsc@arg\lsc@invariant%
    \def\lsc@am{\lsc@invariant}%
  \else\ifx\lsc@arg\lsc@initial%
    \def\lsc@am{\lsc@initial}%
  \else\ifx\lsc@arg\lsc@iterative%
    \def\lsc@am{\lsc@iterative}%
  \else%
    \errmessage{LSC error: \lsc@arg: FullLSC interpretation must be "invariant", "initial", or "iterative"!}%
    \def\lsc@am{???}%
  \fi\fi\fi%
  %
  \sbox{\lsc@acambox}{%
    \psframebox[fillstyle=solid,framesep=0]{%
      \small%
      \begin{tabular}{ll}%
        LSC:&{#1}\\[\lsc@acamboxblskipcorrection]%
        AC:&{#2}\\[\lsc@acamboxblskipcorrection]%
        AM:&{\lsc@am}{\ \hfill}%
        \ifthenelse{\equal{\lsc@i}{}}{%
        }{\begin{tabular}{ll}%
           I:&{\lsc@i}%
          \end{tabular}}%
      \end{tabular}\hspace{.5em}}}%
  %
  \settoheight{\lsc@acamheight}{\usebox{\lsc@acambox}}%
  \psaddtolength{\lsc@ulY}{\lsc@acamheight}%
  \settodepth{\lsc@acamheight}{\usebox{\lsc@acambox}}%
  \psaddtolength{\lsc@ulY}{\lsc@acamheight}%
}
%
% \lsc@prechart{<prechartloc>}
%
\newcommand{\lsc@prechart}[1]{%
  \pssetlength{\lsc@kwidth}{\lsc@width}%
  \pssetlength{\lsc@kwidth}{.5\lsc@kwidth}%
  \pssetlength{\lsc@kxwidth}{\lsc@kwidth}%
  %
  \pssetlength{\lsc@frametop}{\lsc@pccorrection}%
  %
  \ifthenelse{\equal{#1}{}}{%
    %
    % no pre-chart: just adjust length
    %
    \pssetlength{\lsc@kheight}{0}%
  }{%
    \psaddtolength{\lsc@kxwidth}{0.25\lscLocationWidth}%
    %
    % draw the pre-chart
    %
    \pssetlength{\lsc@kheight}{#1\lscLocationHeight}%
    \psaddtolength{\lsc@kheight}{\lsc@pccorrection}%
    %
    \rput(0.5\lsc@width,\lsc@pccorrection){%
      \pspolygon[linestyle=dashed](-\lsc@kxwidth,-0.5\lsc@kheight)%
                                  (-\lsc@kwidth,0)%
                                  (\lsc@kwidth,0)%
                                  (\lsc@kxwidth,-0.5\lsc@kheight)%
                                  (\lsc@kwidth,-\lsc@kheight)%
                                  (-\lsc@kwidth,-\lsc@kheight)}%
    %
    \psaddtolength{\lsc@frametop}{-\lsc@kheight}%
  }%
}
%
% \lsc@frame{solid|dashed}
%
\newcommand{\lsc@frame}[1]{%
   %
   % draw the universal/existential box
   %
   \pssetlength{\lsc@frameheight}{\lsc@lrY}%
   \psaddtolength{\lsc@frameheight}{\lsc@kheight}%
   \psaddtolength{\lsc@frameheight}{-\lsc@pccorrection}%
   %
   \rput(0.5\lsc@width,\lsc@frametop){%
     \psframe[linestyle=#1]%
       (-\lsc@kxwidth,0)(\lsc@kxwidth,\lsc@frameheight)}%
}


% % exported interface:  % % % % % % % % % % % % % % % % % % % % % % % % % % %

%% additional space between the instance line and the local invariant
%  condition (in addition to the default space)
%
%      |....................................
%      |                                   O ______
%      |                                   |<_cond_>
%      |...................................O
%      |
%
%      |< basic offset >|< lscLocInvOffset >
%
\newlength{\lscLocinvOffset}
\pssetlength{\lscLocinvOffset}{0}

% \lscAsynSnd{<id>}
%
\newcommand{\lscAsynSnd}[1]{%
  \lsc@msg{a}{snd}{#1}}

% \lscAsynRcv{<id>}
%
\newcommand{\lscAsynRcv}[1]{%
  \lsc@msg{a}{rcv}{#1}}

% \lscInstSnd{<id>}
%
\newcommand{\lscInstSnd}[1]{%
  \lsc@msg{i}{snd}{#1}}

% \lscInstRcv{<id>}
%
\newcommand{\lscInstRcv}[1]{%
  \lsc@msg{i}{rcv}{#1}}

% \lscTimerSet[r|l]{<timername>}{<timerduration>}
%
\newcommand{\lscTimerSet}[3][r]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@r%
    \lsc@schedhook{timer}{\lsc@timerset{\lsc@hgoffset}{#2}{#3}}%
  \else\ifx\lsc@arg\lsc@l%
    \lsc@schedhook{timer}{\lsc@timerset{-\lsc@hgoffset}{#2}{#3}}%
  \else%
    \errmessage{LSC error: \lsc@arg: TimerSet position must be "l" (left) or "r" (right)!}%
  \fi\fi%
}

% \lscTimerReset[r|l]{<timername>}
%
\newcommand{\lscTimerReset}[2][r]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@r%
    \lsc@schedhook{timer}{\lsc@timerreset{\lsc@hgoffset}{#2}}%
  \else\ifx\lsc@arg\lsc@l%
    \lsc@schedhook{timer}{\lsc@timerreset{-\lsc@hgoffset}{#2}}%
  \else%
    \errmessage{LSC error: \lsc@arg: TimerReset position must be "l" (left) or "r" (right)!}%
  \fi\fi%
}

% \lscTimeout[r|l]{<timername>}
%
\newcommand{\lscTimeout}[2][r]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@r%
    \lsc@schedhook{timer}{\lsc@timeout{\lsc@hgoffset}{#2}}%
  \else\ifx\lsc@arg\lsc@l%
    \lsc@schedhook{timer}{\lsc@timeout{-\lsc@hgoffset}{#2}}%
  \else%
    \errmessage{LSC error: \lsc@arg: Timeout position must be "l" (left) or "r" (right)!}%
  \fi\fi%
}


% \lscAct{<content>}
%
\newcommand{\lscAct}[1]{%
  \lsc@schedhook{actcond}{%
    \rput[t](\lsc@X,\lsc@Y){%
      \psframebox[fillstyle=solid]{#1}}}}

% schedule a single instance line condition for drawing
%
% \lscCond{hot|cold}{<content>}
%
\newcommand{\lscCond}[2]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@schedhook{actcond}{\lsc@hotcond{#2}}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@schedhook{actcond}{\lsc@coldcond{#2}}%
  \else%
    \errmessage{LSC error: \lsc@arg: Condition temperature must be "hot" or "cold"!}%
  \fi\fi%
}

% \lscKill
%
\newcommand{\lscKill}{%
  \rput(\lsc@X,\lsc@Y){%
    \psline(-\lscKillLength,\lscKillLength)(\lscKillLength,-\lscKillLength)%
    \psline(-\lscKillLength,-\lscKillLength)(\lscKillLength,\lscKillLength)}}

% \lscCreate{<id>}
%
\newcommand{\lscCreate}[1]{%
  \expandafter\ifx\csname lsc@createsrc#1\endcsname\relax%
    \rput[b](\lsc@X,\lsc@Y){%
      \pnode{\csname lsc@createsrc#1node\endcsname}}%
    %
    \expandafter\xdef\csname lsc@createsrc#1\endcsname{\lsc@true}%
    %
    \lsc@createarrow{#1}%
  \else%
    \errmessage{LSC error: #1: Creation arrow source already defined!}%
  \fi%
}

% draw the background of a multi-instance line condition for the current
% instance; 'Off' means, the condition lies behind the current instance line,
% i.e. the condition does not synchronise it
%
% \lscWidecondOff{<id>}
%
\newcommand{\lscWidecondOff}[1]{%
  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
    \lsc@schedhook{bgblock}{\lsc@firstblock}%
  \else%
    \lsc@schedhook{bgblock}{\lsc@otherblock}%
  \fi%
  \lsc@widecondloc{#1}}%

% (see above) 'On' means, the condition lies before the current instance line,
% i.e. the condition synchronises on it
%
% \lscWidecondOn{<id>}
%
\newcommand{\lscWidecondOn}[1]{%
  \expandafter\ifx\csname lsc@wc#1leftmostX\endcsname\relax%
    \lsc@schedhook{fgblock}{\lsc@firstblock}%
  \else%
    \lsc@schedhook{fgblock}{\lsc@otherblock}%
  \fi%
  \lsc@widecondloc{#1}}%

% mark the beginning/end of local invariant <id>.  It is actually drawn later,
% using \lscLocinv after beginning and end have been marked, by convention
% after all 'lscinst' environments.
%
% \lscLocinvStart{<id>}
% \lscLocinvBegin{<id>}
%
\newcommand{\lscLocinvStart}[1]{%
  \expandafter\ifx\csname lsc@li#1startX\endcsname\relax%
    \expandafter\xdef\csname lsc@li#1startX\endcsname{\the\lsc@X}%
    \expandafter\xdef\csname lsc@li#1startY\endcsname{\the\lsc@Y}%
  \else%
    \errmessage{LSC error: #1: local invariant begin already defined!}%
  \fi%
}
\let\lscLocinvBegin\lscLocinvStart%

% \lscLocinvEnd{<id>}
%
\newcommand{\lscLocinvEnd}[1]{%
  \expandafter\ifx\csname lsc@li#1endX\endcsname\relax%
    \expandafter\xdef\csname lsc@li#1endX\endcsname{\the\lsc@X}%
    \expandafter\xdef\csname lsc@li#1endY\endcsname{\the\lsc@Y}%
  \else%
    \errmessage{LSC error: #1: local invariant end already defined!}%
  \fi%
}

% draw an atom circle at the current location and label it with <id>.  Using
% this ID, it can be labelled later. 
%
% \lscAtom{<id>}
%
\newcommand{\lscAtom}[1]{%
  \lsc@schedhook{atom}{%
    \rput(\lsc@X,\lsc@Y){%
      \cnode[linestyle=dashed,dash=2pt 2pt]{\lsc@atomradius}{#1}}}}

% label the atom <id> with <content>, positioning the label explicitly by
% giving the angle.
%
% \lscLabelAtomAt{<angle}{<id>}{<content>}
%
\newcommand{\lscLabelAtomAt}[3]{%
  \nccircle[linestyle=none,angleA=#1]{-}{#2}{0.175}%
  \Bput{#3}}

% a shortcut for the (anticipated) four most common angles to put an atom
% label.
%
% \lscLabelAtom[ra|rb|la|lb]{<id>}{<content>}
%
\newcommand{\lscLabelAtom}[3][ra]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@ra%
    \lscLabelAtomAt{-45}{#2}{#3}%
  \else\ifx\lsc@arg\lsc@rb%
    \lscLabelAtomAt{-135}{#2}{#3}%
  \else\ifx\lsc@arg\lsc@la%
    \lscLabelAtomAt{45}{#2}{#3}%
  \else\ifx\lsc@arg\lsc@lb%
    \lscLabelAtomAt{135}{#2}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Atom label position must be "ra", "rb", "la", or "lb"!}%
  \fi\fi\fi\fi%
}

%% draw an instance line at the current location with all scheduled
%  conditions, timers, simregion kullers, etc.
%
% \lscLine[<timinginterval>]{hot|cold|none}{<length>}
%
% 'none' is not a semantical concept of LSCs but may be used to draw
% "pathological" or schematic LSCs needing vertical space
%
\newcommand{\lscLine}[3][]{%
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@line{#1}{solid}{#3}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@line{#1}{dashed}{#3}%
  \else\ifx\lsc@arg\lsc@none%
    \lsc@line{#1}{none}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Instance line temperature must be "hot", "cold", or none!}%
  \fi\fi\fi%
}

%% draw an environment instance line in the Sequence Diagram style
%  (cf. \lscLine)
%
% \lscEnvLine[<timinginterval>]{hot|cold}{<length>}
%
\newcommand{\lscEnvLine}[3][]{%
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@envline{#1}{solid}{#3}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@envline{#1}{none}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Environment instance line temperature must be "hot" or "cold"!}%
  \fi\fi%
}

%% set the name/line width for the cut with ID <id>.
%
% \lscSetNamedCutColour{<id>}{<colourname>}
%
\newcommand{\lscSetNamedCutColour}[2]{%
  \lsc@setCutColour{named#1}{#2}}

% \lscSetNamedCutWidth{<id>}{<length>}
%
\newcommand{\lscSetNamedCutWidth}[2]{%
  \lsc@setCutWidth{named#1}{#2}}

% \lscSetNamedCutWidth{<id>}{<linestyle>}
%
\newcommand{\lscSetNamedCutLinestyle}[2]{%
  \lsc@setCutLinestyle{named#1}{#2}}

% \lscSetCutColour{<colourname>}
%
\newcommand{\lscSetCutColour}[1]{%
  \def\lscCutColour{#1}}

% \lscSetCutWidth{<length>}
%
\newcommand{\lscSetCutWidth}[1]{%
  \setlength{\lscCutWidth}{#1}}

% \lscSetCutLinestyle{<linestyle>}
%
\newcommand{\lscSetCutLinestyle}[1]{%
  \def\lscCutLinestyle{#1}}

%% draw a named cut.  Using different IDs one may draw multiple cuts into a
%  single LSC -- whatever this might be good for one time.
%
% \lscNamedCut{<id>}
%
\newcommand{\lscNamedCut}[1]{%
  \expandafter\ifx\csname lsc@cutnamed#1Colour\endcsname\relax%
    \lscSetNamedCutColour{#1}{\lscCutColour}%
  \fi%
  \expandafter\ifx\csname lsc@cutnamed#1Width\endcsname\relax%
    \lscSetNamedCutWidth{#1}{\lscCutWidth}%
  \fi%
  \expandafter\ifx\csname lsc@cutnamed#1Linestyle\endcsname\relax%
    \lscSetNamedCutLinestyle{#1}{\lscCutLinestyle}%
  \fi%
  \lsc@namedCut{named#1}}

%% draw the default cut through the current location.  The cut might come out
%  corrupted if not all instance environments of the current Lsc comprise
%  exactly one \lscCut.
%
% \lscCut
%
\newcommand{\lscCut}{%
  \lsc@setCutColour{iNtErN@l}{\lscCutColour}%
  \lsc@setCutWidth{iNtErN@l}{\lscCutWidth}%
  \lsc@setCutLinestyle{iNtErN@l}{\lscCutLinestyle}%
  \lsc@namedCut{iNtErN@l}}

%% \rput <content> to the current drawing X/Y position in the LSC; a nested
%  \rput places stuff relative to the current drawing position
%
% \lscPut{<content>}
%
\newcommand{\lscPut}[1]{%
  \rput(\lsc@X,\lsc@Y){#1}}

%% actually draw an asynchronous communication whose beginning and end have
%  been set.
%
% \lscAsyn{<id>}{hot|cold}{<label>}
%
\newcommand{\lscAsyn}[3]{%
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@hotasynarrow{#1}{#3}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@coldasynarrow{#1}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Message temperature must be "hot" or "cold"!}%
  \fi\fi%
  \lsc@clearmsg{a}{#1}}

%% actually draw an instantaneous communication whose beginning and end have
%  been set.
%
% \lscInst{<id>}{hot|cold}{<label>}
%
\newcommand{\lscInst}[3]{%
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@hotinstarrow{#1}{#3}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@coldinstarrow{#1}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Message temperature must be "hot" or "cold"!}%
  \fi\fi%
  \lsc@clearmsg{i}{#1}}

%% actually draw a multi-instance line condition whose locations have been
%  set (consecutively).
%
% \lscWidecond{<id>}{hot|cold}{<label>}
%
\newcommand{\lscWidecond}[3]{%
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@hot%
    \lsc@widecond{#1}{solid}{#3}%
  \else\ifx\lsc@arg\lsc@cold%
    \lsc@widecond{#1}{dashed}{#3}%
  \else%
    \errmessage{LSC error: \lsc@arg: Wide condition temperature must be "hot" or "cold"!}%
  \fi\fi%
}

%% actually draw a local invariant whose beginning and end have been set.
%  Local invariants always appear to the left or to the right of the _whole_
%  LSC not somewhere in the middle (controlled by the optional parameter with
%  legal values 'r' (default) or 'l').  Layouting has been considered to
%  become too complicated otherwise.
%
% \lscLocinv[r|l]{<id>}{incl|excl}{incl|excl}{hot|cold}{<content>}
%
\newcommand{\lscLocinv}[6][r]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@r%
    \pssetlength{\lsc@liX}{\lsc@liR}%
    \psaddtolength{\lsc@liX}{\lscLocinvOffset}%
    \def\lsc@lilr{l}%
  \else\ifx\lsc@arg\lsc@l%
    \pssetlength{\lsc@liX}{\lsc@liL}%
    \psaddtolength{\lsc@liX}{-\lscLocinvOffset}%
    \def\lsc@lilr{r}%
  \else%
    \errmessage{LSC error: \lsc@arg: Local invariant position must be "l" (left) or "r" (right)!}%
    \def\lsc@lilr{x}%
  \fi\fi%
  %
  \ifx\lsc@lilr{x}%
    \relax% get here only if #1 was illegal by def. of \lsc@lilr
  \else%
    \def\lsc@arg{#5}%
    \ifx\lsc@arg\lsc@hot%
      \lsc@locinv{\lsc@lilr}{#2}{#3}{#4}{\lsc@hotkandis{#6}}%
    \else\ifx\lsc@arg\lsc@cold%
      \lsc@locinv{\lsc@lilr}{#2}{#3}{#4}{\lsc@coldkandis{#6}}%
    \else%
      \errmessage{LSC error: \lsc@arg: Local invariant temperature must be "hot" or "cold"!}%
    \fi\fi%
  \fi%
  %
  % undefine begin and end
  %
  \global\expandafter\let\csname lsc@li#2startX\endcsname\relax%
  \global\expandafter\let\csname lsc@li#2startY\endcsname\relax%
  \global\expandafter\let\csname lsc@li#2endX\endcsname\relax%
  \global\expandafter\let\csname lsc@li#2endY\endcsname\relax}

%% mark the locations within the 'coregion' environment as a coregion
%
% \begin{coregion}[r|l]
% \end{coregion}
%
\newenvironment{coregion}[1][l]{%
  % compute the X position of the line parallel to the instance line
  %
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@l%
    \pssetlength{\lsc@crX}{-\lsc@coregoffset}%
  \else\ifx\lsc@arg\lsc@r%
    \pssetlength{\lsc@crX}{\lsc@coregoffset}%
  \else%
    \errmessage{LSC error: \lsc@arg: Coregion position must be "l" (left) or "r" (right)!  Continuing as if "l" was given.}%
    \pssetlength{\lsc@crX}{-\lsc@coregoffset}% use the default
  \fi\fi%
  %
  \rput(\lsc@X,\lsc@Y){%
    \rput(\lsc@crX,\lsc@coregoffset){%
      \pnode{lsccoregbegin}}}%
}{%
  \rput(\lsc@X,\lsc@Y){%
    \rput(\lsc@crX,-\lsc@coregoffset){%
      \pnode{lsccoregend}}}%
  \ncline[linestyle=dotted,dotsep=2pt,linewidth=\lsc@coregwidth]{lsccoregbegin}{lsccoregend}%
}

%% mark the elements within the 'simregion' environment by a dot
%
% \begin{simregion}[b|f]
% \end{simregion}
%
\newenvironment{simregion}[1][b]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@b%
    \lsc@schedhook{bgsimreg}{\lsc@simregionkuller}%
  \else\ifx\lsc@arg\lsc@f%
    \lsc@schedhook{fgsimreg}{\lsc@simregionkuller}%
  \else%
    \errmessage{LSC error: \lsc@arg: Simregion position must be "b" (background) or "f" (foreground)!}%
  \fi\fi%
}{%
}

%% a regular instance line
%
% \begin{lscinst}[MSC|SD|noboxSD|esymMSC|esymSD]{<instancename>}
% \end{lscinst}
%
\newenvironment{lscinst}[2][MSC]{%
  % reset current Y position
  %
  \pssetlength{\lsc@Y}{0}%
  %
  % draw the head
  %
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@noboxSD%
    \lsc@instheadnoboxSD{#2}%
  \else\ifx\lsc@arg\lsc@SD%
    \lsc@instheadSD{solid}{#2}%
  \else\ifx\lsc@arg\lsc@MSC%
    \lsc@instheadMSC{solid}{#2}%
  \else\ifx\lsc@arg\lsc@esymSD%
    \lsc@instheadSD{dashed}{#2}%
  \else\ifx\lsc@arg\lsc@esymMSC%
    \lsc@instheadMSC{dashed}{#2}%
  \else%
    \errmessage{LSC error: #1: Instance kind must be "MSC", "SD", "noboxSD", "esymMSC", or "esymSD"!}%
  \fi\fi\fi\fi\fi%
}{%
  % draw the foot (if necessary)
  %
  \lsc@instend%
}

%% an instance line with ingoing creation arrow
%
% \begin{lsccreateinst}[MSC|SD|noboxSD|esymMSC|esymSD]{<length>}{<id>}{<instancename>}
% \end{lsccreateinst}
%
% <length> is the vertical offset from the regular location of instance
% heads, i.e. with <length> = 0 the position of the instance head is the same
% as with regular instance lines.
% The <id> can be referenced in an lscCreate 
%
\newenvironment{lsccreateinst}[4][MSC]{%
  %
  % reset current Y position (always, to break the layout not completely)
  %
  \pssetlength{\lsc@Y}{0}%
  \global\advance\lsc@Y by-#2\lscLocationHeight%
  %
  \expandafter\ifx\csname lsc@createdest#3\endcsname\relax%
    %
    % common setup for the createarrow pnode
    %
    \pssetlength{\lsc@createinstX}{\lsc@X}%
    \pssetlength{\lsc@createinstY}{\lsc@Y}%
    \psaddtolength{\lsc@createinstY}{\lsc@createoffset}%
    %
    % put the head and the endpoint for the create arrow
    % (and remember whether we are in SD or MSC mode for the footer)
    %
    \def\lsc@arg{#1}%
    \ifx\lsc@arg\lsc@noboxSD%
      \lsc@instheadnoboxSD[\lsc@Y]{#4}%
      \lsc@setcreatenoboxdest{#3}{#4}%
    \else\ifx\lsc@arg\lsc@MSC%
      \lsc@instheadMSC[\lsc@Y]{solid}{#4}%
      \lsc@setcreateboxdest{#3}%
    \else\ifx\lsc@arg\lsc@SD%
      \lsc@instheadSD[\lsc@Y]{solid}{#4}%
      \lsc@setcreateboxdest{#3}%
    \else\ifx\lsc@arg\lsc@esymMSC%
      \lsc@instheadMSC[\lsc@Y]{dashed}{#4}%
      \lsc@setcreateboxdest{#3}%
    \else\ifx\lsc@arg\lsc@esymSD%
      \lsc@instheadSD[\lsc@Y]{dashed}{#4}%
      \lsc@setcreateboxdest{#3}%
    \else%
      \errmessage{LSC error: \lsc@arg: Creation instance kind must be "MSC", "SD", "noboxSD", "esymMSC", or "esymSD"!}%
    \fi\fi\fi\fi\fi%
  \else%
    \errmessage{LSC error: #3: Creation instance already defined!}%
  \fi%
}{%
  \lsc@instend%
}

%% symbolic instance line balloon
%
% \lscBalloon{existential|universal}{<stuff>}
%
\newcommand{\lscBalloon}[2]{%
  \def\lsc@arg{#1}%
  \ifx\lsc@arg\lsc@existential%
    \lsc@balloon{dashed}{#2}%
  \else\ifx\lsc@arg\lsc@universal%
    \lsc@balloon{solid}{#2}%
  \else%
    \errmessage{LSC error: #1: Balloon quantification must be "universal" or "existential"!}%
  \fi\fi%
}

%% the actor symbol
%
% \lscActor
%
\newcommand{\lscActor}{%
  \begin{pspicture}(-0.275,0.275)(0.275,-0.275)%
    \psline(0,0.3)(0,-0.1)%
    \psline(-0.15,0.05)(0.15,0.05)%
    \psline(-0.1,-0.15)(-0.1,-0.275)%
    \psline(0.1,-0.15)(0.1,-0.275)%
    \pscircle[fillstyle=solid](0,0.2){0.1}%
    \pspolygon[fillstyle=solid](0,0.0)(-0.15,-0.15)(0.15,-0.15)%
  \end{pspicture}}

%% the clock symbol
%
% \lscClock
%
\newcommand{\lscClock}{%
  \begin{pspicture}(-0.275,0.275)(0.275,-0.275)%
    \pscircle{0.275}%
    \pscircle{0.225}%
    \psline(0,0.225)(0,0)(0.225,0)%
  \end{pspicture}}

%% the environment symbol
%
% \lscEnv
%
\newcommand{\lscEnv}{%
  \begin{pspicture}(-0.5,0.275)(0.5,-0.275)%
    \psarc(-0.3,0.2){0.1}{0}{180}%
    \psarc(-0.1,0.2){0.1}{0}{180}%
    \psarc(0.1,0.2){0.1}{0}{180}%
    \psarc(0.3,0.2){0.1}{0}{180}%
    \psarc(-0.3,-0.2){0.1}{180}{0}%
    \psarc(-0.1,-0.2){0.1}{180}{0}%
    \psarc(0.1,-0.2){0.1}{180}{0}%
    \psarc(0.3,-0.2){0.1}{180}{0}%
    \psarc(-0.4,0.1){0.1}{90}{-90}%
    \psarc(-0.4,-0.1){0.1}{90}{-90}%
    \psarc(0.4,0.1){0.1}{-90}{90}%
    \psarc(0.4,-0.1){0.1}{-90}{90}%
    \rput(0,0){{\footnotesize ENV}}%
  \end{pspicture}}

% \begin{Lsc}[<prechartloc>]{existential|universal|none}{<nrinsts>}{<nrlocs>}
% \end{Lsc}
%
\newenvironment{Lsc}[4][]{%
  \lsc@init{#3}{#4}%
  %
  \ifthenelse{\equal{#1}{} \and \equal{#2}{none}}{%
    %
    % special case: no prechart, no frame
    %
    \psaddtolength{\lsc@ulY}{-\lsc@instheadruledepth}%
    \psaddtolength{\lsc@ulY}{\lsc@instheadruleheight}%
  }{%
    % have prechart or frame: correct height
    %
    \lsc@addpccorrection%
    %
    \ifthenelse{\equal{#1}{}}{%
    }{%
      % have prechart: correct width
      %
      \lsc@addpcwidthcorrection%
    }%
  }%
  %
  % add height correction if we shall draw a frame 
  %
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@none%
    \relax%
  \else\ifx\lsc@arg\lsc@existential%
    \lsc@addframecorrection%
  \else\ifx\lsc@arg\lsc@universal%
    \lsc@addframecorrection%
  \else%
    \errmessage{LSC error: \lsc@arg: LSC kind must be "existential", "universal", or "none"!}%
  \fi\fi\fi%
  %
  % start the picture
  %
  \begin{pspicture}(\lsc@ulX,\lsc@ulY)(\lsc@lrX,\lsc@lrY)%
  %
  % draw the prechart (also sets up some lengths for the frame)
  %
  \lsc@prechart{#1}%
  %
  % draw the universal/existential frame
  %
  \def\lsc@arg{#2}%
  \ifx\lsc@arg\lsc@existential%
    \lsc@frame{dashed}%
  \else\ifx\lsc@arg\lsc@universal%
    \lsc@frame{solid}%
  \else\ifx\lsc@arg\lsc@none%
    \relax%
  \else%
    \relax% error message is printed above 
  \fi\fi\fi%
}{%
  \end{pspicture}%
}%

% \begin{FullLsc}[<prechartloc>]{<name>}{<ac>}{invariant|initial|iterative}{strict|weak|}{existential|universal}{<nrinsts>}{<nrlocs>}
% \end{FullLsc}
%
\newenvironment{FullLsc}[8][]{%
  \lsc@init{#7}{#8}%
  %
  \lsc@addpccorrection%
  \lsc@addframecorrection%
  %
  \ifthenelse{\equal{#1}{}}{%
  }{%
    \lsc@addpcwidthcorrection%
  }%
  %
  \lsc@mkacambox{#2}{#3}{#4}{#5}%
  %
  % start the picture
  %
  \begin{pspicture}(\lsc@ulX,\lsc@ulY)(\lsc@lrX,\lsc@lrY)%
  %
  % draw the prechart (also sets up some lengths for the frame)
  %
  \lsc@prechart{#1}%
  %
  % draw the universal/existential frame
  %
  \def\lsc@arg{#6}%
  \ifx\lsc@arg\lsc@existential%
    \lsc@frame{dashed}%
  \else\ifx\lsc@arg\lsc@universal%
    \lsc@frame{solid}%
  \else%
    \errmessage{LSC error: \lsc@arg: LSC quantification must be "existential" or "universal"!}%
  \fi\fi%
  %
  \rput[lb](0,\lsc@pccorrection){%
    \usebox{\lsc@acambox}}
}{%
  \end{pspicture}
}%

\endinput