1 files changed, 42 insertions, 0 deletions
diff --git a/assignment1.tex b/assignment1.tex
new file mode 100644
index 0000000..7693073
--- /dev/null
+++ b/assignment1.tex
@@ -0,0 +1,42 @@
+\documentclass[10pt,a4paper]{article}
+
+\usepackage{geometry}
+\usepackage[english]{babel}
+
+\usepackage{enumitem}
+\setenumerate[1]{label=\alph*)}
+
+\usepackage{fancyhdr}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+\fancyhead{}
+\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+\pagestyle{fancy}
+
+\usepackage{sv}
+
+\title{Software Verification - assignment 1}
+\author{Camil Staps}
+
+\begin{document}
+
+\maketitle
+\thispagestyle{fancy}
+
+\setcounter{section}{2}
+\section{Expressing the ABP in LTL}
+
+\begin{enumerate}
+    \item $\always(\lnot(A_{S0}\land A_{S1}))$.
+    \item $\always(A_{S0}\lor A_{S1})$.
+    \item $\always\eventually(A_{S0}\lor A_{S1})$.
+    \item $\always(A_{Sb}\then\eventually B_{Sb})$, $b\in\{0,1\}$.
+    \item $\always(A_{Sb}\then\next B_{Rb})$, $b\in\{0,1\}$.
+    \item $\always(B_{R0}\then B_{S0}\until B_{R1})$.
+    \item $\always(A_{S0}\then \lnot A_{S1}\until A_{R0})$.
+    \item Cannot be expressed: there are no atomic propositions defined for `$A$ can send'.
+    \item $\always(A_{Sb}\then(\eventually B_{Rb})\lor(\always\lnot B_{Rb}))$, $b\in\{0,1\}$. However, this is rather silly, since $\always((\eventually p)\lor(\always\lnot p))$ always holds.
+\end{enumerate}
+
+\end{document}
+