up

[mc1516.git] / e2.tex

diff --git a/e2.tex b/e2.tex
index ad644cf..bae921e 100644 (file)
--- a/e2.tex
+++ b/e2.tex
@@ -13,52 +13,59 @@
 
 \everymath{\displaystyle}
 
+\author{Mart Lubbers}
+\date{\today}
+\title{Model Checking Excercises 2}
+
 \begin{document}
+\maketitle
 \begin{enumerate}
+       \item\strut\\
+               \begin{tabular}{ll}
+                       $TS\nvDash\varphi_1$ & $s_1\ra \overline{s_3\ra s_4}$\\
+                       $TS\vDash\varphi_2$ & Yes, all loops go via $s_2,s_3$ or $s_5$
+                       where $c$ holds.\\
+                       $TS\vDash\varphi_3$ & Yes, $\nx\neg c$ is only true when the next
+                       state is $s_4$.\\
+                       & From $s_4$ you can only go to a state where $c$ holds.\\
+                       $TS\nvDash\varphi_4$ & $s_2\ra\ldots$\\
+                       $TS\vDash\varphi_5$ & Yes, starting in $s_1$ $b\vee c$ holds after
+                       the first transition\\
+                       & Starting in $s_2$ $b\vee c$ holds immediatly.\\
+                       $TS\vDash\varphi_6$ & $s_1\ra\overline{s_4\ra s_2}$
+               \end{tabular}
        \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)$
+               \begin{equation}
+                       \xymatrix{
+                               \ar[r] &
+                               *+[F]{s_0}\ar@/^/[r]^{\neg a}\ar@(d,l)^{a} &
+                               *+[F]{s_1}\ar@/^/[l]^{\neg b\wedge a}
+                                       \ar@(d,r)_{\neg b\wedge \neg a}
+                                       \ar[r]^{b} &
+                               *+[Fo]{s_2}\ar@(d,r)_{true}
+                       }
+               \end{equation}
+               
+               \begin{equation}
+                       \xymatrix{
+                               \ar[r] &
+                               *+[Fo]{s_0}\ar@(d,l)^{\neg a}\ar[r]^{a} &
+                               *+[F]{s_1}\ar@(d,l)^{true}\\
+                               \ar[r] & *+[F]{s_2}\ar@(d,l)^{\emptyset}\ar[r]^{a\vee b} &
+                               *+[Fo]{s_3}\ar@/^/[l]^{\emptyset}\ar@(d,r)_{true}
+                       }
+               \end{equation}
+               
+               \begin{equation}
+                       \xymatrix{
+                               \ar[r] &
+                               *+[Fo]{s_0}\ar[r]^{\neg a}\ar[d]_{a} &
+                               *+[F]{s_1}\ar@(d,r)_{true}\\
+                               & *+[Fo]{s_2}\ar@(d,l)^{true}
+                       }
+               \end{equation}
        \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}$
+               $\ev\al(a\wedge\ev b)\text{ or}\\
+               \al\ev b\wedge\ev\al a$
 \end{enumerate}
 \end{document}