From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 14 Feb 2016 13:02:45 +0000 (+0100)
Subject: e2 done
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=7d2dd5da5158f79ce666f5eb3945b18e5135de0b;p=mc1516.git

e2 done
---

diff --git a/Makefile b/Makefile
index 1c8e48e..3fbb9ab 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 LATEX:=latex
 DOT:=dot
-DOCUMENTS:=e1.pdf
+DOCUMENTS:=e1.pdf e2.pdf
 
 .PHONY: all clean clobber graphs
 
diff --git a/e1.tex b/e1.tex
index 66d3a9d..a975cf7 100644
--- a/e1.tex
+++ b/e1.tex
@@ -13,19 +13,14 @@
 
 \everymath{\displaystyle}
 
+\author{Mart Lubbers}
+\date{\today}
+\title{Model Checking Excercises 1}
+
 \begin{document}
+\maketitle
 \begin{enumerate}
 	\item
-		$\xymatrix{
-				& l_0 & l_1 & l_2 & l_3 & l_5 & l_6 & l_7\\
-			l_0 & 0ff\ar[d] & 0ff & 0ff\\
-			l_1 & 0ff\ar[d] & 0ff & 0ff\\
-			l_2 & 1ff\ar[d] & 1ff & 0ff\\
-			l_3 & 1tf\ar[d] & 1tf & 0ff\\
-			l_5 & 1tf\ar[d] & 1tf & 0ff\\
-			l_6 & 1tf\ar[d] & 1tf & 0ff\\
-			l_7 & 1ff       & 1ff & 0ff 
-		}$
 	\item
 		$\al(crit_0\veebar crit_1)$
 	\item 
diff --git a/e2.tex b/e2.tex
new file mode 100644
index 0000000..bec6c3b
--- /dev/null
+++ b/e2.tex
@@ -0,0 +1,69 @@
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{booktabs}
+\usepackage[all]{xypic}
+
+\newcommand{\ra}{\rightarrow}
+\newcommand{\un}{\text{ \textsf{U} }}
+\newcommand{\ev}{\lozenge}
+\newcommand{\al}{\square}
+\newcommand{\nx}{\bigcirc}
+
+\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
+		\begin{equation}
+			\xymatrix{
+				\ar[r] &
+				*+[F]{s_0}\ar@/^/[r]^{\neg a}\ar@(d,l)^{a} &
+				*+[F]{s_1}\ar@/^/[l]^{\neg b}\ar[r]^{b} &
+				*+[Fo]{s_2}\ar@(d,r)_{true}
+			}
+		\end{equation}
+		
+		\begin{equation}
+			\xymatrix{
+				\ar[r] &
+				*+[Fo]{s_0}\ar@(d,l)^{true}\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@(d,l)^{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 
+		$\ev\al(a\wedge\ev b)$
+\end{enumerate}
+\end{document}