update

[mc1516.git] / e1.tex

diff --git a/e1.tex b/e1.tex
index 6155f3b..ec5fcd3 100644 (file)
--- a/e1.tex
+++ b/e1.tex
@@ -3,6 +3,7 @@
 \usepackage{a4wide}
 \usepackage{amssymb}
 \usepackage{amsmath}
+\usepackage[all]{xypic}
 
 \newcommand{\ra}{\rightarrow}
 \newcommand{\un}{\text{ \textsf{U} }}
@@ -13,24 +14,43 @@
 \begin{document}
 \begin{enumerate}
        \item
+               $\xymatrix{
+                       \ar[dr]\\
+                               & *+[o][F-]{s_0}\\
+                       *+[o][F-]{nc_1} & & *+[o][F-]{nc_1}
+               }$
        \item
-       \item
+               $\al(crit_0\veebar crit_1)$
+       \item 
+               We define:\\
+               $\displaystyle AP=\bigcup_{i\in N}\{lift_n, door_n,call_n\},
+               N=\{0, 1, 2, 3\}$
+               \begin{enumerate}
+                       \item
+                               $\forall n\in N\al(door_m\ra lift_n)$
+                       \item
+                               $\forall n\in N\al(call_n\ra\ev lift_n)$
+                       \item
+                               $\al\ev lift_0$
+                       \item
+                               $\al call_3\rightarrow\bigcirc lift_3$
+               \end{enumerate}
        \item\strut\\
                $\begin{array}{ll}
-                       \phi_1=\ev\al c & 
+                       \varphi_1=\ev\al c & 
                                s_2\ra s_4\overline{\ra s_5}\\
-                       \phi_2=\al\ev c &
+                       \varphi_2=\al\ev c &
                                s_2\ra s_4\overline{\ra s_5}\\
-                       \phi_3=\nx\neg c\rightarrow\nx\nx c &
+                       \varphi_3=\nx\neg c\rightarrow\nx\nx c &
                                s_2\ra s_4\overline{\ra s_5}\\
-                       \phi_4=\al a & 
+                       \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}\\
-                       \phi_5=a\un\al(b\vee c) &
+                       \varphi_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) &
+                       \varphi_6=(\nx\nx b)\un(b\vee c) &
                                s_2\ra s_4\overline{\ra s_5}
                \end{array}$
 \end{enumerate}