From 32f1f4867bad79eb4d5afd179697b92699521698 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Wed, 18 Apr 2018 19:33:40 +0200
Subject: Minor enhancements

---
 Assignment1/intro.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Assignment1/intro.tex')

diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index d07be86..15294ee 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -17,7 +17,8 @@ Eventually, formal computing scientists stopped using past modalities for reason
 In 2003, Nicolas Markey showed that while past modalities do not increase expressive power,
 they can make LTL formulas exponentially more succinct~\cite{Markey2003}.
 In other words, there is a class of PLTL formulae%
-	\footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.}
+	\footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.
+		(Like the book, this section may contain typos and inaccuracies. These are however not intentional.)}
 	for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$.
 Markey achieves this proof by providing a formula that is in exactly this class.
 Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate.
-- 
cgit v1.2.3


From 205e49a4c15d291a2519eedabd683341a153aa03 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Wed, 18 Apr 2018 20:50:11 +0200
Subject: Bars everywhere

---
 Assignment1/assignment1.tex | 10 +++++++---
 Assignment1/intro.tex       |  2 +-
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'Assignment1/intro.tex')

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index e8e34dd..cb1b363 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -78,8 +78,10 @@
 \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}
+\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}
 
@@ -103,6 +105,7 @@
 
 \begin{document}
 
+\both
 \maketitle
 
 \setcounter{section}{5}
@@ -120,16 +123,17 @@
 \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
-\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.
+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
 
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index 15294ee..ddbaa5a 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,8 +1,8 @@
+\erin
 \subsection{Past Modalities in LTL}\label{sec:intro}
 % Explain that past Modalities are not necessary for a complete logic
 % Explain that PLTL does make the logic more succinct (Paper 1)
 %TODO: Give example on what kind of things we want to express with PLTL
-\erin
 As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
 This section discusses this extension.
 The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL.
-- 
cgit v1.2.3