Commit 3786b756 authored by Matthias Lange's avatar Matthias Lange
Browse files

Modelchecking mit nuXmv etwas gekürzt

parent bbb37362
......@@ -107,82 +107,6 @@ LTLSPEC G ( y=4 -> X y=6 )
\end{lstlisting}
\end{frame}
\begin{frame}{Variablendefinition}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & nicht belegt & Es befindet sich zurzeit kein Zug auf diesem Streckenelement \\
\hline
1 & belegt & Es befindet sich zurzeit ein Zug auf dem Streckenelement \\
\hline
2 \& 3 & mehrfach belegt & Es befinden sich mehrere Züge auf einem Streckenelement, mindestens 2 Züge sind verunfallt \\
\hline
\end{tabular}
\caption{Belegtheitsstatus von Track Elementen und Weichen}\label{tab:beleg}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & PLUS & Die Weiche ist in PLUS Position und Züge fahren geradeaus weiter \\
\hline
1 & MINUS & Die Weiche ist in MINUS Position und Züge biegen ab \\
\hline
\end{tabular}
\caption{Status einer Weiche}\label{tab:weiche}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{7cm}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & FREE & Die Route ist frei. Sie wird von keinem Zug belegt und kein Zug möchte diese befahren \\
\hline
1 & MARKED & Ein Zug möchte diese Route befahren \\
\hline
2 & CONFLICTED & Eine Route, die mit dieser Route in Konflikt steht, wird gerade befahren \\
\hline
3 & ACTIVE WAIT & Ein Zug möchte diese Route befahren, die Route ist aber noch durch einen Konflikt gesperrt \\
\hline
4 & LOCKED & Die Route wurde für einen Zug gesperrt/freigegeben und wird bald befahren \\
\hline
5 & OCCUPIED & Ein Zug befährt gerade diese Route \\
\hline
6 & DONE & Ein Zug hat die Route wieder verlassen und sie wird in kurzer Zeit wieder freigegeben \\
\hline
\end{tabular}
\caption{Status einer Route}\label{tab:routes}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & Stop & Ein Zug, der auf diesem Track Element steht, darf nicht weiterfahren \\
\hline
1 & Freie Fahrt & Ein Zug, der auf diesem Track Element steht, darf weiterfahren \\
\hline
\end{tabular}
\caption{Status von Marker Board Signalen}\label{tab:mbs}
\end{table}
\end{frame}
\begin{frame}{Cuts}
\begin{figure}[H]
\centering
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment