From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 5 Feb 2016 20:59:53 +0000 (+0100)
Subject: e1-4 done
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=638b2a6658d5078e822a5e4c1197a2f31e09d584;p=mc1516.git

e1-4 done
---

638b2a6658d5078e822a5e4c1197a2f31e09d584
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..8164e02
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.log
+*.aux
+*.pdf
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..2915da3
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,16 @@
+LATEX:=pdflatex
+DOCUMENTS:=e1.pdf
+
+.PHONY: all clean clobber
+
+all: $(DOCUMENTS)
+
+%.pdf: %.tex
+	$(LATEX) $(basename $<)
+	$(LATEX) $(basename $<)
+
+clobber:
+	$(RM) -v *.pdf
+
+clean:
+	$(RM) -v *.aux *.log
diff --git a/e1.tex b/e1.tex
new file mode 100644
index 0000000..6155f3b
--- /dev/null
+++ b/e1.tex
@@ -0,0 +1,37 @@
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{amssymb}
+\usepackage{amsmath}
+
+\newcommand{\ra}{\rightarrow}
+\newcommand{\un}{\text{ \textsf{U} }}
+\newcommand{\ev}{\lozenge}
+\newcommand{\al}{\square}
+\newcommand{\nx}{\bigcirc}
+
+\begin{document}
+\begin{enumerate}
+	\item
+	\item
+	\item
+	\item\strut\\
+		$\begin{array}{ll}
+			\phi_1=\ev\al c & 
+				s_2\ra s_4\overline{\ra s_5}\\
+			\phi_2=\al\ev c &
+				s_2\ra s_4\overline{\ra s_5}\\
+			\phi_3=\nx\neg c\rightarrow\nx\nx c &
+				s_2\ra s_4\overline{\ra s_5}\\
+			\phi_4=\al a & 
+				\text{Impossible. $a$ only holds in $s_1$ and in $s_5$.}\\
+			& \text{$s_1$ we can only leave through a state where $\neg a$}\\
+			& \text{$s_5$ we can not reach through $s_1$ without passing
+				through a $\neg a$ state}\\
+			\phi_5=a\un\al(b\vee c) &
+				s_1\ra s_4\overline{\ra s_5}\\
+			\phi_6=(\nx\nx b)\un(b\vee c) &
+				s_2\ra s_4\overline{\ra s_5}
+		\end{array}$
+\end{enumerate}
+\end{document}