\usepackage{llncsdoc}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{listings}
\usepackage{synttree}
\usepackage{alltt}
\usepackage{xcolor}

\usepackage{bm}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{delarray}
\usepackage{stmaryrd}

\newcommand{\TypeRule}[3]{\begin{tabular}{c}
#2\\
\hline
#3\\
\end{tabular}~(\small #1) }
\newcommand{\Infer}[3]{\ensuremath{\begin{array}{c}
#2\\
\hline
#3\\
\end{array}~(\small #1) }}

% for draft
\newcommand{\verify}[1]{\textbf{#1}}

% program typesetting
%\newenvironment{code}{\small\begin{alltt}}{\end{alltt}}

% terms
\newcommand{\Feat}{\ensuremath{F}}
\newcommand{\FeatI}[1]{\ensuremath{\Feat_{#1}}}
\newcommand{\Type}{\ensuremath{T}}
\newcommand{\TypeI}[1]{\ensuremath{\Type_{#1}}}
\newcommand{\Name}{\ensuremath{N}}
\newcommand{\Class}{\ensuremath{C}}
\newcommand{\Arg}{\ensuremath{t}}
\newcommand{\ArgI}[1]{\ensuremath{\Arg_{#1}}}

% relationships
\newcommand{\sub}{\ensuremath{\leq}}
\newcommand{\subL}[1]{\ensuremath{\sub_{#1}}}
\newcommand{\tim}{\ensuremath{\times}}
\newcommand{\is}{\ensuremath{=_{def}}}
\newcommand{\etc}{\ensuremath{\ldots}}
\newcommand{\elt}{\ensuremath{\in}}
\newcommand{\res}{\ensuremath{\rightarrow}}

% specifications, templates ...
%\newcommand{\ith}[2]{\ensuremath{#1_{#2}}}
\newcommand{\magicgreek}{\ensuremath{\Sigma}}
\newcommand{\spec}{\ensuremath{S}}
\newcommand{\temp}{\ensuremath{T}}
\newcommand{\tempi}[1]{\ensuremath{\temp_{#1}}}
\newcommand{\specset}{\ensuremath{\mathfrak{\spec}}}
\newcommand{\tempset}{\ensuremath{\mathfrak{\temp}}}
\newcommand{\specterm}{\ensuremath{s}}
%\newcommand{\spectermi}[1]{\ith{\specterm,#1}}
\newcommand{\spectermi}[1]{\ensuremath{\specterm_{#1}}}
\newcommand{\tempterm}{\ensuremath{t}}
%\newcommand{\temptermi}[1]{\ith{\tempterm,#1}}
\newcommand{\temptermi}[1]{\ensuremath{\tempterm_{#1}}}
\newcommand{\qualspecterm}{\ensuremath{qs}}
%\newcommand{\qualspectermi}[1]{\ith{\qualspecterm,#1}}
\newcommand{\qualspectermi}[1]{\ensuremath{\qualspecterm_{#1}}}
\newcommand{\compspec}{\ensuremath{CS}}
\newcommand{\compspeci}[1]{\ensuremath{\compspec_{#1}}}
\newcommand{\matchrel}{\ensuremath{?}}
\newcommand{\matchrelfor}[1]{\matchrel_{#1}}
\newcommand{\matchmod}{\ensuremath{mm}}
\newcommand{\matchmodfor}[1]{\matchmod_{#1}}
\newcommand{\requal}{\ensuremath{\textbf{required}}}
\newcommand{\noqual}{\ensuremath{\varnothing}}
\newcommand{\qual}{\ensuremath{qualifier}}
\newcommand{\comp}{\ensuremath{C}}
\newcommand{\compi}[1]{\ensuremath{\comp_{#1}}}
\newcommand{\compset}{\ensuremath{\mathfrak{C}}}


\newcommand{\match}[0]{?}
\newcommand{\matchv}[2]{\ensuremath{#1\match_v#2}}
\newcommand{\matchc}[2]{\ensuremath{#1\match_c#2}}
\newcommand{\lookup}[2]{\ensuremath{#1\downarrow#2}}
\newcommand{\translate}[1]{\ensuremath{\llbracket#1\rrbracket}}
\newcommand{\unfoldingtype}{\ensuremath{\rightharpoonup}}
\newcommand{\unfoldingclosure}{\ensuremath{\unfoldingtype*}}
\newcommand{\structstype}[1]{\ensuremath{\prec:_{#1}}}

%\lstset{basicstyle=\scriptsize}
%\lstset{tabsize=2}
%\lstset{showstringspaces=false}
%\lstset{%
%language=Eiffel,%
%framesep=2pt,%
%%basicstyle=\small\itshape, %\ttfamily%\tiny,%
%%keywordstyle=\small\bfseries\upshape,%\color{black}\bfseries
%%columns=fullflexible,%
%}


\newcommand{\name}{\ensuremath{\mathcal{COLOS}}}


\lstset{%
language=Eiffel,%
morekeywords={agent,alias,all,and,as,check,class,%
creation,Current,debug,deferred,do,domain,DOUBLE,else,elseif,end,%
ensure,expanded,export,external,false,feature,from,frozen,if,%
implies,in,indexing,infix,inherit,inspect,invariant,is,%
like,local,loop,NONE,not,obsolete,old,once,or,prefix,%
redefine,rename,require,rescue,Result,retry,select,%
separate,strip,then,true,undefine,unique,until,variant,%
when,xor,attribute,atomic,on_abort},
framesep=2pt,%
literate=  {\%}{$\div$~ }1
           {"}{"}1
           {-->}{$\rightarrow$~ }1
           {confform1}{$(\bullet\:, X)\preceq(\top, X)$.}1
           {confform2}{$(\top, X)\npreceq(\bullet\:, X)$.}1
           {confform3}{$(d1, X)\preceq(\top, X)$.}1
           {confform4}{$(\top, X)\npreceq(d1, X)$.}1
           {confform5}{$(\bullet\:, X)\npreceq(d1, X)$.}1
           {confform6}{$(\bullet\:, X)\preceq(\top, X)$.}1
           {confform7}{$(\top, X)\npreceq(d2, X)$.}1
           {confform8}{$(d1, X)\npreceq(d2, X)$.}1,%
}

\pagestyle{empty}
