.

diff --cc Makefile
index 1c8e48e,3fbb9ab..b834717
--- 1/Makefile
--- 2/Makefile
+++ b/Makefile
@@@ -1,6 -1,6 +1,6 @@@
  LATEX:=latex
  DOT:=dot
- DOCUMENTS:=e1.pdf
 -DOCUMENTS:=e1.pdf e2.pdf
++DOCUMENTS:=e1.pdf e2.pdf e3.pdf
  
  .PHONY: all clean clobber graphs
  

diff --cc e3.tex
index 0000000,0000000..33bcca5
new file mode 100644 (file)
--- /dev/null
--- /dev/null
+++ b/e3.tex
@@@ -1,0 -1,0 +1,57 @@@
++\documentclass{article}
++
++\usepackage{a4wide}
++\usepackage{amssymb}
++\usepackage{amsmath}
++\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 3}
++
++\begin{document}
++\maketitle
++\begin{enumerate}
++      \item
++      \item 
++              $\text{TS}\vDash\Phi_1\Leftrightarrow \{s_0\}\subseteq Sat(
++                      \exists\ev\forall\al c)\\
++              Sat(c)= \{s_3, s_4\}\\
++              Sat(\forall\al (s_3\vee s_4))= \{s_4\}\\
++              Sat(\exists\ev(s_4)= \{s_0,s_1\}\\
++              \{s_0\}\subseteq \{s_0,s_1\}\text{ thus }\Phi_1\text{ is satisfied}$
++              \\\strut\\
++              $\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
++                      \forall(a\un \forall\ev c))\\
++              Sat(c)= \{s_3, s_4\}\\
++              Sat(\forall\ev(s_3\vee s_4))=\{s_0,s_1,s_4\}\\
++              Sat(a)= \{s_0, s_1\}\\
++              Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\
++              \{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $
++      \item 
++      \item
++              For formula:
++              $$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$
++              We create an automaton $\neg\varphi$ where
++              $$\begin{array}{rl}
++                      \neg\varphi 
++                      & :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\
++                      & :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\
++                      & :=\ev(a\wedge(\al\neg b\vee
++                              
++                              
++              \end{array}$$
++              Elementary sets:
++              $$\begin{array}{lll}
++                      a & b & 
++              \end{array}$$
++\end{enumerate}
++\end{document}