X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=92092d285d92fc2e228e37e2839a15acf984d11a;hp=9cdd0d2fc4265123a503a43a8eea598faa9c295d;hb=c497f56e8a7f09c4c328bd7560631d8773b7e676;hpb=7a6489f962acdfe0f42b95fa5ecf73d7e18342eb diff --git a/article.tex b/article.tex index 9cdd0d2..92092d2 100644 --- a/article.tex +++ b/article.tex @@ -50,6 +50,10 @@ \newcommand{\pcy}{\pay{C}} \newcommand{\pcn}{\pan{C}} +\newcommand{\pd}{\pa{D}} +\newcommand{\pdy}{\pay{D}} +\newcommand{\pdn}{\pan{D}} + \newcommand{\pl}{\pa{L}} \newcommand{\ply}{\pay{L}} \newcommand{\pln}{\pan{L}} @@ -65,8 +69,8 @@ %\newcommand{\hasparents}{\underaccent{1}{>}} %\newcommand{\hasparents}{{% % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}} -\newcommand{\hasparents}{>_{\mkern-7.0mu _1}} -\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}} +\newcommand{\hasparents}{>_{\mkern-7.0mu _{1:}}} +\newcommand{\areparents}{<_{\mkern-14.0mu _{1:}\mkern+5.0mu}} \renewcommand{\implies}{\Rightarrow} \renewcommand{\equiv}{\Leftrightarrow} @@ -86,13 +90,44 @@ \newcommand{\patch}{{\mathcal P}} \newcommand{\base}{{\mathcal B}} +\newcommand{\depsreq}{{\mathcal G}} + +\newcommand{\allsrcs}{\set U} \newcommand{\patchof}[1]{\patch ( #1 ) } \newcommand{\baseof}[1]{\base ( #1 ) } +\newcommand{\depsreqof}[1]{\depsreq ( #1 ) } + +\newcommand{\foreign}{\pa F} +\newcommand{\isforeign}[1]{#1 \in \foreign} + +\newcommand{\allpatches}{\Upsilon} +\newcommand{\assign}{\leftarrow} +\newcommand{\iassign}{\leftarrow} +%\newcommand{\assign}{' =} + +\newcommand{\alg}[1]{\text{\bf #1}} +\newcommand{\setmerge}{\alg{merge}} +\newcommand{\setmergeof}[3]{\setmerge\left\langle #1 \;\middle\langle #2 \middle\rangle\; #3 \right\rangle} +%\newcommand{\setmergeof}[3]{\setmerge\left\lgroup #1 \;\middle\lmoustache\; #2 \;\middle\rmoustache\; #3 \right\rgroup} +%\newcommand{\setmergeof}[3]{\setmerge\left\rmoustache #1 \middle\rmoustache #2 \middle\lmoustache #3 \right\lmoustache} +%\newcommand{\setmergeof}[3]{\setmerge\left\lfloor #1 \middle\lfloor #2 \middle\rfloor #3 \right\rfloor} \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} } +\newcommand{\hasdirdep}{\succ_{\mkern-7.0mu _1}} +\newcommand{\hasdep}{\succ} +\newcommand{\isdep}{\prec} +\newcommand{\isdirdep}{\prec_{\mkern-18.0mu _1}{\mkern+10mu}} + +\newcommand{\tip}{ T } +\newcommand{\tipa}[1]{ \tip^{#1} } +\newcommand{\tipcn}{ \tipa \pcn } +\newcommand{\tipcy}{ \tipa \pcy } +\newcommand{\tipdn}{ \tipa \pdn } +\newcommand{\tipdy}{ \tipa \pdy } + %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}} \newcommand{\bigforall}{% \mathop{\mathchoice% @@ -116,6 +151,8 @@ \newcommand{\proofstarts}{{\it Proof:}} \newcommand{\proof}[1]{\proofstarts #1 $\qed$} +\newcommand{\statement}[2]{\[\eqn{ #1 }{ #2 }\]} + \newcommand{\gathbegin}{\begin{gather} \tag*{}} \newcommand{\gathnext}{\\ \tag*{}} @@ -124,6 +161,8 @@ \begin{document} +\chapter{Data model} + \input{notation.tex} \input{invariants.tex} \input{lemmas.tex} @@ -134,5 +173,13 @@ \input{create-tip.tex} \input{anticommit.tex} \input{merge.tex} +\input{pseudomerge.tex} + +\chapter{Update strategy} + +\input{strategy.tex} +\input{ranking.tex} +\input{trav-alg.tex} +\input{trav-proofs.tex} \end{document}