mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
26 lines
1.0 KiB
TeX
26 lines
1.0 KiB
TeX
\section{TLA$^+$ Specifications}
|
|
|
|
\label{sec:tla}
|
|
%% ============================================================================
|
|
|
|
The TLA$^+$ models live in \texttt{lux/formal/tla/}:
|
|
|
|
\begin{itemize}
|
|
\item \texttt{DAGEVM.tla} + \texttt{MC\_DAGEVM.cfg} — state variables
|
|
$\mathsf{accepted}$, $\mathsf{finalRank}$, $\mathsf{mempool}$;
|
|
actions $\mathsf{Propose}$, $\mathsf{Finalize}$; invariants
|
|
\texttt{TypeOK}, \texttt{Safety}, \texttt{NoDoubleSpend},
|
|
\texttt{Serializability}, \texttt{ConflictsAlongEdges}; property
|
|
\texttt{Liveness}.
|
|
\item \texttt{DAGZChain.tla} + \texttt{MC\_DAGZChain.cfg} — state
|
|
variables $\mathsf{accepted}$, $\mathsf{spent}$, $\mathsf{committed}$,
|
|
$\mathsf{finalRank}$; invariants \texttt{NoDoubleSpend},
|
|
\texttt{AntichainDisjoint}.
|
|
\end{itemize}
|
|
|
|
TLC model-checking runs against small instances
|
|
($|\mathsf{Keys}| = 3, |\mathsf{Vertices}| = 6$) and enumerates the full
|
|
reachable state space in bounded time.
|
|
|
|
%% ============================================================================
|