Commit 756629cf authored by Felix Brüning's avatar Felix Brüning
Browse files

FDR4 kapitel verbessert

parent c3853daa
......@@ -191,21 +191,102 @@ assert S0 [T= M0
\end{frame}
\begin{frame}[fragile]{Modellierung eines Track-Elements}
\begin{figure}[H]
\centering
\includegraphics[width=0.35\textwidth]{STM_TrackElement}
\caption{Zustandsautomat eines Track-Elementes}
\label{FSMte}
\end{figure}
\begin{lstlisting}label={teinitleftstate}]
TRACK_ELEMENT(id, s0, s1) =
rail.s0 -> occupied.id -> TRAIN_FROM_LEFT(id, s0, s1)
[]
rail.s1 -> occupied.id -> TRAIN_FROM_RIGHT(id, s0, s1)
[]
free.id -> TRACK_ELEMENT(id, s0, s1)
TRAIN_FROM_LEFT(id, s0, s1) =
rail.s1 -> TRACK_ELEMENT(id, s0, s1) -- drive through
[]
rail.s0 -> crash.id -> STOP
[]
release.id -> free.id -> TRACK_ELEMENT(id, s0, s1)
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]{CSP-Code einer Weiche unvst.}
\begin{lstlisting}[label={markedlockedstate}]
MARKED_P(id, s0, s1, s2) =
set.id.str -> P_LOCKED_STR(id, s0, s1, s2)
\begin{figure}[H]
\centering
\includegraphics[width=0.9\textwidth]{STM_Point}
\caption{Zustandsautomaten einer Weiche}
\label{FSMpoint}
\end{figure}
\begin{lstlisting}[label={markedlockedstate}]
MARKED_P(id, s0, s1, s2) =
set.id.str -> P_LOCKED_STR(id, s0, s1, s2)
[]
set.id.crss -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s1, s2} @ rail.x -> crash.id -> STOP)
[]
reqsec.id -> derailing.id -> STOP
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]{Sperr-Zustände einer Weiche}
\begin{lstlisting}
P_LOCKED_STR(id, s0, s1, s2) =
rail.s2 -> P_LOCKED_STR_OCC_FROM_RIGHT(id, s0, s1, s2)
[]
rail.s0 -> P_LOCKED_STR_OCC_FROM_LEFT(id, s0, s1, s2)
[]
set.id.crss -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s1, s2} @ rail.x -> crash.id -> STOP)
rail.s1 -> derailing.id -> STOP
[]
release.id -> POINT(id, s0, s1, s2)
[]
reqsec.id -> derailing.id -> STOP
[]
set.id.str -> derailing.id -> STOP
[]
set.id.crss -> derailing.id -> STOP
...
P_LOCKED_CRSS_OCC_FROM_LEFT(id, s0, s1, s2) =
rail.s1 -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s2} @ rail.x -> crash.id -> STOP)
[]
reqsec.id -> derailing.id -> STOP
[]
set.id.str -> derailing.id -> STOP
[]
set.id.crss -> derailing.id -> STOP
\end{lstlisting}
\end{frame}
P_LOCKED_STR(id, s0, s1, s2) =
rail.s2 -> P_LOCKED_STR_OCC_FROM_RIGHT(id, s0, s1, s2)
[]
rail.s0 -> P_LOCKED_STR_OCC_FROM_LEFT(id, s0, s1, s2)
\begin{frame}[fragile]{Kleines Gleisnetz}
\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{mil-gleisnetz-klein}
\caption{Kleines Gleisnetz}
\label{klgleisnetz}
\end{figure}
\begin{lstlisting}[caption={Synchronisation der Streckenabschnitte}, label={sync_small_netw}]
NETWORK = (( ((POINT(0,7,1,2) [|{rail.1}|] TRACK_ELEMENT(1,1,3))
[|{rail.2}|] TRACK_ELEMENT(2,2,4))
[|{ rail.3, rail.4 }|]
((POINT(5,9,5,6)
[|{rail.5}|] TRACK_ELEMENT(3,3,5))
[|{rail.6}|] TRACK_ELEMENT(4,4,6)) )
[|{rail.7, rail.9}|] TRACK_ELEMENT(6,7,9))
\end{lstlisting}
\end{frame}
......
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