blob: cb1b36336127893e4a7c5713d97c313acfa3445c (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
\documentclass[a4paper]{scrartcl}
\usepackage[backend=biber,natbib]{biblatex}
\bibliography{library}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\renewcommand{\qedsymbol}{$\blacksquare$}
\let\leq\leqslant
\let\le\leqslant
\let\geq\geqslant
\let\ge\geqslant
% See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
% definitions and examples.
\newtheoremstyle{mydefinition}%
{2em}{2em}% Space above and below
{}% Body font
{}% Indent
{\bfseries}% Theorem head font
{}% Punctuation after theorem head
{0pt}% Space after theorem head
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{mydefinition}
\newtheorem{xdefinition}{Definition}
\newenvironment{definition}%
{\pushQED{\qed}\begin{xdefinition}}%
{\popQED\end{xdefinition}}
\newtheoremstyle{myexample}%
{2em}{2em}% Space above and below
{}% Body font
{}% Indent
{\itshape}% Theorem head font
{}% Punctuation after theorem head
{0pt}% Space after theorem head
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{myexample}
\newtheorem{xexample}{Example}
\newenvironment{example}%
{\pushQED{\qed}\begin{xexample}}%
{\popQED\end{xexample}}
\newtheorem{xremark}{Remark}
\newenvironment{remark}%
{\pushQED{\qed}\begin{xremark}}%
{\popQED\end{xremark}}
\newtheoremstyle{exercise}{1em}{1em}{}{}{\scshape}{.}{1em}{}
\theoremstyle{exercise}
\newtheorem{exercise}{Exercise}
\newtheoremstyle{theorem}%
{1em}{1em}%
{\itshape}%
{}%
{\itshape\bfseries}%
{}%
{0pt}%
{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}
\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{relsize}
\usepackage{parskip}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{multicol}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\crefname{xdefinition}{Definition}{Definitions}
\crefname{xexample}{Example}{Examples}
\crefname{xremark}{Remark}{Remarks}
\crefname{exercise}{Exercise}{Exercises}
\crefname{algorithm}{Algorithm}{Algorithms}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\changechangebar}[2][2pt]{\ifchangebar\cbend\fi\cbcolor{#2}\cbstart[#1]\changebartrue}
\newcommand{\erin}{\changechangebar{yellow}}
\newcommand{\camil}{\changechangebar{red}}
\newcommand{\both}{\changechangebar[1pt]{orange}}
\renewcommand*{\arraystretch}{1.3}
\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
\DeclareMathOperator{\Uop}{\mathbf{U}}
\DeclareMathOperator{\Wop}{\mathbf{W}}
\DeclareMathOperator{\Xop}{\bigcirc}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
\DeclareMathOperator{\Pop}{\bigcirc^{--1}}
\newcommand{\wff}{\emph{wff}} % Well-formed formula
\newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff
\newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff
\newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff
\title{Model Checking}
\subtitle{Assignment 1}
\author{Camil Staps \and Erin van der Veen}
\begin{document}
\both
\maketitle
\setcounter{section}{5}
\setcounter{subsection}{2}
\input{intro}
\input{syntax}
\input{semantics}
\input{equivalence}
\input{conversion}
%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper
\input{bad-prefix}
\input{summary}
\input{bibliographic-notes}
\input{exercises}
\both
\printbibliography
\section*{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
Erin has started writing the text.
This text was then copy-edited, slightly corrected where needed and expanded by Camil.
(The result was then copy-edited, slightly corrected where needed and expanded by Erin.
The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$
In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil.
Thin orange bars indicate material that cannot be attributed to either.
Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend
\end{document}
|
