1f3afde500
A .DS_Store A Presentations/.DS_Store A Presentations/20251215-Emerson-Pres/.DS_Store A Presentations/20251215-Emerson-Pres/ERLM_SABO_DRAFT_PRES.pdf A Presentations/20251215-Emerson-Pres/ERLM_SABO_FINAL_PRES.pdf A Presentations/20251215-Emerson-Pres/actual-presentation-outline.md A Presentations/20251215-Emerson-Pres/bouncing_ball_hybrid.py A Presentations/20251215-Emerson-Pres/images/.DS_Store
41 lines
1.5 KiB
TeX
41 lines
1.5 KiB
TeX
% Thrust 1: Procedures to Logic
|
|
\begin{frame}{Thrust 1: NASA's FRET tool translates procedures into unambiguous logic}
|
|
|
|
\begin{center}
|
|
\begin{tikzpicture}[node distance=2cm, auto]
|
|
\tikzstyle{box} = [rectangle, rounded corners, minimum width=7cm, minimum height=1.2cm, text centered, draw=black, font=\small]
|
|
|
|
\node[box, fill=yellow!20] (nl) {
|
|
Natural Language (Procedure)
|
|
};
|
|
|
|
\node[box, fill=green!20, below=of nl] (tl) {
|
|
Temporal Logic Formula
|
|
};
|
|
|
|
\draw[->, >=stealth, very thick] (nl) -- node[right] {FRET} (tl);
|
|
\end{tikzpicture}
|
|
\end{center}
|
|
|
|
\vspace{0.5cm}
|
|
|
|
\begin{center}
|
|
\begin{tikzpicture}
|
|
\draw[thick, fill=gray!20] (0,0) rectangle (12,3.5);
|
|
\node[align=center, text width=10cm] at (6,1.75) {
|
|
\textbf{FIGURE: FRET Interface Screenshot/Mockup}\\[0.2cm]
|
|
Show FRETish structured input:\\
|
|
[Scope] [Condition] [Component] SHALL [Timing] [Response]\\[0.2cm]
|
|
Example with actual SCRAM requirement\\
|
|
Show realizability checking finding conflicts
|
|
};
|
|
\end{tikzpicture}
|
|
\end{center}
|
|
|
|
\note[item]{The Challenge: Natural language is ambiguous; machines need precise specifications}
|
|
\note[item]{Example Translation: Natural language procedure becomes temporal logic formula}
|
|
\note[item]{FRETish Structure: 6 components eliminate ambiguity}
|
|
\note[item]{Realizability Checking catches errors before implementation}
|
|
\note[item]{Output: Unambiguous temporal logic ready for synthesis}
|
|
\end{frame}
|