diff options
| -rw-r--r-- | Assignment1/assignment1.tex | 3 | ||||
| -rw-r--r-- | Assignment1/bad-prefix.tex | 7 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 2 | ||||
| -rw-r--r-- | Assignment1/semantics.tex | 2 |
4 files changed, 8 insertions, 6 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index a725397..449615d 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper]{scrartcl} +\documentclass[a4paper,parskip=half]{scrartcl} \usepackage[backend=biber,natbib]{biblatex} \bibliography{library} @@ -65,7 +65,6 @@ \tikzset{>=stealth} \tikzset{state/.append style={minimum size=15pt}} \usepackage{relsize} -\usepackage{parskip} \usepackage{cleveref} \usepackage{enumitem} \usepackage{multicol} diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex index e357359..c4b10fa 100644 --- a/Assignment1/bad-prefix.tex +++ b/Assignment1/bad-prefix.tex @@ -30,8 +30,11 @@ However, it is not guaranteed to find a minimal bad prefix (for instance, when a \caption{Finding a bad prefix for a safety property from a counterexample $vw^\omega$} \label{alg:bad-prefix} \vspace{5pt} - \textit{Input:} finite transition system $TS$, safety property $P$ and a counterexample $vw^\omega$.\\ - \textit{Output:} an $i\in\mathbb N$ for which $vw^i$ is a bad prefix.\\[-5pt] + \textit{Input:} finite transition system $TS$, safety property $P$ and a counterexample $vw^\omega$. + + \textit{Output:} an $i\in\mathbb N$ for which $vw^i$ is a bad prefix. + + \vspace{5pt} \hrule \begin{algorithmic}[0] \State $\mathcal A \gets \text{an NBA such that $\mathcal L_\omega(\mathcal A) = \textsl{Words}(\lnot P)$}$ diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex index 930119b..48591d8 100644 --- a/Assignment1/exercises.tex +++ b/Assignment1/exercises.tex @@ -110,7 +110,7 @@ \end{answer} \item Let $A=a_0,\dots,a_{2^n-1}$ be any permutation of $2^{AP\setminus\{p_0\}}$. - Define $w_K=b_{K,0}\dots b_{K,2^n-1}$ with + Define the series $w_K=b_{K,0}\dots b_{K,2^n-1}$ with \[ b_{K,i} \defeq \begin{cases} diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 05e96fb..1c0786d 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -101,7 +101,7 @@ This is done in \cref{ex:dual-modalities}. The semantics over words extend to transition systems similar to the LTL case in Definition 5.7. The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$. -\begin{figure}[h] +\begin{figure}[ht] \centering \begin{tikzpicture}[initial text={},node distance=3cm,->] \node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$}; |