%% oo-resource-notation.sty - LaTeX macros for specifying shared
%% resources in the object oriented style
%% Manuel Carro 2001, Julio Mariño 2003, A. Herranz 2011

\NeedsTeXFormat{LaTeX2e}

% \ProvidesPackage{oosrn}[{OO Shared Resource Notation package}]
\RequirePackage{zed-csp}
%\RequirePackage{oz}
\RequirePackage{ifthen}

\newboolean{insidectadsol}
\setboolean{insidectadsol}{false}

\newboolean{insideformula}
\setboolean{insideformula}{false}

%% The indentX commands are a temporary kludge, and should be removed
%% when the environment is more mature.

\newcommand{\indenta}{
  \ifthenelse{\boolean{insidectadsol}}
  {\noindent\hspace*{2ex}}
  {\noindent}
  }

\newcommand{\indentb}{
  \ifthenelse{\boolean{insidectadsol}}
  {\noindent\hspace*{4ex}}
  {\noindent}
  }

\newcommand{\indentc}{
  \ifthenelse{\boolean{insidectadsol}}
  {\noindent\hspace*{6ex}}
  {\noindent}
  }

\newcommand{\indentd}{
  \ifthenelse{\boolean{insidectadsol}}
  {\noindent\hspace*{8ex}}
  {\noindent}
  }


%% The commands & envs. below can be used

\newenvironment{ctadsol}
  {
    \setboolean{insidectadsol}{true}
    \medskip
    }
  {\setboolean{insidectadsol}{false}}


%% Force indentation inside a ctadsol environment
%% useful e.g. for adding dots

\newcommand{\taba}{\indenta}
\newcommand{\tabb}{\indentb}
\newcommand{\tabc}{\indentc}
\newcommand{\tabd}{\indentd}


\newcommand{\nombrectad}[1]{
  \noindent
  \textbf{CADT} #1 \\
  }

\newcommand{\usa}[1]{
  \indenta\textbf{USES} #1 \\
  }

\newcommand{\operaciones}{
  \noindent\textbf{OPERATIONS} \\
  }

\newcommand{\operacion}[2]{
  \indenta\textbf{ACTION} #1:
  %\begin{minipage}[t]{0.8\textwidth}
    \ensuremath{#2}
  %\end{minipage}
  \\
  }

\newcommand{\funcion}[2]{
  \indenta\textbf{FUNCTION} #1:
  \begin{minipage}[t]{0.8\textwidth}
    \emph{#2}
  \end{minipage}
  \\
  }

\newcommand{\constructor}[2]{
  \indenta\textbf{CONSTRUCTOR} #1:
  \begin{minipage}[t]{0.8\textwidth}
    \emph{#2}
  \end{minipage}
  \\
  }

\newcommand{\semantica}{
  \noindent
  \textbf{SEMANTICS} \\
  }

\newcommand{\dominio}{
  \indenta\textbf{DOMAIN:} \\
  }

\newcommand{\estado}[1]{
  \indentb\textbf{STATE: \self = }
  \begin{minipage}[t]{0.8\textwidth}
    \ensuremath{#1}
  \end{minipage}
  \\
  }

\newcommand{\tipo}[1]{
  \indentb\textbf{TYPE:}
  \begin{minipage}[t]{0.8\textwidth}
    \emph{#1}
  \end{minipage}
  }

\newcommand{\invariante}[1]{
  \setboolean{insideformula}{true}
  \indentb\textbf{INVARIANT:}
  \begin{minipage}[t]{0.8\textwidth}
    \ensuremath{#1}
  \end{minipage}
  \setboolean{insideformula}{false}
  %\\
  }

\newcommand{\invariantenl}[1]{
  \setboolean{insideformula}{true}
  \indentb\textbf{\emph{INVARIANT:}}
  \begin{minipage}[t]{0.8\textwidth}
    \emph{#1}
  \end{minipage}
  \setboolean{insideformula}{false}
  \\
  }

\newcommand{\inicial}[2]{
  \setboolean{insideformula}{true}
  % \indentb\textbf{INITIAL(\textmd{#1}):}
  \indentb\textbf{INITIAL:}
  %\begin{minipage}[t]{0.8\textwidth}
    \ensuremath{#2}
  %\end{minipage}
  \setboolean{insideformula}{false}
  \smallskip
  \\
  }

\newcommand{\semdom}{\semantica\dominio}

\newcommand{\protoconc}[2]{
  \indentb\textbf{PROTOCOLS:}\hspace{1ex}
  \begin{minipage}[t]{0.7\textwidth}
    \ensuremath{#1}
  \end{minipage}\\
  \indentb\textbf{CONCURRENCY:}\hspace{1ex}
  \begin{minipage}[t]{0.7\textwidth}
    \ensuremath{#2}
  \end{minipage}
}

\newcommand{\protocolos}[1]{
  \indentb\textbf{PROTOCOLS:}\hspace{1ex}
  \begin{minipage}[t]{0.8\textwidth}
    \ensuremath{#1}
  \end{minipage}
}

\newcommand{\nomop}[1]{
  \indentc\textbf{#1}\\
}


\newcommand{\genassert}[2]{
  \setboolean{insideformula}{true}
  \indenta\textbf{#1:~}%
%  \begin{minipage}[t]{0.5\textwidth}
    \ensuremath{#2}\\
%  \end{minipage}
  \setboolean{insideformula}{false}
}

\newcommand{\genassertblue}[2]{
  \setboolean{insideformula}{true}
  \indenta\textbf{#1:~}%
%  \begin{minipage}[t]{0.5\textwidth}
    \ensuremath{\color{blue}#2}\\
%  \end{minipage}
  \setboolean{insideformula}{false}
}

\renewcommand{\pre}[1]{\genassert{PRE}{#1}}
\newcommand{\prek}[1]{\genassert{PRE}{#1}}

\newcommand{\cpre}[1]{\genassert{CPRE}{#1}}

\newcommand{\waiting}[1]{\genassertblue{\textcolor{blue}{WAITING}}{#1}}

\newcommand{\enabled}[1]{\genassert{\textcolor{blue}{ENABLED}}{\textcolor{blue}{#1}}}

\newcommand{\post}[1]{\genassert{POST}{#1}}

\newcommand{\prenl}[1]{\genassert{\emph{PRE}}{\emph{#1}}}

\newcommand{\cprenl}[1]{\genassert{\emph{CPRE}}{\emph{#1}}}

\newcommand{\postnl}[1]{\genassert{\emph{POST}}{\emph{#1}}}

\newcommand{\donde}[1]{
  \noindent
  \ifthenelse{\boolean{insideformula}}
  {\relax}  % No indent
  {\indentb}  % or make it at PRE/CPRE/POST level
  \textnormal{\textbf{WHERE:}}
  \begin{minipage}[t]{0.88\textwidth}
    \textnormal{#1}
  \end{minipage}
  }


%% useful macros
%\newcommand{\void}{\ensuremath{\epsilon}}
\newcommand{\void}{} %% OJO!!
%\newcommand{\sal}{\ensuremath{^{\scriptsize\textrm{out}}}}
\newcommand{\sal}{} %% OJO!! 
\newcommand{\ent}{\ensuremath{^\textrm{in}}}
%% al final, no estamos usando tipografía matemática
%% en las especificaciones
\newcommand{\alter}{\ensuremath{|\;}}

\newcommand{\cierto}{\mathrm{True}}
\newcommand{\falso}{\mathrm{False}}
\newcommand{\result}{\mathrm{result}}
\newcommand{\self}{\ensuremath{\mathrm{self}}}
%\newcommand{\self}{}

% Commands to be removed:
% \newcommand{\but}{\ensuremath{\;\backslash\;}}
% %% I do not like the spacing \| gives
% \newcommand{\conc}{\ensuremath{|\!|}}
\newcommand{\st}{\ensuremath{\mathbin{\raisebox{0.2ex}{\scalebox{0.75}{\ensuremath{\bullet}}}}}}
% \newcommand{\tq}{\st}
\newcommand{\por}{\ensuremath{\cross}}
\newcommand{\bool}{\ensuremath{\mathbb{B}}}
\newcommand{\tfun}{\rightarrow}


\newcommand{\true}{\mathrm{true}}
\newcommand{\false}{\mathrm{false}}
\newcommand{\but}{\ensuremath{\;\backslash\;}}
% \newcommand{\len}[1]{\textsf{Length}(#1)}
\newcommand{\lng}[1]{\textsf{Length}(#1)}
\newcommand{\floor}[1]{\lfloor #1 \rfloor}
