blob: b4ed04c307de7751d5800fa2736bf0a23712431f (
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
|
\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}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{relsize}
\usepackage{parskip}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\erin}{\ifchangebar\cbend\fi\cbcolor{yellow}\cbstart\changebartrue}
\newcommand{\camil}{\ifchangebar\cbend\fi\cbcolor{red}\cbstart\changebartrue}
\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}}
\title{Model Checking}
\subtitle{Assignment 1}
\author{Camil Staps \and Erin van der Veen}
\begin{document}
\maketitle
\setcounter{section}{5}
\setcounter{subsection}{2}
\input{intro}
\input{syntax}
\input{semantics}
\input{specifying-properties}
\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}
\printbibliography
\section*{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
\camil
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.
Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend
\end{document}
|
