Changeset 1428 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 20, 2011, 3:32:03 PM (9 years ago)

Author:

mulligan

Message:

finished d4.3 report

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (1 diff)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -641 +641 @@
 We list some important functions and axioms in the backend semantics:
 
+\paragraph{From RTLabs/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{make\_initial\_state} & Build an initial state \\
+\texttt{eval\_statement} & Evaluate a single RTLabs statement \\
+\texttt{is\_final} & Check whether a state is in a `final' configuration \\
+\texttt{RTLabs\_exec} & Execute an RTLabs program
+\end{tabular*}
+\end{center}
+
+\paragraph{From RTL/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{rtl\_exec\_extended} & Execute a single step of the RTL language's extended instructions \\
+\texttt{rtl\_fullexec} & Execute an RTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From ERTL/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{ertl\_exec\_extended} & Execute a single step of the ERTL language's extended instructions \\
+\texttt{ertl\_fullexec} & Execute an ERTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From LTL/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{ltl\_fullexec} & Execute an LTL program
+\end{tabular*}
+\end{center}
+
+\paragraph{From LIN/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{lin\_fullexec} & Execute a LIN program
+\end{tabular*}
+\end{center}
+
+\paragraph{From LIN/joint\_LTL\_LIN\_semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{ltl\_lin\_exec\_extended} & Execute a single step of the joint LTL-LIN language's extended instructions \\
+\texttt{ltl\_lin\_fullexec} & Execute a joint LTL-LIN language program
+\end{tabular*}
+\end{center}
+
+\paragraph{From joint/semantics.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{eval\_statement} & Evaluate a single joint language statement \\
+\texttt{is\_final} & Check whether a state is in a `final' configuration \\
+\texttt{joint\_fullexec} & Execute a joint language program
+\end{tabular*}
+\end{center}
+
+\paragraph{From joint/SemanticUtils.ma}
+\begin{center}
+\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
+Title & Description \\
+\hline
+\texttt{graph\_fetch\_statement} & Fetch a statement from a control flow graph
+\end{tabular*}
+\end{center}
+
 \end{document}