week 1

3 files changed, 77 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..b7e21a8
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,27 @@
+*.aux
+*.glo
+*.idx
+*.fdb_latexmk
+*.fls
+*.log
+*.toc
+*.ist
+*.acn
+*.acr
+*.alg
+*.bbl
+*.blg
+*.dvi
+*.glg
+*.gls
+*.ilg
+*.ind
+*.lof
+*.lot
+*.maf
+*.mtc
+*.mtc1
+*.out
+*.pdf
+*.swp
+*.synctex.gz
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}
+
diff --git a/sv.sty b/sv.sty
new file mode 100644
index 0000000..ed9dd0a
--- /dev/null
+++ b/sv.sty
@@ -0,0 +1,8 @@
+\RequirePackage{amssymb}
+
+\let\eventually\lozenge
+\let\always\square
+\def\until{\mathop{\mathsf U}}
+\let\next\bigcirc
+
+\let\then\Rightarrow