e2.tex

   1 \documentclass{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{amssymb}
   5 \usepackage{amsmath}
   6 \usepackage[all]{xypic}
   7
   8 \newcommand{\ra}{\rightarrow}
   9 \newcommand{\un}{\text{ \textsf{U} }}
  10 \newcommand{\ev}{\lozenge}
  11 \newcommand{\al}{\square}
  12 \newcommand{\nx}{\bigcirc}
  13
  14 \everymath{\displaystyle}
  15
  16 \author{Mart Lubbers}
  17 \date{\today}
  18 \title{Model Checking Excercises 2}
  19
  20 \begin{document}
  21 \maketitle
  22 \begin{enumerate}
  23         \item\strut\\
  24                 \begin{tabular}{ll}
  25                         $TS\nvDash\varphi_1$ & $s_1\ra \overline{s_3\ra s_4}$\\
  26                         $TS\vDash\varphi_2$ & Yes, all loops go via $s_2,s_3$ or $s_5$
  27                         where $c$ holds.\\
  28                         $TS\vDash\varphi_3$ & Yes, $\nx\neg c$ is only true when the next
  29                         state is $s_4$.\\
  30                         & From $s_4$ you can only go to a state where $c$ holds.\\
  31                         $TS\nvDash\varphi_4$ & $s_2\ra\ldots$\\
  32                         $TS\vDash\varphi_5$ & Yes, starting in $s_1$ $b\vee c$ holds after
  33                         the first transition\\
  34                         & Starting in $s_2$ $b\vee c$ holds immediatly.\\
  35                         $TS\vDash\varphi_6$ & $s_1\ra\overline{s_4\ra s_2}$
  36                 \end{tabular}
  37         \item
  38                 \begin{equation}
  39                         \xymatrix{
  40                                 \ar[r] &
  41                                 *+[F]{s_0}\ar@/^/[r]^{\neg a}\ar@(d,l)^{a} &
  42                                 *+[F]{s_1}\ar@/^/[l]^{\neg b\wedge a}
  43                                         \ar@(d,r)_{\neg b\wedge \neg a}
  44                                         \ar[r]^{b} &
  45                                 *+[Fo]{s_2}\ar@(d,r)_{true}
  46                         }
  47                 \end{equation}
  48
  49                 \begin{equation}
  50                         \xymatrix{
  51                                 \ar[r] &
  52                                 *+[Fo]{s_0}\ar@(d,l)^{\neg a}\ar[r]^{a} &
  53                                 *+[F]{s_1}\ar@(d,l)^{true}\\
  54                                 \ar[r] & *+[F]{s_2}\ar@(d,l)^{\emptyset}\ar[r]^{a\vee b} &
  55                                 *+[Fo]{s_3}\ar@/^/[l]^{\emptyset}\ar@(d,r)_{true}
  56                         }
  57                 \end{equation}
  58
  59                 \begin{equation}
  60                         \xymatrix{
  61                                 \ar[r] &
  62                                 *+[Fo]{s_0}\ar[r]^{\neg a}\ar[d]_{a} &
  63                                 *+[F]{s_1}\ar@(d,r)_{true}\\
  64                                 & *+[Fo]{s_2}\ar@(d,l)^{true}
  65                         }
  66                 \end{equation}
  67         \item
  68                 $\ev\al(a\wedge\ev b)\text{ or}\\
  69                 \al\ev b\wedge\ev\al a$
  70 \end{enumerate}
  71 \end{document}