\documentclass[a4paper]{slides}
\usepackage{tla,german,latexsym}

\addtolength{\topmargin}{-20mm}
\addtolength{\textheight}{20mm}

\begin{document}

\begin{slide}
\setlength{\parskip}{0.1\parskip}

\textbf{Spezifikationen in aktueller TLA$^+$-Syntax:} \\

\begin{module}{Spezifikations-Schema}
  \begin{nodecls}
    \CONSTANTS Const_1, \dots, Const_N \\
    \VARIABLES Var_1, \dots, Var_N
  \end{nodecls}
\midbar
  \begin{nodecls}
    \EXTENDS Mod_1, \dots, Mod_N \\
    M == \INSTANCE Mod \WITH \\
    ___ModConst <- Const, ModVar <- Var
  \end{nodecls}
\midbar
  Definition von Teilformeln, inbesondere \\
  f"ur Ausgangszustand und Actions \\
\midbar
  die eigentliche Spezifikation:
  \begin{nodecls}
    Spec == \begin{conj} 
      Init \\
      [][SomeAction]_{Vars} \\
    \end{conj}
  \end{nodecls}
\end{module}

\end{slide}


\begin{slide}

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

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

\end{slide}


\begin{slide}

\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}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}
\setlength{\parskip}{0.1\parskip}

\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}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}
\setlength{\parskip}{0.1\parskip}

\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}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}

\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}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}

\textbf{Das $\Phi$-Beispiel aus der Vorlesung:}

$
Init_{\Phi} == (x = 0)      /\ (y = 0)    \\
{\cal M}_1  == (x' = x + 1) /\ (y' = y)   \\
{\cal M}_2  == (y' = y + 1) /\ (x' = x)   \\
{\cal M}    == {\cal M}_1   \/ {\cal M}_2 \\
\Phi        == Init_{\Phi}  /\ [][{\cal M}]_{<< x, y >>}
$

\vfill

\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}

\end{slide}


\begin{slide}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}

\textbf{Das $\Phi$-Beispiel in 2 getrennten Modulen:}

\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}

\vfill

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}


\begin{slide}

\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 == \begin{conj}
                    C_2.Step \\
                    \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}

\end{slide}


\begin{slide}

\begin{verbatim}
\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}
\end{verbatim}

\end{slide}

\end{document}
