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.
93 lines
2.6 KiB
TeX
93 lines
2.6 KiB
TeX
\section{TLA+ Fundamentals}
|
|
|
|
|
|
\subsection{State Machines}
|
|
|
|
TLA+ models systems as state machines. A state is an assignment of values to variables.
|
|
A specification consists of:
|
|
|
|
\begin{enumerate}[nosep]
|
|
\item \textbf{Variables}: The state components (e.g., \texttt{round}, \texttt{messages},
|
|
\texttt{decisions}).
|
|
\item \textbf{Init}: A predicate describing the initial states.
|
|
\item \textbf{Next}: A predicate describing allowed transitions (an action).
|
|
\item \textbf{Spec}: The overall specification, typically $\texttt{Init} \wedge \Box[\texttt{Next}]_{\texttt{vars}}$.
|
|
\end{enumerate}
|
|
|
|
\subsection{Your First TLA+ Specification}
|
|
|
|
\begin{lstlisting}[language=TLA,caption={A simple counter in TLA+}]
|
|
---- MODULE Counter ----
|
|
EXTENDS Naturals
|
|
|
|
VARIABLES count
|
|
|
|
Init == count = 0
|
|
|
|
Increment == count' = count + 1
|
|
|
|
Decrement == count > 0 /\ count' = count - 1
|
|
|
|
Next == Increment \/ Decrement
|
|
|
|
Spec == Init /\ [][Next]_count
|
|
|
|
\* Property: count is always non-negative
|
|
NonNegative == count >= 0
|
|
|
|
\* TLC checks: is NonNegative an invariant of Spec?
|
|
====
|
|
\end{lstlisting}
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{count'} denotes the value of \texttt{count} in the \emph{next} state.
|
|
\item \texttt{[Next]\_count} means: either \texttt{Next} happens, or \texttt{count}
|
|
stays unchanged (stuttering).
|
|
\item \texttt{NonNegative} is an invariant: a property that must hold in every reachable
|
|
state.
|
|
\end{itemize}
|
|
|
|
\subsection{Temporal Logic}
|
|
|
|
TLA+ uses temporal operators to express properties about sequences of states:
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lll@{}}
|
|
\toprule
|
|
\textbf{Operator} & \textbf{Notation} & \textbf{Meaning} \\
|
|
\midrule
|
|
Always & $\Box P$ & $P$ holds in every state \\
|
|
Eventually & $\Diamond P$ & $P$ holds in some future state \\
|
|
Leads-to & $P \leadsto Q$ & Whenever $P$ holds, $Q$ eventually holds \\
|
|
Stutter & $[A]_v$ & Either action $A$ occurs or $v$ is unchanged \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Temporal operators in TLA+.}
|
|
\end{table}
|
|
|
|
Safety properties have the form $\Box P$ (``something bad never happens'').
|
|
Liveness properties have the form $\Diamond P$ or $P \leadsto Q$ (``something good
|
|
eventually happens'').
|
|
|
|
\subsection{Sets, Functions, and Records}
|
|
|
|
TLA+ has rich built-in data structures:
|
|
|
|
\begin{lstlisting}[language=TLA,caption={TLA+ data structures}]
|
|
\* Sets
|
|
Validators == {"v1", "v2", "v3", "v4"}
|
|
Quorum == {S \in SUBSET Validators : Cardinality(S) >= 3}
|
|
|
|
\* Functions (maps)
|
|
balances == [v \in Validators |-> 0]
|
|
|
|
\* Records
|
|
Message == [type : {"PROPOSE", "VOTE", "COMMIT"},
|
|
round : Nat,
|
|
sender : Validators]
|
|
\end{lstlisting}
|
|
|
|
%% ============================================================
|