From 638b2a6658d5078e822a5e4c1197a2f31e09d584 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 5 Feb 2016 21:59:53 +0100 Subject: [PATCH 1/1] e1-4 done --- .gitignore | 3 +++ Makefile | 16 ++++++++++++++++ e1.tex | 37 +++++++++++++++++++++++++++++++++++++ 3 files changed, 56 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 e1.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..8164e02 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.log +*.aux +*.pdf diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..2915da3 --- /dev/null +++ b/Makefile @@ -0,0 +1,16 @@ +LATEX:=pdflatex +DOCUMENTS:=e1.pdf + +.PHONY: all clean clobber + +all: $(DOCUMENTS) + +%.pdf: %.tex + $(LATEX) $(basename $<) + $(LATEX) $(basename $<) + +clobber: + $(RM) -v *.pdf + +clean: + $(RM) -v *.aux *.log diff --git a/e1.tex b/e1.tex new file mode 100644 index 0000000..6155f3b --- /dev/null +++ b/e1.tex @@ -0,0 +1,37 @@ +\documentclass{article} + +\usepackage{a4wide} +\usepackage{amssymb} +\usepackage{amsmath} + +\newcommand{\ra}{\rightarrow} +\newcommand{\un}{\text{ \textsf{U} }} +\newcommand{\ev}{\lozenge} +\newcommand{\al}{\square} +\newcommand{\nx}{\bigcirc} + +\begin{document} +\begin{enumerate} + \item + \item + \item + \item\strut\\ + $\begin{array}{ll} + \phi_1=\ev\al c & + s_2\ra s_4\overline{\ra s_5}\\ + \phi_2=\al\ev c & + s_2\ra s_4\overline{\ra s_5}\\ + \phi_3=\nx\neg c\rightarrow\nx\nx c & + s_2\ra s_4\overline{\ra s_5}\\ + \phi_4=\al a & + \text{Impossible. $a$ only holds in $s_1$ and in $s_5$.}\\ + & \text{$s_1$ we can only leave through a state where $\neg a$}\\ + & \text{$s_5$ we can not reach through $s_1$ without passing + through a $\neg a$ state}\\ + \phi_5=a\un\al(b\vee c) & + s_1\ra s_4\overline{\ra s_5}\\ + \phi_6=(\nx\nx b)\un(b\vee c) & + s_2\ra s_4\overline{\ra s_5} + \end{array}$ +\end{enumerate} +\end{document} -- 2.20.1