Spezifikationen in aktueller TLA^{+} -Syntax:

module Spezifikations-Schema

constants Const_{1}, …, Const_{N} variables Var_{1}, …, Var_{N}

extends Mod_{1}, …, Mod_{N} M =^{Δ} instance Mod with

ModConst ← Const, ModVar ← Var

Definition von Teilformeln, inbesondere für Ausgangszustand und Actions

die eigentliche Spezifikation:

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

module Deklarationen

constants Const_{1}, …, Const_{N} variables Var_{1}, …, Var_{N}

\begin{module}{Deklarationen}
  \begin{nodecls}
    \CONSTANTS Const_1, \dots, Const_N \\
    \VARIABLES Var_1, \dots, Var_N
  \end{nodecls}
\end{module}

module Einbindung anderer Module

extends Mod_{1}, …, Mod_{N} instance Mod with

ModConst ← Const, ModVar ← Var M =^{Δ} instance Mod with

ModConst ← Const, ModVar ← Var

\begin{module}{Einbindung anderer Module}
\begin{nodecls}
\EXTENDS Mod_1, \dots, Mod_N \\
\INSTANCE Mod \WITH \\
___ModConst <- Const, ModVar <- Var \\
M == \INSTANCE Mod \WITH \\
___ModConst <- Const, ModVar <- Var
\end{nodecls}
\end{module}

module Ausgangszustand

Init =^{Δ} ∧ Const_{1} = Wert_{1} ∧ … ∧ Const_{N} = Wert_{N} ∧ Var_{1} = InitWert_{1} ∧ … ∧ Var_{N} = InitWert_{N}

\begin{module}{Ausgangszustand}
\begin{nodecls}
Init == \begin{conj}
Const_1 = Wert_1 \\
\dots \\
Const_N = Wert_N \\
Var_1 = InitWert_1 \\
\dots \\
Var_N = InitWert_N \\
\end{conj} \\
\end{nodecls}
\end{module}

module Actions

Act_{1} =^{Δ} ∧ PreConditions_{1} ∧ PostConditions_{1} ∧ unchanged UnchangedVars_{1}

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

\begin{module}{Actions}
\begin{nodecls}
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{nodecls}
\end{module}

module Die Gesamt-Spezifikation

Vars =^{Δ} ⟨Var_{1}, …, Var_{N} ⟩ SomeAction =^{Δ} \begin{matrix}∨ Act_{1} \\ ∨ … \\ ∨ Act_{N} \end{matrix}

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

\begin{module}{Die Gesamt-Spezifikation}
\begin{nodecls}
Vars == << Var_1, \dots, Var_N >> \\
SomeAction == \begin{disj}
                Act_1 \\
                \dots \\
                Act_N \\
              \end{disj} \\
Spec == \begin{conj}
          Init \\
          [][SomeAction]_{Vars} \\
        \end{conj}
\end{nodecls}
\end{module}

Das Φ-Beispiel aus der Vorlesung:

Init_{Φ} =^{Δ} (x = 0) ∧ (y = 0)

M_{1} =^{Δ} (x′ = x + 1) ∧ (y′ = y)

M_{2} =^{Δ} (y′ = y + 1) ∧ (x′ = x)

M =^{Δ} M_{1} ∨ M_{2}

Φ =^{Δ} Init_{Φ} ∧ □[M]_{⟨x,y ⟩}

module Φ-Beispiel

variables x, y

Init_{Φ} =^{Δ} \begin{matrix}∧ x = 0 \\ ∧ y = 0 \end{matrix}

M_{1} =^{Δ} ∧ x′ = x + 1 ∧ unchanged y

M_{2} =^{Δ} ∧ y′ = y + 1 ∧ unchanged x

M =^{Δ} \begin{matrix}∨ M_{1} \\ ∨ M_{2} \end{matrix}

Φ =^{Δ} \begin{matrix}∧ Init_{Φ} \\ ∧ □[M]_{⟨x,y ⟩} \end{matrix}

\begin{module}{$\Phi$-Beispiel}
\begin{nodecls}
\VARIABLES x, y
\end{nodecls}
\begin{nodecls}
Init_{\Phi} == \begin{conj}
                 x = 0 \\
                 y = 0 \\
               \end{conj} \\
{\cal M}_1 == \begin{conj}
                x' = x + 1 \\
                \UNCHANGED y \\
              \end{conj} \\
{\cal M}_2 == \begin{conj}
                y' = y + 1 \\
                \UNCHANGED x \\
              \end{conj} \\
{\cal M} == \begin{disj}
              {\cal M}_1 \\
              {\cal M}_2 \\
            \end{disj} \\
\Phi == \begin{conj}
          Init_{\Phi} \\
          [][{\cal M}]_{<< x, y >>} \\
        \end{conj}
\end{nodecls}
\end{module}

Das Φ-Beispiel in 2 getrennten Modulen:

module Counter

variable v

Init =^{Δ} v = 0

Step =^{Δ} v′ = v + 1

Spec =^{Δ} ∧ Init ; ∧ □[Step]_{v}

\begin{module}{Counter}
\begin{nodecls}
  \VARIABLE v
\end{nodecls}
\begin{nodecls}
  Init == v = 0 \\
  Step == v' = v + 1 \\
  Spec == \begin{conj}
            Init \\
            [][Step]_v \\
          \end{conj}
\end{nodecls}
\end{module}

module Φ-Beispiel-2

variables x, y C_{1} =^{Δ} instance Counter with v ← x C_{2} =^{Δ} instance Counter with v ← y

Init_{Φ} =^{Δ} ∧ C_{1}.Init ; ∧ C_{2}.Init M_{1} =^{Δ} ∧ C_{1}.Step ∧ unchanged y M_{2} =^{Δ} ∧ C_{2}.Step ∧ unchanged x

M =^{Δ} \begin{matrix}∨ M_{1} \\ ∨ M_{2} \end{matrix}

Φ =^{Δ} \begin{matrix}∧ Init_{Φ} \\ ∧ □[M]_{⟨x,y ⟩} \end{matrix}

\begin{module}{$\Phi$-Beispiel-2}
\begin{nodecls}
\VARIABLES x, y
\end{nodecls}
\begin{nodecls}
C_1 == \INSTANCE Counter \WITH v <- x \\
C_2 == \INSTANCE Counter \WITH v <- y \\
\end{nodecls}
\begin{nodecls}
Init_{\Phi} == \begin{conj}
                 C_1.Init \\
                 C_2.Init \\
               \end{conj} \\
{\cal M}_1 == \begin{conj}
                C_1.Step \\
                \UNCHANGED y \\
              \end{conj} \\
{\cal M}_2 == ...
{\cal M}   == ...
\Phi       == ...
\end{nodecls}
\end{module}