From a0282f7c1e7095254656d17dfea7fbf9bf076c9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ben=20Br=C3=BCcker?= <Benbruecker@student.ru.nl>
Date: Sun, 29 Dec 2013 15:10:08 +0100
Subject: [PATCH] Abstracted channels, much better now

---
 Model/model.xml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/Model/model.xml b/Model/model.xml
index a9c6bab..02c0a45 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -1,16 +1,19 @@
 <?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>Network</name><parameter>chan &amp;SYN_in, chan &amp;ACK_in, chan &amp;SYN_ACK_in, chan &amp;SYN_out, chan &amp;ACK_out, chan &amp;SYN_ACK_out</parameter><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
+const int HOSTS = 2;
 
-clock transmission_time;</declaration><location id="id0" x="-1216" y="-640"><name x="-1384" y="-656">SynAckPacketInTransit</name></location><location id="id1" x="-704" y="-640"><name x="-688" y="-656">AckPacketInTransit</name></location><location id="id2" x="-960" y="-864"><name x="-1104" y="-888">SynPacketInTransit</name></location><location id="id3" x="-960" y="-608"><name x="-1008" y="-584">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-1144" y="-576">SYN_ACK_out!</label><nail x="-1216" y="-576"/></transition><transition><source ref="id1"/><target ref="id3"/><label kind="synchronisation" x="-840" y="-584">ACK_out!</label><nail x="-704" y="-576"/></transition><transition><source ref="id2"/><target ref="id3"/><label kind="synchronisation" x="-928" y="-784">SYN_out!</label><nail x="-928" y="-864"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="synchronisation" x="-1088" y="-672">SYN_ACK_in?</label><label kind="assignment" x="-1144" y="-656">transmission_time := 0</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="synchronisation" x="-832" y="-672">ACK_in?</label><label kind="assignment" x="-920" y="-656">transmission_time := 0</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-1056" y="-784">SYN_in?</label><label kind="assignment" x="-1144" y="-768">transmission_time := 0</label><nail x="-992" y="-864"/></transition></template><template><name>Host_Handshake</name><parameter>chan &amp;SYN_out, chan &amp;ACK_out, chan &amp;SYN_ACK_out, chan &amp;SYN_in, chan &amp;ACK_in, chan &amp;SYN_ACK_in</parameter><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_out!</label></transition><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-552" y="-120">ACK_out!</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-664" y="-160">SYN_ACK_out!</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="synchronisation" x="-552" y="-216">SYN_in?</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="synchronisation" x="-88" y="-56">SYN_ACK_in?</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-256" y="-120">SYN_in?</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-256" y="-216">SYN_out!</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_in?</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_out!</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>chan SYN_1toN, ACK_1toN, SYN_ACK_1toN, SYN_2toN, ACK_2toN, SYN_ACK_2toN;
-chan SYN_Nto1, ACK_Nto1, SYN_ACK_Nto1, SYN_Nto2, ACK_Nto2, SYN_ACK_Nto2;
+chan SYN[HOSTS+1], ACK[HOSTS+1], SYN_ACK[HOSTS+1];
 
-// Place template instantiations here.
-Network1 = Network(SYN_1toN, ACK_1toN, SYN_ACK_1toN, SYN_Nto2, ACK_Nto2, SYN_ACK_Nto2);
-Network2 = Network(SYN_2toN, ACK_2toN, SYN_ACK_2toN, SYN_Nto1, ACK_Nto1, SYN_ACK_Nto1);
-Host1Handshake = Host_Handshake(SYN_1toN, ACK_1toN, SYN_ACK_1toN, SYN_Nto1, ACK_Nto1, SYN_ACK_Nto1);
-Host2Handshake = Host_Handshake(SYN_2toN, ACK_2toN, SYN_ACK_2toN, SYN_Nto2, ACK_Nto2, SYN_ACK_Nto2);
+int target_address; //Global variable to pass the target address to the network</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
+
+void set_target() {
+    target = target_address;
+}</declaration><location id="id0" x="-1216" y="-640"><name x="-1384" y="-656">SynAckPacketInTransit</name></location><location id="id1" x="-704" y="-640"><name x="-688" y="-656">AckPacketInTransit</name></location><location id="id2" x="-960" y="-864"><name x="-1104" y="-888">SynPacketInTransit</name></location><location id="id3" x="-960" y="-608"><name x="-1008" y="-584">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-1144" y="-576">SYN_ACK[target]!</label><nail x="-1216" y="-576"/></transition><transition><source ref="id1"/><target ref="id3"/><label kind="synchronisation" x="-832" y="-584">ACK[target]!</label><nail x="-704" y="-576"/></transition><transition><source ref="id2"/><target ref="id3"/><label kind="synchronisation" x="-928" y="-784">SYN[target]!</label><nail x="-928" y="-864"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="synchronisation" x="-1144" y="-688">SYN_ACK[network]?</label><label kind="assignment" x="-1144" y="-672">set_target()</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="synchronisation" x="-920" y="-688">ACK[network]?</label><label kind="assignment" x="-920" y="-672">set_target()</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-1136" y="-784">SYN[network]?</label><label kind="assignment" x="-1136" y="-768">set_target()</label><nail x="-992" y="-864"/></transition></template><template><name>Host_Handshake</name><parameter>const int local, const int remote, const int network</parameter><declaration>
+void set_target() {
+    target_address = remote;
+}</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="-456" y="-384">Closed</name></location><init ref="id11"/><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-544" y="-440">ACK[local]?</label><nail x="-512" y="-384"/><nail x="-512" y="-416"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-368" y="-536">SYN[local]?</label><nail x="-320" y="-512"/><nail x="-352" y="-512"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-496" y="-536">SYN_ACK[local]?</label><nail x="-448" y="-512"/><nail x="-416" y="-512"/></transition><transition><source ref="id4"/><target ref="id7"/><label kind="synchronisation" x="-272" y="-40">ACK[network]!</label><label kind="assignment" x="-272" y="-24">set_target()</label></transition><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-552" y="-136">ACK[network]!</label><label kind="assignment" x="-552" y="-120">set_target()</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-664" y="-160">SYN_ACK[network]!</label><label kind="assignment" x="-664" y="-144">set_target()</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="synchronisation" x="-552" y="-216">SYN[local]?</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="synchronisation" x="-88" y="-56">SYN_ACK[local]?</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-256" y="-120">SYN[local]?</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-272" y="-232">SYN[network]!</label><label kind="assignment" x="-272" y="-216">set_target()</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[local]?</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[network]!</label><label kind="assignment" x="-208" y="-368">set_target()</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>Network1 = Network(0);
+Network2 = Network(0);
+Host1Handshake = Host_Handshake(1,2,0);
+Host2Handshake = Host_Handshake(2,1,0);
 
-// List one or more processes to be composed into a system.
 system Network1, Network2 ,Host1Handshake,Host2Handshake;
 </system></nta>
\ No newline at end of file