Ch1 minor

vehicle-lang · Jul 11, 2023 · 4f8889f · 4f8889f
1 parent aeeed99
commit 4f8889f
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/Slides/Chapter1/Chapter1.pdf b/Slides/Chapter1/Chapter1.pdf
diff --git a/Slides/Chapter1/Chapter1.tex b/Slides/Chapter1/Chapter1.tex
@@ -156,7 +156,7 @@
 \item ... get to practice working with Vehicle 
 \item ... use the famous ACAS Xu benchmark to show Vehicle's work flow --
 from specification to verification
-\item ... try to identify PL problems that are being resolved by Vehicle 
+\item ... identify PL problems (cf Introduction) that are resolved by Vehicle 
 
 \end{itemize}
 
@@ -362,7 +362,7 @@ \section{Vehicle' Syntax}
 
 \pause
 
-\begin{block}{Our first acquaintance with quantifiers!}
+\begin{block}{Our first acquaintance with predicates and quantifiers!}
  One of the main advantages of \textbf{Vehicle} is that it can be used to state and prove specifications that describe the network’s behaviour over an infinite set of values.
 \end{block}
 
@@ -372,7 +372,7 @@ \section{Vehicle' Syntax}
 \begin{frame}[fragile]
 \frametitle{Functions and types}
 
-\begin{block}{Function Composition: Exercise!}
+\begin{block}{Function Composition: Exercise}
 
 Infer	the types of functions `acasXu`  and `normalise`:
 
@@ -590,9 +590,8 @@ \section{Vehicle' Syntax}
 \begin{frame}
 \frametitle{Concluding Exercise}
 
-Which of the four PL problems we covered?
+Which of the four PL problems we addressed?
 
-\pause
 \begin{itemize}
 \item[$I^O$] Interoperability -- properties are not portable between training/counter-example search/ verification.