%\usepackage{amsmath,amssymb,stmaryrd}
\usepackage{graphicx}
\usepackage{url}
\usefonttheme[onlymath]{serif}

\setbeamersize{text margin left=2mm, text margin right=1mm, %
  sidebar width left=0mm, sidebar width right=3mm}
\graphicspath{{../images/}}
\author{Stephen F.\ Siegel}
\institute{Department of Computer and Information Sciences\\University
  of Delaware}
%\newenvironment{pic}[4]{\begin{pgfpictureboxed}{#1}{#2}{#3}{#4}}{\end{pgfpictureboxed}}
\newenvironment{pic}[4]{\begin{pgfpicture}{#1}{#2}{#3}{#4}}{\end{pgfpicture}}

\newcommand{\myurl}[1]{\textcolor{blue}{\url{#1}}}

\newcommand{\foot}[1]{%
  \usefoottemplate{\hspace{0mm}\raisebox{1mm}[0mm][0mm]{%
      \makebox[0pt][l]{\tiny
        \color{blue!50}
        S.F.\ Siegel $\diamond$
        University of Delaware $\diamond$
        #1 \hspace{1mm}
        {\color{black!100}\insertframenumber}}}}}

\newcommand{\code}[1]{\textcolor{blue}{\texttt{#1}}}

\newcommand{\U}{{\ttfamily\symbol{'137}}}
\newcommand{\lb}{\texttt{\char`\{}}
\newcommand{\rb}{\texttt{\char`\}}}
\newcommand{\bs}{\texttt{\char`\\}}
\newcommand{\ra}{\rightarrow}
\renewcommand{\implies}{\Rightarrow}
\renewcommand{\iff}{\Leftrightarrow}
%\renewcommand{\emptyset}{\varphi}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\spin}{\textsc{Spin}}
\newcommand{\mpispin}{\textsc{Mpi-Spin}}
\newcommand{\x}{\mathbf{x}}
\newcommand{\y}{\mathbf{y}}
\newcommand{\mat}[4]{\bigl(\begin{smallmatrix}#1&#2\\#3&#4\end{smallmatrix}\bigr)}

\newcommand{\model}{\mathcal{M}}
\newcommand{\vocab}{\mathcal{V}}
\newcommand{\vars}{\mathcal{X}}
\newcommand{\valof}[1]{\llbracket #1 \rrbracket}
\newcommand{\valofma}[1]{\valof{#1}_{\model}(\alpha)}
\newcommand{\true}{\textbf{T}}
\newcommand{\false}{\textbf{F}}
\newcommand{\satisfies}{\models}
\newcommand{\infers}{\vdash}
\newcommand{\sep}{\hspace{3mm}}
\newcommand{\Vars}{\textsf{Vars}}
\newcommand{\FV}{\textsf{FV}}
\newcommand{\fmap}[1]{\lceil#1\rceil}
\newcommand{\myForm}{\textbf{Form}}
\newcommand{\Prop}{\textbf{Prop}}
\newcommand{\PL}{\textsf{PL}}
\newcommand{\FOL}{\textsf{FOL}}
\newcommand{\BV}{\textsf{BV}}
\newtheorem{proposition}{Proposition}
\newcommand{\attribute}[1]{\par\begin{flushright}\tiny\textcolor{gray}{---\
      #1}\end{flushright}\par}
\newcommand{\pSymbs}{\textsf{pSymbs}}
\newcommand{\NPL}{\mathcal{N}_{\textsf{PL}}}
\newcommand{\Herb}{\mathcal{H}}
\newcommand{\DHerb}{D_\Herb}
\newcommand{\IH}{I_\Herb}
\newcommand{\sorts}{\mathcal{S}}
\newcommand{\bool}{\textsf{bool}}

\newcommand{\theory}{\mathcal{T}}
\newcommand{\aread}{\textit{read}}
\newcommand{\awrite}{\textit{write}}
\newcommand{\sarrow}{\leadsto}

\newenvironment{hoare}{%
  \begin{displaymath}%
    \renewcommand{\arraystretch}{4}%
    \begin{array}[t]{r@{.\hspace{4mm}}l@{\hspace{5mm}}l}%
    }{%
    \end{array}%
  \end{displaymath}%
}

\newcommand{\bigtrip}[3]{%
  {%
    \renewcommand{\arraystretch}{1}%
    \begin{array}[c]{l}%
      {\color{blue}\{#1\}}\\\hspace{5mm}#2\\{\color{blue}\{#3\}}%
    \end{array}%
  }%
}
\newcommand{\ttrip}[3]{%
  {%
    \renewcommand{\arraystretch}{1}%
    \begin{array}[c]{l}%
      {\color{blue}[#1]}\\\hspace{5mm}#2\\{\color{blue}[#3]}%
    \end{array}%
  }%
}
\newcommand{\trip}[3]{%
  {\color{blue}\{#1\}}\: #2\: {\color{blue}\{#3\}}%
}
\newcommand{\assign}{\textit{assign}}
\newcommand{\seq}{\textit{seq}}
\newcommand{\conseq}{\textit{conseq}}
\newcommand{\pwhile}{\textbf{while}}
\newcommand{\pdo}{\textbf{do}}
\newcommand{\rwhile}{\textit{while}}
\newcommand{\pskip}{\textbf{skip}}
\newcommand{\pif}{\textbf{if}}
\newcommand{\pelse}{\textbf{else}}
\newcommand{\pthen}{\textbf{then}}

\newcommand{\Ax}{\text{Ax}}
\newcommand{\I}{\text{I}}
\newcommand{\E}{\text{E}}
\newcommand{\W}{\text{W}}
\newcommand{\RAA}{\text{RAA}}

\newcommand{\B}{\mathbb{B}}

\newcommand{\opstyle}[1]{\textsf{\textcolor{blue}{#1}}}
\newcommand{\TS}{\opstyle{TS}}
\newcommand{\TT}{\opstyle{TT}}
\newcommand{\LT}{\opstyle{LT}}
\newcommand{\LL}{\opstyle{LL}}
\newcommand{\TL}{\opstyle{TL}}
\newcommand{\TE}{\opstyle{TE}}
\newcommand{\ET}{\opstyle{ET}}

\newcommand{\Act}{\opstyle{Act}}
\newcommand{\AP}{\opstyle{AP}}
\newcommand{\ul}{\opstyle{ul}}
\newcommand{\ur}{\opstyle{ur}}
\newcommand{\dl}{\opstyle{dl}}
\newcommand{\dr}{\opstyle{dr}}
\newcommand{\defeq}{\stackrel{\text{def}}{=}}
\newcommand{\Post}{\opstyle{Post}}
\newcommand{\Pre}{\opstyle{Pre}}
\newcommand{\Reach}{\opstyle{Reach}}
\newcommand{\dom}{\opstyle{dom}}
%\newcommand{\true}{\textit{true}}
%\newcommand{\false}{\textit{false}}
\newcommand{\Eval}{\opstyle{Eval}}
\newcommand{\Cond}{\opstyle{Cond}}
\newcommand{\Loc}{\opstyle{Loc}}
\newcommand{\Effect}{\opstyle{Effect}}
\newcommand*{\hra}{\ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow}}
% use \xhookrightarrow{g:\alpha} instead
\newcommand{\xra}[1]{\xrightarrow{#1}}
\newcommand{\xhra}[1]{\xhookrightarrow{#1}}

\newcommand{\PG}{\opstyle{PG}}
\newcommand{\Var}{\opstyle{Var}}
\newcommand{\tpc}{\;|||\;}
\newcommand{\dpc}{\;||\;}
\newcommand{\hand}[1]{\;||_{#1}\;}

\newcommand{\Val}{\opstyle{Val}}

\newcommand{\Chan}{\opstyle{Chan}}
\newcommand{\capacity}{\opstyle{cap}}
\newcommand{\Comm}{\opstyle{Comm}}
\newcommand{\CS}{\opstyle{CS}}

\newcommand{\len}{\opstyle{len}}

\newcommand{\trace}{\opstyle{trace}}
\newcommand{\Traces}{\opstyle{Traces}}
\newcommand{\exinf}{\stackrel{\scriptstyle\infty}{\exists}}
\newcommand{\Set}{\opstyle{Set}}
\newcommand{\Stack}{\opstyle{Stack}}
%\newcommand{\bool}{\opstyle{boolean}}
\newcommand{\State}{\opstyle{State}}

\newcommand{\BadPref}{\opstyle{BadPref}}
\newcommand{\MinBadPref}{\opstyle{MinBadPref}}

\newenvironment{mybox}[1]{%
  \begin{footnotesize}%
    \color{red}%
    \begin{tabular}{@{}|c|@{}}%
      \hline\\[-2.5mm]%
      \begin{minipage}{#1}%
        \color{black}%
      }{%
      \end{minipage}%
      \\[-2.5mm] \\ \hline%
    \end{tabular}%
  \end{footnotesize}%
}

\newenvironment{mycbox}[1]{%
  \begin{center}%
    \begin{mybox}{#1}%
    }{%
    \end{mybox}%
  \end{center}%
}

% CIVL-C keywords

\newcommand{\cckey}{\$}
\newcommand{\cc}[1]{\mbox{\textcolor{blue}{\texttt{\cckey{}#1}}}}
\newcommand{\cproc}{\cc{proc}}
\newcommand{\cself}{\cc{self}}
\newcommand{\cinput}{\cc{input}}
\newcommand{\coutput}{\cc{output}}
\newcommand{\cspawn}{\cc{spawn}}
\newcommand{\cwait}{\cc{wait}}
\newcommand{\cassert}{\cc{assert}}
\newcommand{\ctrue}{\cc{true}}
\newcommand{\cfalse}{\cc{false}}
\newcommand{\cassume}{\cc{assume}}
\newcommand{\cwhen}{\cc{when}}
\newcommand{\cchoose}{\cc{choose}}
\newcommand{\cchooseint}{\cc{choose{\U}int}}
\newcommand{\cinvariant}{\cc{invariant}}
\newcommand{\crequires}{\cc{requires}}
\newcommand{\censures}{\cc{ensures}}
\newcommand{\cresult}{\cc{result}}
\newcommand{\cat}{\texttt{@}}
\newcommand{\ccollective}{\cc{collective}}

\newcommand{\cheap}{\cc{heap}}
\newcommand{\cscope}{\cc{scope}}
\newcommand{\cregion}{\cc{region}}
\newcommand{\cmalloc}{\cc{malloc}}