From e7caabe061b89a12715f03a1ca05479feaab945d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ben=20Br=C3=BCcker?= <Benbruecker@student.ru.nl>
Date: Sat, 28 Dec 2013 15:29:21 +0100
Subject: [PATCH] Initial version of the naive model

---
 Model/model.xml | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/Model/model.xml b/Model/model.xml
index ff21437..315a160 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -1,7 +1,14 @@
 <?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.
-</declaration><template><name x="5" y="5">Template</name><declaration>// Place local declarations here.
-</declaration><location id="id0" x="16" y="-40"></location><init ref="id0"/></template><system>// Place template instantiations here.
-Process = Template();
+</declaration><template><name>Network</name><declaration>const int MAX_TT = 2000; // Arbitrary Max Round Trip Time for now
+const int MIN_TT = 200; // Arbitrary Max Round Trip Time for now
+
+chan SYN, ACK, SYN_ACK;
+
+clock transmission_time;</declaration><location id="id0" x="-1056" y="-416"><name x="-1096" y="-400">PacketLost</name></location><location id="id1" x="-864" y="-544"><name x="-912" y="-624">PacketInTransit</name></location><location id="id2" x="-480" y="-544"><name x="-536" y="-624">PacketDelivered</name></location><location id="id3" x="-1248" y="-544"><name x="-1304" y="-624">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id3"/><nail x="-1248" y="-416"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="-856" y="-480">transmission_time &gt; MAX_TT</label><nail x="-864" y="-416"/></transition><transition><source ref="id2"/><target ref="id3"/><nail x="-480" y="-288"/><nail x="-1344" y="-288"/><nail x="-1344" y="-544"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="-776" y="-584">transmission_time &lt;= MAX_TT</label><label kind="synchronisation" x="-680" y="-560">SYN!</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="synchronisation" x="-1080" y="-568">SYN?</label><label kind="assignment" x="-1136" y="-584">transmission_time := 0</label></transition></template><template><name>Host_Handshake</name><declaration>chan SYN, ACK, SYN_ACK;</declaration><location id="id4" x="-96" y="0"></location><location id="id5" x="-384" y="-96"></location><location id="id6" x="-672" y="-192"></location><location id="id7" x="-384" y="0"><name x="-416" y="16">Established</name></location><location id="id8" x="-672" y="-96"><name x="-752" y="-104">SynRcvd</name></location><location id="id9" x="-96" y="-96"><name x="-72" y="-104">SynSent</name></location><location id="id10" x="-384" y="-192"><name x="-400" y="-232">Listen</name></location><location id="id11" x="-384" y="-384"><name x="-440" y="-416">Closed</name></location><init ref="id11"/><transition><source ref="id4"/><target ref="id7"/><label kind="synchronisation" x="-248" y="-24">ACK!</label></transition><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-552" y="-120">ACK!</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-664" y="-160">SYN_ACK!</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="synchronisation" x="-552" y="-216">SYN?</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="synchronisation" x="-88" y="-56">SYN_ACK?</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-256" y="-120">SYN?</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-256" y="-216">SYN!</label><nail x="-128" y="-192"/><nail x="-128" y="-128"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="synchronisation" x="-552" y="-24">ACK?</label><nail x="-672" y="0"/></transition><transition><source ref="id9"/><target ref="id11"/><nail x="-64" y="-128"/><nail x="-64" y="-416"/><nail x="-352" y="-416"/></transition><transition><source ref="id11"/><target ref="id9"/><label kind="synchronisation" x="-208" y="-384">SYN!</label><nail x="-96" y="-384"/></transition><transition><source ref="id10"/><target ref="id11"/><nail x="-352" y="-224"/><nail x="-352" y="-352"/></transition><transition><source ref="id11"/><target ref="id10"/><nail x="-416" y="-352"/><nail x="-416" y="-224"/></transition></template><system>// Place template instantiations here.
+Network1 = Network();
+Host1_Handshake = Host_Handshake();
+Host2_Handshake = Host_Handshake();
 
 // List one or more processes to be composed into a system.
-system Process;</system></nta>
\ No newline at end of file
+system Network,Host1_Handshake,Host2_Handshake;
+</system></nta>
\ No newline at end of file