From 7d2dd5da5158f79ce666f5eb3945b18e5135de0b Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 14 Feb 2016 14:02:45 +0100 Subject: [PATCH] e2 done --- Makefile | 2 +- e1.tex | 15 ++++-------- e2.tex | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 75 insertions(+), 11 deletions(-) create mode 100644 e2.tex 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} -- 2.20.1