\NeedsTeXFormat{LaTeX2e}
\ProvidesClass{thesis}[2021/10/28 Master Thesis]
\ProcessOptions\relax
\LoadClass[a4paper,12pt,twoside,openright]{memoir}
% Colors
\RequirePackage{xcolor}
\include{rwth-colors.tex}
% Calc required for chapter header calculations
\RequirePackage{calc}
% Pagesize
% Memoir documentation: https://ctan.org/pkg/memoir?lang=de
\setbinding{10mm} 
\settypeblocksize{600pt}{1.1\lxvchars}{*}
\setlrmargins{*}{*}{1.5}
\setulmargins{4cm}{*}{*}
\setheadfoot{2\onelineskip}{2\onelineskip}
\setmarginnotes{17pt}{3.5cm}{\onelineskip}
\checkandfixthelayout
% Headings and Page Style
\pagestyle{ruled}
\copypagestyle{chapter}{plain}
\makeevenfoot{chapter}{\thepage}{}{}
\makeoddfoot{chapter}{}{}{\thepage}
% Fonts
\RequirePackage{amsfonts}
\RequirePackage{mathspec}
% undo the wrong changes made by mathspec
\let\RequirePackage\original@RequirePackage
\let\usepackage\RequirePackage
\RequirePackage{fontspec}
\setprimaryfont[
UprightFont={*},
ItalicFont={* Italic},
BoldFont={* Semibold},
BoldItalicFont={* Semibold Italic},
Scale=MatchLowercase]{Source Serif Pro}
%
% Sans Font: Source Sans Pro Light/Semibold
\setallsansfonts[
UprightFont={*},
ItalicFont={* Italic},
BoldFont={* Semibold},
BoldItalicFont={* Semibold Italic},
Scale=MatchLowercase]{Source Sans Pro}
%
% Mono Font: Source Code Pro Light/Semibold (No Italics available)
\setallmonofonts[
UprightFont={* Light},
BoldFont={* Semibold},
Scale=MatchLowercase]{Source Code Pro}
%
% Replace math greek fonts by Source Serif Pro (No Italics available -> Use fake italics)
\setmathfont(Greek)[
  UprightFont={*},
  ItalicFont={* Italic},
  BoldFont={* Semibold},
  BoldItalicFont={* Semibold Italic},
  Scale=MatchLowercase,
  AutoFakeSlant=0.15
]{Source Serif Pro}
%%%
% Division Styles
\colorlet{chaptercolor}{rwth-50}
% helper ms
\newcommand\numlifter[1]{\raisebox{-2cm}[0pt][0pt]{\smash{#1}}}
\newcommand\numindent{\kern37pt}
\newlength\chaptertitleboxheight
\makechapterstyle{hansen}{
	\renewcommand\printchaptername{\raggedleft}
	\renewcommand\printchapternum{%
		\begingroup%
		\leavevmode%
		\chapnumfont%
		\strut%
		\numlifter{\thechapter}%
		\numindent%
		\endgroup%
	}
	\renewcommand*{\printchapternonum}{%
		\vphantom{\begingroup%
			\leavevmode%
			\chapnumfont%
			\numlifter{\vphantom{9}}%
			\numindent%
			\endgroup}
		\afterchapternum}
	\setlength\midchapskip{0pt}
	\setlength\beforechapskip{0.5\baselineskip}
	\setlength{\afterchapskip}{3\baselineskip}
	\renewcommand\chapnumfont{%
		\fontsize{4cm}{0cm}%
		\bfseries%
		\sffamily%
		\color{chaptercolor}%
	}
	\renewcommand\chaptitlefont{%
		\normalfont%
		\huge%
		\bfseries%
		\raggedleft%
	}%
	\settototalheight\chaptertitleboxheight{%
		\parbox{\textwidth}{\chaptitlefont \strut bg\\bg\strut}}
	\renewcommand\printchaptertitle[1]{%
		\parbox[t][\chaptertitleboxheight][t]{\textwidth}{%
			%\microtypesetup{protrusion=false}% add this if you use microtype
			\chaptitlefont\strut ##1\strut}%
	}
}
% Chapter Style
\chapterstyle{hansen}
% Section Style
\setsecheadstyle{\Large\bfseries\color{rwth-75}\raggedright}
%
%%%
% Ortography
\usepackage[ngerman,english]{babel}
%
% Bibliography
\PassOptionsToPackage{backend=biber,style=numeric}{biblatex}
\RequirePackage{biblatex}
% \addbibresource{../literatur.bib} % Put this in the document
% Language
\PassOptionsToPackage{english,ngerman}{babel}
\RequirePackage{babel}
\PassOptionsToPackage{german=quotes}{csquotes}
\RequirePackage{csquotes}
% Superscripts for 1st, 2nd, 3rd, 4th
% \nth{3}
\usepackage[super]{nth}

% Define RWTH style colors
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For HKS colors use the spotcolor package
% which predefines a number of such colors
% Main blue color is HKS 44 K
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% RGB colors used for screen
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The main blue color, 100 and 50 are the
% most commonly used ones
% e.g. in the logo
\definecolor{rwth}   {RGB}{  0  84 159}
\definecolor{rwth-75}{RGB}{ 64 127 183}
\definecolor{rwth-50}{RGB}{142 186 229}
\definecolor{rwth-25}{RGB}{199 221 242}
\definecolor{rwth-10}{RGB}{232 241 250}
% All the other colors
% Secondary colors
\definecolor{black}   {RGB}{  0   0   0}
\definecolor{black-75}{RGB}{100 101 103}
\definecolor{black-50}{RGB}{156 158 159}
\definecolor{black-25}{RGB}{207 209 210}
\definecolor{black-10}{RGB}{236 237 237}
\definecolor{magenta}   {RGB}{227   0 102}
\definecolor{magenta-75}{RGB}{233  96 136}
\definecolor{magenta-50}{RGB}{241 158 177}
\definecolor{magenta-25}{RGB}{249 210 218}
\definecolor{magenta-10}{RGB}{253 238 240}
\definecolor{yellow}   {RGB}{255 237   0}
\definecolor{yellow-75}{RGB}{255 240  85}
\definecolor{yellow-50}{RGB}{255 245 155}
\definecolor{yellow-25}{RGB}{255 250 209}
\definecolor{yellow-10}{RGB}{255 253 238}
% The extended color spectrum
\definecolor{petrol}   {RGB}{  0  97 101}
\definecolor{petrol-75}{RGB}{ 45 127 131}
\definecolor{petrol-50}{RGB}{125 164 167}
\definecolor{petrol-25}{RGB}{191 208 209}
\definecolor{petrol-10}{RGB}{230 236 236}
\definecolor{turkis}   {RGB}{  0 152 161}
\definecolor{turkis-75}{RGB}{  0 177 183}
\definecolor{turkis-50}{RGB}{137 204 207}
\definecolor{turkis-25}{RGB}{202 231 231}
\definecolor{turkis-10}{RGB}{235 246 246}
\definecolor{grun}   {RGB}{ 87 171  39}
\definecolor{grun-75}{RGB}{141 192  96}
\definecolor{grun-50}{RGB}{184 214 152}
\definecolor{grun-25}{RGB}{221 235 206}
\definecolor{grun-10}{RGB}{242 247 236}
\definecolor{maigrun}   {RGB}{189 205   0}
\definecolor{maigrun-75}{RGB}{208 217  92}
\definecolor{maigrun-50}{RGB}{224 230 154}
\definecolor{maigrun-25}{RGB}{240 243 208}
\definecolor{maigrun-10}{RGB}{249 250 237}
\definecolor{orange}   {RGB}{246 168   0}
\definecolor{orange-75}{RGB}{250 190  80}
\definecolor{orange-50}{RGB}{253 212 143}
\definecolor{orange-25}{RGB}{254 234 201}
\definecolor{orange-10}{RGB}{255 247 234}
\definecolor{rot}   {RGB}{204   7  30}
\definecolor{rot-75}{RGB}{216  92  65}
\definecolor{rot-50}{RGB}{230 150 121}
\definecolor{rot-25}{RGB}{243 205 187}
\definecolor{rot-10}{RGB}{250 235 227}
\definecolor{bordeaux}   {RGB}{161  16  53}
\definecolor{bordeaux-75}{RGB}{182  82  86}
\definecolor{bordeaux-50}{RGB}{205 139 135}
\definecolor{bordeaux-25}{RGB}{229 197 192}
\definecolor{bordeaux-10}{RGB}{245 232 229}
\definecolor{violett}   {RGB}{ 97  33  88}
\definecolor{violett-75}{RGB}{131  78 117}
\definecolor{violett-50}{RGB}{168 133 158}
\definecolor{violett-25}{RGB}{210 192 205}
\definecolor{violett-10}{RGB}{237 229 234}
\definecolor{lila}   {RGB}{122 111 172}
\definecolor{lila-75}{RGB}{155 145 193}
\definecolor{lila-50}{RGB}{188 181 215}
\definecolor{lila-25}{RGB}{222 218 235}
\definecolor{lila-10}{RGB}{242 240 247}

\documentclass{thesis}
\usepackage{lipsum}
\usepackage{amsthm}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\addbibresource{literature.bib}
\begin{document}
    \frontmatter
    \input{ch0_frontmatter}
    \mainmatter
    \chapter{Introduction}
    \input{ch1_introduction}
    \chapter{Theory}
    \input{ch2_preliminaries}
    \input{ch3_theory}
    \chapter{Implementation}
    \input{ch4_implementation}
    \chapter{Conclusion}
    \input{ch5_conclusion}
    Foo
    \backmatter
    \printbibliography[title={References}]
\end{document}

@default_files = ('main.tex');
$out_dir = 'build';
$clean_ext = "xdv";
$pdf_mode=5;

% TeX root = main.tex

% TeX root = main.tex
\section{Conclusion}
\lipsum
\section{Future Work}
\lipsum

% TeX root = main.tex
\section{Implementation}
\lipsum
\section{Correctness}
\lipsum
\section{Performance}
\lipsum

% TeX root = main.tex
\section{Theory}
\lipsum
\section{Correctness}
\lipsum
\section{Non-probabilistic ITS}
\lipsum

% TeX root = main.tex
\section{Preliminaries}
\begin{comment}
- Term Rewrite Systems (TRS)
- Transition Systems
    - A set of States S
    - A start location S_0 \in S
    - A set of transitions T \in S x C x S
- Integer Transition Systems (ITS)
\end{comment}
\begin{definition}[Linear Constraints]
    Let $V$ be a fixed set of integer Variables $\{x_1, x_2, \dots, n\} $. A linear constraint is defined as $\psi = a_0 + a_1 x_1 + \dots + a_n x_n \diamond 0$ where $a_i \in \mathbb{N}$ are integer coefficients, $x_i \in V$ are variables and $\diamond \in \{>, <, \geq, \leq, =\}$.
=======
\section{Preliminaries} 
\begin{definition}[Linear Constraints] 
    Let $V$ be a fixed set of integer
    Variables $\{x_1, x_2, \dots, n\} $. A linear constraint is defined as $\psi
    = a_0 + a_1 x_1 + \dots + a_n x_n \diamond 0$ where $a_i \in \mathbb{N}$ are
    integer coefficients, $x_i \in V$ are variables and $\diamond \in \{>, <, 
    \geq, \leq, =\}$. \end{definition}
\begin{definition}[Assignment] 
    An assignment $\sigma : V \mapsto \mathbb{Z}$ assigns an integer value to
    each variable in $V$. $\sigma$ is a solution for a linear constraint $\psi$
\end{definition} \
\section{Probabilistic integer programs}
In general, an \textit{integer programs} is a programs that only uses variables
with integer values. Many equivalent mathematical structures have been
developed over the year to formalize integer program. The one used in this
thesis is the integer transition system.
An integer transition system represents a program as locations and transitions
between those locations. A run inside the the transiton system is a sequence of
configurations -- that is a location and a variable assignment --
where every configuration is reachable via a transition from the previous
configuration. 
Non-deterministic programs have mutually non-exclusive transitions leaving the
same location. Hence it is unclear which transition is taken at a possible
runtime. In order to simulate the program, one must take all possible
transitions into account. 
Probabilistic programs are similar to non-determistic ones, but the transition
taken is decied on a probabilistic basis. Imagine an oracle that throws some
dice to determin the taken transition. 
In order to allow both concepts in a program, we use the concept of
\textit{general transitions} A general transition is a set of transitions with
the probabilities adding up to 1 acting as a single transition for the
non-determinism. Non-determinism can only occur between general transitions and
it is resolved first before probabilities are resolved. 
deterministic and non-probabilistic programs are a special case of
probabilistic programs, where very general transition consist of a single
transition and all general transitions are mutually exclusive. 
Let's get to the formal definitions. We will follow the definition of F. Meyer
\cite{https://link.springer.com/chapter/10.1007/978-3-319-66167-4_8}.
\begin{definition}[Probabilistic Integer Program] 
    \newcommand{\V}[0]{\mathcal{V}} % Variables
    \newcommand{\PV}[0]{\mathcal{V}} % Program variables
    \newcommand{\Z}[0]{\mathbb{Z}} % whole numbers, integers
    \newcommand{\GT}[0]{GT} % General transitions
    $(\V, L, \GT, l_0)$ is a probabilistic integer transition system where 
    \begin{enumerate}
        \item $\V$ is a finite set of program variables
        \item $L$ is a finite non-empty set of location
        \item $\GT$ is a finite set of general transitions, where a general 
            transition $g \in \GT$ is a finit non-empty set of transitions 
            $t = (l, p, τ, η, l')$ with: 
            \begin{enumerate} 
                \item a source and target location $l,l' \in L$.
                \item a probability $p \geq 0$, that the transition is taken when 
                    the correspondig general transition $g$ is executed. 
                \item a guard $τ \in C$
                \item an update function $η : \PV \mapsto \Z[\V] \cup D$, mapping every 
                    program variable to a polynomial or a bounded distribution 
                    function. All $t \in g$ must share the same start location 
                    $l$, guard $τ$. 
            \end{enumerate}
            Moreover, the probabilities of the 
            transitions must add up to $1$. We call $τ_g$ the guard of 
            the general transition $g$ and $l_g$ the start location
        \item $l_0 \in L$ is the start location of the program.
    \end{enumerate}
\end{definition}
In this thesis we will see a log of integer programs, so let's get familiar 
with a couple of examples. 
% TODO: examples
Various languages exist to represent integer programs in a computer readable
form; namely Koat2\cite{}, IntC, Some weird XML Onthology
\cite{https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd}
% - CINT
% - Koat Format 
% For probabilistic: PIP 
\section{Linear Ranking Funktions}
\newacronym{lrf}{LRF}{Linear Ranking Function}
\newacronym{prf}{PRF}{Polynomial Ranking Function}
\newacronym{mprf}{M\Phi{}RF}{Multiphase Ranking Function}
Ranking functions are a widely use tool to prove termination and runtime-bounds of integer transition systems. The simplest variant of ranking functions are \gls{lrf}
We seek a function $f(x_1,\dots,x_n) = a_1x_1 + \cdots + a_nx_n + a_0$ with the rationals as a co-domain, such that 
\begin{enumerate} 
    \item $f(\bar{x}) \leq 0$ for any valuation $\bar{x}$ that satisfies the loop constraints;
    \item $f(\bar{x}) - f(\bar{x}') \geq 1$ for any transition leadtion from $\bar{x}$ to $\bar{x}'$
\end{enumerate}
\cite{benamram2017}\todo{plagiat}
Intuition: The ranking function decreases for every walkable transition. If such a ranking function exists, the loop terminates. \todo{not sure about this, guess}
\section{Lexicographic ranking functions}
We expand the \gls{lrf} to a tuple of \gls{lrf}. Where whenever lexicograpically higher function decreases lower ones can increase again.
Example for a tuple. 
$$
\langle f_1, f_2\rangle \text{s. th.}
$$
\section{Multiphase-ranking Functions}
\section{Goal}

% TeX root = main.tex
\section{Related Works}

% TeX root = main.tex
\begin{titlingpage}
    \newlength{\logoheight}	\setlength{\logoheight}{5cm}
    \setlength{\droptitle}{-3em}
    
    \renewcommand{\maketitlehooka}{%
        \begin{center}
            {\Large Rheinisch-Westfälische Technische Hochschule Aachen\par\noindent}
            Lehr- und Forschungsgebiet Informatik 2\par\noindent Programmiersprachen und Verifikation\\
            Prof. Dr. Jürgen Giesl\\
            \vspace{\logoheight}
            %\includegraphics[height=\logoheight]{PETs4DS.pdf}\\
            \vspace*{1em}
            {\LARGE\scshape Master Thesis}
            \vspace*{1.5em}
        \end{center}
    }
    \pretitle{\begin{center}\bfseries\HUGE\color{rwth-75}}
        \title{Control-Flow Refinement in a Framework for Automated (Probabilistic) Complexity Analysis}
    \posttitle{\end{center}\vskip 4em}
    
    \preauthor{\begin{center}\Large}
        \author{Yoann Maurice Kehler}
    \postauthor{\end{center}\vskip 2em}
    
    \predate{\begin{center}\Large}
    \date{\today}
    \postdate{\end{center}\vskip 2em}
    \renewcommand{\maketitlehookd}{%
        \vfill
        \centerfloat
        \begin{tabular}{ll}
            \color{rwth}\nth{1} Advisor		& Nils Lommen, MSc\\
            \color{rwth}\nth{2} Advisor		& Eleanore Meyer, MSc\\
            \color{rwth}\nth{1} Supervisor	& Prof. Jürgen Giesl\\
            \color{rwth}\nth{2} Supervisor 	& Prof. Erika Ábrahám\\	
        \end{tabular}
    }
    \calccentering{\unitlength}
    \begin{adjustwidth*}{\unitlength}{-\unitlength}
        \maketitle
    \end{adjustwidth*}
\end{titlingpage}
\begin{abstract}
    Hallo Welt dies ist ein tolles Abstract Es aktualisiert sogar, wenn man im Buffer Dinge schreibt. 
    Heheheheheheheheheheh!
    \begin{itemize}
        \item Fooooooo!
    \end{itemize}
    \lipsum[1-3]
\end{abstract}
\maxtocdepth{subsection}
\cleardoublepage
\cleardoublepage
\tableofcontents

# cfr-tex
A master thesis