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.
30 lines
984 B
TeX
30 lines
984 B
TeX
\section{Practical Guide: Your First TLA+ Specification}
|
|
|
|
|
|
\subsection{Installation}
|
|
|
|
\begin{lstlisting}[language=bash,caption={Installing TLA+ tools}]
|
|
# TLA+ Toolbox (IDE with TLC built in)
|
|
# Download from https://lamport.azurewebsites.net/tla/toolbox.html
|
|
|
|
# Or use the VS Code extension
|
|
code --install-extension alygin.vscode-tlaplus
|
|
|
|
# Command-line TLC
|
|
java -jar tla2tools.jar -workers auto MySpec.tla
|
|
\end{lstlisting}
|
|
|
|
\subsection{Workflow}
|
|
|
|
\begin{enumerate}
|
|
\item Write the specification in TLA+.
|
|
\item Define safety invariants (properties that must always hold).
|
|
\item Define liveness properties (properties that must eventually hold).
|
|
\item Run TLC with small parameters.
|
|
\item If TLC finds a violation, study the trace and fix the specification (or the protocol).
|
|
\item Gradually increase parameters until confident.
|
|
\item Convert key TLC traces into implementation-level tests.
|
|
\end{enumerate}
|
|
|
|
%% ============================================================
|