Commit fc2f1980 authored by Patrick Wilde's avatar Patrick Wilde
Browse files

büchie->büchi, true-selfloops in accept states

parent 63ea5576
......@@ -667,17 +667,17 @@ Sichersheitsanforderungen werden teilweise in LTL dargestellt
\end{itemize}
\end{frame}
\begin{frame}{Safety-Monitor LTL->Büchie}
\begin{frame}{Safety-Monitor LTL->Büchi}
\begin{itemize}
\item Umwandeln von negierten Safety-Formeln in Büchie-Automaten mittels \textbf{ltl3ba}
\item Büchie-Automaten werden in ausführbaren C-Code umgewandelt
\item Umwandeln von negierten Safety-Formeln in Büchi-Automaten mittels \textbf{ltl3ba}
\item Büchi-Automaten werden in ausführbaren C-Code umgewandelt
\item Safety-Monitor prüft mit dem Homing-Algorithmus auf Verletzungen der Sicherheitsanforderungen
\item Verletzungen führen zu einem Notstopp des Systems
\end{itemize}
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/automaton_unmarked.png}
\caption{Büchie-Automat für \textbf{F} $(reached\_target \land $\textbf{X}$ \lnot stopped) \lor overspeed$}
\caption{Büchi-Automat für \textbf{F} $(reached\_target \land $\textbf{X}$ \lnot stopped) \lor overspeed$}
\end{figure}
\end{frame}
......
digraph G {
"accept" [shape="doublecircle"]
"init"
"1"
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
digraph G {
"accept" [shape="doublecircle"]
"init" [style="filled"]
"1"
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
digraph G {
"accept" [shape="doublecircle"]
"init" [style="filled"]
"1" [style="filled"]
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
digraph G {
"accept" [shape="doublecircle", style="filled"]
"init" [style="filled"]
"1" [style="filled"]
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
digraph G {
"accept" [shape="doublecircle"]
"init" [style="filled"]
"1"
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
digraph G {
"accept" [shape="doublecircle", style="filled"]
"init" [style="filled"]
"1"
"init" -> "init" [label="true"]
"init" -> "accept" [label="overspeed"]
"init" -> "1" [label="reached_target"]
"1" -> "accept" [label="!stopped"]
"accept" -> "accept" [label="true"]
}
\ No newline at end of file
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