
% Graphics and colors...
\graphicspath{{../images/}}

% hyphenation...s
\hyphenation{Open-MP}
\definecolor{darkred}{rgb}{0.55, 0.0, 0.0}
\definecolor{bistre}{rgb}{0.47, 0.27, 0.23}
\definecolor{coolblack}{rgb}{0.0, 0.18, 0.39}
\definecolor{Brown}{rgb}{0.59, 0.29, 0.0}

% Comments...
\newcommand{\mycomment}[1]{\texttt{\textcolor{darkred}{#1}}}
\newcommand{\nonterm}[1]{\texttt{\textit{\textcolor{blue}{#1}}}}
\newcommand{\mgcolor}[0]{bistre}
\newcommand{\acslmark}{\textit{\textcolor{red}{a}}}

\newcommand{\myskip}[0]{2mm}
\newcommand{\powerset}{\raisebox{.15\baselineskip}{\Large\ensuremath{\wp}}}
\renewcommand{\vdash}[0]{\models}

% font size...
\newcommand{\codesize}{\tt}

% Type/font styles...
\newcommand{\upsty}[1]{{\ttfamily\textcolor{Brown}{#1}}} %{\textbf{\textcolor{BlueViolet}{#1}}}
\newcommand{\consty}[1]{{\ttfamily\textcolor{Bittersweet}{#1}}}
\newcommand{\setsty}[1]{\textup{\textsf{\textcolor{BlueViolet}{#1}}}}
\newcommand{\code}[1]{{\ttfamily #1}}  % code not CIVL/C keyword
\newcommand{\ccode}[1]{{\textcolor{coolblack}{\ttfamily\fontseries{b}\selectfont{}#1}}}
\newcommand{\myccode}[1]{{\textcolor{blue}{\ttfamily\fontseries{b}\selectfont{}#1}}}
\newcommand{\bluecode}[1]{{\ttfamily\bfseries\color{blue} #1}}
\newcommand{\redcode}[1]{{\ttfamily\bfseries\color{red} #1}}
\newcommand{\funsty}[1]{\ttfamily\bfseries #1}
\newcommand{\typsty}[1]{{\textcolor{blue}{\ttfamily\bfseries\emph{#1}}}}
\newcommand{\ct}[1]{\texttt{#1}}

% Symbols...
\newcommand{\civlImplies}{\Rightarrow}
\newcommand{\ra}{\rightarrow}
\newcommand{\B}{\mathbb{B}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\lb}{\texttt{\char`\{}}
\newcommand{\rb}{\texttt{\char`\}}}
\newcommand{\civlU}{\texttt{\char`\_}}
\newcommand{\U}{\texttt{\char`\_}}
\newcommand{\BSL}{\texttt{\char`\\}}
%\newcommand{\civlU}{{\ttfamily\symbol{'137}}}
\newcommand{\civlUU}{\civlU\civlU}
\newcommand{\biglp}{\textcolor{\mgcolor}{\big(}}
\newcommand{\bigrp}{\textcolor{\mgcolor}{\big)}}
\newcommand{\regxstar}{\textcolor{\mgcolor}{\textit{*}}}
\newcommand{\regxplus}{\textcolor{\mgcolor}{\textit{+}}}
\newcommand{\regxques}{\textcolor{\mgcolor}{\textit{?}}}
\newcommand{\synxbar}{\textcolor{\mgcolor}{\mid}}
\newcommand{\synxdef}{\textcolor{\mgcolor}{:=}}
\newcommand{\synxdots}{\textcolor{\mgcolor}{\ldots}}




% Spaces...
\newcommand{\sspc}{\hspace{1mm}} % small space 

% Tools...
\newcommand{\civl}{CIVL}
\newcommand{\spin}{\textsc{Spin}}
\newcommand{\mpispin}{\textsc{MPI-Spin}}
\newcommand{\tass}{TASS}
\newcommand{\partypes}[0]{\text{\normalsize{P}\scriptsize{AR}\normalsize{T}\scriptsize{YPES}}}
\newcommand{\isp}{ISP}
\newcommand{\mopper}{MOPPER}
\newcommand{\promela}{Promela}

% MPI primitives...
% functions
\newcommand{\MPISend}{\funsty{MPI\civlU{}Send}}
\newcommand{\MPIRecv}{\funsty{MPI\civlU{}Recv}}
\newcommand{\MPIBarrier}{\funsty{MPI\civlU{}Barrier}}
\newcommand{\MPIReduce}{\funsty{MPI\civlU{}\-Reduce}}
\newcommand{\MPIAllreduce}{\funsty{MPI\civlU{}Allreduce}}
\newcommand{\MPIInit}{\funsty{MPI\civlU{}Init}}
\newcommand{\MPIInitthread}{\funsty{MPI\civlU{}Init}\civlU{}thread}
\newcommand{\MPIFinalize}{\funsty{MPI\civlU{}Finalize}}
\newcommand{\MPIDup}{\funsty{MPI\civlU{}Comm\civlU{}dup}}
\newcommand{\MPIFree}{\funsty{MPI\civlU{}Comm\civlU{}free}}
\newcommand{\MPIWtime}{\funsty{MPI\civlU{}Wtime}}
\newcommand{\MPIReducescatter}{\funsty{MPI\civlU{}Reducescatter}}
\newcommand{\MPIAlltoallv}{\funsty{MPI\civlU{}Alltoallv}}
\newcommand{\MPIAlltoallw}{\funsty{MPI\civlU{}Alltoallw}}
\newcommand{\MPICommsize}{\funsty{MPI\civlU{}Comm\civlU{}size}}
\newcommand{\MPICommrank}{\funsty{MPI\civlU{}Comm\civlU{}rank}}
\newcommand{\MPIGetcount}{\funsty{MPI{\civlU}Get{\civlU}count}}
\newcommand{\MPISendrecv}{\funsty{MPI{\civlU}Sendrecv}}
\newcommand{\MPIBcast}{\funsty{MPI{\civlU}Bcast}}
\newcommand{\MPIAllgather}{\funsty{MPI{\civlU}Allgather}}
\newcommand{\MPICommdup}{\funsty{MPI{\civlU}Comm{\civlU}dup}}
\newcommand{\MPICommfree}{\funsty{MPI{\civlU}Comm{\civlU}free}}
\newcommand{\MPIScatter}{\funsty{MPI{\civlU}Scatter}}
\newcommand{\MPIGather}{\funsty{MPI{\civlU}\-Gath\-er}}
\newcommand{\MPIGatherv}{\funsty{MPI{\civlU}Gatherv}}
\newcommand{\MPIScatterv}{\funsty{MPI{\civlU}Scatterv}}
\newcommand{\MPIAlltoall}{\funsty{MPI{\civlU}Alltoall}}

% types
\newcommand{\MPIDatatype}{\typsty{MPI\civlU{}Datatype}}
\newcommand{\MPIComm}{\typsty{MPI\civlU{}Comm}}
\newcommand{\MPIStatus}{\typsty{MPI\civlU{}Status}}
\newcommand{\MPIOp}{\typsty{MPI\civlU{}Op}}
\newcommand{\MPIRequest}{\typsty{MPI\civlU{}Request}}

% constants
\newcommand{\MPICOMMWORLD}{\code{MPI\civlU{}COMM\civlU{}WORLD}}
\newcommand{\MPIPROCNULL}{\code{MPI\civlU{}PROC\civlU{}NULL}}
\newcommand{\MPIANYSOURCE}{\code{MPI\civlU{}ANY\civlU{}SOURCE}}
\newcommand{\MPIANYTAG}{\code{MPI\civlU{}ANY\civlU{}TAG}}
\newcommand{\MPISTATUSIGNORE}{\code{MPI\civlU{}STATUS\civlU{}IGNORE}}
\newcommand{\MPIUNINIT}{\code{\civlU{}MPI\civlU{}UNINIT}}
\newcommand{\MPIINIT}{\code{\civlU{}MPI\civlU{}INIT}}
\newcommand{\MPIFINALIZED}{\code{\civlU{}MPI\civlU{}FINALIZED}}
\newcommand{\REDUCETAG}{\code{\civlU{}REDUCE\civlU{}TAG}}



% Displaying code...
\newcounter{lc}  % global variable for line count
\DeclareRobustCommand{\showline}{%
  \stepcounter{lc}%
  {\scriptsize\makebox[1mm][r]{\textcolor{blue}{\arabic{lc}}}\hspace{.5mm}}%
}

\newenvironment{program}{%
  \linespread{1.0}
  \normalsize\tt\setcounter{lc}{0}
  \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}%
  }{%  
  \end{tabular}% 
}

\newenvironment{programContinue}[1]{%
  \linespread{1.0}
  \normalsize\tt\setcounter{lc}{#1}
  \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}%
  }{%  
  \end{tabular}% 
}

\newenvironment{programNoNum}{%
  \normalsize\tt\setcounter{lc}{0}
  \begin{tabular}{@{}l@{}}%
  }{%  
  \end{tabular}% 
}

\newenvironment{programSmall}{%
  \linespread{1.0}
  \footnotesize\tt\setcounter{lc}{0}
  \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}%
  }{%  
  \end{tabular}% 
}

\newenvironment{programSuperSmall}{%
  \linespread{1.0}
  \scriptsize\tt\setcounter{lc}{0}
  \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}%
  }{%  
  \end{tabular}% 
}

\newcommand{\transsep}[1]{
  \vspace{-1.5mm}\par
  \begin{tabular}{@{}r@{}}
    \scriptsize\it\textcolor{blue}{#1}\\[-2.5mm]
    \rule{\columnwidth}{0.5pt}\\[-1.4mm]
    \scriptsize\it\textcolor{blue}{transformed to CIVL-C}
  \end{tabular}
  \vspace{-1.5mm}\par
}

\newenvironment{listing}{
  \codesize\tt\setcounter{lc}{0}
  \begin{flushleft}
  }{
  \end{flushleft}
}

\newcommand{\lno}{\showline \ }

% CIVL-C keywords...
\newcommand{\cckey}{\$}
\newcommand{\cc}[1]{\mbox{\textcolor{blue}{\texttt{\cckey{}#1}}}}

\newcommand{\cabstract}{\cc{abstract}}
\newcommand{\cproc}{\cc{proc}}
\newcommand{\cprocNull}{\cc{proc{\civlU}null}}
\newcommand{\cself}{\cc{self}}
\newcommand{\cinput}{\cc{input}}
\newcommand{\coutput}{\cc{output}}
\newcommand{\cspawn}{\cc{spawn}}
\newcommand{\csystem}{\cc{system}}
\newcommand{\catomicf}{\cc{atomic{\civlU}f}}
\newcommand{\cwait}{\cc{wait}}
\newcommand{\cwaitall}{\cc{waitall}}
\newcommand{\cassert}{\cc{assert}}
\newcommand{\ctrue}{\cc{true}}
\newcommand{\cfalse}{\cc{false}}
\newcommand{\cassume}{\cc{assume}}
\newcommand{\catom}{\cc{atom}}
\newcommand{\catomic}{\cc{atomic}}
\newcommand{\cwhen}{\cc{when}}
\newcommand{\cchoose}{\cc{choose}}
\newcommand{\cchooseint}{\cc{choose{\civlU}int}}
\newcommand{\cinvariant}{\cc{invariant}}
\newcommand{\cexit}{\funsty{\$exit}}
\newcommand{\cresult}{\cc{result}}
\newcommand{\cat}{\texttt{@}}
\newcommand{\ccollective}{\cc{collective}}
\newcommand{\cequals}{\cc{equals}}
\newcommand{\cfor}{\cc{for}}
\newcommand{\cparfor}{\cc{parfor}}
\newcommand{\cscope}{\cc{scope}}
\newcommand{\cscoperoot}{\cc{root}}
\newcommand{\chere}{\cc{here}}
\newcommand{\cregion}{\cc{region}}
\newcommand{\cmalloc}{\cc{malloc}}
\newcommand{\cfree}{\cc{free}}
\newcommand{\cforall}{\cc{forall}}
\newcommand{\cexists}{\cc{exists}}
\newcommand{\cimplies}{\ct{=>}}
\newcommand{\crange}{\cc{range}}
\newcommand{\cdomain}{\cc{domain}}
\newcommand{\cdomainof}[1]{\cc{domain}\ct{(}#1\ct{)}}
\newcommand{\clambda}{\cc{lambda}}

%%% CIVL-C functions %%%
\newcommand{\capply}{\funsty{\$apply}}
\newcommand{\ccontains}{\funsty{\$contains}}
\newcommand{\ccopy}{\funsty{\$copy}}
\newcommand{\cscopeof}{\funsty{\$scopeof}}
\newcommand{\cscopeparent}{\funsty{\$scope{\civlU}parent}}
\newcommand{\cbundlesize}{\funsty{\$bundle{\civlU}size}}
\newcommand{\cbundlepack}{\funsty{\$bundle{\civlU}pack}}
\newcommand{\cbundleunpack}{\funsty{\$bundle{\civlU}unpack}}
\newcommand{\cbundleunpackapply}{\funsty{\$bundle{\civlU}unpack{\civlU}apply}}
\newcommand{\cmessagepack}{\funsty{\$message{\civlU}pack}}
\newcommand{\cmessagesource}{\funsty{\$message{\civlU}source}}
\newcommand{\cmessagetag}{\funsty{\$message{\civlU}tag}}
\newcommand{\cmessagedest}{\funsty{\$message{\civlU}dest}}
\newcommand{\cmessagesize}{\funsty{\$message{\civlU}size}}
\newcommand{\cmessageunpack}{\funsty{\$message{\civlU}unpack}}
\newcommand{\ccommsize}{\funsty{\$comm{\civlU}size}}
\newcommand{\ccommplace}{\funsty{\$comm{\civlU}place}}
\newcommand{\ccommseek}{\funsty{\$comm{\civlU}seek}}
\newcommand{\ccommprobe}{\funsty{\$comm{\civlU}probe}}
\newcommand{\ccommcreate}{\funsty{\$comm{\civlU}create}}
\newcommand{\ccommdestroy}{\funsty{\$comm{\civlU}destroy}}
\newcommand{\ccommenqueue}{\funsty{\$comm{\civlU}enqueue}}
\newcommand{\ccommdequeue}{\funsty{\$comm{\civlU}dequeue}}
\newcommand{\cgcommcreate}{\funsty{\$gcomm{\civlU}create}}
\newcommand{\cgcommdestroy}{\funsty{\$gcomm{\civlU}destroy}}
\newcommand{\cgcommdup}{\funsty{\$gcomm{\civlU}dup}}
\newcommand{\cgbarriercreate}{\funsty{\$gbarrier{\civlU}create}}
\newcommand{\cbarriercreate}{\funsty{\$barrier{\civlU}create}}
\newcommand{\cbarriercall}{\funsty{\$barrier{\civlU}call}}
\newcommand{\cbarrierenter}{\funsty{\$barrier{\civlU}enter}}
\newcommand{\cbarrierexit}{\funsty{\$barrier{\civlU}exit}}
\newcommand{\cgbarrierdestroy}{\funsty{\$gbarrier{\civlU}destroy}}
\newcommand{\cbarrierdestroy}{\funsty{\$barrier{\civlU}destroy}}
\newcommand{\ccollectcheck}{\funsty{\$collator{\civlU}check}}
\newcommand{\cgcheckercreate}{\funsty{\$gcollator{\civlU}create}}
\newcommand{\cgcheckerdestroy}{\funsty{\$gcollator{\civlU}destroy}}
\newcommand{\ccheckercreate}{\funsty{\$collator{\civlU}create}}
\newcommand{\ccheckerdestroy}{\funsty{\$collator{\civlU}destroy}}
\newcommand{\cpointeradd}{\funsty{\$pointer{\civlU}add}}
\newcommand{\cseqinit}{\funsty{\$seq{\civlU}init}}
\newcommand{\cseqlen}{\funsty{\$seq{\civlU}length}}
\newcommand{\cseqinsert}{\funsty{\$seq{\civlU}insert}}
\newcommand{\cseqrm}{\funsty{\$seq{\civlU}remove}}
\newcommand{\cseqapp}{\funsty{\$seq{\civlU}append}}
\newcommand{\cnexttimecount}{\funsty{\$next{\civlU}time\civlU{}count}}
\newcommand{\celaborate}{\funsty{\$elaborate}}
\newcommand{\cmpisend}{\funsty{\$mpi\civlU{}send}}
\newcommand{\cmpirecv}{\funsty{\$mpi\civlU{}recv}}
\newcommand{\cmpisendrecv}{\funsty{\$mpi\civlU{}sendrecv}}
\newcommand{\csizeofdatatype}{\funsty{sizeofDatatype}}
\newcommand{\cmpicheckbuffer}{\funsty{\$mpi\civlU{}check\civlU{}buffer}}
\newcommand{\cmpicreatecoroutineentry}{\funsty{\$mpi\civlU{}create\civlU{}routine\civlU{}entry}}
\newcommand{\cmpidiffcoroutineentries}{\funsty{\$mpi\civlU{}diff\civlU{}coroutine\civlU{}entries}}
\newcommand{\cmpireduce}{\funsty{\$mpi\civlU{}reduce}}
\newcommand{\cmpicollectivesend}{\funsty{\$mpi\civlU{}collective\civlU{}send}}
\newcommand{\cmpicollectiverecv}{\funsty{\$mpi\civlU{}collective\civlU{}recv}}
\newcommand{\cmpibcast}{\funsty{\$mpi\civlU{}bcast}}
\newcommand{\cmpigather}{\funsty{\$mpi\civlU{}gather}}
\newcommand{\cmpigatherv}{\funsty{\$mpi\civlU{}gatherv}}
\newcommand{\cmpiscatter}{\funsty{\$mpi\civlU{}scatter}}
\newcommand{\cmpiscatterv}{\funsty{\$mpi\civlU{}scatterv}}
\newcommand{\cmpipointeradd}{\funsty{\$mpi\civlU{}pointer\civlU{}add}}
\newcommand{\cmpinewgcomm}{\funsty{\$mpi\civlU{}new\civlU{}gcomm}}
\newcommand{\cmpigetgcomm}{\funsty{\$mpi\civlU{}get\civlU{}gcomm}}
\newcommand{\cmpicommdup}{\funsty{\$mpi\civlU{}comm\civlU{}dup}}
\newcommand{\cmpicommfree}{\funsty{\$mpi\civlU{}comm\civlU{}free}}
\newcommand{\cmpirootscope}{\funsty{\$mpi\civlU{}root\civlU{}scope}}
\newcommand{\cmpiprocscope}{\funsty{\$mpi\civlU{}proc\civlU{}scope}}
\newcommand{\cmpiassertconsistbtype}{\funsty{\$mpi\civlU{}assert\civlU{}consistent\civlU{}basetype}}
\newcommand{\cmpitime}{\funsty{\$mpi\civlU{}time}}
\newcommand{\cmpigcommcreate}{\funsty{\$mpi\civlU{}gcomm\civlU{}create}}
\newcommand{\cmpigcommdestroy}{\funsty{\$mpi\civlU{}gcomm\civlU{}destroy}}
\newcommand{\cmpicommcreate}{\funsty{\$mpi\civlU{}comm\civlU{}create}}
\newcommand{\cmpicommdestroy}{\funsty{\$mpi\civlU{}comm\civlU{}destroy}}
\newcommand{\cmpigcomm}{\funsty{\$mpi\civlU{}gcomm}}
\newcommand{\cmpicomm}{\funsty{\$mpi\civlU{}comm}}

%%% CIVL-C types %%%
\newcommand{\cbarrier}{\typsty{\$barrier}}
\newcommand{\cgbarrier}{\typsty{\$gbarrier}}
\newcommand{\cqueue}{\typsty{\$queue}}
\newcommand{\cbundle}{\typsty{\$bundle}}
\newcommand{\cmessage}{\typsty{\$message}}
\newcommand{\ccomm}{\typsty{\$comm}}
\newcommand{\cgcomm}{\typsty{\$gcomm}}
\newcommand{\ccollectchecker}{\typsty{\$collator}} 
\newcommand{\ccollator}{\typsty{\$collator}}
\newcommand{\cgcollectchecker}{\typsty{\$gcollator}}
\newcommand{\ccollectrecord}{\typsty{\$collator{\civlU}entry}}
\newcommand{\coperation}{\typsty{\$operation}}
\newcommand{\cgcollator}{\typsty{\$gcollator}}
\newcommand{\cmpistate}{\typsty{\$mpi\civlU{}state}}



%%%C keywords%%%
\newcommand{\typedef}{\ccode{typedef}}
\newcommand{\enum}{\ccode{enum}}
\newcommand{\struct}{\ccode{struct}}
\newcommand{\void}{\ccode{void}}
\newcommand{\inttype}{\ccode{int}}
\newcommand{\cchar}{\ccode{char}}
\newcommand{\cdouble}{\ccode{double}}
\newcommand{\creturn}{\ccode{return}}
\newcommand{\cif}{\ccode{if}}
\newcommand{\sizeof}{\ccode{sizeof}}
\newcommand{\bool}{\ccode{sizeof{\civlU}Bool}}
\newcommand{\cconst}{\ccode{const}}
\newcommand{\memset}{\ccode{memset}}
\newcommand{\cmemcpy}{\ccode{memcpy}}



%%%% Mini-language %%%%
\newcommand{\minibarrier}{\texttt{\textcolor{pink}{barrier}}}
\newcommand{\mininprocs}{\texttt{\textcolor{pink}{nprocs}}}
\newcommand{\miniproc}{\texttt{\textcolor{pink}{proc}}}
\newcommand{\minipid}{\texttt{\textcolor{pink}{pid}}}
\newcommand{\minisend}[2]{\texttt{\textcolor{pink}{send} #1 \textcolor{pink}{to} #2}}
\newcommand{\minirecv}[2]{\texttt{\textcolor{pink}{recv} #1 \textcolor{pink}{from} #2}}
\newcommand{\miniwildcard}[1]{\texttt{\textcolor{pink}{any} #1}}
\newcommand{\miniassert}[1]{\texttt{\textcolor{pink}{assert #1}}}
\newcommand{\minireturn}{\texttt{\textcolor{pink}{return}}}
\newcommand{\miniwhile}{\texttt{\textcolor{pink}{while}}}
\newcommand{\miniif}{\texttt{\textcolor{pink}{if}}}
\newcommand{\minielse}{\texttt{\textcolor{pink}{else}}}
%%%% propertes %%%%
%\newcommand{\prop}[1]{\textbf{F\textsf{#1}}}
\newcommand{\prop}[1]{\textsf{#1}}


%%%% variables %%%%
\newcommand{\NP}{\texttt{NP}}

%%%% chapter symbol %%%%
\newcommand{\Chp}{Chapter }

%%%% MINIMP %%%%
\newcommand{\send}[2]{\ccode{send} #1 \ccode{to} #2}
\newcommand{\recv}[2]{\ccode{recv} #1 \ccode{from} #2}
\newcommand{\recvany}[2]{\ccode{recv} #1 \ccode{from any} #2}
%%%%%%%%%%%%%%

%%%% notations %%%%
\newcommand{\enque}[2]{\mymath{#1\texttt{!}#2}}
\newcommand{\deque}[2]{\mymath{#1\texttt{?}#2}}
\newcommand{\lco}{\langle}
\newcommand{\rco}{\rangle}
\newcommand{\cocond}[1]{\lco{}#1\rco{}}
\newcommand{\proc}{\texttt{p}}
\newcommand{\eval}{\texttt{eval}}
\newcommand{\Var}{\texttt{Var}}
\newcommand{\len}{\texttt{len}}
\newcommand{\ttC}{\texttt{c}}
\newcommand{\ttE}{\texttt{e}}
\newcommand{\ttI}{\texttt{i}}
\newcommand{\ttJ}{\texttt{j}}
\newcommand{\ttK}{\texttt{k}}
\newcommand{\ttN}{\texttt{n}}
\newcommand{\model}{\mathcal{M}}
\newcommand{\progseg}[3]{#1{\colon}#2~{#3}}
\newcommand{\progsegs}[5]{#1{\colon}#2~{#3}\colon{}#4~{#5}}
\newcommand{\vocab}{\mathcal{V}}
\newcommand{\corule}{\mathcal{R}}
\newcommand{\mylabel}{\mathcal{L}}
\newcommand{\mytxcmt}[1]{\textcolor{red}{#1}}
\newcommand{\dom}{\textsf{Val}}
\newcommand{\sym}{\textsf{Sym}}
\newcommand{\symexpr}{\exprv_{\dom{}\cup{}\textsf{Sym}}}
\newcommand{\pathcond}{\textsf{pc}}
\newcommand{\mypathcond}{\textsf{PC}}
\newcommand{\myundef}{\textsf{UNDEF}}
\newcommand{\domtmp}{\textsf{Val}}
%\newcommand{\nprocs}[1]{\mathbb{N}^{<#1}}
\newcommand{\nprocs}[1]{[#1]}
\newcommand{\minimp}[0]{\textsc{MiniMP}}
\newcommand{\minispec}[0]{\textsc{MiniSpec}}
\newcommand{\mcalgo}[0]{\textsc{Mc}}
\newcommand{\mcalgodelta}[0]{\textsc{Mc}$^\Delta$}
\newcommand{\emana}[0]{\textsf{emanate}}
\newcommand{\errorpaths}[0]{\leadsto^*_{\textsf{error}}}
\newcommand{\mayInterfere}[0]{\textsf{mayInterfere}}
%%
\newcommand{\var}[0]{\textsf{Var}}
\newcommand{\myprocedure}[0]{\textsf{Procedure}}
\newcommand{\globvar}[0]{\textsf{Global}}
\newcommand{\locvar}[0]{\textsf{locvar}}
\newcommand{\stmt}[0]{\textsf{AStmt}_{\vocab}}
\newcommand{\exprv}[0]{\textsf{Expr}}
\newcommand{\sexprv}[0]{\textsf{SExpr}}
\newcommand{\seventv}[0]{\textsf{SEvent}}
\newcommand{\sabsentv}[0]{\textsf{SAbsent}}
\newcommand{\bexprv}[0]{\textsf{BExpr}}
\newcommand{\pexprv}[0]{\textsf{PExpr}}
\newcommand{\transT}[0]{\textsf{transStmt}}
\newcommand{\myskipstmt}[0]{\textsf{skip}}
\newcommand{\myrettostmt}[2]{\textsf{return }#1\textsf{ to }#2}
\newcommand{\myemptyguard}[0]{\textsf{empty}}
\newcommand{\myallemptyguard}[0]{\textsf{allempty}}
\newcommand{\myframes}[0]{\textsf{Frame}}
\newcommand{\myframe}[0]{\textsf{frame}}
\newcommand{\myprocStates}[0]{\textsf{ProcState}}
\newcommand{\myprocState}[0]{\textsf{procState}}
\newcommand{\myprocGraphFunc}[0]{\textsf{pg}}
\newcommand{\mymem}[0]{\textsf{mem}}
\newcommand{\mygmem}[0]{\textsf{gmem}}
\newcommand{\mystack}[0]{\textsf{stack}}
\newcommand{\mychan}[0]{\textsf{chan}}
\newcommand{\mystate}[0]{\textsf{state}}
\newcommand{\mystates}[0]{\textsf{State}}
\newcommand{\mytop}[0]{\textsf{top}}
\newcommand{\mytoploc}[0]{\textsf{toploc}}
\newcommand{\mynp}[0]{\textsf{np}}
\newcommand{\myhead}[0]{\textsf{head}}
\newcommand{\mytail}[0]{\textsf{tail}}
\newcommand{\myloc}[0]{\textsf{Loc}}
\newcommand{\mynexts}[0]{\textsf{nexts}}
\newcommand{\mysrc}[0]{\textsf{src}}
\newcommand{\mydest}[0]{\textsf{dest}}
\newcommand{\myproc}[0]{\textsf{proc}}
\newcommand{\myact}[0]{\textsf{act}}
\newcommand{\mypathtrans}[0]{\textsf{Tr}}
\newcommand{\mypathstates}[0]{\textsf{St}}
\newcommand{\myabsentpred}[3]{\textsf{no }#1\textsf{ after }#2\textsf{
    until }#3}
\newcommand{\myenter}[0]{\textsf{enter}}
\newcommand{\myexit}[0]{\textsf{exit}}
\newcommand{\myproj}[1]{\textsf{proj}_{#1}}
\newcommand{\mypre}[0]{\textsf{pre}}
\newcommand{\myaeval}[1]{\myeval{#1}^{\textsf{absent}}}
\newcommand{\myseval}[1]{\myeval{#1}^{\textsf{spec}}}
\newcommand{\mypeval}[3]{\textsf{pe}(#1, #2, #3)}
\newcommand{\mypevaltitle}[0]{\textsf{pe}}
%% actions
%% acsls
\newcommand{\acslold}{\ccode{\BSL{}old}}
\newcommand{\acslon}{\ccode{\BSL{}on}}
\newcommand{\acslforall}{\ccode{\BSL{}forall}}
\newcommand{\acslexists}{\ccode{\BSL{}exists}}
\newcommand{\acslresult}{\ccode{\BSL{}result}}
\newcommand{\acslsend}{\ccode{\BSL{}send}}
\newcommand{\acslenter}{\ccode{\BSL{}enter}}
\newcommand{\acslexit}{\ccode{\BSL{}exit}}
\newcommand{\acslabsent}[3]{\ccode{\BSL{}no} #1 \ccode{\BSL{}after} #2
  \ccode{\BSL{}until} #3}
\newcommand{\acslgamma}[3]{\acslabsent{\acslsend{(#1,
      #2)}}{\acslexit{(#1)}}{\acslexit{(#3)}}}
\newcommand{\acslguarantee}[3]{\acslabsent{\acslsend{(#1,
      #2)}}{\acslenter{(#1)}}{\acslenter{(#3)}}}
\newcommand{\acslwaitsfor}[2]{\acslabsent{\acslexit{(#1)}}{\acslenter{(#1)}}{\acslenter{(#2)}}}
%% 
\newcommand{\myactskip}[0]{\textsf{skip}}
\newcommand{\myactassign}[2]{#1\texttt{ = }#2}
\newcommand{\myactret}[1]{\textsf{ret #1}}
\newcommand{\myactretto}[1]{\textsf{assignRetTo} #1}
\newcommand{\myactsend}[2]{\textsf{send(#1, #2)}}
\newcommand{\myactrecv}[2]{\textsf{recv(#1, #2)}}
\newcommand{\myactrefresh}[0]{\textsf{refresh}}
%% end-of-actions
%%
%% #recvs and #sends
\newcommand{\mynsends}[3]{\textsf{nsends}_{#1}(#2, #3)}
\newcommand{\mynrecvs}[3]{\textsf{nrecvs}_{#1}(#2, #3)}
\newcommand{\myinterfere}[2]{\textsf{interfere}_{#1}^{#2}}
\newcommand{\mycspre}[2]{\textsf{preCS}({#1}, {#2})}
\newcommand{\mycspost}[2]{\textsf{postCS}({#1}, {#2})}
\newcommand{\myCoChanPre}[0]{\textsf{preCoChan}}
\newcommand{\myCoChanPost}[0]{\textsf{postCoChan}}
%%
%%
%%
\newcommand{\tri}[0]{\textsf{tri}}
\newcommand{\Tri}[0]{\textsf{Tri}}
\newcommand{\ruleguarantee}{\textsf{guarantees}}
\newcommand{\ruleinfer}[3]{#1\textsf{ and }#2\textsf{ infer }#3}
\newcommand{\myruleinfer}[4]{#1\textsf{ and }#2\textsf{ infer$_{#4}$ } #3}
\newcommand{\nosendsubset}{\textsf{noSend}}
\newcommand{\rulecancels}{\textsf{cancels}}
%%
\newcommand{\mymath}[1]{\mathit{#1}}
\newcommand{\myeval}[1]{[\![\mymath{#1}]\!]}
\newcommand{\coLoc}{\mymath{coLoc}}
\newcommand*{\tran}[2]{\genfrac{}{}{0pt}{}{#1}{#2}}
\newcommand{\param}{\vspace{7mm}}
\newcommand{\tranin}[2]{#1\textbf{\textit{ in }}#2}
\newcommand{\cotriple}{\lco{}\psi,\,\Gamma{}\rco{}~\progseg{l}{C}{l'}~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\cotriplenoloc}{\lco{}\psi,\,\Gamma{}\rco{}~C~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\cotriplearg}[1]{\lco{}\psi,\,\Gamma{}\rco{}~#1~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\cosubtriple}[1]{\lco{}\psi_{#1},\,\Gamma_{#1}\rco{}~C_{#1}~\lco{}\phi_{#1},\,\Upsilon_{#1}\rco{}}
%%%% \mycosubtriple: subscript, pre, post, progseg:
\newcommand{\mycosubtriple}[4]{\lco{}{#2},\,\Gamma_{#1}\rco{}~{#4}~\lco{}{#3},\,\Upsilon_{#1}\rco{}}
%%%%
\newcommand{\cosubtripleloc}[3]{\lco{}\psi_{#1},\,\Gamma_{#1}\rco{}~#2{:}C_{#1}\texttt{;}#3~\lco{}\phi_{#1},\,\Upsilon_{#1}\rco{}}
\newcommand{\cotripleloc}{\lco{}\psi,\,\Gamma{}\rco{}~l{:}C\texttt{;}l'~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\cotripleseq}[2]{\lco{}\psi,\,\Gamma{}\rco{}~C_{#1}\texttt{;}C_{#2}~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\cotripleseqloc}[2]{\lco{}\psi,\,\Gamma{}\rco{}~l{:}C_{#1}\texttt{;}l'{:}C_{#2}~\lco{}\phi,\,\Upsilon{}\rco{}}
\newcommand{\PID}{\texttt{PID}}
\newcommand{\mygamma}[3]{\BSL{}absent(\BSL{}send($#1$, $#2$),
  \BSL{}exit($#1$), \BSL{}exit($#3$))}
\newcommand{\mywaitsfor}[2]{\BSL{}absent(\BSL{}exit($#1$),
  \BSL{}enter($#1$), \BSL{}enter($#2$))}
\newcommand{\myguaranty}[3]{\BSL{}absent(\BSL{}send($#1$, $#2$),
  \BSL{}enter($#1$), \BSL{}enter($#3$))}
\newcommand{\mygammaVal}[4]{absent(send($#1$, $#2$),
  exit$_{#4}$($#1$), exit$_{#4}$($#3$))}
\newcommand{\mywaitsforVal}[4]{absent(exit$_{#4}$($#1$),
  enter$_{#3}$($#1$), enter$_{#3}$($#2$))}
\newcommand{\myguarantyVal}[4]{absent(send($#1$, $#2$),
  enter$_{#4}$($#1$), enter$_{#4}$($#3$))}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\mygammaMPI}[2]{\BSL{}absenceof \BSL{}sendfrom($#1$, $#2$) \BSL{}after
  \BSL{}exit($#1$) \BSL{}until \BSL{}exit}
\newcommand{\mywaitsforMPI}[1]{\BSL{}absenceof \BSL{}exit \BSL{}after
  \BSL{}enter \BSL{}until \BSL{}exit(#1)}
\newcommand{\myguarantyMPI}[3]{\BSL{}absenceof \BSL{}sendto($#1$, $#2$) \BSL{}after
  \BSL{}enter \BSL{}until \BSL{}enter($#3$)}

\newcommand{\mygammaCIVL}[2]{\$absent\U{}sendfrom($#1$, $#2$)}
\newcommand{\mywaitsforCIVL}[1]{\$absent\U{}exit($#1$)}
\newcommand{\myguarantyCIVL}[3]{\$absent\U{}sendto($#1$, $#2$, $#3$)}


\newcommand{\myseqrule}[0]{
  $\frac{
    \cocond{\psi, \Gamma_0}~C_0~\cocond{\delta, \Upsilon_0},\,
    \cocond{\delta, \Gamma_1}~C_1~\cocond{\phi, \Upsilon_1}
  }{
    \cocond{\psi, \Gamma}~C_0\texttt{;}C_1~\cocond{\phi, \Upsilon}
  }$
}

\newcommand{\indepcond}[4]{
  $#1 \vdash{} exit^{#2}_{#3} \preceq{} t_{#3} \preceq{} t_{#4}
  \preceq{} exit^{#2}_{#4}$ }
%%%%%%%%%%%%%%%%%%%%%%%%%% Tool %%%%%%%%%%%%%%%%%%%%
