TLA^{+} : • ist eine Spezifikationssprache

• basiert auf der temporalen Logik TLA (Temporal Logik of Actions)

• ermöglicht eine modulare Schreibweise von Spezifikationen

• ermöglicht strukturierte formale Beweise • kann mit Hilfe des Pakets tla mit L^{A}TEX

gesetzt werden

module Die Struktur eines Moduls

parameters Deklaration der Variablen und Konstanten

import include

Einbindung anderer Module

predicates Initialisierung der Variablen, ggf. Belegung von Konstanten

definitions Definition von Mengen, Funktionen etc.

actions Definition der Operationen

temporal die eigentliche Spezifikation

module Der Rahmen

\begin{module}{Der Rahmen}
\midbar
\end{module}

module Deklarationen

parameters

Const_{1}, …, Const_{N} : constant var_{1}, …, var_{N} : variable

\begin{module}{Deklarationen}
  \begin{decls}{parameters}
    Const_1, \dots, Const_N : \CONSTANT \\
    var_1, \dots, var_N : \VARIABLE \\
  \end{decls}
\end{module}

module Einbindung anderer Module

import Mod_{1}, …, Mod_{N} include ModName as ModAlias

with varName_{1} ← varAlias_{1} …

varName_{N} ← varAlias_{N}

…

\begin{module}{Einbindung anderer Module}
\begin{decls}{}
\IMPORT\ Mod_1, \dots, Mod_N \\
\INCLUDE\ ModName \AS\ ModAlias \\
  \quad \WITH\ \begin{noj}
                 varName_1 <- varAlias_1 \\
                 \dots \\
                 varName_N <- varAlias_N \\
               \end{noj} \\
\dots
\end{decls}
\end{module}

module Initialisierung

predicates Init =^{Δ} ∧ Const_{1} = ConstValue_{1} ∧ … ∧ Const_{N} = ConstValue_{N} ∧ var_{1} = InitValue_{1} ∧ … ∧ var_{N} = InitValue_{N}

\begin{module}{Initialisierung}
\begin{decls}{predicates}
Init == \begin{conj}
Const_1 = ConstValue_1 \\
\dots \\
Const_N = ConstValue_N \\
var_1 = InitValue_1 \\
\dots \\
var_N = InitValue_N \\
\end{conj} \\
\end{decls}
\end{module}

module Definitionen

definitions

Vars =^{Δ} ⟨var_{1}, …, var_{N} ⟩ …

\begin{module}{Definitionen}
  \begin{decls}{definitions}
    Vars == << var_1, \dots, var_N >> \\
    \dots \\
  \end{decls}
\end{module}

module Operationen

actions Act_{1} =^{Δ} ∧ PreConditions_{1} ∧ PostConditions_{1} ∧ unchanged unchangedVars_{1}

… Act_{N} =^{Δ} ∧ PreConditions_{N} ∧ PostConditions_{N} ∧ unchanged unchangedVars_{N}

\begin{module}{Operationen}
\begin{decls}{actions}
Act_1 == \begin{conj}
PreConditions_1 \\
PostConditions_1 \\
\UNCHANGED unchangedVars_1 \\
\end{conj} \\
\dots \\
Act_N == \begin{conj}
PreConditions_N \\
PostConditions_N \\
\UNCHANGED unchangedVars_N \\
\end{conj} \\
\end{decls}
\end{module}

module Die eigentliche Spezifikation

temporal

SomeAction =^{Δ} \begin{matrix}∨ Act_{1} \\ ∨ … \\ ∨ Act_{N} \end{matrix}

Spec =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

\begin{module}{Die eigentliche Spezifikation}
  \begin{decls}{temporal}
    SomeAction == \begin{disj}
                    Act_1 \\
                    \dots \\
                    Act_N \\
                  \end{disj} \\
    Spec == \begin{conj}
              Init \\
              [][SomeAction]_{Vars} \\
            \end{conj}
  \end{decls}
\end{module}

Abbrevs in TLA^{+} :

=^{Δ}  ==  equals by definition (\deq)

⇒  =>      \Rightarrow
\  :\:     \backslash
□  []      \Box
◇  <>      \Diamond
⇝  ~>      \leadsto
¬  ~       \lnot
⟵  <--     \longleftarrow
←  <-      \leftarrow
⟨  <<      \langle
⟩  >>      \rangle
⟶  -->     \longrightarrow
→  ->      \rightarrow
⊢  |-      \vdash
⊧  |=      \models
↦  |->     \mapsto
≠  #       \neq
∨  \/      \lor
∧  /\␣     \land

/\%  … at the end of a line

“text” "text"  {\rm ``{\sf text}''}

(a TLA^{+} string constant)

_.      \, (a small space)
__Produces a ‘unit’ space
___Produces two ‘unit’ spaces
__..._Produces n ‘unit’ spaces

Aussagen- und Prädikatenlogik:

\TRUE  true
\FALSE  false
/\␣ oder /\%  ∧
\/  ∨
\neg  ¬
=>  ⇒

\equiv  ≡  Äquivalenz (⟺)

\A x : p  ∀ x : p
\E x : p  ∃ x : p
\A x \in S : p ∀ x ∈ S : p
\E x \in S : p ∃ x ∈ S : p

Temporale Logik:

\CHOOSE x : p choose x : p equals some x

satisfying p

p'  p′  p is true in final

state of step

[A]_e  [A]_{e}  A ∨ (e′ = e)
\UNCHANGED e unchanged e e′ = e
[]F  □F  F is always true

Schreibweise von Mengen:

\{e_1,\dots,e_n\} {e_{1}, . . . , e_{n}}
\{x \in S : p\}  {x ∈ S : p}
\{e : x \in S\}  {e : x ∈ S}

… Tupeln:

<<e_1,\dots,e_n>> ⟨e_{1}, …, e_{n} ⟩  n-Tupel
e[i] e[i] i-te Komponente
S_1 \X\dots\X S_n S_{1} × … × S_{n} Produktmenge

… Funktionen:

f[e]  f [e]  Funktions-Anwendung
\DOMAIN f  Domain f  Definitionsmenge
[x \in S |-> e] [x ∈ S ↦ e] Funktions-Definition
[S -> T]  [S → T ]  Menge von Funktionen

… und Records:

e.h  e.h  Record-Komponente
[h_{1} ↦ e_{1}, …, h_{n} ↦ e_{n}] Record-Definition

[h_1 |-> e_1, \dots, h_n |-> e_n]

{[h_{1} : S_{1}, …, h_{n} : S_{n}]} Menge von Records

{[h_1 : S_1, \dots, h_n : S_n]}

Bedingte Ausdrücke:

if p then e_{1}
else e_{2}

\IF p \THEN e_1 \ELSE e_2 \FI

case \begin{matrix}p_{1} → e_{1} \\ … \\ p_{n} → e_{n} \end{matrix}

\CASE \begin{noj}
        p_1 -> e_1 \\
        \dots \\
        p_n -> e_n \\
      \end{noj}

Lokale Definition von x_{1}, …, x_{n}:

let x_{1} =^{Δ} e_{1} ; …; x_{n} =^{Δ} e_{n}

in e

\LET x_1 == e_1 \\
  \dots \\
  x_n == e_n
\IN e \NI