diff --git a/doc/AVATAR/Makefile b/doc/AVATAR/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..71b7245aa13e3bf2488c7a841c05d1954792ab75
--- /dev/null
+++ b/doc/AVATAR/Makefile
@@ -0,0 +1,7 @@
+
+FIGDIR := fig
+BUILDDIR := build
+
+include ../mli.mk
+
+$(BUILDDIR)/avatar_documentation.pdf: $(FIGURES)
diff --git a/doc/AVATAR/avatar_documentation.tex b/doc/AVATAR/avatar_documentation.tex
new file mode 100644
index 0000000000000000000000000000000000000000..9ea30807c7e7d5f79d2a5e3b21c29870d490ac18
--- /dev/null
+++ b/doc/AVATAR/avatar_documentation.tex
@@ -0,0 +1,613 @@
+\documentclass[12pt]{article}
+\usepackage{amsmath}
+\usepackage{latexsym}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{graphicx}
+\usepackage{txfonts}
+\usepackage{wasysym}
+\usepackage{adjustbox}
+\usepackage{ragged2e}
+\usepackage{tabularx}
+\usepackage{hhline}
+\usepackage{float}
+\usepackage{multirow}
+\usepackage{makecell}
+\usepackage{fancyhdr}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{listings}
+\usepackage[a4paper,bindingoffset=0.2in,headsep=0.5cm,left=1in,right=1in,bottom=3cm,top=2cm,headheight=2cm]{geometry}
+\usepackage{hyperref}
+\usepackage{listings}
+\usepackage[most]{tcolorbox}
+
+\lstset{language=C,basicstyle=\scriptsize\ttfamily,keywordstyle=\bfseries, commentstyle=\textit,stringstyle=\ttfamily, showspaces=false,showstringspaces=false, frame=single,
+ breaklines=true,
+ postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space},
+}
+
+\everymath{\displaystyle}
+\pagestyle{fancy}
+\fancyhf{}
+\rfoot{Page \thepage}
+\begin{document}
+\sloppy
+
+\begin{center}
+
+\includegraphics[width=0.2\textwidth]{fig/logotpt}
+\vspace{10 pt}\\
+\Huge TTool \\
+\vspace{10 pt}
+\Large \url{ttool.telecom-paristech.fr}
+\vspace{20 pt}\\
+\underline{\Large Use of TTool explained through the creation of a coffee machine.}
+\vspace{30 pt}
+\end{center}
+
+\begin{table}[H]
+\large
+\centering
+\begin{adjustbox}{width=\textwidth}
+\begin{tabular}{ |p{1.6cm}|p{6.0cm}|p{4.2cm}|p{4.2cm}| }
+\hhline{----}
+ & \textbf{Document Manager} & \textbf{Contributors} & \textbf{Checked by} \\
+\hhline{----}
+\textbf{Name} & Ludovic APVRILLE & \multirow{2}{4.2cm}{Christophe Manseau, Philippe Paquette,
+Ludovic APVRILLE} &
+\multirow{2}{*}{Ludovic APVRILLE} \\
+\hhline{--~~}
+\textbf{Contact} & ludovic.apvrille@telecom-paristech.fr & & \\
+\hhline{--~~}
+\textbf{Date} & \today & & \\
+\hline
+\end{tabular}
+\end{adjustbox}
+\end{table}
+
+\newpage
+\tableofcontents
+
+% \newpage
+% \listoffigures
+
+\newpage
+\section{Preface}
+
+\subsection{Table of Versions}
+
+\begin{table}[H]
+\large
+\centering
+\begin{adjustbox}{width=\textwidth}
+\begin{tabular}{ |p{1.5cm}|p{2.5cm}|p{9.0cm}|p{3.0cm}| }
+\hhline{----}
+\textbf{Version} & \textbf{Date} & \textbf{Description $ \& $ Rationale of
+Modifications} & \textbf{Sections Modified} \\
+\hhline{----}
+1.0 & July 7, 2018 & First draft & \\
+\hline
+\end{tabular}
+\end{adjustbox}
+\end{table}
+
+\subsection{Table of References and Applicable Documents}
+
+\begin{table}[H]
+\large
+\centering
+\begin{adjustbox}{width=\textwidth}
+\begin{tabular}{ |p{2.66in}|p{2.66in}|p{0.95in}|p{0.43in}| }
+\hhline{----}
+\textbf{Reference} & \textbf{Title $ \& $ Edition} & \textbf{Author or
+Editor} & \textbf{Year}
+\\
+\hhline{----}
+ & & & \\
+\hline
+\end{tabular}
+\end{adjustbox}
+\end{table}
+
+\subsection{Acronyms and glossary}
+
+\begin{table}[H]
+\large
+\centering
+\begin{adjustbox}{width=\textwidth}
+\begin{tabular}{ |p{1.24in}|p{5.45in}| }
+\hhline{--}
+\textbf{Term} & \textbf{Description} \\
+\hhline{--}
+ & \\
+\hline
+\end{tabular}
+\end{adjustbox}
+\end{table}
+
+\newpage
+\section{Introduction}
+
+TTool is an open-source toolkit dedicated to the design of embedded systems based on UML and SysML diagrams. The source files of TTool can be downloaded from the website: http://ttool.telecom-paristech.fr/download.html
+after having accepted the license agreement. To install the tool, simply unpack the archive in your home directory and follow the installation process of your operating system.
+
+\section{Getting Started}
+\subsection{Opening from terminal}
+
+After downloading it from the Internet, the most effective way to open TTool is to open it from your computer terminal. Open the folder in which the application is located and then open using the command:
+\begin{lstlisting}{bash}
+
+ start ttool_windows
+
+
+\end{lstlisting}
+
+or
+\begin{lstlisting}{bash}
+
+open ttool_macosx
+
+
+\end{lstlisting}
+
+or \begin{lstlisting}{bash}
+
+Run ttool_linux
+
+\end{lstlisting}
+
+
+\subsection{Start new project}
+To create a new project, click on the “new†button as shown in Figure \ref{fig:createfile} below or select file and then new on the main tab. As shown in Figure \ref{fig:createmethod}, the main TTool window contains three different areas, the Project navigation window, the Design window and the Map view window; allowing the user to navigate through the files of the project and rapidly search for elements of a design, observe and create the SysML diagrams of the design, and have a bird’s eye view of the current diagram respectively.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/createfile.png}
+\caption{Create a file} \label{fig:createfile}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/createmethod.png}
+\caption{Create an AVATAR Methodology} \label{fig:createmethod}
+\end{figure*}
+
+To begin, we will start with the creation of a Methodology diagram as the one shown on Figure \ref{fig:methoddiagram}. In order to do this, right click on the design window and select “New AVATAR Methodology†(Figure \ref{fig:createmethod}). For each box on this diagram another diagram from the development of the project will be selected, however, this example will not include any properties or prototyping and therefore, these two boxes will remain blank. After all the other diagrams are created by following the steps in the remainder of this manual, one will go back to the methodology diagram, double click on each box, select the diagram corresponding to it and click on the arrow as shown in figure \ref{fig:selectdiagram} in order to select it.
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/methoddiagram.png}
+\caption{Methodology Diagram} \label{fig:methoddiagram}
+\end{figure*}
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/selectdiagram.jpg}
+\caption{Selecting Diagrams} \label{fig:selectdiagram}
+\end{figure*}
+
+
+\section{Analysis}
+\subsection{Assumptions}
+
+As shown in figure \ref{fig:assumptionswindow}, right click on the panel tab and add a “New Modeling Assumptions†diagram. By right clicking on the panel it can be moved left or right. You will now have an Assumptions panel and underneath it an Assumptions diagram tab. You can right click on this tab in order to rename it, in this example, we changed its name to ‘System’. You will then add an assumption box by clicking on the AST button as shown in figure \ref{fig:assumptionswindow}. You can add as many assumptions as needed in order to fully explain what is being taken into account for the system.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/assumptionswindow.jpg}
+\caption{Assumptions Window} \label{fig:assumptionswindow}
+\end{figure*}
+
+\begin{enumerate}
+\item Edit AVATAR Modeling Assumptions Diagram
+\item Add a comment: add a comment to the diagram
+\item Comment connector
+\item AST: add an assumption box to the diagram
+\item Diagram reference: add a box who refers to another diagram
+\item Element reference: add a box who refers to an Avatar element
+\item Composite: Splits up a compound asuumptions into elementary ones
+\item Versioning: classify changes that are made to the original model
+\item Impact: indicate that the assumption at the origin of the link as a direct impact on the referenced element at the end on the link.
+\item Composition connector: relations between a diagram reference and elements references
+\end{enumerate}
+
+To edit each of these boxes one should double click on them. A window as the one shown in figure \ref{fig:assumptionsedit} will appear. In this window one can modify the name and type of the assumption, as well as other attributes such as durability, source, status and scope. Also, a little description of the assumption can be added in the box on the lower left corner. Furthermore, different types of links, or connections, can be added between the different boxes by clicking on the respective button shown in Figure \ref{fig:assumptionswindow} and then on the perimeter of each of the boxes you wish to link.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/assumptionsedit.jpg}
+\caption{Assumptions Editing} \label{fig:assumptionsedit}
+\end{figure*}
+
+Finally, in this example we have created two assumption diagrams; one for the system itself and one for the environment. The first one contains all the assumptions made directly about the system, while the second includes assumptions that may not be directly included in the system, but will affect its performance as shown in Figure \ref{fig:envassumptions}. One can add as many diagrams as one pleases by simply right clicking next to the existing diagram and selecting ``New AVATAR Modeling Assumptions Diagram'' and following the previously mentioned steps.
+It is important to keep in mind that these assumptions will allow the creator and others needing to interact with the system what was and was not considered during design. Therefore, one should attempt to be as descriptive as possible. This will make future improvements and changes easier while providing essential information about the system itself, resulting in a more complete design.
+
+As shown in figure \ref{fig:systemassumptions}, the system assumptions made for the coffee are those who enable the system to perform without malfunction. In this case, the system designed is the controller
+The environment assumptions were divided in two main categories. The sensors and the actuators. In this example, due to the short number of environment assumptions, they were all created on the same diagram as shown on figure \ref{fig:envassumptions}. It should be noted that there could be three diagrams for the environment assumptions only. The first one would indicate the link between the environment and the two other diagrams, which would be the sensors diagram and the actuators diagram.
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/systemassumptions.jpg}
+\caption{System Assumptions} \label{fig:systemassumptions}
+\end{figure*}
+
+The coffee machine has two type of sensors, a currency detector and pushbuttons. Together, they allow the users to order a cup of coffee or a cup tea and to pay for it. For their part, the actuators shall allow the users to receive their order. This part was fulfilled by the mechanical device. A mechanism permitting a transfer of information to the users was added to improve the ease of use of the coffee machine. As for the system, the assumptions enable the system to perform without malfunction.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/environmentassumptions.jpg}
+\caption{Environment Assumptions} \label{fig:envassumptions}
+\end{figure*}
+
+\subsection{Requirements}
+A requirement is a capability or a condition that the system must satisfy. It can be about a function that the system shall perform or a performance condition that must be achieved. Figure \ref{fig:reqbox} shows the standard form and information of a requirement box.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.3\textwidth]{fig/reqbox.jpg}
+\caption{Requirement Box} \label{fig:reqbox}
+\end{figure*}
+
+\begin{itemize}
+\item Requirement name
+\item ID: unique identifier
+\item Text: text requirement
+\item Kind: status
+\item Risk: priority
+\item Reference elements
+\end{itemize}
+
+There are two parts where the requirements can be expressed. The use cases, which is a part of the analysis diagram, can be useful to express the functional requirements. However, it is not suitable for non-functional requirements. For its part, the requirements diagram enables to introduce text-based requirements, providing a way to express the non-functional requirements. This diagram follows after setting up the assumptions for our system.
+ We will create one or several diagrams defining the requirements that the coffee machine controller will have. To do this, right click on the panel tab as before, but instead select “New Requirement Diagramsâ€. Just as before, a new diagram tab will appear underneath. Once again, this diagram tab can be renamed as preferred following the same steps we used in the assumption diagrams.
+ For the coffee machine, we will divide the requirements in three parts. The requirements related to the inputs, the control and the outputs.
+ The first diagram is named ``General Requirement Diagram''. It contains the link between the three parts mentioned above, which will all have their own requirements diagram.
+
+ Figure \ref{fig:reqdiagram} shows the structural elements available to build the requirements diagram.
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.7\textwidth]{fig/reqdiagram.jpg}
+\caption{Structural elements of the requirements diagram} \label{fig:reqdiagram}
+\end{figure*}
+
+\begin{enumerate}
+\item Edit Requirements Diagram
+\item Add a comment: add a comment to the diagram
+\item Comment connector
+\item Requirement: add a requirement box to the diagram
+\item Property: add a property box to the diagram
+\item Composition: a relationship who defines the requirements hierarchy
+\item DeriveReqt: a relationship who links two requirements of the same hierarchy but at different levels of abstraction
+\item Copy: a relationship that connect a slave requirement a master requirement
+\item Refine: a relationship who links used between a requirement that refine another
+\item Verify: a relationship who defines how a model element verifies a requirement
+\item Element reference
+\item Satisfy: a relationship who show that a concept satisfies a requirement
+\item Show/hide element attributes
+\item Enhance
+
+\end{enumerate}
+
+Figure \ref{fig:reqgeneral} represents the general requirement diagram obtained for the coffee machine controller.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/reqgeneral.jpg}
+\caption{General Requirement Diagram} \label{fig:reqgeneral}
+\end{figure*}
+
+
+In a similar way to that of the assumptions, a new requirement can be added by selecting the requirement button shown in figure \ref{fig:reqdiagram}. Once created, it can also be modified by double clicking on it. When the new window pops up, one can provide a description and change the ID, Type, Risk and Reference attributes of each requirement.
+ The next step was to create the inputs diagram, the control diagram and the outputs diagram. By using the requirement box and relationships described in figure \ref{fig:reqdiagram}, we obtained the diagrams shown in Figures \ref{fig:inputreq} and \ref{fig:controlreq}.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/inputreq.jpg}
+\caption{Inputs requirements diagram} \label{fig:inputreq}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/controlreq.jpg}
+\caption{Control requirements diagram} \label{fig:controlreq}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/outputreq.jpg}
+\caption{Output requirements diagram} \label{fig:outputreq}
+\end{figure*}
+
+\subsection{Use Case}
+ Once again, right click on the panel tab. This time select the “New Analysis†option, which will give you a window like the one shown in Figure \ref{fig:createusecase}. We will begin the analysis process with a Use Case Diagram. To add it, right click on the window and select “New Use Case Diagramâ€. This diagram will allow us to represent the system, the actors acting on it and the different instances or use cases that will be modeled. All these elements can be observed in Figure \ref{fig:usecase}. To add each of them you should use the buttons shown in Figure \ref{fig:structusecase}. To change the names, double click on each on them.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/createusecase.png}
+\caption{Create Use Case Diagram} \label{fig:createusecase}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/structusecase.jpg}
+\caption{Structural elements of the use case diagram} \label{fig:structusecase}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/usecase.jpg}
+\caption{Use Case Diagram} \label{fig:usecase}
+\end{figure*}
+
+
+
+\begin{enumerate}
+\item Edit Use Case Diagram
+\item Add a comment: add a comment to the diagram
+\item Comment connector
+\item Add a border: create a system box who defines the boundaries of the system
+\item Actor: add an actor to the diagram
+\item Actor (Box Format): add an actor box to the diagram
+\item Add a use case
+\item Actor <->use case: links an actor to a use case
+\item Include: a relationship who links a function to a subfunction whose mandatorily included
+\item Extend: a relationship who links a function to a sibfunction whose optionally included
+\item Specialization: links a `parent' function whose specialized by a `child' function
+\end{enumerate}
+
+As it can be seen in the figure \ref{fig:usecase}, on the left hand of the diagram, one can find the actors that initialize a process, while on the right we have the actors or elements that are activated as a result of it. The box in the middle represents the enclosed system and the four bubbles inside of it are the use cases, they represent the actions that the system will perform and are linked to the actor(s) involved in them. They are usually one or two words working as a verb.
+
+Once done, the next step is to create an activity diagram. Just as before, right click on the diagram tab and select “New Activity Diagramâ€. In TTool, an activity diagram is portrayed in the form of what is commonly known as a flowchart. The elements that can be added to it are shown on the button tab and they include activities, partitions, the start and end of the activity, choices and tabs for whether there is a signal being sent or received.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.4\textwidth]{fig/actdiagram.jpg}
+\caption{Activity Diagram} \label{fig:actdiagram}
+\end{figure*}
+
+In the example shown in Figure \ref{fig:actdiagram}, only a start, activities and a junction are used. After each of the elements is added, they can be edited by double clicking on them. The activity boxes should represent each of the steps that the system will perform. In addition, to edit the choice elements, click on each of the brackets or guards that appear on each of the rhombus connectors and write in the condition that must be satisfied for each option. Finally, the arrows, or associations, can be added by clicking on the respective button and then by clicking on a point on the perimeter of each of the elements being linked.
+ The final section of the analysis is creating a scenario or sequence. As in previous, cases right click on the diagram tab and select “New Sequence Diagram.†This diagram will allow us to showcase the logical progression of actions as well as the different instances in which different actors or components come into play during the execution of the system. Using the different buttons at the top of the window one can add instances, timers and indicate whether the message being transmitted is synchronous or asynchronous1 among other elements.
+To add an actor, click the “Instance†button and place it on the window. Then, double click as if to edit. When the pop up window appears, check the box that says “actorâ€. After setting up the main structure of the system use the arrows mentioned before to represent the messages being sent between the different elements, add text describing the process by double clicking on them after setting them in place. Though not shown in this example, when adding a timer one must also indicate the amount of time assigned to it and its attributes.
+
+As it can be observed in Figure \ref{fig:paymentseqdiagram} and \ref{fig:choiceseqdiagram}, the sequence diagram functions as a visual description of the flow of messages and information inside the system. If required, one can create more than one diagram in the same window, or add as many sequence diagrams as necessary.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/paymentseqdiagram.jpg}
+\caption{Logical progession of the `Payment' sequence diagram} \label{fig:paymentseqdiagram}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/choiceseqdiagram.jpg}
+\caption{Logical progression of the `ChoiceAndService' sequence diagram} \label{fig:choiceseqdiagram}
+\end{figure*}
+
+\section{Design}
+ Just as with all the previous sections, to start the design one will right click on the panel tab and select “New Designâ€. This will open the window to create a “Block Diagramâ€-- here we will create the main structure of our system. To add a block, click on the block button shown in figure \ref{fig:blockdiagram}. You will create as many blocks as actors/parts you have determined in the previous parts of the creation process.
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/blockdiagram.jpg}
+\caption{Structural elements of the block diagram} \label{fig:blockdiagram}
+\end{figure*}
+
+
+\begin{enumerate}
+\item Edit interaction overview diagram
+\item Add a comment: add a comment to the diagram
+\item Security pragmas
+\item Safety property
+\item Performance property
+\item Comment connector
+\item Block
+\item Crypto block
+\item Add an avatar firewall
+\item Data type
+\item Library function
+\item Crypto library function
+\item Composition connector
+\item Port connector
+\item Show/hide element attributes
+
+\end{enumerate}
+
+The coffee machine controller has five blocks: the pushbuttons, the token slot, the controller of the machine, the mechanical block, and the numerical screen. The name of each block can be edited by double clicking on the top part of the block and writing in the desired name. In addition, every time a block is created, a new tab corresponding to that block will appear next to the block diagram. We will look further into each of them later in this manual.
+
+ Following the creation of the blocks, attributes and signals for each of them will be added. To do this, double click on the bottom part of the block. A pop up window as the one shown in Figure \ref{fig:setattribute} will show up. In the ‘Attributes’ section we will indicate the elements or variables that will interact with that section of the machine and whether they are integers, timer or Boolean values. In this example only the token slot, the controller and the pushbuttons have ‘Attributes’. In the two first of them we can find “T†(short for token), which is an integer. This can be defined by selecting “int†from the drop down menu in the section indicated in Figure \ref{fig:setattribute}. In addition, in the two last of them we can find timers.
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.5\textwidth]{fig/setattribute.png}
+\caption{Setting attributes of a block} \label{fig:setattribute}
+\end{figure*}
+
+
+Furthermore, the ‘signals’ represent the information being sent and received by each component of the machine. On the same pop up window as before, click on the signals tab on the top. To add a signal, just select whether it is coming in or going out in the box shown in Figure \ref{fig:setsignal} and then give it a name. If two blocks have communication between them, one should have the outgoing signal, and the other the receiving signal.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.5\textwidth]{fig/setsignal.png}
+\caption{Setting signals of a block} \label{fig:setsignal}
+\end{figure*}
+
+
+ Finally, one will add port connections by clicking on the respective button shown in Figure21, and then selecting a point on the perimeter of the blocks being connected. Following, double click on the connector; a new window will pop up (Figure \ref{fig:portconn}).
+
+ \begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.5\textwidth]{fig/portconn.png}
+\caption{Port Connection between blocks} \label{fig:portconn}
+\end{figure*}
+
+ Here you will select the outgoing and incoming pairs of signals and one by one add them as shown in Figure \ref{fig:portconn}. In addition, you can select whether this message is asynchronous or synchronous on the boxes in the inferior part of the window. Once all the signals and connections between each of the blocks are set, we can move on to the diagrams for each of the blocks.
+The block diagram created for the coffee machine controller is shown in Figure \ref{fig:blockdiag}.
+
+ \begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/blockdiag.jpg}
+\caption{Block diagram} \label{fig:blockdiag}
+\end{figure*}
+
+Once the block diagram is finished, we will go to the tabs that appeared for each of the blocks. Here, we will show through a flow chart the process through which each element goes to complete its specified task. Unlike before, in this case the black dot that indicates the process is starting is automatically added. We will complete the design from there down. Also, differently than in the activity diagram created during the analysis, here we can add the states in which the machine, or part of the machine is, choices, signals being sent and received and stops. Each of these buttons are shown in Figure \ref{fig:structelementsblock}.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/structelementsblock.png}
+\caption{Structural elements of each block diagram} \label{fig:structelementsblock}
+\end{figure*}
+
+\begin{enumerate}
+\item Edit AVATAR state machine diagram
+\item Add a comment: add a comment to the diagram
+\item Comment connector
+\item Connect two operators together
+\item Start: add a starting point to the diagram
+\item Stop: add a stopping point which will be the final state when it is reached (the block instance `dies')
+\item State
+\item Choice: add transitions that can be taken following specific conditions
+\item Select random: add an attribute that can give a random value to a variable
+\item Send signal: add an output signal
+\item Receive signal: add an input signal
+\item Library function call
+\item Set timer: add a timer that will start when it is reached
+\item Reset timer: stop the timer's clock and reset it
+\item Wait for timer expiration
+\item Enhance
+\item Show/hide AVATAR IDs
+\end{enumerate}
+
+Using as reference what was already indicated in the block diagram, we will determine when messages are being sent and the states in which the machine is before and after each iteration. The diagrams for the mechanical block, numerical screen, controller, token slot and pushbuttons can be observed as example in Figures \ref{fig:mechdiagram} to \ref{fig:pushbuttondiagram} respectively.
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/mechdiagram.jpg}
+\caption{Mechanical block diagram} \label{fig:mechdiagram}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/numdiagram.jpg}
+\caption{Numerical screen diagram} \label{fig:numdiagram}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/controllerdiagram.jpg}
+\caption{Controller diagram} \label{fig:controllerdiagram}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.9\textwidth]{fig/tokendiagram.jpg}
+\caption{Token slot diagram} \label{fig:tokendiagram}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.5\textwidth]{fig/pushdiagram.jpg}
+\caption{Pushbuttons diagram} \label{fig:pushbuttondiagram}
+\end{figure*}
+
+\section{Verification}
+ Finally, the last step of the process is to verify that the system we have created works properly and follows each of the steps we desire it to. In order to do this, we will use the “Syntax Analysis†tool, which is shown in Figure \ref{fig:syntaxanalysis}. After you click on it, a screen like the one in this same figure will appear. There you can select whether you want to check the syntax of the whole system or individual parts. After this is determined, click on start syntax analysis and wait a second. After the software is done it will either pop up an error message like the one in Figure \ref{fig:syntaxerror}, meaning that the system has not been designed correctly; or if no errors are found, the “Interactive Simulation†button (Figure \ref{fig:syntaxanalysis}), which was once greyed out, will now be blue and you will be able to click on it.
+
+\begin{enumerate}
+\item Syntax Analysis
+\item Select elements to analyze
+\item Start analysis
+\item Interactive Simulation (currently greyed out)
+
+
+\end{enumerate}
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/syntaxanalysis.jpg}
+\caption{Syntax analysis} \label{fig:syntaxanalysis}
+\end{figure*}
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.3\textwidth]{fig/syntaxerror.png}
+\caption{Syntax analysis error message} \label{fig:syntaxerror}
+\end{figure*}
+
+ If this is the case, then you will click on it and a window like the one in Figure \ref{fig:interactivesim} will appear on your screen. Click on run simulation and wait. The software will then go through a full iteration of the machine and show each step in the way portrayed by Figures \ref{fig:simstep1} and \ref{fig:simstep2} below. This tool is very useful in that it allows us to see how the different parts of the machine communicate as well as each step of the process programmed.
+\subsection{Reachability Graphs}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/interactivesim.png}
+\caption{Interactive Simulation} \label{fig:interactivesim}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/simstep1.png}
+\caption{Simulation steps (part 1)} \label{fig:simstep1}
+\end{figure*}
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/simstep2.png}
+\caption{Simulation steps (part 2)} \label{fig:simstep2}
+\end{figure*}
+
+
+ Another interesting feature in the TTool software is the ability to graph or map the processes. This generates a graph that allows us to see all the different pathways that the system follows to reach its final state, each showing a different scenario. In addition, one can select a specific initial and final state, which simplifies said graph and gives a neater depiction of the process. Figure \ref{fig:rg} shows an example.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/rg.png}
+\caption{Reachability graph} \label{fig:rg}
+\end{figure*}
+
+\subsection{Latency Analysis}
+
+
+Many real-time safety-critical systems interact continuously with the environment and users. New input from the outside world is processed by the system, which then effectuates a response observable in the real world. The timing of such responses can greatly impact functionality and safety.
+
+Latency analysis is performed in multiple steps. First, the quantitative requirement on latency must be defined. Next, the text requirement must be translated to determine which modeling elements the critical events refer to, after which latencies can be measured in simulation. The results are then conveniently displayed on the modeling diagrams. This example uses the updated Coffee Machine model that can be found in the TTool sample modeling repository.
+
+Figure \ref{fig:latencyreq} shows a requirement related to timing: The Coffee Machine must take less than X seconds to finish a drink command after payment has been received.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.3\textwidth]{build/latencyreq-svg.pdf}
+\caption{Latency Requirement for Coffee Machine} \label{fig:latencyreq}
+\end{figure*}
+
+The operators relating to this requirement are the last `getCoin(x)' and the idle state after processing `WaitingForFirstCoin'. Figure \ref{fig:latencycheckpoint} shows how the two operators are tagged with `Latency Checkpoints', in the form of blue flags.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{build/latencycheckpoint-svg.pdf}
+\caption{Latency Checkpoints on Activity Diagram} \label{fig:latencycheckpoint}
+\end{figure*}
+
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/latencymeasure.png}
+\caption{Latency Measurement Panel} \label{fig:latencymeasurement}
+\end{figure*}
+
+After syntax analysis, run interactive simulation, and then on the Latency Panel (Figure \ref{fig:latencymeasurement}), we indicate that we should measure the latency between these two checkpoints by selecting the operators and clicking the `Add latency' button. After running 100 steps of the simulation, the minimum, maximum, average, standard deviation of the latency measurements is displayed as shown in Figure \ref{fig:latencyresults}.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/latencyresults.png}
+\caption{Latency Results} \label{fig:latencyresults}
+\end{figure*}
+
+
+\section{Conclusion}
+
+ All in all, TTool is a useful software, which allows the user to generate systems using SysML. By guiding the user through each of the steps of the process (Methodology, Assumptions, Requirements, Analysis and Design) it serves as a platform for better structured, and comprehensive designs. These models provide all the information required to understand the present state of the design and enable easy changes in the future. It is straightforward and intuitive and it has many more features than the ones shown in this manual, therefore making it a very complete tool in the development and simulation of engineering designs.
+
+\end{document}
diff --git a/doc/AVATAR/fig/actdiagram.jpg b/doc/AVATAR/fig/actdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..1242faaed96df5c5d3589514ef0cfc6446f2dc80
Binary files /dev/null and b/doc/AVATAR/fig/actdiagram.jpg differ
diff --git a/doc/AVATAR/fig/assumptionsedit.jpg b/doc/AVATAR/fig/assumptionsedit.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..de8ded925b57dfd766d23ac69120c5e4f74d023b
Binary files /dev/null and b/doc/AVATAR/fig/assumptionsedit.jpg differ
diff --git a/doc/AVATAR/fig/assumptionswindow.jpg b/doc/AVATAR/fig/assumptionswindow.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..e57e7dca11e8147bea331e6a895962d5983863df
Binary files /dev/null and b/doc/AVATAR/fig/assumptionswindow.jpg differ
diff --git a/doc/AVATAR/fig/blockdiag.jpg b/doc/AVATAR/fig/blockdiag.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..d63a3a98068821579bbecc727a8e372791fef51d
Binary files /dev/null and b/doc/AVATAR/fig/blockdiag.jpg differ
diff --git a/doc/AVATAR/fig/blockdiagram.jpg b/doc/AVATAR/fig/blockdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..99e4f39d8992b09e881a90ec52162a1834c2d75d
Binary files /dev/null and b/doc/AVATAR/fig/blockdiagram.jpg differ
diff --git a/doc/AVATAR/fig/choiceseqdiagram.jpg b/doc/AVATAR/fig/choiceseqdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..240f32a9505df83b207d011b3bc07c9d58505b96
Binary files /dev/null and b/doc/AVATAR/fig/choiceseqdiagram.jpg differ
diff --git a/doc/AVATAR/fig/controllerdiagram.jpg b/doc/AVATAR/fig/controllerdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..fa98561cc7d0f3b2cfa7a77fa68825513a303f26
Binary files /dev/null and b/doc/AVATAR/fig/controllerdiagram.jpg differ
diff --git a/doc/AVATAR/fig/controlreq.jpg b/doc/AVATAR/fig/controlreq.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..e0370efcde27fdaad0eb1240bad5180856ed32e1
Binary files /dev/null and b/doc/AVATAR/fig/controlreq.jpg differ
diff --git a/doc/AVATAR/fig/createfile.png b/doc/AVATAR/fig/createfile.png
new file mode 100644
index 0000000000000000000000000000000000000000..201c6077c23efa6b5bd420d01277e3756d9bd555
Binary files /dev/null and b/doc/AVATAR/fig/createfile.png differ
diff --git a/doc/AVATAR/fig/createmethod.png b/doc/AVATAR/fig/createmethod.png
new file mode 100644
index 0000000000000000000000000000000000000000..b6c2af8a24406ef5372d62f7238655bbe867f0b3
Binary files /dev/null and b/doc/AVATAR/fig/createmethod.png differ
diff --git a/doc/AVATAR/fig/createusecase.png b/doc/AVATAR/fig/createusecase.png
new file mode 100644
index 0000000000000000000000000000000000000000..6ce14cc9238114e9cdac1cb5ada73acfccfb9239
Binary files /dev/null and b/doc/AVATAR/fig/createusecase.png differ
diff --git a/doc/AVATAR/fig/environmentassumptions.jpg b/doc/AVATAR/fig/environmentassumptions.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..813198a740da2586405c0b5579eb2853e246c7a1
Binary files /dev/null and b/doc/AVATAR/fig/environmentassumptions.jpg differ
diff --git a/doc/AVATAR/fig/inputreq.jpg b/doc/AVATAR/fig/inputreq.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..ac0e551577a897e5d8279c23d54c8bb4dd4e00c9
Binary files /dev/null and b/doc/AVATAR/fig/inputreq.jpg differ
diff --git a/doc/AVATAR/fig/interactivesim.png b/doc/AVATAR/fig/interactivesim.png
new file mode 100644
index 0000000000000000000000000000000000000000..81347d3b65a655bfee66901dae367ec678821152
Binary files /dev/null and b/doc/AVATAR/fig/interactivesim.png differ
diff --git a/doc/AVATAR/fig/latencycheckpoint.svg b/doc/AVATAR/fig/latencycheckpoint.svg
new file mode 100644
index 0000000000000000000000000000000000000000..c81361636b74deb87dad89fbc85207d831aef654
--- /dev/null
+++ b/doc/AVATAR/fig/latencycheckpoint.svg
@@ -0,0 +1,1089 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:#000000;stroke-width:1;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1;stroke-dasharray:none;stroke-dashoffset:0;font-family:Dialog"
+ id="svg2"
+ version="1.1"
+ inkscape:version="0.48.4 r9939"
+ width="530.06403"
+ height="423.05258"
+ sodipodi:docname="latencycheckpoint.svg">
+ <metadata
+ id="metadata409">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview407"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="0.63429569"
+ inkscape:cx="-638.33908"
+ inkscape:cy="370.1195"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="g15" />
+ <!--Generated by the Batik Graphics2D SVG Generator-->
+ <defs
+ id="genericDefs">
+ <defs
+ id="defs1">
+ <clipPath
+ id="clipPath1"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ id="path9"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z"
+ inkscape:connector-curvature="0" />
+ </clipPath>
+ </defs>
+ <clipPath
+ id="clipPath1-4"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path9-6"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath1-9"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path9-5"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath3623"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path3625"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath3627"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path3629"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath1-2"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path9-56"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath3669"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path3671"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ <clipPath
+ id="clipPath3673"
+ clipPathUnits="userSpaceOnUse">
+ <path
+ inkscape:connector-curvature="0"
+ id="path3675"
+ d="m 0,0 1759,0 0,1410 L 0,1410 0,0 z" />
+ </clipPath>
+ </defs>
+ <g
+ id="g15"
+ style="fill:#c1daf1;stroke:#c1daf1;font-family:sans-serif"
+ transform="translate(-17.5,-291.61827)">
+ <line
+ clip-path="url(#clipPath1-9)"
+ id="line313-5"
+ y2="275"
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:none;stroke:#000000;stroke-width:1.55847013;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1;stroke-dasharray:none;stroke-dashoffset:0;font-family:sans-serif"
+ y1="235"
+ x2="277"
+ x1="273"
+ transform="matrix(0.99547903,0.03910594,-0.09498163,0.40985969,48.82634,237.83607)" />
+ <polygon
+ clip-path="url(#clipPath1-9)"
+ id="polygon315-6"
+ points="281,265 277,275 271,266 "
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;font-family:sans-serif"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,48.756666,69.119257)" />
+ <polygon
+ clip-path="url(#clipPath1-9)"
+ id="polygon317-0"
+ points="281,265 277,275 271,266 "
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:none;stroke:#000000;stroke-width:1;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1;stroke-dasharray:none;stroke-dashoffset:0;font-family:sans-serif"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,48.756666,69.119257)" />
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect17"
+ height="354"
+ ry="2.5"
+ rx="2.5"
+ style="stroke:none"
+ width="577"
+ y="370"
+ x="18"
+ transform="matrix(0.91692203,0,0,0.8051578,1.4954035,72.091615)" />
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect19"
+ height="354"
+ ry="2.5"
+ rx="2.5"
+ style="fill:none;stroke:#000000;stroke-width:1.16384006"
+ width="577"
+ y="370"
+ x="18"
+ transform="matrix(0.91692203,0,0,0.8051578,1.4954035,72.091615)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text21"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="385"
+ x="273"
+ transform="translate(-10.108238,-3.1592567)">Beverage</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line23"
+ y2="387"
+ style="fill:none;stroke:#000000;stroke-width:1.04432046"
+ y1="387"
+ x2="595"
+ x1="18"
+ transform="matrix(0.91692203,0,0,1,1.4954035,0)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line29"
+ y2="501"
+ style="fill:none;stroke:#80b4cd"
+ y1="501"
+ x2="499"
+ x1="368" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line33"
+ y2="521"
+ style="fill:none;stroke:#80b4cd"
+ y1="501"
+ x2="368"
+ x1="368" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line35"
+ y2="511"
+ style="fill:none;stroke:#80b4cd"
+ y1="501"
+ x2="509"
+ x1="499" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line37"
+ y2="511"
+ style="fill:none;stroke:#80b4cd"
+ y1="521"
+ x2="509"
+ x1="499" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line39"
+ y2="500"
+ style="fill:none;stroke:#000000"
+ y1="500"
+ x2="498"
+ x1="367" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line41"
+ y2="520"
+ style="fill:none;stroke:#000000"
+ y1="520"
+ x2="498"
+ x1="367" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line43"
+ y2="520"
+ style="fill:none;stroke:#000000"
+ y1="500"
+ x2="367"
+ x1="367" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line45"
+ y2="510"
+ style="fill:none;stroke:#000000"
+ y1="500"
+ x2="508"
+ x1="498" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line47"
+ y2="510"
+ style="fill:none;stroke:#000000"
+ y1="520"
+ x2="508"
+ x1="498" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text49"
+ xml:space="preserve"
+ style="fill:#000000;stroke:none"
+ y="515"
+ x="372">ejectCoin(nbOfCoins)</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text51"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="498"
+ x="489">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text53"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#ff0000;stroke:none"
+ y="499"
+ x="490">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text55"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="498"
+ x="497">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text57"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#ff0000;stroke:none"
+ y="499"
+ x="498">L</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line63"
+ y2="528"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="193"
+ x1="52" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line65"
+ y2="548"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="193"
+ x1="193" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line69"
+ y2="538"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="62"
+ x1="52" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line71"
+ y2="538"
+ style="fill:none;stroke:#80b4cd"
+ y1="548"
+ x2="62"
+ x1="52" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line73"
+ y2="527"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="192"
+ x1="51" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line75"
+ y2="547"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="192"
+ x1="192" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line77"
+ y2="547"
+ style="fill:none;stroke:#000000"
+ y1="547"
+ x2="192"
+ x1="51" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line79"
+ y2="537"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="61"
+ x1="51" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line81"
+ y2="537"
+ style="fill:none;stroke:#000000"
+ y1="547"
+ x2="61"
+ x1="51" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text83"
+ xml:space="preserve"
+ style="fill:#000000;stroke:none"
+ y="542"
+ x="63">pushCoffeeButton()</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text85"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="525"
+ x="173">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text87"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#00e800;stroke:none"
+ y="526"
+ x="174">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text89"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="525"
+ x="181">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text91"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#404040;stroke:none"
+ y="526"
+ x="182">L</text>
+ <circle
+ sodipodi:ry="7.5"
+ sodipodi:rx="7.5"
+ sodipodi:cy="406.5"
+ sodipodi:cx="256.5"
+ clip-path="url(#clipPath1)"
+ id="circle93"
+ cy="406.5"
+ cx="256.5"
+ r="7.5"
+ style="fill:#000000;stroke:none"
+ transform="translate(42.961036,-1.5765518)"
+ d="m 264,406.5 c 0,4.14214 -3.35786,7.5 -7.5,7.5 -4.14214,0 -7.5,-3.35786 -7.5,-7.5 0,-4.14214 3.35786,-7.5 7.5,-7.5 4.14214,0 7.5,3.35786 7.5,7.5 z" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line95"
+ y2="419"
+ style="fill:none;stroke:#000000;stroke-width:0.65273952"
+ y1="414"
+ x2="256"
+ x1="256"
+ transform="matrix(1,0,0,2.3470385,42.961036,-559.13435)" />
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect97"
+ height="40"
+ ry="2.5"
+ rx="2.5"
+ style="fill:#c1dafb;stroke:none"
+ width="132"
+ y="435"
+ x="189"
+ transform="matrix(1.0654517,0,0,1,21.951036,-1.5765518)" />
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect99"
+ height="40"
+ ry="2.5"
+ rx="2.5"
+ style="fill:none;stroke:#000000;stroke-width:0.96640682"
+ width="132"
+ y="435"
+ x="189"
+ transform="matrix(1.0707301,0,0,1,20.256682,-1.5765518)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text101"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="450"
+ x="183"
+ transform="translate(42.961036,-1.5765518)">WaitingForSelection</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line103"
+ y2="452"
+ style="fill:none;stroke:#000000;stroke-width:0.96879774"
+ y1="452"
+ x2="321"
+ x1="189"
+ transform="matrix(1.0654517,0,0,1,21.951036,-1.5765518)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line109"
+ y2="528"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="356"
+ x1="232" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line111"
+ y2="548"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="356"
+ x1="356" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line113"
+ y2="548"
+ style="fill:none;stroke:#80b4cd"
+ y1="548"
+ x2="356"
+ x1="232" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line115"
+ y2="538"
+ style="fill:none;stroke:#80b4cd"
+ y1="528"
+ x2="242"
+ x1="232" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line117"
+ y2="538"
+ style="fill:none;stroke:#80b4cd"
+ y1="548"
+ x2="242"
+ x1="232" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line119"
+ y2="527"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="355"
+ x1="231" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line121"
+ y2="547"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="355"
+ x1="355" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line123"
+ y2="547"
+ style="fill:none;stroke:#000000"
+ y1="547"
+ x2="355"
+ x1="231" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line125"
+ y2="537"
+ style="fill:none;stroke:#000000"
+ y1="527"
+ x2="241"
+ x1="231" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line127"
+ y2="537"
+ style="fill:none;stroke:#000000"
+ y1="547"
+ x2="241"
+ x1="231" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text129"
+ xml:space="preserve"
+ style="fill:#000000;stroke:none"
+ y="542"
+ x="243">pushTeaButton()</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text131"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="525"
+ x="336">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text133"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#00e800;stroke:none"
+ y="526"
+ x="337">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text135"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="525"
+ x="344">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text137"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#404040;stroke:none"
+ y="526"
+ x="345">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text139"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="368"
+ x="576"
+ transform="translate(-46.508277,-2.7589656)">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text141"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#ff0000;stroke:none"
+ y="369"
+ x="577"
+ transform="translate(-46.508277,-2.7589656)">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text143"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="368"
+ x="584"
+ transform="translate(-46.508277,-2.7589656)">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text145"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#ff0000;stroke:none"
+ y="369"
+ x="585"
+ transform="translate(-46.508277,-2.7589656)">L</text>
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect155"
+ height="40"
+ ry="2.5"
+ rx="2.5"
+ style="stroke:none"
+ width="137"
+ y="748"
+ x="221"
+ transform="matrix(1.02848,0,0,1,-14.42824,-73.829139)" />
+ <rect
+ clip-path="url(#clipPath1)"
+ id="rect157"
+ height="40"
+ ry="2.5"
+ rx="2.5"
+ style="fill:none;stroke:#000000;stroke-width:0.9860571"
+ width="137"
+ y="748"
+ x="221"
+ transform="matrix(1.02848,0,0,1,-14.42824,-73.829139)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text159"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="763"
+ x="219"
+ transform="translate(-4.2323832,-73.829139)">WaitingForFirstCoin</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line161"
+ y2="765"
+ style="fill:none;stroke:#000000;stroke-width:0.9860571"
+ y1="765"
+ x2="358"
+ x1="221"
+ transform="matrix(1.02848,0,0,1,-14.42824,-73.829139)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon163"
+ points="209,748 217,753 209,758 "
+ style="fill:#0000ff;stroke:none"
+ transform="translate(-8.2734983,-71.32086)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line165"
+ y2="768"
+ style="fill:none;stroke:#000000"
+ y1="748"
+ x2="209"
+ x1="209"
+ transform="translate(-8.2734983,-71.32086)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line167"
+ y2="753"
+ style="fill:none;stroke:#000000"
+ y1="748"
+ x2="217"
+ x1="209"
+ transform="translate(-8.2734983,-71.32086)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line169"
+ y2="753"
+ style="fill:none;stroke:#000000"
+ y1="758"
+ x2="217"
+ x1="209"
+ transform="translate(-8.2734983,-71.32086)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line203"
+ y2="281"
+ style="fill:none;stroke:#80b4cd"
+ y1="281"
+ x2="319"
+ x1="237"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line205"
+ y2="301"
+ style="fill:none;stroke:#80b4cd"
+ y1="281"
+ x2="319"
+ x1="319"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line207"
+ y2="301"
+ style="fill:none;stroke:#80b4cd"
+ y1="301"
+ x2="319"
+ x1="237"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line209"
+ y2="291"
+ style="fill:none;stroke:#80b4cd"
+ y1="281"
+ x2="247"
+ x1="237"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line211"
+ y2="291"
+ style="fill:none;stroke:#80b4cd"
+ y1="301"
+ x2="247"
+ x1="237"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line213"
+ y2="280"
+ style="fill:none;stroke:#000000"
+ y1="280"
+ x2="318"
+ x1="236"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line215"
+ y2="300"
+ style="fill:none;stroke:#000000"
+ y1="280"
+ x2="318"
+ x1="318"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line217"
+ y2="300"
+ style="fill:none;stroke:#000000"
+ y1="300"
+ x2="318"
+ x1="236"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line219"
+ y2="290"
+ style="fill:none;stroke:#000000"
+ y1="280"
+ x2="246"
+ x1="236"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line221"
+ y2="290"
+ style="fill:none;stroke:#000000"
+ y1="300"
+ x2="246"
+ x1="236"
+ transform="translate(20.592214,43.150313)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text223"
+ xml:space="preserve"
+ style="fill:#000000;stroke:none"
+ y="295"
+ x="248"
+ transform="translate(20.592214,43.150313)">getCoin(x)</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text225"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="278"
+ x="299"
+ transform="translate(20.592214,43.150313)">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text227"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#00e800;stroke:none"
+ y="279"
+ x="300"
+ transform="translate(20.592214,43.150313)">R</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text229"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#000000;stroke:none"
+ y="278"
+ x="307"
+ transform="translate(20.592214,43.150313)">L</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text231"
+ xml:space="preserve"
+ style="font-weight:bold;fill:#404040;stroke:none"
+ y="279"
+ x="308"
+ transform="translate(20.592214,43.150313)">L</text>
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon233"
+ points="232,285 224,290 224,280 "
+ style="fill:#0000ff;stroke:none"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line235"
+ y2="300"
+ style="fill:none;stroke:#000000"
+ y1="280"
+ x2="224"
+ x1="224"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line237"
+ y2="285"
+ style="fill:none;stroke:#000000"
+ y1="280"
+ x2="232"
+ x1="224"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line239"
+ y2="285"
+ style="fill:none;stroke:#000000"
+ y1="290"
+ x2="232"
+ x1="224"
+ transform="translate(20.592214,43.150313)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line313"
+ y2="275"
+ style="fill:none;stroke:#000000;stroke-width:1.55847013"
+ y1="235"
+ x2="277"
+ x1="273"
+ transform="matrix(0.99547903,0.03910594,-0.09498163,0.40985969,48.720749,189.6844)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon315"
+ points="271,266 281,265 277,275 "
+ style="fill:#000000;stroke:none"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,48.720749,21.734009)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon317"
+ points="271,266 281,265 277,275 "
+ style="fill:none;stroke:#000000"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,48.720749,21.734009)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon345"
+ points="250,426 260,426 255,435 "
+ style="fill:#000000;stroke:none"
+ transform="translate(43.797129,-3.1093887)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon347"
+ points="250,426 260,426 255,435 "
+ style="fill:none;stroke:#000000"
+ transform="translate(43.797129,-3.1093887)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line349"
+ y2="522"
+ style="fill:none;stroke:#000000;stroke-width:0.98073441"
+ y1="475"
+ x2="121"
+ x1="222"
+ transform="matrix(1.0188733,-0.09751862,0.09827718,1.011009,-50.7992,7.7384624)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon351"
+ points="126,513 130,522 121,522 "
+ style="fill:#000000;stroke:none"
+ transform="matrix(0.99538026,-0.09601112,0.09601112,0.99538026,-51.010639,17.980572)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon353"
+ points="126,513 130,522 121,522 "
+ style="fill:none;stroke:#000000"
+ transform="matrix(0.99538026,-0.09601112,0.09601112,0.99538026,-51.010639,17.980572)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line355"
+ y2="748"
+ style="fill:none;stroke:#000000;stroke-width:1.39377868"
+ y1="552"
+ x2="255"
+ x1="121"
+ transform="matrix(0.84089278,0,0,0.61216952,19.350508,209.74691)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon357"
+ points="254,738 255,748 245,743 "
+ style="fill:#000000;stroke:none"
+ transform="translate(-16.750863,-75.181812)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon359"
+ points="254,738 255,748 245,743 "
+ style="fill:none;stroke:#000000"
+ transform="translate(-16.750863,-75.181812)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text361"
+ xml:space="preserve"
+ style="fill:#694b0b;stroke:none"
+ y="587"
+ x="32">after (coffeeMinDelay,coffeeMaxDelay)</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text363"
+ xml:space="preserve"
+ style="fill:#7710f3;stroke:none"
+ y="602"
+ x="32">nbOfCoins = 0</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text365"
+ xml:space="preserve"
+ style="fill:#7710f3;stroke:none"
+ y="617"
+ x="32">beverageReady()</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line373"
+ y2="748"
+ style="fill:none;stroke:#000000;stroke-width:6.07575417"
+ y1="552"
+ x2="289"
+ x1="293"
+ transform="matrix(-0.04511605,0,0,0.60043863,305.20564,217.36251)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon375"
+ points="284,739 294,739 289,748 "
+ style="fill:#000000;stroke:none"
+ transform="translate(3.1531035,-75.083278)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon377"
+ points="284,739 294,739 289,748 "
+ style="fill:none;stroke:#000000"
+ transform="translate(3.1531035,-75.083278)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text379"
+ xml:space="preserve"
+ style="fill:#694b0b;stroke:none"
+ y="594"
+ x="284"
+ transform="translate(11.035862,8.6710348)">after (teaMinDelay,teaMaxDelay)</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text381"
+ xml:space="preserve"
+ style="fill:#7710f3;stroke:none"
+ y="609"
+ x="284"
+ transform="translate(11.035862,8.6710348)">nbOfCoins = 0</text>
+ <text
+ clip-path="url(#clipPath1)"
+ id="text383"
+ xml:space="preserve"
+ style="fill:#7710f3;stroke:none"
+ y="624"
+ x="284"
+ transform="translate(11.035862,8.6710348)">beverageReady()</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line385"
+ y2="495"
+ style="fill:none;stroke:#000000;stroke-width:1.42803943"
+ y1="455"
+ x2="437"
+ x1="321"
+ transform="matrix(0.58289926,0,0,0.84125193,177.04744,80.113122)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon387"
+ points="427,496 430,487 437,495 "
+ style="fill:#000000;stroke:none"
+ transform="matrix(0.93419784,0.35675538,-0.35675538,0.93419784,203.28409,-119.54698)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon389"
+ points="427,496 430,487 437,495 "
+ style="fill:none;stroke:#000000"
+ transform="matrix(0.93419784,0.35675538,-0.35675538,0.93419784,203.28409,-119.54698)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text391"
+ xml:space="preserve"
+ style="fill:#694b0b;stroke:none"
+ y="448"
+ x="395"
+ transform="translate(-19.312759,20.101035)">after (coinDelay)</text>
+ <line
+ clip-path="url(#clipPath1)"
+ id="line393"
+ y2="748"
+ style="fill:none;stroke:#000000;stroke-width:1.41437519"
+ y1="525"
+ x2="323"
+ x1="437"
+ transform="matrix(0.75683764,0,0,0.66049275,104.6854,175.0882)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon395"
+ points="331,742 323,748 322,738 "
+ style="fill:#000000;stroke:none"
+ transform="translate(24.436552,-75.083278)" />
+ <polygon
+ clip-path="url(#clipPath1)"
+ id="polygon397"
+ points="331,742 323,748 322,738 "
+ style="fill:none;stroke:#000000"
+ transform="translate(24.436552,-75.083278)" />
+ <text
+ clip-path="url(#clipPath1)"
+ id="text399"
+ xml:space="preserve"
+ style="fill:#7710f3;stroke:none"
+ y="552"
+ x="420"
+ transform="translate(7.2461379,6.6887427)">nbOfCoins = 0</text>
+ <text
+ transform="translate(44.442105,-1.89345)"
+ clip-path="url(#clipPath1-4)"
+ id="text223-2"
+ xml:space="preserve"
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;font-family:sans-serif"
+ y="295"
+ x="248">...</text>
+ <line
+ clip-path="url(#clipPath1-2)"
+ id="line313-53"
+ y2="275"
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:none;stroke:#000000;stroke-width:0.96735489;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1;stroke-dasharray:none;stroke-dashoffset:0;font-family:sans-serif"
+ y1="235"
+ x2="277"
+ x1="273"
+ transform="matrix(0.99547903,0.10150047,-0.09498163,1.0638013,42.915765,196.70673)" />
+ <polygon
+ clip-path="url(#clipPath1-2)"
+ id="polygon315-2"
+ points="277,275 271,266 281,265 "
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;font-family:sans-serif"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,42.915765,225.87356)" />
+ <polygon
+ clip-path="url(#clipPath1-2)"
+ id="polygon317-3"
+ points="277,275 271,266 281,265 "
+ style="font-size:12px;font-style:normal;font-weight:normal;fill:none;stroke:#000000;stroke-width:1;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:10;stroke-opacity:1;stroke-dasharray:none;stroke-dashoffset:0;font-family:sans-serif"
+ transform="matrix(0.99547903,0.09498163,-0.09498163,0.99547903,42.915765,225.87356)" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line31"
+ y2="521"
+ style="fill:none;stroke:#80b4cd"
+ y1="521"
+ x2="499"
+ x1="368" />
+ <line
+ clip-path="url(#clipPath1)"
+ id="line67"
+ y2="548"
+ style="fill:none;stroke:#80b4cd"
+ y1="548"
+ x2="193"
+ x1="52" />
+ </g>
+</svg>
diff --git a/doc/AVATAR/fig/latencymeasure.png b/doc/AVATAR/fig/latencymeasure.png
new file mode 100644
index 0000000000000000000000000000000000000000..e1ee20792681ea3a83d8abb3c1231d6fca3110b1
Binary files /dev/null and b/doc/AVATAR/fig/latencymeasure.png differ
diff --git a/doc/AVATAR/fig/latencyreq.svg b/doc/AVATAR/fig/latencyreq.svg
new file mode 100644
index 0000000000000000000000000000000000000000..5aee1f2e93f1d9f453d19b7d369601e4af2368ad
--- /dev/null
+++ b/doc/AVATAR/fig/latencyreq.svg
@@ -0,0 +1,133 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="170.92467"
+ height="121.43608"
+ viewbox="262 35 344 597"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="latencyreq.svg">
+ <metadata
+ id="metadata88">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ <dc:title />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs86" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="1918"
+ inkscape:window-height="1040"
+ id="namedview84"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="2.1123696"
+ inkscape:cx="265.14424"
+ inkscape:cy="38.045502"
+ inkscape:window-x="123"
+ inkscape:window-y="52"
+ inkscape:window-maximized="0"
+ inkscape:current-layer="svg2" />
+ <rect
+ style="fill:#e4f1f2"
+ x="1.1852627"
+ y="0.21649158"
+ width="169.01634"
+ height="27.756596"
+ id="rect588" />
+ <rect
+ style="fill:#cdc46d"
+ x="1.1852627"
+ y="28.286575"
+ width="169.01634"
+ height="92.509399"
+ id="rect590" />
+ <line
+ style="fill:none;stroke:#000000;stroke-width:1"
+ x1="0.5"
+ y1="28.080811"
+ x2="170.42467"
+ y2="28.080811"
+ id="line586" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.99999976"
+ x="0.50099754"
+ y="0.49999988"
+ width="169.72462"
+ height="120.43608"
+ id="rect584" />
+ <text
+ x="36.275017"
+ y="10.727005"
+ style="font-size:10px;font-family:SansSerif"
+ id="text592"><<Requirement>></text>
+ <text
+ x="14.090246"
+ y="24.391359"
+ style="font-size:12px;font-family:SansSerif"
+ id="text594">LatencyCoffeeMachine</text>
+ <text
+ x="5.5013599"
+ y="40.080795"
+ style="font-size:12px;font-family:SansSerif"
+ id="text596">ID=17</text>
+ <text
+ x="3.716814"
+ y="52.794571"
+ style="font-size:12px;font-family:SansSerif"
+ id="text598">Text="The Coffee Machine</text>
+ <text
+ x="5.5013599"
+ y="63.501785"
+ style="font-size:12px;font-family:SansSerif"
+ id="text3263">must take less 10 seconds</text>
+ <text
+ x="4.7875233"
+ y="75.03212"
+ style="font-size:12px;font-family:SansSerif"
+ id="text600-6">to finish processing each</text>
+ <text
+ x="4.911459"
+ y="86.096458"
+ style="font-size:12px;font-family:SansSerif"
+ id="text602-8">order after payment is</text>
+ <text
+ x="5.148159"
+ y="97.458107"
+ style="font-size:12px;font-family:SansSerif"
+ id="text3066">received."</text>
+ <text
+ x="3.716814"
+ y="100.35051"
+ style="font-size:12px;font-family:SansSerif"
+ id="text3267" />
+ <text
+ x="4.0737324"
+ y="113.06432"
+ style="font-size:12px;font-family:SansSerif"
+ id="text604-3">Kind="Performance"</text>
+</svg>
diff --git a/doc/AVATAR/fig/latencyresults.png b/doc/AVATAR/fig/latencyresults.png
new file mode 100644
index 0000000000000000000000000000000000000000..348e79c5f73e33ae1f9e3310b830df3ab18c90fd
Binary files /dev/null and b/doc/AVATAR/fig/latencyresults.png differ
diff --git a/doc/AVATAR/fig/mechdiagram.jpg b/doc/AVATAR/fig/mechdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..550645448689a5a28bb1dbed23f546f55a7b799a
Binary files /dev/null and b/doc/AVATAR/fig/mechdiagram.jpg differ
diff --git a/doc/AVATAR/fig/methoddiagram.png b/doc/AVATAR/fig/methoddiagram.png
new file mode 100644
index 0000000000000000000000000000000000000000..686d270eb3be13b8223d3eef9d95830afa883190
Binary files /dev/null and b/doc/AVATAR/fig/methoddiagram.png differ
diff --git a/doc/AVATAR/fig/numdiagram.jpg b/doc/AVATAR/fig/numdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..7b50f2b96cf416aa3b05100f840ba4404a93ca78
Binary files /dev/null and b/doc/AVATAR/fig/numdiagram.jpg differ
diff --git a/doc/AVATAR/fig/outputreq.jpg b/doc/AVATAR/fig/outputreq.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..5645146079a8cf6952bc37bdd44c728d6f3460ba
Binary files /dev/null and b/doc/AVATAR/fig/outputreq.jpg differ
diff --git a/doc/AVATAR/fig/paymentseqdiagram.jpg b/doc/AVATAR/fig/paymentseqdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..d92ee8769bdd8752b1668b117cac6172278aa855
Binary files /dev/null and b/doc/AVATAR/fig/paymentseqdiagram.jpg differ
diff --git a/doc/AVATAR/fig/portconn.png b/doc/AVATAR/fig/portconn.png
new file mode 100644
index 0000000000000000000000000000000000000000..ead376f331c9676de5ba389235ba3307727fc0b5
Binary files /dev/null and b/doc/AVATAR/fig/portconn.png differ
diff --git a/doc/AVATAR/fig/pushdiagram.jpg b/doc/AVATAR/fig/pushdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..1e37c8c8dd3a50e1b90d1a650ae7241364888d66
Binary files /dev/null and b/doc/AVATAR/fig/pushdiagram.jpg differ
diff --git a/doc/AVATAR/fig/reqbox.jpg b/doc/AVATAR/fig/reqbox.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..c7904a1c97f36b545004349f8bfdd0f5e7ec6998
Binary files /dev/null and b/doc/AVATAR/fig/reqbox.jpg differ
diff --git a/doc/AVATAR/fig/reqdiagram.jpg b/doc/AVATAR/fig/reqdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..8062f796d850d02dd7c480abf6a7ab33dce281b5
Binary files /dev/null and b/doc/AVATAR/fig/reqdiagram.jpg differ
diff --git a/doc/AVATAR/fig/reqgeneral.jpg b/doc/AVATAR/fig/reqgeneral.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..075ce532a4b85fa78749844905eaff938ecaba09
Binary files /dev/null and b/doc/AVATAR/fig/reqgeneral.jpg differ
diff --git a/doc/AVATAR/fig/rg.png b/doc/AVATAR/fig/rg.png
new file mode 100644
index 0000000000000000000000000000000000000000..254ba2554006b57428921a05d73ef9dbe7e46e3f
Binary files /dev/null and b/doc/AVATAR/fig/rg.png differ
diff --git a/doc/AVATAR/fig/rg1.jpg b/doc/AVATAR/fig/rg1.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..ee551930ae6170577a4c00a73737c4fcdf871d6f
Binary files /dev/null and b/doc/AVATAR/fig/rg1.jpg differ
diff --git a/doc/AVATAR/fig/selectdiagram.jpg b/doc/AVATAR/fig/selectdiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..490434c57a080189b9613dec8fec1c7cde405eaa
Binary files /dev/null and b/doc/AVATAR/fig/selectdiagram.jpg differ
diff --git a/doc/AVATAR/fig/setattribute.png b/doc/AVATAR/fig/setattribute.png
new file mode 100644
index 0000000000000000000000000000000000000000..7994033f36d61c220823cd1c1d9a2ed212435cdb
Binary files /dev/null and b/doc/AVATAR/fig/setattribute.png differ
diff --git a/doc/AVATAR/fig/setsignal.png b/doc/AVATAR/fig/setsignal.png
new file mode 100644
index 0000000000000000000000000000000000000000..2517028665cb28c7278e221fae5e1c467c3d4aab
Binary files /dev/null and b/doc/AVATAR/fig/setsignal.png differ
diff --git a/doc/AVATAR/fig/simstep1.png b/doc/AVATAR/fig/simstep1.png
new file mode 100644
index 0000000000000000000000000000000000000000..b9ea1421d1f7e0b588fab3e5f004dc8ce795c63a
Binary files /dev/null and b/doc/AVATAR/fig/simstep1.png differ
diff --git a/doc/AVATAR/fig/simstep2.png b/doc/AVATAR/fig/simstep2.png
new file mode 100644
index 0000000000000000000000000000000000000000..43bffd45b7f391e8ffc8838a3693c20d1225e923
Binary files /dev/null and b/doc/AVATAR/fig/simstep2.png differ
diff --git a/doc/AVATAR/fig/structelementsblock.png b/doc/AVATAR/fig/structelementsblock.png
new file mode 100644
index 0000000000000000000000000000000000000000..233307ef5d854fd64e84aca59951b8f1d63bc3ad
Binary files /dev/null and b/doc/AVATAR/fig/structelementsblock.png differ
diff --git a/doc/AVATAR/fig/structusecase.jpg b/doc/AVATAR/fig/structusecase.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..499067baed95569324f0d81425fcffc79659b7b6
Binary files /dev/null and b/doc/AVATAR/fig/structusecase.jpg differ
diff --git a/doc/AVATAR/fig/syntaxanalysis.jpg b/doc/AVATAR/fig/syntaxanalysis.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..9a6d8e955c871cb733b7397024329855a3c9075f
Binary files /dev/null and b/doc/AVATAR/fig/syntaxanalysis.jpg differ
diff --git a/doc/AVATAR/fig/syntaxerror.png b/doc/AVATAR/fig/syntaxerror.png
new file mode 100644
index 0000000000000000000000000000000000000000..dde075304cb87e62fb10691665b490be8ebb32b7
Binary files /dev/null and b/doc/AVATAR/fig/syntaxerror.png differ
diff --git a/doc/AVATAR/fig/systemassumptions.jpg b/doc/AVATAR/fig/systemassumptions.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..853ff1369ad7b97dd83e30e0ac1847caee96edbf
Binary files /dev/null and b/doc/AVATAR/fig/systemassumptions.jpg differ
diff --git a/doc/AVATAR/fig/tokendiagram.jpg b/doc/AVATAR/fig/tokendiagram.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..12ab33d7dcd6a241d206dd9045ad185e7debf81d
Binary files /dev/null and b/doc/AVATAR/fig/tokendiagram.jpg differ
diff --git a/doc/AVATAR/fig/usecase.jpg b/doc/AVATAR/fig/usecase.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..c1294fd9a43983fdd17975fdd0faa281ca3056f4
Binary files /dev/null and b/doc/AVATAR/fig/usecase.jpg differ
diff --git a/doc/SysMLSec/fig/automaticgeneration.png b/doc/SysMLSec/fig/automaticgeneration.png
index 291d004ec17390a9ac0b49aafac20576011e5c50..8eab6689642463fe8abaf0bdc0afee20e0927adb 100644
Binary files a/doc/SysMLSec/fig/automaticgeneration.png and b/doc/SysMLSec/fig/automaticgeneration.png differ
diff --git a/src/main/java/tmltranslator/SecurityPattern.java b/src/main/java/tmltranslator/SecurityPattern.java
index a9018cb0e269083159e8e7a49346f42826b48c4a..e63e64d8614d690b8ceecfefd0346e49f9d17614 100644
--- a/src/main/java/tmltranslator/SecurityPattern.java
+++ b/src/main/java/tmltranslator/SecurityPattern.java
@@ -44,8 +44,8 @@ import avatartranslator.AvatarState;
public class SecurityPattern {
- public String name;
- public String type;
+ public String name="";
+ public String type="";
public int overhead=0;
public int size=0;
public int encTime=0;
@@ -88,8 +88,12 @@ public class SecurityPattern {
s += "\" encTime=\"" + encTime;
s += "\" decTime=\"" + decTime;
s += "\" originTask=\"" + originTask;
- s += "\" state1=\"" + state1.getName();
- s += "\" state2=\"" + state2.getName();
+ if (state1!=null){
+ s += "\" state1=\"" + state1.getName();
+ }
+ if (state2!=null){
+ s += "\" state2=\"" + state2.getName();
+ }
s += "\" nonce=\"" + nonce;
s += "\" formula=\"" + formula;
s += "\" key=\"" + key;
diff --git a/src/main/java/tmltranslator/TMLActivityElementChannel.java b/src/main/java/tmltranslator/TMLActivityElementChannel.java
index e7a93f9bbc2f3d37e831bf91a619d6efbd48a1db..34dd5221b5a0bbcb73a76e3dd3f14e7dd703503b 100755
--- a/src/main/java/tmltranslator/TMLActivityElementChannel.java
+++ b/src/main/java/tmltranslator/TMLActivityElementChannel.java
@@ -54,6 +54,7 @@ public class TMLActivityElementChannel extends TMLActivityElement {
protected ArrayList<TMLChannel> channels;
protected String nbOfSamples;
private boolean isAttacker;
+ protected boolean isEncForm; //If the Cryptographic
public TMLActivityElementChannel(String _name, Object _referenceObject) {
super(_name, _referenceObject);
@@ -88,7 +89,14 @@ public class TMLActivityElementChannel extends TMLActivityElement {
public String getNbOfSamples() {
return nbOfSamples;
}
-
+
+ public boolean getEncForm(){
+ return isEncForm;
+ }
+ public void setEncForm(boolean form){
+ isEncForm = form;
+ }
+
public void replaceChannelWith(TMLChannel oldChan, TMLChannel newChan) {
if (channels.contains(oldChan)) {
channels.remove(oldChan);
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index f342c93fd4f84213235d14e60a612dd3ae793395..cbaa84ea0ac57ccd1dd1c0737fed09c5f5eee968 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -92,7 +92,12 @@ public class TML2Avatar {
public TML2Avatar(TMLMapping<?> tmlmap, boolean modelcheck, boolean sec) {
this.tmlmap = tmlmap;
+
this.tmlmodel = tmlmap.getTMLModeling();
+
+ for (TMLTask task: this.tmlmodel.getTasks()){
+ System.out.println("MOD " + task.getActivityDiagram().toXML());
+ }
allStates = new ArrayList<String>();
attrsToCheck = new ArrayList<String>();
mc = modelcheck;
@@ -1134,10 +1139,21 @@ public class TML2Avatar {
List<String> tmp = new ArrayList<String>();
secChannelMap.put(ae.securityPattern.name, tmp);
}
+
secChannelMap.get(ae.securityPattern.name).add(ch.getName());
- as.addValue(ae.securityPattern.name + "_encrypted");
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ if (aec.getEncForm()){
+ as.addValue(ae.securityPattern.name + "_encrypted");
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ else {
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ as.addValue(ae.securityPattern.name);
+
+ }
}
} else {
as.addValue(getName(ch.getName()) + "_chData");
@@ -1217,14 +1233,21 @@ public class TML2Avatar {
AvatarAttribute data = new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null);
block.addAttribute(data);
} else {
- //send encrypted data or unecrypted security pattern
+ //send encrypted data
//
- //if (){
- // }
- // else {
+ if (aec.getEncForm()){
as.addValue(ae.securityPattern.name + "_encrypted");
AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
block.addAttribute(data);
+ }
+ else {
+ //Send unecrypted form
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
+ AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ as.addValue(ae.securityPattern.name);
+ }
if (!secChannelMap.containsKey(ae.securityPattern.name)) {
List<String> tmp = new ArrayList<String>();
@@ -1712,10 +1735,23 @@ public class TML2Avatar {
//Add authenticity pragmas
for (String s: signalAuthOriginMap.keySet()){
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
if (signalAuthDestMap.containsKey(s)){
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
- //System.out.println("adding pragma " + s);
- avspec.addPragma(pragma);
+ if (secChannelMap.containsKey(s)){
+ for (String channel: secChannelMap.get(s)){
+ TMLChannel ch = tmlmodel.getChannelByShortName(channel);
+ if (ch!=null){
+ if (ch.checkAuth){
+ avspec.addPragma(pragma);
+ break;
+ }
+ }
+ }
+
+ }
+ else {
+ avspec.addPragma(pragma);
+ }
}
}
diff --git a/src/main/java/ui/GTMLModeling.java b/src/main/java/ui/GTMLModeling.java
index 405730f7d80b6e4f2c189d205103b98bdfe04d7f..545af8aa925b49b37457394b07315957ad9aa89e 100755
--- a/src/main/java/ui/GTMLModeling.java
+++ b/src/main/java/ui/GTMLModeling.java
@@ -1993,6 +1993,7 @@ public class GTMLModeling {
} else {
tmlreadchannel = new TMLReadChannel("read channel", tgc);
tmlreadchannel.setNbOfSamples(modifyString(((TMLADReadChannel) tgc).getSamplesValue()));
+ tmlreadchannel.setEncForm(((TMLADReadChannel) tgc).getEncForm());
tmlreadchannel.addChannel(channel);
//security pattern
if (securityPatterns.get(((TMLADReadChannel) tgc).getSecurityContext()) != null) {
@@ -2303,6 +2304,7 @@ public class GTMLModeling {
if (!error) {
tmlwritechannel = new TMLWriteChannel("write channel", tgc);
tmlwritechannel.setNbOfSamples(modifyString(((TMLADWriteChannel) tgc).getSamplesValue()));
+ tmlwritechannel.setEncForm(((TMLADWriteChannel) tgc).getEncForm());
for (int i = 0; i < channels.length; i++) {
channel = tmlm.getChannelByName(getFromTable(tmltask, channels[i]));
tmlwritechannel.addChannel(channel);
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 856e18fc7f0258a3e7d4fcbbecdb9bf7353208d5..ea027f795e28f5544ec5318dc0a3d94d323b993f 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -738,9 +738,55 @@ public class GTURTLEModeling {
}
return path;
}
+
+ public boolean pathExists(TMLMapping<TGComponent> map, HwBridge firewallNode, TMLTask t1){
+ List<HwLink> links = map.getTMLArchitecture().getHwLinks();
+ List<HwNode> found = new ArrayList<HwNode>();
+ List<HwNode> done = new ArrayList<HwNode>();
+ List<HwNode> path = new ArrayList<HwNode>();
+
+ HwExecutionNode node1 = (HwExecutionNode) map.getHwNodeOf(t1);
+
+ Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
+ for (HwLink link : links) {
+ if (link.hwnode == node1) {
+ found.add(link.bus);
+ }
+ }
+ while (found.size() > 0) {
+ System.out.println("found " + found);
+ HwNode curr = found.remove(0);
+ for (HwLink link : links) {
+ //System.out.println("LINK " + link.hwnode.getName() + " " + link.bus.getName());
+ if (curr == link.bus) {
+
+ if (link.hwnode.getName().equals(firewallNode.getName())) {
+ return true;
+ }
+ if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
+ found.add(link.hwnode);
+ }
+ } else if (curr == link.hwnode) {
+ if (!done.contains(link.bus) && !found.contains(link.bus)) {
+ found.add(link.bus);
+ }
+ }
+ }
+ done.add(curr);
+ }
+ System.out.println("!pathExists " + t1.getName() + " " + firewallNode);
+ return false;
+ }
public TMLMapping<TGComponent> drawFirewall(TMLMapping<TGComponent> map) {
+
+
+ Map<String, Integer> channelIndexMap = new HashMap<String, Integer>();
//
+ //Request Index indicates channel or update rules
+ //index = 0 : update rules
+ //index = 1-n: channel
+ int index=1;
TGComponent comp = map.getTMLModeling().getTGComponent();
TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) comp.getTDiagramPanel().tp;
// TMLComponentDesignPanel tmlcdp = map.getTMLCDesignPanel();
@@ -786,6 +832,8 @@ public class GTURTLEModeling {
HashMap<TMLChannel, TMLChannel> outChans = new HashMap<TMLChannel, TMLChannel>();
if (TraceManager.devPolicy == TraceManager.TO_CONSOLE) {
firewallComp = new TMLCPrimitiveComponent(tmlcdp.tmlctdp.getMaxX()-100, tmlcdp.tmlctdp.getMaxY()-100, tmlcdp.tmlctdp.getMinX(), tmlcdp.tmlctdp.getMaxX(), tmlcdp.tmlctdp.getMinY(), tmlcdp.tmlctdp.getMaxY(), false, null, tcp.tmlctdp);
+ TAttribute reqIndex = new TAttribute(2, "index", "0", 0);
+ firewallComp.getAttributeList().add(reqIndex);
tcp.tmlctdp.addComponent(firewallComp, 0, 0, false, true);
firewallComp.setValueWithChange(firewallNode.getName());
firewallADP = tcp.getTMLActivityDiagramPanel(firewallNode.getName());
@@ -802,9 +850,23 @@ public class GTURTLEModeling {
TMLActivity act = firewall.getActivityDiagram();
TraceManager.addDev("FirewallADP " + firewallADP);
+
+
for (TMLChannel chan : channelsCopy) {
+
+
+
TMLTask orig = chan.getOriginTask();
TMLTask dest = chan.getDestinationTask();
+
+ //If firewall does not filter these tasks, continue on
+ if (!pathExists(map, firewallNode, orig) && !pathExists(map, firewallNode, dest)){
+ toAdd.add(chan);
+ continue;
+ }
+
+ channelIndexMap.put(chan.getName(), index);
+ index++;
TMLPort origPort = chan.getOriginPort();
TMLPort destPort = chan.getDestinationPort();
TMLChannel wr = new TMLChannel(chan.getName() + "_firewallIn", chan.getReferenceObject());
@@ -978,9 +1040,13 @@ public class GTURTLEModeling {
loop.setInfinite(true);
start.addNext(loop);
act.addElement(loop);
- //Add choice
+ //Add choice for update or channel
+
+
+
TMLChoice choice = new TMLChoice("chooseChannel", adChoice);
+// choice.setGuard("[channelIndex=="+channelIndexMap.get(ch.name)+"]",i-1);
act.addElement(choice);
loop.addNext(choice);
map.getCorrespondanceList().addCor(choice, adChoice);
@@ -1032,9 +1098,13 @@ public class GTURTLEModeling {
}
}
+ //Replace channel operator with new firewallIn and firewallOut operators
+
//Redo all reference objects
- map.getCorrespondanceList().useDIPLOIDs();
+ //map.getCorrespondanceList().useDIPLOIDs();
+
+ //Redo syntax checking
return map;
}
diff --git a/src/main/java/ui/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
index 5930fb6c94ef76a6e449b1548e3c4771e293a279..8bb011e5e40293e8fb807c93a1791dee60fa9218 100644
--- a/src/main/java/ui/SecurityGeneration.java
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -690,6 +690,7 @@ public class SecurityGeneration implements Runnable {
if (channel.equals(wChannel.getChannelName()) && wChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing write channel " + wChannel.getChannelName());
wChannel.setSecurityContext(channelSecMap.get(channel));
+ wChannel.setEncForm(true);
}
}
@@ -782,6 +783,7 @@ public class SecurityGeneration implements Runnable {
if (channel.equals(wChannel.getChannelName()) && wChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing write channel " + wChannel.getChannelName());
wChannel.setSecurityContext(channelSecMap.get(channel));
+ wChannel.setEncForm(true);
tad.repaint();
}
}
@@ -813,6 +815,7 @@ public class SecurityGeneration implements Runnable {
String chanName = writeChannel.getChannelName();
TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + chanName);
writeChannel.setSecurityContext(channelSecMap.get(chanName));
+ writeChannel.setEncForm(true);
xpos = chan.getX();
ypos = chan.getY();
fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
@@ -832,7 +835,7 @@ public class SecurityGeneration implements Runnable {
tad.addComponent(req, xpos, ypos + yShift, false, true);
fromStart.setP2(req.getTGConnectingPointAtIndex(0));
- tad.addComponent(fromStart, xpos, ypos, false, true);
+ //tad.addComponent(fromStart, xpos, ypos, false, true);
//Add connection
fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
@@ -850,6 +853,7 @@ public class SecurityGeneration implements Runnable {
//Add write channel operator
wr = new TMLADWriteChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
wr.setChannelName("data_" + chanName + "_" + task.getName().split("__")[1]);
+ wr.setEncForm(false);
wr.setSecurityContext(channelSecMap.get(chanName));
tad.addComponent(wr, xpos, ypos + yShift, false, true);
@@ -961,9 +965,10 @@ public class SecurityGeneration implements Runnable {
String chanName = readChannel.getChannelName();
TMLChannel tmlc = tmlmodel.getChannelByName(title + "__" + chanName);
readChannel.setSecurityContext(channelSecMap.get(chanName));
- xpos = chan.getX();
- ypos = chan.getY();
- fromStart = tad.findTGConnectorEndingAt(chan.getTGConnectingPointAtIndex(0));
+ readChannel.setEncForm(true);
+ xpos = chan.getX()+1;
+ ypos = chan.getY()+1;
+ fromStart = tad.findTGConnectorStartingAt(chan.getTGConnectingPointAtIndex(1));
point = fromStart.getTGConnectingPointP2();
int yShift = 50;
@@ -997,10 +1002,11 @@ public class SecurityGeneration implements Runnable {
wr.setSecurityContext(channelSecMap.get(chanName));
tad.addComponent(wr, xpos, ypos + yShift, false, true);
-
+ //Add connector between request and write
fromStart.setP2(wr.getTGConnectingPointAtIndex(0));
tad.addComponent(fromStart, xpos, ypos, false, true);
+ //Add connector between write and ???
fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
tad.addComponent(fromStart, xpos, ypos, false, true);
fromStart.setP1(wr.getTGConnectingPointAtIndex(1));
@@ -1085,6 +1091,7 @@ public class SecurityGeneration implements Runnable {
TMLADReadChannel rd = new TMLADReadChannel(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
rd.setChannelName("retData_" + chanName + "_" + task.getName().split("__")[1]);
rd.setSecurityContext(channelSecMap.get(chanName));
+ rd.setEncForm(false);
tad.addComponent(rd, xpos, ypos + yShift, false, true);
fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
@@ -1096,10 +1103,11 @@ public class SecurityGeneration implements Runnable {
fromStart.setP1(rd.getTGConnectingPointAtIndex(1));
yShift += 50;
- //Direct the last TGConnector back to the start of the read channel operator
+ //Direct the last TGConnector back to the start of the operator after the read channel
fromStart.setP2(point);
+
//Shift components down to make room for the added ones, and add security contexts to write channels
for (TGComponent tg : tad.getComponentList()) {
if (tg.getY() >= ypos && tg != wr && tg != req && tg != rd && tg!=wr2 && tg!=nonce && tg!=wr3) {
@@ -1210,6 +1218,7 @@ public class SecurityGeneration implements Runnable {
if (channel.equals(readChannel.getChannelName()) && readChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
readChannel.setSecurityContext(channelSecMap.get(readChannel.getChannelName()));
+ readChannel.setEncForm(true);
}
}
@@ -1300,6 +1309,7 @@ public class SecurityGeneration implements Runnable {
yShift = 40;
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
readChannel.setSecurityContext(channelSecMap.get(readChannel.getChannelName()));
+ readChannel.setEncForm(true);
tad.repaint();
//Add decryption operator if it does not already exist
xpos = readChannel.getX();
@@ -1322,6 +1332,7 @@ public class SecurityGeneration implements Runnable {
if (channel.equals(readChannel.getChannelName()) && readChannel.getSecurityContext().equals("")) {
TraceManager.addDev("Securing read channel " + readChannel.getChannelName());
readChannel.setSecurityContext( channelSecMap.get(readChannel.getChannelName()));
+ readChannel.setEncForm(true);
}
}
@@ -1524,8 +1535,14 @@ public class SecurityGeneration implements Runnable {
rd.setChannelName("data_" + ch.name + "_" + ch.task);
rd.setSecurityContext(channelSecMap.get(ch.name));
tad.addComponent(rd, xc, 300, false, true);
- //Connect choice and readchannel
+ //Recieve plaintext data if encrypting
+ if (ch.secType != HSMChannel.DEC) {
+ rd.setEncForm(false);
+ }
+
+ //Connect choice and readchannel
+
fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
fromStart.setP1(choice.getTGConnectingPointAtIndex(i));
fromStart.setP2(rd.getTGConnectingPointAtIndex(0));
@@ -1559,6 +1576,10 @@ public class SecurityGeneration implements Runnable {
TMLADWriteChannel wr = new TMLADWriteChannel(xc, 600, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
wr.setChannelName("retData_" + ch.name + "_" + ch.task);
+ //Return plaintext data if decrypting
+ if (ch.secType == HSMChannel.DEC) {
+ wr.setEncForm(false);
+ }
tad.addComponent(wr, xc, 600, false, true);
diff --git a/src/main/java/ui/tmlad/TMLADReadChannel.java b/src/main/java/ui/tmlad/TMLADReadChannel.java
index a72fd4e6de43cb064e0c85780a2450f669830ce4..97b2a4358cde48b05e00ece0fbda06432b9d9e4d 100755
--- a/src/main/java/ui/tmlad/TMLADReadChannel.java
+++ b/src/main/java/ui/tmlad/TMLADReadChannel.java
@@ -93,7 +93,8 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
public int reachabilityInformation;
-
+ public boolean isEncForm = true;
+
public TMLADReadChannel(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -182,7 +183,12 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
g.drawString(value, x + linebreak + textX0, y + textY1);
if (!securityContext.equals("")) {
+ c = g.getColor();
+ if (!isEncForm){
+ g.setColor(Color.RED);
+ }
g.drawString("sec:" + securityContext, x + 3 * width / 4, y + height + textY1 - decSec);
+ g.setColor(c);
}
drawReachabilityInformation(g);
if (getCheckLatency()) {
@@ -284,16 +290,19 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
tab1.help = help;
TabInfo tab2 = new TabInfo("Security");
- labels = new String[2];
- values = new String[2];
+ labels = new String[3];
+ values = new String[3];
labels[0] = "Security Pattern";
values[0] = securityContext;
labels[1] = "Attacker?";
values[1] = isAttacker ? "Yes" : "No";
+ labels[2] = "Encrypted Form?";
+ values[2] = isEncForm ? "Yes" : "No";
help = new ArrayList<String[]>();
String[] choice = new String[]{"Yes", "No"};
help.add(tdp.getMGUI().getCurrentCryptoConfig());
help.add(choice);
+ help.add(choice);
tab2.labels=labels;
tab2.values = values;
tab2.help = help;
@@ -313,6 +322,7 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
nbOfSamples = jdmsat.getString(0, 1);
securityContext = jdmsat.getString(1, 0);
isAttacker = jdmsat.getString(1, 1).equals("Yes");
+ isEncForm = jdmsat.getString(1, 2).equals("Yes");
makeValue();
return true;
}
@@ -337,6 +347,8 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
sb.append(securityContext);
sb.append("\" isAttacker=\"");
sb.append(isAttacker ? "Yes" : "No");
+ sb.append("\" isEncForm=\"");
+ sb.append(isEncForm ? "Yes" : "No");
sb.append("\" />\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -363,6 +375,12 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
nbOfSamples = elt.getAttribute("nbOfSamples");
securityContext = elt.getAttribute("secPattern");
isAttacker = elt.getAttribute("isAttacker").equals("Yes");
+ isEncForm = elt.getAttribute("isEncForm").equals("Yes");
+ if (elt.getAttribute("isEncForm").equals("") || !elt.hasAttribute("isEncForm")){
+ if (!securityContext.equals("")){
+ isEncForm=true;
+ }
+ }
}
}
}
@@ -399,6 +417,14 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
public void setStateAction(int _stateAction) {
stateOfError = _stateAction;
}
+ public boolean getEncForm(){
+ return isEncForm;
+ }
+
+ public void setEncForm(boolean encForm){
+ isEncForm=encForm;
+ }
+
public void setChannelName(String s) {
channelName = s;
diff --git a/src/main/java/ui/tmlad/TMLADWriteChannel.java b/src/main/java/ui/tmlad/TMLADWriteChannel.java
index 07ca8cde9fa33edd50e9d451e73f780af1526fb9..3eb3ca19ac03d308891229890dce37ff025d1af7 100755
--- a/src/main/java/ui/tmlad/TMLADWriteChannel.java
+++ b/src/main/java/ui/tmlad/TMLADWriteChannel.java
@@ -94,6 +94,8 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
public int reachabilityInformation;
+ public boolean isEncForm = true;
+
public TMLADWriteChannel(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -176,7 +178,12 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
}
g.drawString(value, x + (width - w) / 2, y + textY);
if (!securityContext.equals("")) {
+ c = g.getColor();
+ if (!isEncForm){
+ g.setColor(Color.RED);
+ }
g.drawString("sec:" + securityContext, x + 3 * width / 4, y + height + textY - decSec);
+ g.setColor(c);
}
if (getCheckLatency()) {
@@ -304,16 +311,19 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
tab1.help = help;
TabInfo tab2 = new TabInfo("Security");
- labels = new String[2];
- values = new String[2];
+ labels = new String[3];
+ values = new String[3];
labels[0] = "Security Pattern";
values[0] = securityContext;
labels[1] = "Attacker?";
values[1] = isAttacker ? "Yes" : "No";
+ labels[2] = "Encrypted Form?";
+ values[2] = isEncForm ? "Yes" : "No";
help = new ArrayList<String[]>();
help.add(tdp.getMGUI().getCurrentCryptoConfig());
help.add(choice);
+ help.add(choice);
tab2.labels=labels;
tab2.values = values;
tab2.help = help;
@@ -334,9 +344,10 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
nbOfSamples = jdmsat.getString(0, 1);
securityContext = jdmsat.getString(1, 0);
isAttacker = jdmsat.getString(1, 1).equals("Yes");
+ isEncForm = jdmsat.getString(1, 2).equals("Yes");
makeValue();
- System.out.println(channelName + " " + securityContext + " " + isAttacker);
+
return true;
}
@@ -355,6 +366,8 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
sb.append(securityContext);
sb.append("\" isAttacker=\"");
sb.append(isAttacker ? "Yes" : "No");
+ sb.append("\" isEncForm=\"");
+ sb.append(isEncForm ? "Yes" : "No");
sb.append("\" />\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -387,6 +400,12 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
nbOfSamples = elt.getAttribute("nbOfSamples");
securityContext = elt.getAttribute("secPattern");
isAttacker = elt.getAttribute("isAttacker").equals("Yes");
+ isEncForm = elt.getAttribute("isEncForm").equals("Yes");
+ if (elt.getAttribute("isEncForm").equals("") || !elt.hasAttribute("isEncForm")){
+ if (!securityContext.equals("")){
+ isEncForm=true;
+ }
+ }
}
}
}
@@ -435,6 +454,15 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
return isAttacker;
}
+ public boolean getEncForm(){
+ return isEncForm;
+ }
+
+
+ public void setEncForm(boolean encForm){
+ isEncForm=encForm;
+ }
+
public void setStateAction(int _stateAction) {
stateOfError = _stateAction;
}