LaTeX Formal Methods Reference¶
The general idea of this reference is to provide a cheatsheet for writing math in LaTeX for someone who’s not particularily sure of either, such as myself. Each table contains a description of some symbol or concept, a rendering of the symbol, a LaTeX source, and, optionally, some odd notes on the concept or rendering. I hope to continue expanding this reference until I run out of Universe to fit it in. This is what I’v got so far though:
Contents
I lean heavily on Chapter 2 of Andrew Harry’s Formal Methods Fact File: VDM and Z for most of the theoretical contents of the tables. I also used Richard Hammack’s Book of Proof for some formulas and descriptions. Detexify and Wikibooks are invaluable reasorces for LaTeX stuff. Also, afor more complete reference of LaTeX symbols try The Comprehensive LaTeX Symbol List by Scott Pakin.
There are two sections related to transactional memory. One lists some of the symbols used by Guerraoui and Kapałka in Principles of Transactional Memory as well as from other work on that subject, which are used fairly commonly to describe various things pertaining to TM histories. The other lists symbols devised by Paweł T. Wojciechowski to render TM histories (or traces) without having to make drawings.
Please note that the symbols here are rendered via JavaScript by
sphinx.ext.mathjax or sphinx.ext.jsmath and may therefore differ from
what LaTeX will render. I am also not able to render some symbols at all
here that will work perfectly fine in LaTeX, in which case I will note so
by the relevant concept.
I provide (automatically generate) the source for the LaTeX for of all concepts, but not for the formulas sometimes found in notes. Their source can be viewed nevertheless by right-clicking them and selecting Show Source from the drop down menu (thanks to Sphinx and MathJax). This works for the second column just as well.
This is a (perpetual) work in progress, so comments etc. are especially welcome.
Variable Names¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Sets | \(A,B,C\) | A,B,C |
upper-case letters |
| Indexed sets | \(A_1, A_2, \ldots, A_n\) | A_1, A_2, \ldots, A_n |
the index may be of any type, not nec. an integer |
| Statements | \(P, Q, R, S\) | P, Q, R, S |
fun fact: rearranged they stand for Senatus Populusque Romanus |
| Statements with variables | \(P(x), Q(x), R(x), S(x)\) | P(x), Q(x), R(x), S(x) |
Set Theory¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Set | \(\{a,b,c\}\) | \{a,b,c\} |
set enumeration |
| Set | \(\{\,x \mid P(x)\,\}\) or \(\{\,x : P(X)\,\}\) | \{\,x \mid P(x)\,\} or \{\,x : P(X)\,\} |
set comprehension (described implicitly with the property \(P\)) aka set-builder notation |
| Infinite set | \(\{1,2,3,\ldots\}\) | \{1,2,3,\ldots\} |
and so on |
| Infinite set | \(\{\ldots,1,2,3,\ldots\}\) | \{\ldots,1,2,3,\ldots\} |
and so on |
| Empty set | \(\varnothing\) or \(\emptyset\) or \(\{\}\) | \varnothing or \emptyset or \{\} |
|
| Powerset | \(\mathbb{P}(S)\) or \(\mathcal{P}(S)\) | \mathbb{P}(S) or \mathcal{P}(S) |
set of all possible subsets of set \(S\), \(|\mathbb{P}(S)| = 2^{|S|}\) |
| Member | \(x \in A\) | x \in A |
|
| Not member | \(x \not\in A\) | x \not\in A |
|
| Subset | \(A \subset B\) or \(A \subseteq B\) | A \subset B or A \subseteq B |
|
| Not subset | \(A \not\subset B\) or \(A \nsubseteq B\) | A \not\subset B or A \nsubseteq B |
|
| Set equality | \(A = B\) | A = B |
\(A \subseteq B \text{ and } B \subseteq A\) |
| Union | \(A \cup B\) | A \cup B |
|
| Intersection | \(A \cap B\) | A \cap B |
|
| Distributed or generalized union | \(\bigcup SS\) | \bigcup SS |
over set of sets |
| Distributed or generalized intersection | \(\bigcap SS\) | \bigcap SS |
over set of sets |
| Relative complement | \(A - B\) or \(A \setminus B\) | A - B or A \setminus B |
\(\{\,x \mid x \in A \text{ and } x \not\in B\,\}\) |
| Absolute complement | \(A + B\) | A + B |
\((A - B) \cup (B - A)\) |
| Disjoint sets | \(A \cap B = \varnothing\) | ||
| Set cardinality (aka size) | \(\mathbf{card}(S)\) or \(|S|\) | \mathbf{card}(S) or |S| |
number of members of \(S\) |
| Boolean set | \(\mathbb{B}\) or \(\{\mathrm{true}, \mathrm{false}\}\) or \(\{tt, ff\}\) or \(\{1, 0\}\) | \mathbb{B} or \{\mathrm{true}, \mathrm{false}\} or \{tt, ff\} or \{1, 0\} |
|
| Natural numbers set | \(\mathbb{N}\) or \(\mathbb{N}^+\) | \mathbb{N} or \mathbb{N}^+ |
\(\mathbb{N}^+ = \mathbb{N} \setminus \{0\}\) |
| Integer numbers set | \(\mathbb{Z}\) | \mathbb{Z} |
|
| Rational numbers set | \(\mathbb{Q}\) | \mathbb{Q} |
\(\frac{a}{b}\), \(a\) - numerator, \(b\) - denominator, \(b \neq 0\) |
| Real numbers set | \(\mathbb{R}\) | \mathbb{R} |
|
| Set of prime numbers | \(\mathbb{N}\) | \mathbb{N} |
|
| Set of irrational numbers | \(\mathbb{I}\) | \mathbb{I} |
|
| Set of complex numbers | \(\mathbb{C}\) | \mathbb{C} |
Cartesian Products¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Ordered Pair | \((a,b)\) | (a,b) |
|
| Triple | \((a,b,c)\) | (a,b,c) |
|
| N-tuple | \((e_1, \ldots, e_n)\) | (e_1, \ldots, e_n) |
|
| Cartesian product | \(A \times B\) | A \times B |
\(\{\,(a,b) \mid a \in A, b \in B\,\}\) |
| Cartesian plane | \(\mathbb{R} \times \mathbb{R}\) | \mathbb{R} \times \mathbb{R} |
\(\{\,(x,y) \mid x,y \in \mathbb{R}\,\}\) |
| Cartesian power | \(A^n\) | A^n |
\(A \times A \times \ldots \times A = \{x_1,x_2,\ldots, x_n | x_1,x_2,\ldots,x_n \in A\}\) |
Types¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| User defined type | \(\mathrm{DEFINEDTYPE} = \{2,4,8\}\) | \mathrm{DEFINEDTYPE} = \{2,4,8\} |
a set defined explicitly, or by set comprehension |
| Product type | \(\mathbb{B} \times \mathbb{B}\) | \mathbb{B} \times \mathbb{B} |
a set of tuples (here, \(\{(tt,tt),(tt,ff),(ff,ff),(ff,tt)\}\)) |
| Two-argument function signature | \(\textrm{func}:\mathbb{R} \times \mathbb{N} \rightarrow \mathbb{N}\) | \textrm{func}:\mathbb{R} \times \mathbb{N} \rightarrow \mathbb{N} |
type of arguments is product type |
| Enumerated type | \(\textrm{signal} = \textrm{RED}~|~\textrm{ORANGE}~|~\textrm{GREEN}\) | \textrm{signal} = \textrm{RED}~|~\textrm{ORANGE}~|~\textrm{GREEN} |
type union of literals |
Mathematical Operators¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Absolute operator | \(\mathbf{abs}\ {-20} = 20\) | \mathbf{abs}\ {-20} = 20 |
unary |
| Floor/integer part operator | \(\mathbf{floor}\ 2.5 = 2\) | \mathbf{floor}\ 2.5 = 2 |
unary |
| Integer division operator | \(5\ \mathbf{div}\ 2 = 2\) | 5\ \mathbf{div}\ 2 = 2 |
binary |
| Remainder operator | \(5\ \mathbf{rem}\ {-2} = 1\) | 5\ \mathbf{rem}\ {-2} = 1 |
binary |
| Modulus operator | \(5\ \mathbf{mod}\ {-2} = -1\) | 5\ \mathbf{mod}\ {-2} = -1 |
binary |
| Equality | \(a = b\) | a = b |
binary |
| Inequality | \(a \neq b\) | a \neq b |
binary |
| Less than | \(a > b\) | a > b |
binary |
| Less than or equal | \(a \ge b\) | a \ge b |
binary |
| More than | \(a < b\) | a < b |
binary |
| More than or equal | \(a \le b\) | a \le b |
binary |
Bags¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Bag | \([\![ a,b,b,c,d ]\!]\) | [\![ a,b,b,c,d ]\!] |
Members can repeat, unordered, also \llbracket and \rrbracket from package stmaryrd look better |
| Count operator | \(\mathbf{count}[\![ a,b,b,c,d ]\!] b = 2\) | \mathbf{count}[\![ a,b,b,c,d ]\!] b = 2 |
How many times element \(b\) occurs in bag |
| Bag cardinality | \(\mathbf{card}(B)\) | \mathbf{card}(B) |
Number of members of \(B\) |
| Bag union (1) | \([\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,b,b,c,c,d ]\!]\) | [\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,b,b,c,c,d ]\!] |
Maximum number an element occurs |
| Bag union (2) | \([\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,a,b,b,b,c,c,c,d,c ]\!]\) | [\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,a,b,b,b,c,c,c,d,c ]\!] |
Sum of elements |
| Bag intersection | \([\![ a,b,b,c,d ]\!] \cap [\![ a,b,c,c,d ]\!] = [\![ a,b,c,d ]\!]\) | [\![ a,b,b,c,d ]\!] \cap [\![ a,b,c,c,d ]\!] = [\![ a,b,c,d ]\!] |
Minimum number an element occurs |
| Bag difference | \([\![ a,b,b,c,d ]\!] - [\![ a,b,c,c,d ]\!] = [\![ b,c ]\!]\) | [\![ a,b,b,c,d ]\!] - [\![ a,b,c,c,d ]\!] = [\![ b,c ]\!] |
Subtract the number of elements in the second bag from the first |
Sequences¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Empty sequence | [] | [] | |
| Sequence (explicit declaration) | \([ a,b,b,d ]\) | [ a,b,b,d ] |
In that order. This is the typical representation. |
| Sequence (implicit declaration) | \([\,e \mid P(e)\,]\) | [\,e \mid P(e)\,] |
Set comprehension (described implicitly with the property \(P\)) |
| Head of a sequence | \(\mathbf{hd}~A\) | \mathbf{hd}~A |
\(\mathbf{hd}~[ a,b,b,c ] = a\) |
| Tail of a sequence | \(\mathbf{tl}~A\) | \mathbf{tl}~A |
\(\mathbf{tl}~[ a,b,b,c ] = [ b,b,c ]\) |
| Length of a sequence | \(\mathbf{len}~A\) | \mathbf{len}~A |
\(\mathbf{len}~[ a,b,b,c ] = 4\) |
| Element selection (by application) | \(A(n)\) | A(n) |
Select the \(n\)-th element of the sequence |
| Indices of a sequence | \(\mathbf{inds}~A\) | \mathbf{inds}~A |
\(\mathbf{inds}~[ a,b,c ] = \{1,2,3\}\) |
| Elements of a sequence | \(\mathbf{elems}~A\) | \mathbf{elems}~A |
\(\mathbf{elems}~[ a,b,b,c ] = \{a,b,c\}\) |
| Sequence concatenation | Symbol varies between notations | ||
| List | \(<a,b,c>\) or \((a,b,c)\) or \(abc\) | <a,b,c> or (a,b,c) or abc |
An alternative notation and naming used by some formal notations |
| Empty list | \(()\) | () |
Formal Logic¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Conjunction (AND) | \(\wedge\) or \(\&\) or \(.\) | \wedge or \& or . |
Alternatively \with from package cmll instead of \&. |
| Alternative (OR) | \(\vee\) or \(|\) or \(+\) | \vee or | or + |
|
| Negation (NOT) | \(\neg\) or \(\sim\) | \neg or \sim |
|
| Implication | \(\rightarrow\) or \(\Rightarrow\) or \(\supset\) | \rightarrow or \Rightarrow or \supset |
\(\text{premise} \rightarrow \text{conclussion}\) |
| Equivalence | \(\leftrightarrow\) or \(\Leftrightarrow\) or \(\equiv\) | \leftrightarrow or \Leftrightarrow or \equiv |
Equivalence Laws¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Commutation (conjunctions) | \((P \wedge Q) \equiv (Q \wedge P)\) | (P \wedge Q) \equiv (Q \wedge P) |
|
| Commutation (alternatives) | \((P \vee Q) \equiv (Q \vee P)\) | (P \vee Q) \equiv (Q \vee P) |
|
| Commutation (equivalences) | \((P \leftrightarrow Q) \equiv (Q \leftrightarrow P)\) | (P \leftrightarrow Q) \equiv (Q \leftrightarrow P) |
|
| Association (conjunctions) | \(P \wedge (Q \wedge R) \equiv (P \wedge Q) \wedge R\) | P \wedge (Q \wedge R) \equiv (P \wedge Q) \wedge R |
|
| Association (alternatives) | \(P \vee (Q \vee R) \equiv (P \vee Q) \vee R\) | P \vee (Q \vee R) \equiv (P \vee Q) \vee R |
|
| Distribution (1) | \(P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R)\) | P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) |
|
| Distribution (2) | \(P \wedge (Q \vee R) \equiv (P \wedge Q) \vee (P \wedge R)\) | P \wedge (Q \vee R) \equiv (P \wedge Q) \vee (P \wedge R) |
|
| De Morgan’s Law (negation of conjunction) | \(\neg(P \wedge Q) \equiv \neg P \vee \neg Q\) | \neg(P \wedge Q) \equiv \neg P \vee \neg Q |
|
| De Morgan’s Law (negation of alternative) | \(\neg(P \vee Q) \equiv \neg P \wedge \neg Q\) | \neg(P \vee Q) \equiv \neg P \wedge \neg Q |
|
| Double Negation | \(\neg\neg P \equiv P\) | \neg\neg P \equiv P |
|
| Excluded Middle | \(P \vee \neg P \equiv tt\) | P \vee \neg P \equiv tt |
|
| Contradiction | \(P \wedge \neg P \equiv ff\) | P \wedge \neg P \equiv ff |
|
| Material Implication | \(P \rightarrow Q \equiv \neg P \vee Q\) | P \rightarrow Q \equiv \neg P \vee Q |
|
| Material Equivalence (1) | \((P \leftrightarrow Q) \equiv (P \rightarrow Q) \wedge (Q \rightarrow P)\) | (P \leftrightarrow Q) \equiv (P \rightarrow Q) \wedge (Q \rightarrow P) |
|
| Material Equivalence (2) | \((P \leftrightarrow Q) \equiv (P \wedge Q) \vee (\neg Q \wedge \neg P)\) | (P \leftrightarrow Q) \equiv (P \wedge Q) \vee (\neg Q \wedge \neg P) |
|
| Exportation | \((P \wedge Q) \rightarrow R \equiv P \rightarrow (Q \rightarrow R)\) | (P \wedge Q) \rightarrow R \equiv P \rightarrow (Q \rightarrow R) |
|
| Or-Simplification | \(P \vee P \equiv P\) | P \vee P \equiv P |
|
| Or-Simplification (true) | \(P \vee tt \equiv tt\) | P \vee tt \equiv tt |
|
| Or-Simplification (false) | \(P \vee ff \equiv P\) | P \vee ff \equiv P |
|
| And-Simplification | \(P \wedge P \equiv P\) | P \wedge P \equiv P |
|
| And-Simplification (true) | \(P \wedge tt \equiv P\) | P \wedge tt \equiv P |
|
| And-Simplification (false) | \(P \wedge ff \equiv ff\) | P \wedge ff \equiv ff |
Logic Forms¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Modus Ponens | \(P \rightarrow Q, P \vdash Q\) | P \rightarrow Q, P \vdash Q |
Andrew Harry uses \uptherefore from MnSymbol |
| Modus Tollens | \(P \rightarrow Q, \neg Q \vdash \neg P\) | P \rightarrow Q, \neg Q \vdash \neg P |
|
| Hypothetical Syllogism | \(P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R\) | P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R |
|
| Constructive Dillema | \(P \rightarrow Q \wedge R \rightarrow S, P \vee R \vdash Q \vee S\) | P \rightarrow Q \wedge R \rightarrow S, P \vee R \vdash Q \vee S |
|
| Destructive Dillema | \(P \rightarrow Q \wedge R \rightarrow S, \neg Q \vee \neg S \vdash \neg P \vee \neg R\) | P \rightarrow Q \wedge R \rightarrow S, \neg Q \vee \neg S \vdash \neg P \vee \neg R |
|
| Conjunction | \(P, Q \vdash P \wedge Q\) | P, Q \vdash P \wedge Q |
|
| Addition | \(P \vdash P \vee Q\) | P \vdash P \vee Q |
Predicate Logic¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Universal qualifier (all) | \(\forall_x\) | \forall_x |
|
| Universal specification | \(\forall_x \bullet P_x\) | \forall_x \bullet P_x |
\(\forall_x \bullet \mathrm{man}(x) \rightarrow \mathrm{mortal}(x)\) |
| Existential qualifier (exists) | \(\exists_x\) | \exists_x |
|
| Existential specification | \(\exists_x \bullet P_x\) | \exists_x \bullet P_x |
\(\exists_x \bullet \mathrm{Socrates}(x) \wedge \mathrm{man}(x)\) |
| Ranging over types (1) | \(\forall_x \in X\) or \(\forall_x : X\) | \forall_x \in X or \forall_x : X |
The former suggests \(X\) is a set, the latter that it is a type |
| Ranging over types (2) | \(\exists_x \in X\) or \(\exists_x : X\) | \exists_x \in X or \exists_x : X |
The former suggests \(X\) is a set, the latter that it is a type |
| Covnersion between qualifiers (1) | \(\forall_x \bullet P_x \equiv \neg\exists_x \bullet \neg P_x\) | \forall_x \bullet P_x \equiv \neg\exists_x \bullet \neg P_x |
Alternatively \(\nexists_x\) |
| Covnersion between qualifiers (2) | \(\neg\forall_x \bullet P_x \equiv \exists_x \bullet \neg P_x\) | \neg\forall_x \bullet P_x \equiv \exists_x \bullet \neg P_x |
|
| Covnersion between qualifiers (3) | \(\neg\forall_x \bullet \neg P_x \equiv \exists_x \bullet P_x\) | \neg\forall_x \bullet \neg P_x \equiv \exists_x \bullet P_x |
|
| Covnersion between qualifiers (4) | \(\forall_x \bullet \neg P_x \equiv \neg\exists_x \bullet P_x\) | \forall_x \bullet \neg P_x \equiv \neg\exists_x \bullet P_x |
Alternatively \(\nexists_x\) |
Relationships and Functions¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| A mapping | \(x \mapsto y\) or \((x, y)\) | x \mapsto y or (x, y) |
|
| Function signiature | \(f:X \rightarrow Y\) | f:X \rightarrow Y |
Mapping from \(X\) (domain) to \(Y\) (co-domain). What is allowed to be in \(X\), \(Y\) is described by the precondition, postcondition. |
| Function definition | \(\mathbf{square}(x) = x^2\ \text{where}\ 1 \le x \le 5\) | \mathbf{square}(x) = x^2\ \text{where}\ 1 \le x \le 5 |
|
| Function defined as co-ordinates | \(\mathbf{square} = \{(1,2), (2,4), (3,9), (4,16), (5,25)\}\) | \mathbf{square} = \{(1,2), (2,4), (3,9), (4,16), (5,25)\} |
The set of right coordinates (here \(\{2,4,9,16,25\}\)) is the range of a function |
| Range | \(\mathrm{range}(f)\) | \mathrm{range}(f) |
\(\mathrm{range}(\{(1,a),(2,b),(3,c)\}) = \{a,b,c\}\) |
| Partial function signiature | \(f:X \nrightarrow Y\) | f:X \nrightarrow Y |
Not all elements from \(X\) are mapped to elements from \(Y\) |
Transactional Memory¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| History | \(H\) | H |
|
| Sequential witness history | \(S\) or \(\hat{S}\) | S or \hat{S} |
|
| Completion | |||
| T-objects | |||
| Transaction | \(T_i\), \(T_j\), \(T_k\) | T_i, T_j, T_k |
|
| Subhistory – transaction | \(H|T_i\) | H|T_i |
A subhistory containing all operations in history \(H\) that are executed within transaction \(T_i\) |
| Subhistory – t-object | \(H|x\) | H|x |
A subhistory containing all operations in history \(H\) that are executed on t-object \(x\) |
| History prefix | \(H = H' \circ H''\) | H = H' \circ H'' |
\(H'\) is a prefix of \(H''\) |
| Commit | |||
| Abort | |||
| Forced abort | |||
| Read | |||
| Write | |||
| Operation | \(\pi\) | \pi |
Notation for Presenting Histories¶
| Concept | Math | LaTeX | Notes |
|---|---|---|---|
| Variables | \(x,y,z\) | x,y,z |
|
| Variable local copy or buffer | \(\underline{x}\) | \underline{x} |
Transaction’s copy of \(x\) |
| Variable versioning | \(\overset{n}{x}\) | \overset{n}{x} |
Variable \(x\) with version \(n\) |
| Transaction identifiers | \(T_i\), \(T_j\), \(T_k\) | T_i, T_j, T_k |
|
| Retried transaction identifiers | \(T_i'\), \(T_i''\), \(T_i'''\) | T_i', T_i'', T_i''' |
Transaction \(T_i\)‘s first, second, etc. retry |
| Read operation | \(r(x)v\) | r(x)v |
Reads value \(v\) from variable \(x\), can be used with specific values, e.g., \(r(x)1\) |
| Write operation | \(w(x)v\) | w(x)v |
Writes value \(v\) to variable \(x\), can be used with specific values, e.g., \(w(x)1\) |
| Read-write operation | \(\{x \xrightarrow{v} y\}\) or \(\{y \xleftarrow{v} x\}\) | \{x \xrightarrow{v} y\} or \{y \xleftarrow{v} x\} |
Shorthand for the sequence \(r(x)v, w(y)v\) |
| Read operation with explicit membership | \(r_i(x)v\) | r_i(x)v |
Read operation executed within \(T_i\) |
| Write operation with explicit membership | \(w_i(x)v\) | w_i(x)v |
Write operation executed within \(T_i\) |
| Operation identifier | \(\mathit{op}, \mathit{op}^r, \mathit{op}^w, \mathit{op}_i\) | \mathit{op}, \mathit{op}^r, \mathit{op}^w, \mathit{op}_i |
Operation, read operation, write operation, operation within \(T_i\) |
| Operation membership | \(\mathit{op} \in T_i\) | \mathit{op} \in T_i |
Shorthand for \(\mathit{op} \in H|T_i\) |
| Transaction start | \([\![\) or \(\llbracket\) | [\![ or \llbracket |
\(\llbracket\) requires the stmaryrd package |
| Transaction commit | \(]\!]\) or \(\rrbracket\) | ]\!] or \rrbracket |
\(\rrbracket\) requires the stmaryrd package |
| Transaction abort | \(\circlearrowright\) or \(\righttoleftarrow\) or \(\curvearrowleft\) | \circlearrowright or \righttoleftarrow or \curvearrowleft |
in amsmath or mathabx or amssymb, respectively |
| Weak transaction start | \([\) | [ |
Used to indicate transactions with relaxed properties, e.g. eventually consistent transactions |
| Weak transaction commit | \(]\) | ] |
Used to indicate transactions with relaxed properties, e.g. eventually consistent transactions |
| Irrevocable operation | \(\mathit{irr}\) or \(\mathit{ir}\) | \mathit{irr} or \mathit{ir} |
|
| Happens-before relation | \(\searrow\) | \searrow |
Often rotated by about 22 degrees to be more visually appealing |
| Point in time | \(\tau\) | \tau |
E.g. transaction \(T_i\) starts at time \(\tau_i\) |
| State at point in time | \(\{ x\!=\!1,y\!=\!2,z\!=\!3 \}\) | \{ x\!=\!1,y\!=\!2,z\!=\!3 \} |
|
| Examples | See examples in our papers, e.g. here or here |