From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 21 Feb 2016 14:51:47 +0000 (+0100)
Subject: .
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=1b86510d643a935932e6532814f8f89f25c2aa9a;p=mc1516.git

.
---

diff --git a/e2.tex b/e2.tex
new file mode 100644
index 0000000..ad644cf
--- /dev/null
+++ b/e2.tex
@@ -0,0 +1,64 @@
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage[all]{xypic}
+
+\newcommand{\ra}{\rightarrow}
+\newcommand{\un}{\text{ \textsf{U} }}
+\newcommand{\ev}{\lozenge}
+\newcommand{\al}{\square}
+\newcommand{\nx}{\bigcirc}
+
+\everymath{\displaystyle}
+
+\begin{document}
+\begin{enumerate}
+	\item
+		$\xymatrix{
+			& l_0 & l_1 & l_2 & l_3 & l_5 & l_6 & l_7\\
+			l_0\\
+			l_1\\
+			l_2\\
+			l_3\\
+			l_5\\
+			l_6\\
+			l_7
+		}$
+	\item
+		$\al(crit_0\veebar crit_1)$
+	\item 
+		We define:\\
+		$ AP=\bigcup_{i\in N}\{lift_n, door_n,call_n\},
+		N=\{0, 1, 2, 3\}$
+		\begin{enumerate}
+			\item
+				$\bigwedge_{n\in N}\al(door_m\ra lift_n)$
+			\item
+				$\bigwedge_{n\in N}\al(call_n\ra\ev(lift_n\wedge door_n))$
+			\item
+				$\al\ev lift_0$
+			\item
+				$\al(call_3\rightarrow\bigcirc (lift_3\wedge door_3))$
+		\end{enumerate}
+	\item\strut\\
+		$\begin{array}{ll}
+			\varphi_1=\ev\al c & 
+				s_2\ra s_4\overline{\ra s_5}\\
+			\varphi_2=\al\ev c &
+				s_2\ra s_4\overline{\ra s_5}\\
+			\varphi_3=\nx\neg c\rightarrow\nx\nx c &
+				s_2\ra s_4\overline{\ra s_5}\\
+			\varphi_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}\\
+			\varphi_5=a\un\al(b\vee c) &
+				s_1\ra s_4\overline{\ra s_5}\\
+			\varphi_6=(\nx\nx b)\un(b\vee c) &
+				s_2\ra s_4\overline{\ra s_5}
+		\end{array}$
+\end{enumerate}
+\end{document}