misc latex macro

macro.sty

% general
\newcommand{\intro}[1]{{\em #1}\/}
\def\mynote#1{$\clubsuit$ {\sf #1 } $\clubsuit$}

\newcommand{\myparagraph}[1]{\medskip \noindent{\bf #1}}

%\def\dpar{{c}}
%\def\dval{\alpha}
\def\prop{{r}} % an atomic proposition
\def\prob{\mathrm{Pr}} % probability measure
\def\expect{\mathrm{E}} % expected value
%\def\pval{{q}} % its interpretation
%\def\pmax{{q_\mathit{max}}}
\newcommand{\clos}{\mathit{clos}}
%\def\bvalues{\mathit{bvals}}
\def\values{\mathit{vals}}
\def\traces{\mathit{trac}}
\def\genqts{(\AP,S,\trans{},\interv{\cdot})}
\def\genqmc{(\AP,S,\Delta,\interv{\cdot})}
\def\genqmdp{(\AP,S,\Delta,\interv{\cdot})}

\def\tuple#1{\langle #1 \rangle} 

% math
\def\ra{\rightarrow}
\def\Lra{\Leftrightarrow}
\def\bs{\backslash}
\renewcommand{\phi}{\varphi}
\def\set#1{\{#1\}}
\def\floor#1{\lfloor#1\rfloor}
\def\angle#1{\langle#1\rangle}

\def\reals{\bbbr}                       % the set of reals R
\def\naturals{\bbbn}                    % the set of naturals N
\def\rationals{\bbbq}                   % the set of rationals Q
\newcommand{\posreals}{\mathbb{R}^{\geq 0}}
\newcommand{\nats}{\mathbb{N}}
\newcommand{\order}{\calo}

% DLTL logic operators/interpretation
\newcommand{\last}{{\text{\textit{last}}}}
\newcommand{\maxi}{{\text{\textit{max}}}}
\newcommand{\mini}{{\text{\textit{min}}}}
\newcommand{\imax}{\mathrel\sqcup} % inline max 
\newcommand{\imin}{\mathrel\sqcap} % inline max 
\newcommand{\argmax}{\mathop{\rm argmax}} % inline max 
\def\nicht{\neg}                        % negation (alias for \neg)
\def\und{\imin}                         % and
\def\oder{\imax}                        % or
\def\true{\mbox{\sc t}}                 % T for true
\def\false{\mbox{\sc f}}                % F for false

\newcommand{\until}{\,{\cal U}}
\newcommand{\dualuntil}{\widehat{\until}}
\newcommand{\uuntil}{\,\tilde{\cal U}}  % Dual of Until (Release)
\newcommand{\meanw}{{\cal M}}   % Meanwhile
\def\next{\begin{picture}(8,6)(-4,-2) \put(0,1){\circle{6}} \end{picture}}
%\def\next{\textstyle{\bigcirc}}
%\def\nnext{\textstyle{\bigodot}}
%\def\nnext{\begin{picture}(8,6)(-4,-2) \put(0,1){\circle{6}} \put(-1,1){\line(1,0){2}} \end{picture}}
\def\dualnext{\widehat\next}

%\newcommand{\dotminus}{\stackrel{\mbox{\lower.5cm\hbox{$_{\centerdot$}}}}{-}}
%\newcommand{\dotminus}{\stackrel{{}_\centerdot}-}
%\newcommand{\dotminus}{-{}^\centerdot}
\newcommand{\dotminus}{
\begin{picture}(12,6)(-4,-2) 
  \put(-1, 0){ \makebox(0,0){$-$} }
  \put(-1, 2){ \makebox(0,0){$\cdot$} } 
  \end{picture}}
%\renewcommand{\dotminus}{\overset{\cdot}{\smash[t]-}}

\newcommand{\isleq}{{\widehat \leq}}
\newcommand{\plus}{{\widehat +}}
\newcommand{\mult}{{\cdot}}

%% SEMANTICS 
\def\sem#1{[\![#1]\!]}
\newcommand{\val}{v}

% lts and mc
\newcommand{\AP}{\Sigma}
\newcommand{\A}{{\cal A}}
\newcommand{\lts}{{\cal S}}
\newcommand{\qts}{{\cal S}}
\newcommand{\mdp}{{\cal S}}
\newcommand{\qmdp}{{\cal S}}
\newcommand{\mc}{{\cal S}}
\newcommand{\qmc}{{\cal S}}
\newcommand{\vals}{{\cal V}}
%\newcommand{\bvals}{{\cal V}}
\newcommand{\pars}{{\cal A}}
\newcommand{\distr}{{\cal D}}
\newcommand{\facts}{{\cal I}}

\newcommand{\tpm}{P}% transition probability matrix
\newcommand{\xint}{E}
\newcommand{\sched}{{\text{\textit{Sched}}}}
\newcommand{\mdsched}{{\text{\textit{DSched}}}}
\newcommand{\pts}{\mathit{pts}}
\newcommand{\trajs}{\traces} 
\newcommand{\ftrajs}{{\text{\textit{FTraj}}}}
\newcommand{\strajs}{{\text{\textit{STraj}}}}
\newcommand{\looptrajs}{{\cal L}}
\newcommand{\stra}{\pi} % strategy 
\newcommand{\bigstra}{\Pi} % set of strategies
\newcommand{\pd}{a} % probability distribution over next state

\newcommand{\bigsqp}[1]{\Bigl[ #1 \Bigr]} % parentheses for expectation
\newcommand{\measurable}{\calb} % set of measurable distributions
% Set of prob distributions over a set

\newcommand{\pre} {\exists\!\pppre}
\newcommand{\dpre}{\forall\!\pppre}
\newcommand{\randrho}{\Omega} % random path 

\newcommand{\binsize}[1]{|#1|_b} % binary encoding size
\newcommand{\lfrac}[2]{#1 / #2} % fractions... according to Luca

\def\zero{{\bf 0}}
\def\one{{\bf 1}}
\def\interv#1{[#1]}

% names of logics
\newcommand{\ctl}{\text{{\sc Ctl}}}
%\newcommand{\dctl}{\text{\sc Dctl}}
\newcommand{\dltl}{\text{\sc Dltl}}
\newcommand{\dltlforms}{\Phi}
\newcommand{\ltl}{\text{\sc Ltl}}
\newcommand{\qltl}{\text{\sc QLtl}}
\newcommand{\qctl}{\text{\sc QCtl}}
\newcommand{\dctl}{\text{\sc DCtl}}
\newcommand{\dmu}{\text{\sc D}\mu}
\newcommand{\dctleq}{\text{\sc Dctl}_=}
\newcommand{\dctlnuw}{\text{\sc Dctl}_{\until,\wait}}
\newcommand{\dctllongrun}{\text{\sc Dctl}_{\triangle}}

% sim and bisim
\newcommand{\qsim}{{\preceq}}
\newcommand{\qbis}{{\simeq}}
\newcommand{\symdist}{d^{\rm E}}
\newcommand{\asymdist}{d^{\rm I}}

% **********Automaten
\newcommand{\states}[1]{{S_{#1}}}
\newcommand{\start}[1]{{S^0_{#1}}}
\newcommand{\acts}[1]{{{\rm Act}_{#1}}}
\newcommand{\trans}[1]{{\delta_{#1}}}
\newcommand{\reach}[1]{{\it  reach_{#1}}}
\newcommand{\genBuchi}[1]{{\cal B}_{#1}}
\newcommand{\step}[2]{\smash[t]{\xrightarrow{#1}_{#2}}}

\newcommand{\Inf}{\text{\it Inf}}
\def\Adet{\A_\phi^{\text{det}}}

%% LUCA's STUFF


% ===================================================================== call.sty 

\def\cala{{\cal A}}
\def\calb{{\cal B}}
\def\calc{{\cal C}}
\def\cald{{\cal D}}
\def\cale{{\cal E}}
\def\calf{{\cal F}}
\def\calg{{\cal G}}
\def\calh{{\cal H}}
\def\cali{{\cal I}}
\def\calj{{\cal J}}
\def\calk{{\cal K}}
\def\call{{\cal L}}
\def\calm{{\cal M}}
\def\caln{{\cal N}}
\def\calo{{\cal O}}
\def\calp{{\cal P}}
\def\calq{{\cal Q}}
\def\calr{{\cal R}}
\def\cals{{\cal S}}
\def\calt{{\cal T}}
\def\calu{{\cal U}}
\def\calv{{\cal V}}
\def\calw{{\cal W}}
\def\calx{{\cal X}}
\def\caly{{\cal Y}}
\def\calz{{\cal Z}}

% ========================================================== (old tl.sty, edited)

% Generic mathematical symbols 

\def\eqpun{\;}        % space after eq for punct
\def\subs{\subseteq}
\def\Dom{\mbox{\rm Dom}\,}
\def\Im{\mbox{\rm Im}\,}
\def\sat{\models}     % |=
\def\stsat{\mid\!\sat}      % ||=
\def\defined{\stackrel{\rm def}{=}} % = w. 'def' on top
\def\union{\cup}
\def\inters{\cap}
\def\power#1{2^{#1}}
\def\eqspa{\hspace*{2em}} % space betw. equation on the same line 
\def\semb#1{[\![ #1 ]\!]}   % [[ #1 ]]
\def\tuple#1{\langle #1 \rangle}    % < #1 >
\def\set#1{\{ #1 \}}      % { #1 }
\def\go{\rightarrow}      % -->
\def\setm{\setminus}      % \
\def\ita#1{{\text{\textit{#1}}}}        % to italicise something

% Logical operators 

\def\im{\rightarrow}      % implication
\def\biim{\,\leftrightarrow\,}    % biimplication
\def\qdot{\:.\:}      % . for quantification
\def\@spartx{\hspace{0.4em}}
\def\tiff{\ita{\@spartx iff \@spartx}}
\def\tand{\ita{\@spartx and \@spartx}}
\def\tor{\ita{\@spartx or \@spartx}}
\def\timplies{\ita{\@spartx implies \@spartx}}
\def\tnot{\ita{\@spartx not \@spartx}}

% text fonts

\def\xit#1{{\text{\textit{#1}}}}
\def\xem#1{{\text{\emph{#1}}}}
\def\xtt#1{{\text{\texttt{#1}}}} 
\def\xbf#1{{\text{\textbf{#1}}}} 

% standard TL operators

\def\@bo{{\raisebox{-0.2ex}{$\Box$}}}   % internal 
\def\@dia{{\raisebox{-0.2ex}{$\Diamond$}}}  % internal 
\def\bo{\@bo}         % box
\def\diam{{\@dia}}        % diamond
%\def\until{\mbox{$\:\cal U$}}            % U
\def\unless{\mbox{$\:\cal W\:$}}    % W
\def\awaits{\mbox{$\:\cal W\:$}}    % W
\def\since{\mbox{$\:\cal S\:$}}           % S
\def\backto{\mbox{$\:\cal B\:$}}    % B
\def\pbox{\mbox{\rm\makebox[0em][l]{$\@bo$}\makebox[0.8em]{--}}} % past box
\def\pdiam{\mbox{\rm\makebox[0em][l]{$\@dia$}\makebox[0.8em]{--}\hspace{0.05em}}} % past diamond
%\def\prev{\mbox{\rm\makebox[0em][l]{$\next$}\makebox[1.0em]{$-$}\,}} % previous 

\def\prev{\begin{picture}(8,6)(-4,-2)
\put(0,1){\circle{6}} 
\put(-3,1){\line(1,0){6}}
\end{picture}}

% To put notes
\def\mynote#1{$\clubsuit$ {\sf #1 } $\clubsuit$}
%\def\mynote#1{}

% Misc enhancements to LaTeX

\def\beq{\begin{equation}}
\def\eeq{\end{equation}}

% Naming equations or axioms: use \begin{namedeq}{EQ} to obtain
% an equation labelled with name (EQ). This does not disrupt the 
% numbering of the equations. It is to be used when the \theequation
% comand is normally set to \arabic{equation}, otherwise a new environment
% with the appropriate end text should be defined.
\newenvironment{namedeq}[1]{\renewcommand{\theequation}{#1}
  \begin{equation}}{\end{equation}
  \renewcommand{\theequation}{\arabic{equation}}
  \addtocounter{equation}{-1}}

% Naming equations or axioms, for eqnarray: use \begin{namedeqar}{EQ-} to
% obtain equations named (EQ-1), (EQ-2), ...
% As the above, this works if arabic is the default.
% \newenvironment{namedeqar}[1]{\renewcommand{\theequation}{#1\arabic{
% to be completed: need to declare a counter

% This fixes a bug in equations.sty, having to do with the way
% equations behave when fleqn.sty is also used.
% do not use eqalign. Instead:
% better version of eqalignno (with number):
\newenvironment{eqtab}{\begin{equation}
  \begin{eqalign}}{\end{eqalign}\end{equation}}
% better version of eqalignno* (without number):
\newenvironment{eqtabn}{\begin{displaymath}
  \begin{eqalign}}{\end{eqalign}\end{displaymath}}

% bold letters from llncs:

\def\bbbb{{\rm I\!B}}
\def\bbbr{{\rm I\!R}} %reelle Zahlen
\def\bbbm{{\rm I\!M}}
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
\def\bbbf{{\rm I\!F}}
\def\bbbh{{\rm I\!H}}
\def\bbbk{{\rm I\!K}}
\def\bbbp{{\rm I\!P}}

%-----------------------
%
% Stuff added by BCD
%

\def\natural{\mathbb{N}}
\def\naturalx{\natural_{\infty}}
\def\naturaln#1{\natural_{#1}}
\def\runs#1#2{{\lbrack}{#1}{\rbrack}^{#2}}
\def\runsf#1{\runs{#1}{*}}
\def\runsi#1{\runs{#1}{\omega}}
\def\runsm#1{\runs{#1}{\infty}}
\def\runsn#1#2{\runs{#1}{#2}}
\def\runsln#1#2{\runsn{#1}{\leq{#2}}}
\def\size#1{|{#1}|}
\def\horizon#1#2{{#1}|^{\leq #2}}
\def\atlength#1#2{{#1}|^{#2}}