Commit 04f0d99a authored by Petyo Bogdanov Ilov's avatar Petyo Bogdanov Ilov

Documentation init commit

parent a825c4e4
\relax
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\bibstyle{alpha}
\bibdata{src/bib/Literatur}
\relax
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\bibstyle{alpha}
\bibdata{src/bib/Literatur}
This diff is collapsed.
\BOOKMARK [0][-]{chapter.1}{Introduction}{}% 1
\BOOKMARK [0][-]{chapter.1}{Einleitung}{}% 1
\BOOKMARK [1][-]{section.1.1}{Eins - Eins}{chapter.1}% 2
\BOOKMARK [2][-]{subsection.1.1.1}{Eins - Eins - Eins}{section.1.1}% 3
\BOOKMARK [0][-]{chapter.2}{Z3 theorem solver}{}% 4
\BOOKMARK [1][-]{section.2.1}{Z3 basics}{chapter.2}% 5
\BOOKMARK [0][-]{chapter.3}{Elimination of internal variables of automatons that including non-linear parts}{}% 6
\BOOKMARK [1][-]{section.3.1}{Exemplified workflow of matching internal variables }{chapter.3}% 7
\BOOKMARK [2][-]{subsection.3.1.1}{Automatons for comparison}{section.3.1}% 8
\BOOKMARK [2][-]{subsection.3.1.2}{First step of the procedure. Detecting non-linear equations.}{section.3.1}% 9
\BOOKMARK [2][-]{subsection.3.1.3}{Second step of the procedure. Calculation of non linear coefficients.}{section.3.1}% 10
\BOOKMARK [2][-]{subsection.3.1.4}{Unfolding and simulation}{section.3.1}% 11
\BOOKMARK [0][-]{chapter.4}{Code Listings}{}% 12
\BOOKMARK [0][-]{chapter.5}{Zusammenfassung und Ausblick}{}% 13
\BOOKMARK [0][-]{figure.caption.11}{Literaturverzeichnis}{}% 14
\BOOKMARK [0][-]{appendix.A}{z.B. Programmdokumentation}{}% 15
\BOOKMARK [0][-]{chapter.1}{Introduction}{}% 1
\BOOKMARK [0][-]{chapter.2}{Related Work}{}% 2
\BOOKMARK [0][-]{chapter.3}{Theoretical Background}{}% 3
\BOOKMARK [1][-]{section.3.1}{Input/Output Extended Finite Automaton\(I/O-EFA\)}{chapter.3}% 4
\BOOKMARK [1][-]{section.3.2}{Input/Output Transition System}{chapter.3}% 5
\BOOKMARK [1][-]{section.3.3}{Simulation relation}{chapter.3}% 6
\BOOKMARK [0][-]{chapter.4}{Using Isabelle prove assistant for compatibility check}{}% 7
\BOOKMARK [1][-]{section.4.1}{Simulink components}{chapter.4}% 8
\BOOKMARK [1][-]{section.4.2}{Application of Isabelle}{chapter.4}% 9
\BOOKMARK [1][-]{section.4.3}{Global variables test using Isabelle theorem prover}{chapter.4}% 10
\BOOKMARK [0][-]{chapter.5}{Elimination of internal variables of I/O-EFA automatons that including non-linear parts}{}% 11
\BOOKMARK [1][-]{section.5.1}{Z3 Solver basics}{chapter.5}% 12
\BOOKMARK [1][-]{section.5.2}{Exemplified workflow of matching internal variables of I/O-EFAs containing non-linear dependencies}{chapter.5}% 13
\BOOKMARK [2][-]{subsection.5.2.1}{Previous approach}{section.5.2}% 14
\BOOKMARK [2][-]{subsection.5.2.2}{Automatons for comparison}{section.5.2}% 15
\BOOKMARK [2][-]{subsection.5.2.3}{First step of the procedure. Detecting non-linear equations.}{section.5.2}% 16
\BOOKMARK [2][-]{subsection.5.2.4}{Second step of the procedure. Calculation of linear coefficients.}{section.5.2}% 17
\BOOKMARK [2][-]{subsection.5.2.5}{Unfolding and simulation}{section.5.2}% 18
\BOOKMARK [0][-]{chapter.6}{Index tree optimization for transition filtering}{}% 19
\BOOKMARK [1][-]{section.6.1}{Previous approach of transition filtering optimization}{chapter.6}% 20
\BOOKMARK [1][-]{section.6.2}{Building of index tree}{chapter.6}% 21
\BOOKMARK [1][-]{section.6.3}{Evaluation}{chapter.6}% 22
\BOOKMARK [0][-]{chapter.7}{Clone detection and transformation to I/O-FEA of control flow graphs}{}% 23
\BOOKMARK [1][-]{section.7.1}{Approach with control flow graphs trees}{chapter.7}% 24
\BOOKMARK [1][-]{section.7.2}{Applied approach for substitution, clone detection and separation on output port basis}{chapter.7}% 25
\BOOKMARK [2][-]{subsection.7.2.1}{Substitution}{section.7.2}% 26
\BOOKMARK [2][-]{subsection.7.2.2}{Clone detection}{section.7.2}% 27
\BOOKMARK [2][-]{subsection.7.2.3}{Separation on output port basis}{section.7.2}% 28
\BOOKMARK [1][-]{section.7.3}{Improvements}{chapter.7}% 29
\BOOKMARK [0][-]{chapter.8}{Disjunctive Normal Form Optimization}{}% 30
\BOOKMARK [1][-]{section.8.1}{1st Step: Guard to Guard Normal Form \(GNF\) Transformation}{chapter.8}% 31
\BOOKMARK [1][-]{section.8.2}{2nd Step: Guard-NF to Guard Disjunctive Normal Form \(GDNF\) Transformation}{chapter.8}% 32
\BOOKMARK [2][-]{subsection.8.2.1}{3rd Step: Guard-DNF to Hash-Guard Disjunctive Normal Form \(HGDNF\) Transformation}{section.8.2}% 33
\BOOKMARK [2][-]{subsection.8.2.2}{4th Step: HGDNF to Optimized HGDNF Transformation}{section.8.2}% 34
\BOOKMARK [0][-]{chapter.9}{Code Listings}{}% 35
\BOOKMARK [1][-]{section.9.1}{Isabelle listing}{chapter.9}% 36
\BOOKMARK [1][-]{section.9.2}{Z3 listings}{chapter.9}% 37
\BOOKMARK [1][-]{section.9.3}{Java listings}{chapter.9}% 38
\BOOKMARK [0][-]{chapter.10}{Zusammenfassung und Ausblick}{}% 39
\BOOKMARK [0][-]{figure.caption.23}{Literaturverzeichnis}{}% 40
\BOOKMARK [0][-]{appendix.A}{z.B. Programmdokumentation}{}% 41
\BOOKMARK [0][-]{chapter.1}{Introduction}{}% 1
\BOOKMARK [0][-]{chapter.2}{Motivation}{}% 2
\BOOKMARK [0][-]{chapter.3}{Related Work}{}% 3
\BOOKMARK [0][-]{chapter.4}{Theoretical Background}{}% 4
\BOOKMARK [1][-]{section.4.1}{Input/Output Extended Finite Automaton\(I/O-EFA\)}{chapter.4}% 5
\BOOKMARK [1][-]{section.4.2}{Input/Output Transition System}{chapter.4}% 6
\BOOKMARK [1][-]{section.4.3}{Simulation relation}{chapter.4}% 7
\BOOKMARK [0][-]{chapter.5}{Using Isabelle prove assistant for compatibility check}{}% 8
\BOOKMARK [1][-]{section.5.1}{Simulink components}{chapter.5}% 9
\BOOKMARK [1][-]{section.5.2}{Application of Isabelle}{chapter.5}% 10
\BOOKMARK [1][-]{section.5.3}{Global variables test using Isabelle theorem prover}{chapter.5}% 11
\BOOKMARK [0][-]{chapter.6}{Elimination of internal variables of I/O-EFA automatons that including non-linear parts}{}% 12
\BOOKMARK [1][-]{section.6.1}{Z3 Solver basics}{chapter.6}% 13
\BOOKMARK [1][-]{section.6.2}{Exemplified workflow of matching internal variables of I/O-EFAs containing non-linear dependencies}{chapter.6}% 14
\BOOKMARK [2][-]{subsection.6.2.1}{Previous approach}{section.6.2}% 15
\BOOKMARK [2][-]{subsection.6.2.2}{Automatons for comparison}{section.6.2}% 16
\BOOKMARK [2][-]{subsection.6.2.3}{First step of the procedure. Detecting non-linear equations.}{section.6.2}% 17
\BOOKMARK [2][-]{subsection.6.2.4}{Second step of the procedure. Calculation of linear coefficients.}{section.6.2}% 18
\BOOKMARK [2][-]{subsection.6.2.5}{Unfolding and simulation}{section.6.2}% 19
\BOOKMARK [0][-]{chapter.7}{Index tree optimization for transition filtering}{}% 20
\BOOKMARK [1][-]{section.7.1}{Previous approach of transition filtering optimization}{chapter.7}% 21
\BOOKMARK [1][-]{section.7.2}{Building of index tree}{chapter.7}% 22
\BOOKMARK [1][-]{section.7.3}{Evaluation}{chapter.7}% 23
\BOOKMARK [0][-]{chapter.8}{Clone detection and transformation to I/O-FEA of control flow graphs}{}% 24
\BOOKMARK [1][-]{section.8.1}{Approach with control flow graphs trees}{chapter.8}% 25
\BOOKMARK [1][-]{section.8.2}{Applied approach for substitution, clone detection and separation on output port basis}{chapter.8}% 26
\BOOKMARK [2][-]{subsection.8.2.1}{Substitution}{section.8.2}% 27
\BOOKMARK [2][-]{subsection.8.2.2}{Clone detection}{section.8.2}% 28
\BOOKMARK [2][-]{subsection.8.2.3}{Separation on output port basis}{section.8.2}% 29
\BOOKMARK [1][-]{section.8.3}{Improvements}{chapter.8}% 30
\BOOKMARK [0][-]{chapter.9}{Disjunctive Normal Form Optimization}{}% 31
\BOOKMARK [1][-]{section.9.1}{1st Step: Guard to Guard Normal Form \(GNF\) Transformation}{chapter.9}% 32
\BOOKMARK [1][-]{section.9.2}{2nd Step: Guard-NF to Guard Disjunctive Normal Form \(GDNF\) Transformation}{chapter.9}% 33
\BOOKMARK [2][-]{subsection.9.2.1}{3rd Step: Guard-DNF to Hash-Guard Disjunctive Normal Form \(HGDNF\) Transformation}{section.9.2}% 34
\BOOKMARK [2][-]{subsection.9.2.2}{4th Step: HGDNF to Optimized HGDNF Transformation}{section.9.2}% 35
\BOOKMARK [0][-]{chapter.10}{Code Listings}{}% 36
\BOOKMARK [1][-]{section.10.1}{Isabelle listing}{chapter.10}% 37
\BOOKMARK [1][-]{section.10.2}{Z3 listings}{chapter.10}% 38
\BOOKMARK [1][-]{section.10.3}{Java listings}{chapter.10}% 39
\BOOKMARK [0][-]{chapter.11}{Zusammenfassung und Ausblick}{}% 40
\BOOKMARK [0][-]{figure.caption.25}{Literaturverzeichnis}{}% 41
\BOOKMARK [0][-]{appendix.A}{z.B. Programmdokumentation}{}% 42
\documentclass[a4paper,11pt,oneside,openright]{report}
\usepackage{graphicx}
%\usepackage{ngerman}
\usepackage[utf8x]{inputenc}
\usepackage{fancyvrb}
\usepackage{courier}
\usepackage{helvet}
\usepackage{tikz}
\usepackage{xcolor}
\usepackage{pdfpages}
\usepackage[strict]{changepage}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{booktabs, multicol, multirow, bigstrut}
\usepackage{amsmath}
\usepackage{bm}
\usepackage{booktabs, multicol, multirow, bigstrut}
\usepackage{enumitem}
\usepackage{helvet}
\newsavebox\MBox
\newcommand\Cline[2][red]{{\sbox\MBox{$#2$}%
\rlap{\usebox\MBox}\color{#1}\rule[-1.2\dp\MBox]{\wd\MBox}{0.5pt}}}
\pdfoptionpdfminorversion=6
% \definecolor{se_dark_blue}{RGB}{0,103,166} % powerpoint
\definecolor{se_dark_blue}{RGB}{0,96,178} % website
% \definecolor{se_light_blue}{RGB}{119,158,201} % powerpoint
\definecolor{se_light_blue}{RGB}{129,160,225} % website
%% setup listings
\usepackage{listings}
\lstset{
numbers=left,
numberstyle=\tiny,
numbersep=5pt,
xleftmargin=11pt,
xrightmargin=4pt,
frame=single,
aboveskip=0pt,
belowskip=-6pt,
sensitive=true,
float=!t,
breaklines=false,
captionpos=b,
tabsize=2,
showstringspaces=false,
basicstyle=\small\ttfamily,
morecomment=[l]{//},
morecomment=[s][\itshape]{/**}{*/}
}
%% defines the listings laguage named 'MontiArc' derived from the language 'Java'
%% adding the below listed keywords. See
%% ftp://ftp.tex.ac.uk/tex-archive/macros/latex/contrib/listings/listings.pdf
%% for listings documentation
\lstdefinelanguage{MontiArc}[]{Java}{
morekeywords={component, port, in, out, inv, package, import, connect, autoconnect}
}
% Seite einrichten
\setlength{\voffset}{-1in}
\setlength{\hoffset}{-1in}
\setlength{\topmargin}{2.5cm}
\setlength{\headheight}{0cm}
\setlength{\headsep}{0cm}
\setlength{\oddsidemargin}{3,3cm} % innen ein wenig mehr Rand für die Klebebindung
\setlength{\evensidemargin}{2,7cm} % dafür außen ein wenig weniger
\setlength{\textwidth}{15cm}
\setlength{\textheight}{23,5cm}
\setlength{\parindent}{0cm}
\newcommand{\emptyLine}{{\LARGE ~\\}}
\begin{document}
% Einrücken von Absätzen verhindern und 1.5 Zeilen Absatzabstand
\setlength{\parindent}{0pt}
\setlength{\parskip}{1.5ex plus0.5ex minus0.5ex}
% \input{src/tex/cover_de}
\input{src/tex/cover_en} % English cover
\clearpage
% Erklaerung
\includepdf[pages={1},offset=2.5cm -2.5cm]{Formular_Eidesstattliche_Versicherung_neu.pdf}
\clearpage
\input{src/tex/abstract}
\tableofcontents
\clearpage
% Ab erstem Kapitel Seiten arabisch zählen
\setcounter{page}{1}
\pagenumbering{arabic}
\input{src/tex/Introduction}
%\input{src/tex/Motivation}
%\input{src/tex/RelatedWork}
%\input{src/tex/TheoreticalBackground} - schemes Client/Server architecture etc. (vs Peer-to-peer)
%\input{src/tex/Isabelle} FIXME explain about SmartFox and ThreeJS
%\input{src/tex/ExampleDescription} FIXME (Simulator Description) explain about the whole simulator concept (server + client)
% TODO specific things for this topic only
% - Zone separation - Voronoi vs Delaunay triangulation vs Square simple approach + Overlapping
% - MMO principles - AoI, zoning, sharding, cloning, etc.
% - World building and loading
% - Room synchronizations - transfering car from one room to another
% - configuration loading, scenario creation/upload etc.
% - security - WebScoket protocol, handshake, user info, user variables/properties, events (server/client side), Serialization - SFSObjects
% - performance - WS binary protocol, auto-world loading, DB optimization
%\input{src/tex/listings}
%\input{src/tex/conclusion}
% TODO future work
\bibliographystyle{alpha}
\addcontentsline{toc}{chapter}{Bibliography}
\bibliography{src/bib/Literatur}
% Begin Anhang
%\appendix
%\input{src/tex/appendix_docu}
\end{document}
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}
\contentsline {chapter}{\numberline {1}Einleitung}{1}{chapter.1}
\contentsline {section}{\numberline {1.1}Eins - Eins}{1}{section.1.1}
\contentsline {subsection}{\numberline {1.1.1}Eins - Eins - Eins}{1}{subsection.1.1.1}
\contentsline {chapter}{\numberline {2}Z3 theorem solver}{3}{chapter.2}
\contentsline {section}{\numberline {2.1}Z3 basics}{3}{section.2.1}
\contentsline {chapter}{\numberline {3}Elimination of internal variables of automatons that including non-linear parts}{5}{chapter.3}
\contentsline {section}{\numberline {3.1}Exemplified workflow of matching internal variables }{5}{section.3.1}
\contentsline {subsection}{\numberline {3.1.1}Automatons for comparison}{5}{subsection.3.1.1}
\contentsline {subsection}{\numberline {3.1.2}First step of the procedure. Detecting non-linear equations.}{5}{subsection.3.1.2}
\contentsline {subsection}{\numberline {3.1.3}Second step of the procedure. Calculation of non linear coefficients.}{7}{subsection.3.1.3}
\contentsline {subsection}{\numberline {3.1.4}Unfolding and simulation}{7}{subsection.3.1.4}
\contentsline {chapter}{\numberline {4}Code Listings}{9}{chapter.4}
\contentsline {chapter}{\numberline {5}Zusammenfassung und Ausblick}{11}{chapter.5}
\contentsline {chapter}{Literaturverzeichnis}{13}{figure.caption.11}
\contentsline {chapter}{\numberline {A}z.\,B. Programmdokumentation}{15}{appendix.A}
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}
\contentsline {chapter}{\numberline {2}Related Work}{3}{chapter.2}
\contentsline {chapter}{\numberline {3}Theoretical Background}{6}{chapter.3}
\contentsline {section}{\numberline {3.1}Input/Output Extended Finite Automaton(I/O-EFA)}{6}{section.3.1}
\contentsline {section}{\numberline {3.2}Input/Output Transition System}{6}{section.3.2}
\contentsline {section}{\numberline {3.3}Simulation relation}{6}{section.3.3}
\contentsline {chapter}{\numberline {4}Using Isabelle prove assistant for compatibility check}{7}{chapter.4}
\contentsline {section}{\numberline {4.1}Simulink components}{7}{section.4.1}
\contentsline {section}{\numberline {4.2}Application of Isabelle}{9}{section.4.2}
\contentsline {section}{\numberline {4.3}Global variables test using Isabelle theorem prover}{10}{section.4.3}
\contentsline {chapter}{\numberline {5}Elimination of internal variables of I/O-EFA automatons that including non-linear parts}{12}{chapter.5}
\contentsline {section}{\numberline {5.1}Z3 Solver basics}{12}{section.5.1}
\contentsline {section}{\numberline {5.2}Exemplified workflow of matching internal variables of I/O-EFAs containing non-linear dependencies}{14}{section.5.2}
\contentsline {subsection}{\numberline {5.2.1}Previous approach}{14}{subsection.5.2.1}
\contentsline {subsection}{\numberline {5.2.2}Automatons for comparison}{15}{subsection.5.2.2}
\contentsline {subsection}{\numberline {5.2.3}First step of the procedure. Detecting non-linear equations.}{15}{subsection.5.2.3}
\contentsline {subsection}{\numberline {5.2.4}Second step of the procedure. Calculation of linear coefficients.}{17}{subsection.5.2.4}
\contentsline {subsection}{\numberline {5.2.5}Unfolding and simulation}{17}{subsection.5.2.5}
\contentsline {chapter}{\numberline {6}Index tree optimization for transition filtering}{20}{chapter.6}
\contentsline {section}{\numberline {6.1}Previous approach of transition filtering optimization}{20}{section.6.1}
\contentsline {section}{\numberline {6.2}Building of index tree}{21}{section.6.2}
\contentsline {section}{\numberline {6.3}Evaluation}{23}{section.6.3}
\contentsline {chapter}{\numberline {7}Clone detection and transformation to I/O-FEA of control flow graphs}{26}{chapter.7}
\contentsline {section}{\numberline {7.1}Approach with control flow graphs trees}{26}{section.7.1}
\contentsline {section}{\numberline {7.2}Applied approach for substitution, clone detection and separation on output port basis}{29}{section.7.2}
\contentsline {subsection}{\numberline {7.2.1}Substitution}{29}{subsection.7.2.1}
\contentsline {subsection}{\numberline {7.2.2}Clone detection}{30}{subsection.7.2.2}
\contentsline {subsection}{\numberline {7.2.3}Separation on output port basis}{31}{subsection.7.2.3}
\contentsline {section}{\numberline {7.3}Improvements}{32}{section.7.3}
\contentsline {chapter}{\numberline {8}Disjunctive Normal Form Optimization}{33}{chapter.8}
\contentsline {section}{\numberline {8.1}1st Step: Guard to Guard Normal Form (GNF) Transformation}{33}{section.8.1}
\contentsline {section}{\numberline {8.2}2nd Step: Guard-NF to Guard Disjunctive Normal Form (GDNF) Transformation}{34}{section.8.2}
\contentsline {subsection}{\numberline {8.2.1}3rd Step: Guard-DNF to Hash-Guard Disjunctive Normal Form (HGDNF) Transformation}{34}{subsection.8.2.1}
\contentsline {subsection}{\numberline {8.2.2}4th Step: HGDNF to Optimized HGDNF Transformation}{36}{subsection.8.2.2}
\contentsline {chapter}{\numberline {9}Code Listings}{37}{chapter.9}
\contentsline {section}{\numberline {9.1}Isabelle listing}{37}{section.9.1}
\contentsline {section}{\numberline {9.2}Z3 listings}{38}{section.9.2}
\contentsline {section}{\numberline {9.3}Java listings}{42}{section.9.3}
\contentsline {chapter}{\numberline {10}Zusammenfassung und Ausblick}{44}{chapter.10}
\contentsline {chapter}{Literaturverzeichnis}{45}{figure.caption.23}
\contentsline {chapter}{\numberline {A}z.\tmspace +\thinmuskip {.1667em}B. Programmdokumentation}{49}{appendix.A}
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}
\contentsline {chapter}{\numberline {2}Motivation}{3}{chapter.2}
\contentsline {chapter}{\numberline {3}Related Work}{7}{chapter.3}
\contentsline {chapter}{\numberline {4}Theoretical Background}{10}{chapter.4}
\contentsline {section}{\numberline {4.1}Input/Output Extended Finite Automaton(I/O-EFA)}{10}{section.4.1}
\contentsline {section}{\numberline {4.2}Input/Output Transition System}{10}{section.4.2}
\contentsline {section}{\numberline {4.3}Simulation relation}{10}{section.4.3}
\contentsline {chapter}{\numberline {5}Using Isabelle prove assistant for compatibility check}{11}{chapter.5}
\contentsline {section}{\numberline {5.1}Simulink components}{11}{section.5.1}
\contentsline {section}{\numberline {5.2}Application of Isabelle}{13}{section.5.2}
\contentsline {section}{\numberline {5.3}Global variables test using Isabelle theorem prover}{14}{section.5.3}
\contentsline {chapter}{\numberline {6}Elimination of internal variables of I/O-EFA automatons that including non-linear parts}{16}{chapter.6}
\contentsline {section}{\numberline {6.1}Z3 Solver basics}{16}{section.6.1}
\contentsline {section}{\numberline {6.2}Exemplified workflow of matching internal variables of I/O-EFAs containing non-linear dependencies}{18}{section.6.2}
\contentsline {subsection}{\numberline {6.2.1}Previous approach}{18}{subsection.6.2.1}
\contentsline {subsection}{\numberline {6.2.2}Automatons for comparison}{19}{subsection.6.2.2}
\contentsline {subsection}{\numberline {6.2.3}First step of the procedure. Detecting non-linear equations.}{19}{subsection.6.2.3}
\contentsline {subsection}{\numberline {6.2.4}Second step of the procedure. Calculation of linear coefficients.}{21}{subsection.6.2.4}
\contentsline {subsection}{\numberline {6.2.5}Unfolding and simulation}{21}{subsection.6.2.5}
\contentsline {chapter}{\numberline {7}Index tree optimization for transition filtering}{24}{chapter.7}
\contentsline {section}{\numberline {7.1}Previous approach of transition filtering optimization}{24}{section.7.1}
\contentsline {section}{\numberline {7.2}Building of index tree}{25}{section.7.2}
\contentsline {section}{\numberline {7.3}Evaluation}{27}{section.7.3}
\contentsline {chapter}{\numberline {8}Clone detection and transformation to I/O-FEA of control flow graphs}{30}{chapter.8}
\contentsline {section}{\numberline {8.1}Approach with control flow graphs trees}{30}{section.8.1}
\contentsline {section}{\numberline {8.2}Applied approach for substitution, clone detection and separation on output port basis}{33}{section.8.2}
\contentsline {subsection}{\numberline {8.2.1}Substitution}{33}{subsection.8.2.1}
\contentsline {subsection}{\numberline {8.2.2}Clone detection}{34}{subsection.8.2.2}
\contentsline {subsection}{\numberline {8.2.3}Separation on output port basis}{35}{subsection.8.2.3}
\contentsline {section}{\numberline {8.3}Improvements}{36}{section.8.3}
\contentsline {chapter}{\numberline {9}Disjunctive Normal Form Optimization}{37}{chapter.9}
\contentsline {section}{\numberline {9.1}1st Step: Guard to Guard Normal Form (GNF) Transformation}{37}{section.9.1}
\contentsline {section}{\numberline {9.2}2nd Step: Guard-NF to Guard Disjunctive Normal Form (GDNF) Transformation}{38}{section.9.2}
\contentsline {subsection}{\numberline {9.2.1}3rd Step: Guard-DNF to Hash-Guard Disjunctive Normal Form (HGDNF) Transformation}{38}{subsection.9.2.1}
\contentsline {subsection}{\numberline {9.2.2}4th Step: HGDNF to Optimized HGDNF Transformation}{40}{subsection.9.2.2}
\contentsline {chapter}{\numberline {10}Code Listings}{41}{chapter.10}
\contentsline {section}{\numberline {10.1}Isabelle listing}{41}{section.10.1}
\contentsline {section}{\numberline {10.2}Z3 listings}{42}{section.10.2}
\contentsline {section}{\numberline {10.3}Java listings}{46}{section.10.3}
\contentsline {chapter}{\numberline {11}Zusammenfassung und Ausblick}{48}{chapter.11}
\contentsline {chapter}{Literaturverzeichnis}{49}{figure.caption.25}
\contentsline {chapter}{\numberline {A}z.\tmspace +\thinmuskip {.1667em}B. Programmdokumentation}{53}{appendix.A}
#!/bin/bash
# biblatex runs latex and bibtex as often as necessary,
# It detects citation problems and in this case reruns bibtex.
# It detects label-changes and reruns latex (up to 3 times),
# However, if labels are defined twice, it always runs latex three times.
#
# REMARK: a slightly changed bibliography does not cause a bibtex call
# because this is not detected.
#
# BUG: (from latex:) A changed (sub..) section name is not recognised and
# therefore the last run incorporating the changed table of contents (toc)
# not executed.
#
if [ $# -eq 1 ]
then
datei=`dirname $1`/`basename $1 .tex`
latex=latex
elif [ $# -eq 2 ]
then
datei=`dirname $2`/`basename $2 .tex`
latex=$1
else
echo 'usage: $0 [latex-command] latex-file[.tex]'
exit 1
fi
temp=$datei.blx
echo $0: $latex $datei \(pass 1 is always performed\)
$latex $datei
error=$?
if [ $error -ne 0 ]
then exit $error
fi
# part 1: expand of all .aux files in $temp
grep '\\@input{' $datei.aux \
| sed -e 's/\\@input{//g' -e 's/}//g' > $temp.2
echo $0: Expanding .aux-files: $datei.aux `cat $temp.2`
cat $datei.aux `cat $temp.2` > $temp
rm $temp.2
# is there a bibliography entry? (else skip 2-5)
grep '\\bibdata{' $temp >/dev/null
if [ $? -eq 0 ]
then
# part 2: actual and desired citations in $temp.4 and $temp.5
grep '\\citation{' $temp \
| sed -e 's/\\citation{//g' -e 's/}//g' \
| sort -u > $temp.4
grep '\\bibcite{' $temp \
| sed -e 's/\\bibcite{//g' -e 's/}.*$//g' \
| sort -u > $temp.5
echo $0: Required citations: `cat $temp.4 | wc -l`
echo $0: Given citations: `cat $temp.5 | wc -l`
diff $temp.4 $temp.5 >/dev/null
diffs=$?
rm $temp.4 $temp.5
# part 3: check are there citation problems?
grep 'Citation .* undefined' $datei.log >/dev/null
citations=$?
# part 4: is a bib-file newer than the bbl-file?
grep '\\bibdata{' $temp \
| sed -e 's/\\bibdata{//g' -e 's/}/.bib/g' -e 's/,/.bib\
/g' > $temp.2
bibfilenew=0
for i in `cat $temp.2`
do
if [ $i -nt $datei.bbl ]
then
bibfilenew=1
fi
done
rm $temp.2
# part 5: execute bibtex
if [ $citations -eq 0 -o $diffs -ne 0 -o $bibfilenew -eq 0 ]
then
echo $0: bibtex $datei \(citation problems and bibliography entries\)
bibtex $datei
error=$?
if [ $error -ne 0 ]
then exit $error
fi
echo $0: $latex $datei \(because of citation problems\)
$latex $datei
error=$?
if [ $error -ne 0 ]
then exit $error
fi
fi
fi
# part 6: three times repeat, to get cross-references right
for i in 1 2 3
do
grep 'Rerun to get cross-references right' $datei.log >/dev/null
if [ $? -eq 0 ]
then
echo $0: $latex $datei \(to get cross-references right, pass $i\)
$latex $datei
error=$?
if [ $error -ne 0 ]
then exit $error
fi
fi
done
%1 --login -i -c 'make --directory="%2" %3'
\ No newline at end of file
######################################################################
#
# makefile
# fuer normale Latex-Projekte mit ppt-Bildern
#
# Anzupassen sind: TARGET, SOURCES, PICSPPT
# (und sonst normalerweise nichts, also nur die
# folgenden vier Zeilen)
# Ziel:
TARGET=Masterarbeit.pdf
SOURCES=$(wildcard *.tex) $(wildcard tex/*.tex)
PICSPPT=$(wildcard src/pic/*.ppt)
PICSPPTX=$(shell find src/pic/ -regex "[^~]*\.pptx" -type f)
BIB=src/bib/Literatur.bib
IMG=$(wildcard img/*.*)
LISTINGS=$(wildcard src/listings/*.*) $(wildcard lst/*.*)
######################################################################
# alles zusammen (und am Ende einige Hilfsinfos ausgeben)
all: at-start check-commands $(TARGET) warnings
@echo --------------------------
@echo ghostview $(TARGET) \&
@echo gmake clean
# Zu Beginn einige Hilfsinfos ausgeben
at-start:
@echo target: $(TARGET)
@echo tex-files: $(SOURCES)
@echo ppt: $(PICSPPT)
@echo pptx: $(PICSPPTX)
@echo imgs: $(IMG)
.SUFFIXES: $(SUFFIXES) .ppt .gflag .pptx .gxflag .tex .eps .ps .pdf
.PHONY : all at-start clean warnings check-commands biblatex
# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
# generate pics from ppt:
.ppt.gflag:
mkdir -p gen
@echo do ppt2eps $< -o gen
@java -jar commands/ppt2eps/ostp-client-ppt2eps-2.3.4.jar $< -o gen 2> gen/ppt2eps.log
touch $@
# generate pics from pptx:
.pptx.gxflag:
@mkdir -p gen
@echo do ppt2eps $< -o gen
@java -jar commands/ppt2eps/ostp-client-ppt2eps-2.3.4.jar $< -o gen 2> gen/ppt2eps.log
@touch $@
# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
$(TARGET): $(SOURCES) $(BIB) $(PICSPPT:.ppt=.gflag) $(PICSPPTX:.pptx=.gxflag) $(LISTINGS) $(IMG)
./commands/biblatex pdflatex $(TARGET:.pdf=)
pics: at-start $(PICSPPT:.ppt=.gflag) $(PICSPPTX:.pptx=.gxflag)
# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
# ueberfluessigen Schrott loeschen
clean:
@rm -f $(TARGET:.pdf=.aux) $(TARGET:.pdf=.blx) $(TARGET:.pdf=.dvi)
@rm -f $(TARGET:.pdf=.idx) $(TARGET:.pdf=.log) $(TARGET:.pdf=.pdf)
@rm -f $(TARGET:.pdf=.toc) $(TARGET:.pdf=.pdf) $(TARGET:.pdf=.blg)
@rm -f $(TARGET:.pdf=.bbl)
@rm -f $(SOURCES:.tex=.aux)
@rm -f *.bak *~
cleanAll: clean
@rm -rf gen
@rm -f $(PICSPPT:.ppt=.gflag) $(PICSPPTX:.pptx=.gxflag)
# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
# latex-Warnings nochmal kompakt ausgeben:
warnings:
@-echo "------------ Warnings from bib:"
@-grep arning $(TARGET:.pdf=.blg)
@-echo "------------ Warnings from latex:"
@-grep arning: $(TARGET:.pdf=.log) | wc -l
@awk '/arning:/' RS= $(TARGET:.pdf=.log)
# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
# check, ob Kommandos existieren
COMMANDS=latex bibtex grep rm # biblatex