Commit 9e266e92 authored by Bernhard Rumpe's avatar Bernhard Rumpe


parent e925381d
Pipeline #175515 failed with stage
in 56 seconds
# ******************************************************************************
# MontiCAR Modeling Family,
# Copyright (c) 2017, Software Engineering Group at RWTH Aachen,
# All rights reserved.
# This project is free software; you can redistribute it and/or
# modify it under the terms of the GNU Lesser General Public
# License as published by the Free Software Foundation; either
# version 3.0 of the License, or (at your option) any later version.
# This library is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# Lesser General Public License for more details.
# You should have received a copy of the GNU Lesser General Public
# License along with this project. If not, see <>.
# *******************************************************************************
image: maven:3-jdk-8 image: maven:3-jdk-8
This diff is collapsed.
Miha Ambroz, S.~Krasna, and Ivan Prebil.
\newblock 3d road traffic situation simulation system.
\newblock {\em Advances in Engineering Software}, 36(2):77--86, 2005.
Marios Assiotis and Velin Tzanov.
\newblock A distributed architecture for massive multiplayer online
role-playing games.
\newblock May 2005.
Arvid Butting, Oliver Kautz, Bernhard Rumpe, and Andreas Wortmann.
\newblock {Architectural Programming with MontiArcAutomaton}.
\newblock In {\em In 12th International Conference on Software Engineering
Advances (ICSEA 2017)}, pages 213--218. IARIA XPS Press, May 2017.
Christian Berger and Bernhard Rumpe.
\newblock Engineering autonomous driving software.
\newblock {\em CoRR}, abs/1409.6579, 2014.
Sergio Caltagirone, Matthew Keys, Bryan Schlief, and Mary~Jane Willshire.
\newblock Architecture for a massively multiplayer online role playing game
\newblock {\em J. Comput. Sci. Coll.}, 18(2):105--116, December 2002.
Patrick Cozzi.
\newblock {\em {W}eb{GL} {I}nsights}.
\newblock CRC Press, July 2015.
\newblock \url{}.
{\em Proceedings {IEEE} {INFOCOM} 2004, The 23rd Annual Joint Conference of the
{IEEE} Computer and Communications Societies, Hong Kong, China, March 7-11,
2004}. {IEEE}, 2004.
Edsger~W. Dijkstra.
\newblock {\em Selected Writings on Computing: {A} Personal Perspective}.
\newblock Texts and Monographs in Computer Science. Springer, 1982.
\newblock {\em Three.js Essentials}.
\newblock Community experience distilled. Packt Publishing, 2014.
Kurt~M. Dresner and Peter Stone.
\newblock Sharing the road: Autonomous vehicles meet human drivers.
\newblock In {\em {IJCAI} 2007, Proceedings of the 20th International Joint
Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007},
pages 1263--1268, 2007.
\newblock {\em Jetty Web-server}.
I.~Fette and A.~Melnikov.
\newblock The websocket protocol.
\newblock RFC 6455, RFC Editor, December 2011.
\newblock \url{}.
Steven Fortune.
\newblock Voronoi diagrams and delaunay triangulations.
\newblock In {\em Handbook of Discrete and Computational Geometry, Second
Edition.}, pages 513--528. 2004.
Martin Fowler.
\newblock {\em Patterns of enterprise application architecture}.
\newblock Addison-Wesley, Boston, 2003.
Stefan~A. Fiedler, Michael Wallner, and Michael Weber.
\newblock A communication architecture for massive multiplayer games.
\newblock In {\em Proceedings of the 1st Workshop on Network and System Support
for Games, {NETGAMES} 2002, Braunschweig, Germany, April 16-17, 2002, 2003},
pages 14--22, 2002.
Erich Gamma.
\newblock {\em Design patterns : elements of reusable object-oriented
\newblock Addison-Wesley, Reading, Mass, 1995.
Laurent Gautier and Christophe Diot.
\newblock Design and evaluation of mimaze, a multi-player game on the internet.
\newblock In {\em {IEEE} International Conference on Multimedia Computing and
Systems, {ICMCS} 1998, Austin, Texas, USA, June 28 - July 1, 1998}, pages
233--236, 1998.
\newblock {\em SmartFox Server 2X}.
Sebastien Glaser, Benoit Vanholme, Sa{\"{\i}}d Mammar, Dominique Gruyer, and
Lydie Nouveliere.
\newblock Maneuver-based trajectory planning for highly autonomous vehicles on
real road with traffic and driver interaction.
\newblock {\em {IEEE} Trans. Intelligent Transportation Systems},
11(3):589--606, 2010.
George~T. Heineman, Gary Pollice, and Stanley~M. Selkow.
\newblock {\em Algorithms in a nutshell - a desktop quick reference}.
\newblock O'Reilly, 2009.
Jaecheol Kim, Jaeyoung Choi, Dukhyun Chang, Taekyoung Kwon, Yanghee Choi, and
Eungsu Yuk.
\newblock Traffic characteristics of a massively multi-player online role
playing game.
\newblock In {\em Proceedings of the 4th Workshop on Network and System Support
for Games, {NETGAMES} 2005, Hawthorne, New York, USA, October 10-11, 2005},
pages 1--8, 2005.
Kang{-}Won Lee, Bong{-}Jun Ko, and Seraphin~B. Calo.
\newblock Adaptive server selection for large scale interactive online games.
\newblock {\em Computer Networks}, 49(1):84--102, 2005.
Jens M{\"{u}}ller and Sergei Gorlatch.
\newblock A scalable architecture for multiplayer computer games.
\newblock In {\em {INFORMATIK} 2004 - Informatik verbindet, Band 1,
Beitr{\"{a}}ge der 34. Jahrestagung der Gesellschaft f{\"{u}}r Informatik
e.V. (GI), Ulm, 20.-24. September 2004}, pages 154--158, 2004.
Beatrice Ng, Antonio Si, Rynson W.~H. Lau, and Frederick W.~B. Li.
\newblock A multi-server architecture for distributed virtual walkthrough.
\newblock In {\em Proceedings of the {ACM} Symposium on Virtual Reality
Software and Technology, {VRST} 2002, Hong Kong, China, November 11-13,
2002}, pages 163--170, 2002.
\newblock {\em PostgreSQL}.
A.A. Puntambekar.
\newblock {\em Data Structures And Algorithms}.
\newblock Technical Publications, 2009.
Fred~W. Rauskolb, Kai Berger, Christian Lipski, Marcus~A. Magnor, Karsten
Cornelsen, Jan Effertz, Thomas Form, Fabian Graefe, Sebastian Ohl, Walter
Schumacher, J{\"{o}}rn{-}Marten Wille, Peter Hecker, Tobias Nothdurft,
Michael Doering, Kai Homeier, Johannes Morgenroth, Lars~C. Wolf, Christian
Basarke, Christian Berger, Tim G{\"{u}}lke, Felix Klose, and Bernhard Rumpe.
\newblock Caroline: An autonomously driving vehicle for urban environments.
\newblock {\em J. Field Robotics}, 25(9):674--724, 2008.
George Reese.
\newblock {\em Database programming with {JDBC} and Java {(2.} ed.)}.
\newblock O'Reilly, 2000.
\newblock {\em Simple (or Streaming) Text Orientated Messaging Protocol}.
Richard~N. Taylor, Nenad Medvidovic, and Eric~M. Dashofy.
\newblock {\em Software Architecture: Foundations, Theory and Practice}.
\newblock Addison-Wesley, 2007.
Andrew~S. Tanenbaum and David Wetherall.
\newblock {\em Computer networks, 5th Edition}.
\newblock Pearson, 2011.
Chris Urmson, Joshua Anhalt, Drew Bagnell, Christopher~R. Baker, Robert
Bittner, M.~N. Clark, John~M. Dolan, Dave Duggins, Tugrul Galatali,
Christopher Geyer, Michele Gittleman, Sam Harbaugh, Martial Hebert, Thomas~M.
Howard, Sascha Kolski, Alonzo Kelly, Maxim Likhachev, Matthew McNaughton,
Nick Miller, Kevin~M. Peterson, Brian Pilnick, Raj Rajkumar, Paul~E. Rybski,
Bryan Salesky, Young{-}Woo Seo, Sanjiv Singh, Jarrod~M. Snider, Anthony
Stentz, William Whittaker, Ziv Wolkowicki, Jason Ziglar, Hong Bae, Thomas
Brown, Daniel Demitrish, Bakhtiar Litkouhi, Jim Nickolaou, Varsha Sadekar,
Wende Zhang, Joshua Struble, Michael Taylor, Michael Darms, and Dave
\newblock Autonomous driving in urban environments: Boss and the urban
\newblock {\em J. Field Robotics}, 25(8):425--466, 2008.
Craig Walls.
\newblock {\em Spring in action}.
\newblock Manning Publications, Shelter Island, N.Y, 2015.
This is BibTeX, Version 0.99d (TeX Live 2016/Debian)
Capacity: max_strings=100000, hash_size=100000, hash_prime=85009
The top-level auxiliary file: ./Masterarbeit.aux
The style file: alpha.bst
Database file #1: src/bib/Literatur.bib
Warning--to sort, need editor, organization, or key in DBLP:conf/infocom/2004
Warning--empty booktitle in DAfMMO-RPG
Warning--empty publisher in DBLP:reference/cg/Fortune04
You've used 33 entries,
2543 wiz_defined-function locations,
756 strings with 11529 characters,
and the built_in function-call counts, 14387 in all, are:
= -- 1362
> -- 843
< -- 18
+ -- 308
- -- 303
* -- 1075
:= -- 2359
add.period$ -- 100
call.type$ -- 33$ -- 245$ -- 33
cite$ -- 37
duplicate$ -- 562
empty$ -- 982$ -- 336
if$ -- 2922$ -- 1$ -- 0
missing$ -- 38
newline$ -- 165
num.names$ -- 84
pop$ -- 300
preamble$ -- 1
purify$ -- 294
quote$ -- 0
skip$ -- 442
stack$ -- 0
substring$ -- 626
swap$ -- 108
text.length$ -- 18
text.prefix$ -- 13
top$ -- 0
type$ -- 218
warning$ -- 3
while$ -- 111
width$ -- 38
write$ -- 409
(There were 3 warnings)
This diff is collapsed.
This diff is collapsed.
\BOOKMARK [0][-]{chapter.1}{Introduction}{}% 1
\BOOKMARK [0][-]{chapter.2}{Preliminaries}{}% 2
\BOOKMARK [1][-]{section.2.1}{Massive multiplayer online gaming}{chapter.2}% 3
\BOOKMARK [1][-]{section.2.2}{Area of Interest}{chapter.2}% 4
\BOOKMARK [1][-]{section.2.3}{Architectures}{chapter.2}% 5
\BOOKMARK [2][-]{subsection.2.3.1}{Peer-to-peer}{section.2.3}% 6
\BOOKMARK [2][-]{subsection.2.3.2}{Client/server}{section.2.3}% 7
\BOOKMARK [1][-]{section.2.4}{Distributing mechanisms}{chapter.2}% 8
\BOOKMARK [2][-]{subsection.2.4.1}{Sharding}{section.2.4}% 9
\BOOKMARK [2][-]{subsection.2.4.2}{Cloning}{section.2.4}% 10
\BOOKMARK [2][-]{subsection.2.4.3}{Zoning}{section.2.4}% 11
\BOOKMARK [2][-]{subsection.2.4.4}{Instancing}{section.2.4}% 12
\BOOKMARK [1][-]{section.2.5}{Advanced distributed architectures}{chapter.2}% 13
\BOOKMARK [2][-]{subsection.2.5.1}{Proxy-server architecture}{section.2.5}% 14
\BOOKMARK [2][-]{subsection.2.5.2}{Distributed architecture combined with zoning technique}{section.2.5}% 15
\BOOKMARK [1][-]{section.2.6}{Model-View-Controller pattern}{chapter.2}% 16
\BOOKMARK [0][-]{chapter.3}{Technical Requisites}{}% 17
\BOOKMARK [1][-]{section.3.1}{SmartFoxServer}{chapter.3}% 18
\BOOKMARK [2][-]{subsection.3.1.1}{Web Server}{section.3.1}% 19
\BOOKMARK [2][-]{subsection.3.1.2}{Web Services}{section.3.1}% 20
\BOOKMARK [2][-]{subsection.3.1.3}{Data serialization}{section.3.1}% 21
\BOOKMARK [2][-]{subsection.3.1.4}{Scope Management}{section.3.1}% 22
\BOOKMARK [2][-]{subsection.3.1.5}{Data access and server monitoring}{section.3.1}% 23
\BOOKMARK [1][-]{section.3.2}{ThreeJS}{chapter.3}% 24
\BOOKMARK [1][-]{section.3.3}{PostgreSQL database}{chapter.3}% 25
\BOOKMARK [0][-]{chapter.4}{Simulation Platform}{}% 26
\BOOKMARK [1][-]{section.4.1}{Challenges}{chapter.4}% 27
\BOOKMARK [1][-]{section.4.2}{Architecture}{chapter.4}% 28
\BOOKMARK [1][-]{section.4.3}{Basic work-flow}{chapter.4}% 29
\BOOKMARK [2][-]{subsection.4.3.1}{Zone level}{section.4.3}% 30
\BOOKMARK [2][-]{subsection.4.3.2}{Room level}{section.4.3}% 31
\BOOKMARK [1][-]{section.4.4}{Virtual World}{chapter.4}% 32
\BOOKMARK [2][-]{subsection.4.4.1}{Zoning approach}{section.4.4}% 33
\BOOKMARK [1][-]{section.4.5}{Path Finder}{chapter.4}% 34
\BOOKMARK [1][-]{section.4.6}{Database optimization}{chapter.4}% 35
\BOOKMARK [1][-]{section.4.7}{Web Communication}{chapter.4}% 36
\BOOKMARK [1][-]{section.4.8}{Simulation}{chapter.4}% 37
\BOOKMARK [2][-]{subsection.4.8.1}{Simulation Controller}{section.4.8}% 38
\BOOKMARK [2][-]{subsection.4.8.2}{Mediator}{section.4.8}% 39
\BOOKMARK [2][-]{subsection.4.8.3}{Scenarios}{section.4.8}% 40
\BOOKMARK [2][-]{subsection.4.8.4}{Synchronization and Visualization}{section.4.8}% 41
\BOOKMARK [1][-]{section.4.9}{Configuration}{chapter.4}% 42
\BOOKMARK [1][-]{section.4.10}{Security}{chapter.4}% 43
\BOOKMARK [0][-]{chapter.5}{Evaluation}{}% 44
\BOOKMARK [0][-]{chapter.6}{Future Work}{}% 45
\BOOKMARK [1][-]{section.6.1}{Single simulation per vehicle}{chapter.6}% 46
\BOOKMARK [1][-]{section.6.2}{Online model development, test and deployment}{chapter.6}% 47
\BOOKMARK [0][-]{chapter.7}{Conclusion}{}% 48
\BOOKMARK [0][-]{chapter.7}{Bibliography}{}% 49
\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
\usepackage{booktabs, multicol, multirow, bigstrut}
\usepackage{booktabs, multicol, multirow, bigstrut}
% \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
%% defines the listings laguage named 'MontiArc' derived from the language 'Java'
%% adding the below listed keywords. See
%% for listings documentation
morekeywords={component, port, in, out, inv, package, import, connect, autoconnect}
% Seite einrichten
\setlength{\oddsidemargin}{3,3cm} % innen ein wenig mehr Rand für die Klebebindung
\setlength{\evensidemargin}{2,7cm} % dafür außen ein wenig weniger
\newcommand{\emptyLine}{{\LARGE ~\\}}
% Einrücken von Absätzen verhindern und 1.5 Zeilen Absatzabstand
\setlength{\parskip}{1.5ex plus0.5ex minus0.5ex}
\input{src/tex/cover_en} % English cover
% Erklaerung
\includepdf[pages={1},offset=2.5cm -2.5cm]{Formular_Eidesstattliche_Versicherung_neu.pdf}
% Ab erstem Kapitel Seiten arabisch zählen
% Begin Anhang
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}
\contentsline {chapter}{\numberline {2}Preliminaries}{5}{chapter.2}
\contentsline {section}{\numberline {2.1}Massive multiplayer online gaming}{5}{section.2.1}
\contentsline {section}{\numberline {2.2}Area of Interest}{6}{section.2.2}
\contentsline {section}{\numberline {2.3}Architectures}{7}{section.2.3}
\contentsline {subsection}{\numberline {2.3.1}Peer-to-peer}{7}{subsection.2.3.1}