e1.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 \begin{document}
  17 \begin{enumerate}
  18         \item
  19                 $\xymatrix{
  20                         & l_0 & l_1 & l_2 & l_3 & l_5 & l_6 & l_7\\
  21                         l_0\\
  22                         l_1\\
  23                         l_2\\
  24                         l_3\\
  25                         l_5\\
  26                         l_6\\
  27                         l_7
  28                 }$
  29         \item
  30                 $\al(crit_0\veebar crit_1)$
  31         \item
  32                 We define:\\
  33                 $ AP=\bigcup_{i\in N}\{lift_n, door_n,call_n\},
  34                 N=\{0, 1, 2, 3\}$
  35                 \begin{enumerate}
  36                         \item
  37                                 $\bigwedge_{n\in N}\al(door_m\ra lift_n)$
  38                         \item
  39                                 $\bigwedge_{n\in N}\al(call_n\ra\ev(lift_n\wedge door_n))$
  40                         \item
  41                                 $\al\ev lift_0$
  42                         \item
  43                                 $\al(call_3\rightarrow\bigcirc (lift_3\wedge door_3))$
  44                 \end{enumerate}
  45         \item\strut\\
  46                 $\begin{array}{ll}
  47                         \varphi_1=\ev\al c &
  48                                 s_2\ra s_4\overline{\ra s_5}\\
  49                         \varphi_2=\al\ev c &
  50                                 s_2\ra s_4\overline{\ra s_5}\\
  51                         \varphi_3=\nx\neg c\rightarrow\nx\nx c &
  52                                 s_2\ra s_4\overline{\ra s_5}\\
  53                         \varphi_4=\al a &
  54                                 \text{Impossible. $a$ only holds in $s_1$ and in $s_5$.}\\
  55                         & \text{$s_1$ we can only leave through a state where $\neg a$}\\
  56                         & \text{$s_5$ we can not reach through $s_1$ without passing
  57                                 through a $\neg a$ state}\\
  58                         \varphi_5=a\un\al(b\vee c) &
  59                                 s_1\ra s_4\overline{\ra s_5}\\
  60                         \varphi_6=(\nx\nx b)\un(b\vee c) &
  61                                 s_2\ra s_4\overline{\ra s_5}
  62                 \end{array}$
  63 \end{enumerate}
  64 \end{document}