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

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

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

\textbf{TLA$^+$:}

\begin{itemize}
\item ist eine Spezifikationssprache
\item basiert auf der temporalen Logik TLA \\
  (Temporal Logik of Actions)
\item erm"oglicht eine modulare Schreibweise von Spezifikationen
\item erm"oglicht strukturierte formale Beweise
\item kann mit Hilfe des Pakets \texttt{tla} mit \LaTeX\ gesetzt werden
\end{itemize}

\end{slide}


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

\begin{module}{Die Struktur eines Moduls}
  \begin{decls}{parameters}
    $Deklaration der Variablen und Konstanten$
  \end{decls}
\midbar
  \IMPORT \\
  \INCLUDE \\
  \quad Einbindung anderer Module
\midbar 
  \begin{decls}{predicates}
    $Initialisierung der Variablen,$ \\
    $ggf. Belegung von Konstanten$
  \end{decls}
\midbar
  \begin{decls}{definitions}
    $Definition von Mengen, Funktionen etc.$
  \end{decls}
\midbar
  \begin{decls}{actions}
    $Definition der Operationen$
  \end{decls}
\midbar
  \begin{decls}{temporal}
    $die eigentliche Spezifikation$
  \end{decls}
\end{module}

\end{slide}


\begin{slide}

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

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

\end{slide}


\begin{slide}

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

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

\end{slide}


\begin{slide}

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

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

\end{slide}


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

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

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

\end{slide}


\begin{slide}

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

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

\end{slide}


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

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

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

\end{slide}


\begin{slide}

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

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

\end{slide}


\begin{slide}

\textbf{Abbrevs in TLA$^+$:}

\begin{tabular}{lll}
$==$     & \verb$==$     & equals by definition (\verb$\deq$) \\
$=>$     & \verb$=>$     & \verb$\Rightarrow$ \\
$:\:$    & \verb$:\:$    & \verb$\backslash$ \\
$[]$     & \verb$[]$     & \verb$\Box$ \\
$<>$     & \verb$<>$     & \verb$\Diamond$ \\
$~>$     & \verb$~>$     & \verb$\leadsto$ \\
$~$      & \verb$~$      & \verb$\lnot$ \\
$<--$    & \verb$<--$    & \verb$\longleftarrow$ \\
$<-$     & \verb$<-$     & \verb$\leftarrow$ \\
$<<$     & \verb$<<$     & \verb$\langle$ \\
$>>$     & \verb$>>$     & \verb$\rangle$ \\
$-->$    & \verb$-->$    & \verb$\longrightarrow$ \\
$->$     & \verb$->$     & \verb$\rightarrow$ \\
$|-$     & \verb$|-$     & \verb$\vdash$ \\
$|=$     & \verb$|=$     & \verb$\models$ \\
$|->$    & \verb$|->$    & \verb$\mapsto$ \\
$#$      & \verb$#$      & \verb$\neq$ \\
$\/$     & \verb$\/$     & \verb$\lor$ \\
$/\ $    & \verb*$/\ $   & \verb$\land$ \\
         & \verb$/\%$    & \dots at the end of a line \\
$"text"$ & \verb$"text"$ & \verb"{\rm ``{\sf text}''}" \\
         &               & (a TLA$^+$ string constant) \\
         & \verb$_.$     & \verb$\,$ (a small space)\\
         & \verb$__$     &  Produces a `unit' space \\
         & \verb$___$    &  Produces two `unit' spaces \\
         & \verb$__..._$ &  Produces n `unit' spaces \\
\end{tabular}

\end{slide}


\begin{slide}

\textbf{Aussagen- und Pr"adikatenlogik:}

\begin{tabular}{lll}
\verb$\TRUE$          & $\TRUE$          & \\
\verb$\FALSE$         & $\FALSE$         & \\
\verb*$/\ $ {\small oder} \verb$/\%$     & $/\ $ & \\
\verb$\/$             & $\/$             & \\
\verb$\neg$           & $\neg$           & \\
\verb$=>$             & $=>$             & \\
\verb$\equiv$         & $\equiv$         &
  \small "Aquivalenz ($\Longleftrightarrow$) \\
\verb$\A x : p$       & $\A x : p$       & \\
\verb$\E x : p$       & $\E x : p$       & \\
\verb$\A x \in S : p$ & $\A x \in S : p$ & \\
\verb$\E x \in S : p$ & $\E x \in S : p$ & \\
\end{tabular}

\textbf{Temporale Logik:}

\begin{tabular}{lll}
\verb$\CHOOSE x : p$  & $\CHOOSE x : p $ & \small equals some $x$ \\
                      &                  & \small \quad satisfying $p$ \\
\verb$p'$             & $p'$             & \small $p$ is true in final\\
                      &                  & \small \quad state of step \\
\verb$[A]_e$          & $[A]_e$          & \small $A \/ (e'=e)$ \\
\verb$\UNCHANGED e$   & $\UNCHANGED e$   & \small $e'=e$ \\
\verb$[]F$            & $[]F$            & \small $F$ is always true \\
\end{tabular}

\end{slide}


\begin{slide}

\textbf{Schreibweise von Mengen:}

\begin{tabular}{lll}
\verb$\{e_1,\dots,e_n\}$ & $\{e_1,\dots,e_n\}$ & \\
\verb$\{x \in S : p\}$   & $\{x \in S : p\}$   & \\
\verb$\{e : x \in S\}$   & $\{e : x \in S\}$   & \\
\end{tabular}

\textbf{\dots Tupeln:}

\begin{tabular}{lll}
\verb$<<e_1,\dots,e_n>>$ & $<<e_1,\dots,e_n>>$ & \small $n$-Tupel \\
\verb$e[i]$              & $e[i]$      & \small $i$-te Komponente \\
\verb$S_1 \X\dots\X S_n$ & $S_1 \X\dots\X S_n$ & \small Produktmenge \\
\end{tabular}

\textbf{\dots Funktionen:}

\begin{tabular}{lll}
\verb$f[e]$              & $f[e]$      & \small Funktions-Anwendung \\
\verb$\DOMAIN f$         & $\DOMAIN f$ & \small Definitionsmenge \\ 
\verb$[x \in S |-> e]$   & $[x \in S |-> e]$ & \small Funktions-Definition \\ 
\verb$[S -> T]$          & $[S -> T]$  & \small Menge von Funktionen \\ 
\end{tabular}

\textbf{\dots und Records:}

\begin{tabular}{lcl}
\verb$e.h$               & $e.h$       & \small Record-Komponente \\[1em]
\multicolumn{2}{l}{$[h_1 \mapsto e_1, \dots, h_n \mapsto e_n]$} &
  \small Record-Definition \\
\multicolumn{3}{l}{\texttt{%
  [h\char"5F 1 |-> e\char"5F 1, \char"5C dots,
   h\char"5F n |-> e\char"5F n] }} \\[1em]
\multicolumn{2}{l}{$\{[h_1 : S_1,\dots,h_n : S_n]\}$} &
  \small Menge von Records \\
\multicolumn{3}{l}{\texttt{%
  \char"7B [h\char"5F 1 : S\char"5F 1, \char"5C dots,
            h\char"5F n : S\char"5F n]\char"7D }} \\
\end{tabular}

\end{slide}


\begin{slide}

\textbf{Bedingte Ausdr"ucke:}

\begin{minipage}[t]{0.5\textwidth}
$
\IF p
  \THEN e_1
  \ELSE e_2
\FI
$
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\begin{verbatim}
\IF p
  \THEN e_1
  \ELSE e_2
\FI
\end{verbatim}
\end{minipage}

\begin{minipage}[t]{0.5\textwidth}
\CASE $ \begin{noj}
        p_1 -> e_1 \\
        \dots \\
        p_n -> e_n \\
      \end{noj} $
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\begin{verbatim}
\CASE \begin{noj}
        p_1 -> e_1 \\
        \dots \\
        p_n -> e_n \\
      \end{noj}
\end{verbatim}
\end{minipage}

\textbf{Lokale Definition von $x_1$, \dots, $x_n$:}

\begin{minipage}[t]{0.5\textwidth}
$
\LET x_1 == e_1 \\
  \dots \\
  x_n == e_n 
\IN e \NI
$
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\begin{verbatim}
\LET x_1 == e_1 \\
  \dots \\
  x_n == e_n 
\IN e \NI
\end{verbatim}
\end{minipage}

\end{slide}
\end{document}