-
Notifications
You must be signed in to change notification settings - Fork 0
/
tlamath.sty
112 lines (105 loc) · 3.26 KB
/
tlamath.sty
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
% The `tlamath` package provides a compatibility layer atop the TLA+ styles.
%
% To use TLA+ abbreviations in `beamer`, designate the slides as fragile.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{tlamath}
\usepackage{amsmath}
\usepackage{cleveref}
\usepackage{etoolbox}
\usepackage{mdframed}
\usepackage{stmaryrd} % used to define `\dbr`
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Clean up definitions before loading `tlaplus.sty`
% in order to avoid conflicts.
%
% `\proof` is defined in:
% `ieeeconf.cls`
% `amsthm`
% `beamer`
\ifdef{\proof}{
\typeout{WARNING: "proof" already defined, to be deleted}
\let\proof\undefined}{}
\ifdef{\endproof}{
\typeout{WARNING: "endproof" already defined, to be deleted}
\let\endproof\undefined}{}
% `\qed` is defined in:
% `beamer`
\ifdef{\qed}{
\typeout{WARNING: "qed" already defined, to be deleted}
\let\qed\undefined}{}
% `\QED` s defined in:
% `ieeeconf.cls`
\ifdef{\QED}{
\typeout{WARNING: "QED" already defined, to be deleted}
\let\QED\undefined}{}
% `\implies` is defined in:
% `amsthm`
\ifdef{\implies}{
\typeout{WARNING: "implies" already defined, to be deleted}
\let\implies\undefined}{}
% `\E` is defined in Springer's `svmult.cls`
\ifdef{\E}{
\typeout{WARNING: "\E" already defined, to be deleted}
\let\E\undefined}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% safe now to load the TLA+ styles
\usepackage{tlaplus}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% DO NOT USE `hyperref`, because it causes problems with `tla2texplus-book`
% \usepackage[math]{fontspec} % destroys both the math italics of `abbrev`,
% as well as indentation
% \usepackage{hypertlabook} % causes too many errors
% operators
\let\always\undefined
\newcommand{\always}{\Box}
\def\ev{\eventually}
\def\NONE{\textsc{none}}
\newcommand{\tuple}[1]{\langle#1\rangle}
\newcommand{\str}[1]{``#1\text{''}}
\newcommand{\tlastr}[1]{\textsf{``{#1}''}}
\makeatletter
\def\strictarrow{%
\stackrel{\mbox{%
\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle\mathrm{sr}\;\,$}}}{%
-\hspace{-.16em}\triangleright}}
\makeatother
\newcommand{\whilenow}{{-\hspace{-.16em}\triangleright}}
\def\tlaplus{{TLA\textsuperscript{+}}}
\newcommand{\Cl}{\mathcal{C}}
\newcommand{\dbr}[1]{\llbracket #1 \rrbracket}
\DeclareMathOperator{\Ebeh}{\E_{ behavior }}
\DeclareMathOperator{\Abeh}{\A_{ behavior }}
\def\choose{\textsc{choose}}
\newcommand{\ZFNEW}{\textsc{zf new }}
\newcommand{\eqtla}[1]{
\begin{equation}
\begin{aligned}
\nonumber
#1
\end{aligned}
\end{equation}
}
\newcommand{\statearray}[1]{%
\begin{bmatrix}\begin{noj}
#1
\end{noj}\end{bmatrix}}
% definitions for writing algorithms
\def\Def{\textbf{def}\ }
\def\While{\textbf{while}\ }
\def\For{\textbf{for}\ }
\def\If{\textbf{if}\ }
\def\Then{\textbf{then}\ }
\def\Else{\textbf{else}\ }
\def\Return{\textbf{return}\ }
\def\Break{\textbf{break}\ }
\def\Continue{\textbf{continue}\ }
\newcommand{\Procedure}[1]{\textsc{#1}}
\newcommand{\acomment}[1]{\tlacomment{(* #1 *)}}
\newcommand{\algolabel}[1]{\label[algorithm]{#1}}%
\crefname{algorithm}{Algo.}{Algs.}%
% define shading
\usepackage{color}
\definecolor{boxshade}{gray}{0.85}
\setboolean{shading}{true}