% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%
% DC -- A LaTeX style for typesetting Duration Calculus formulae
% 
% (c) Jochen Hoenicke, 2009
%
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{dc}[2009/06/18 Typesetting DC formulae]

\RequirePackage{amsmath,amssymb}

\let\dcalw\Box
\let\dceve\Diamond
\let\dcint\smallint
\def\dc#1{\lceil #1\rceil}
\def\dcev#1#2{\underset{#2}{\lceil #1\rceil}}
\def\dcseq{\longrightarrow}
\def\dclead#1{\overset{#1}{\longrightarrow}}
\def\dcleadev#1#2{\underset{#2}{\overset{#1}{\longrightarrow}}}
\def\dcleadin#1{\overset{#1}{\longrightarrow_0}}
\def\dcleadinev#1#2{\underset{#2}{\overset{#1}{\longrightarrow_0}}}
\newcommand{\dcnoevent}{\mathop{\boxminus}}
\newcommand{\dcevent}{\mathop{\updownarrow}}
\newcommand{\dcnotevent}{\mathop{\!\not\,\updownarrow}}

% DC event definitions
%\def\dcchop{;}
\newcommand{\dcchop}{\mathbin{\mbox{\bf ;}}}
\def\dcchopev#1{\mathbin{\underset{#1}{\dcchop}}}
\newenvironment{dcenv}{\csp}{\endcsp}

% DC with Liveness [L] und <L>:
\font\dc@bigwasy = wasy10 at 15pt
\def\dc@Square{\hbox{\dc@bigwasy\char"32}}
\def\dc@Diamond{\hbox{\dc@bigwasy\char"33}}

\newcommand{\dc@inbox}[1]{\setbox0=\hbox{$\dc@Square$}%
\hbox to 0cm{\rlap{$\dc@Square$}}%
\hbox to \wd0{\hfill\vbox to \ht0{%
\vfill\hbox{\ensuremath{\scriptscriptstyle #1}}\vfill}\hfill}}

\newcommand{\dc@indiam}[1]{\setbox0=\hbox{$\dc@Diamond$}%
\hbox to 0cm{\rlap{$\dc@Diamond$}}%
\hbox to \wd0{\hfill\raisebox{1.5pt}{\vbox to \ht0{%
\vfill\hbox{\ensuremath{\scriptscriptstyle #1}}\vfill}}\hfill}}
\newcommand{\dceveL}{\dc@indiam{L}}
\newcommand{\dcalwL}{\dc@inbox{L}} 

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

\newcommand{\obs}{\mathit{obs}}
%
\newcommand{\domf}{\mathcal{D}}
\newcommand{\domval}{d}
\newcommand{\timedom}{\mathsf{Time}}
%
\newcommand{\evo}{\pi}
%
\newcommand{\dt}{\,\mathit{dt}}

\newcommand{\true}{\mathit{true}}
\newcommand{\false}{\mathit{false}}
\newcommand{\TT}{\mathsf{tt}}
\newcommand{\FF}{\mathsf{ff}}
%
\newcommand{\globvars}{\mathsf{GVar}}
\newcommand{\obss}{\mathsf{Obs}}
%
\newcommand{\val}{\mathcal{V}}
\newcommand{\vals}{\mathsf{Val}}
%
\newcommand{\inter}{\mathcal{I}}
%
\newcommand{\intvs}{\mathsf{Intv}}
%
\newcommand{\term}{\theta}

\newcommand{\Prop}[1]{%
  \ifmmode\relax\else`\fi\ensuremath{\mathsf{#1}}\ifmmode\relax\else'\fi}
%
\newcommand{\Spec}{\Prop{Spec}}
\newcommand{\Req}{\Prop{Req}}
\newcommand{\ReqA}{\Prop{Req\dash1}}
\newcommand{\Des}{\Prop{Des}}
\newcommand{\DesA}{\Prop{Des\dash1}}
\newcommand{\DesB}{\Prop{Des\dash2}}
\newcommand{\Ctrl}{\Prop{Ctrl}}
\newcommand{\Asm}{\Prop{Asm}}

\newcommand{\phase}{\pi}

\endinput