From 68392873584ed256573b6bdc34e43f28b9be0558 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <admin@recondor.com>
Date: Sun, 2 Feb 2014 15:43:34 +0100
Subject: [PATCH] Changed the model to remove old transmissions from the
 network

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

diff --git a/Model/model.xml b/Model/model.xml
index 6e47453..e44ad37 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -38,15 +38,14 @@ void set_target() {
 	target = target_address;
 }
 
-void receive_packet(){
+void receive_packet() {
 	transfer := to_network;
 	initialize(to_network);
 }
 
-void send_packet(){
+void send_packet() {
 	from_network := transfer;
-}
-</declaration><location id="id0" x="-5312" y="-1536"><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5160" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-5296" y="-1560">initialize(from_network)</label><nail x="-5280" y="-1592"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="-5384" y="-1624">c &lt;= TTL</label><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="-5296" y="-1664">packets_lost &gt; 0</label><label kind="assignment" x="-5288" y="-1648">packets_lost--</label></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5432" y="-1560">Packet[network]?</label><label kind="assignment" x="-5432" y="-1544">set_target(),
+}</declaration><location id="id0" x="-5312" y="-1536"><name x="-5304" y="-1560">AcceptMaybe</name><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5160" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name><label kind="invariant" x="-5384" y="-1656">c &lt;= TTL</label></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="-5296" y="-1664">packets_lost &gt; 0</label><label kind="assignment" x="-5288" y="-1648">packets_lost--</label></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5568" y="-1568">Packet[network]?</label><label kind="assignment" x="-5568" y="-1552">set_target(),
 receive_packet(),
 c:=0</label><nail x="-5440" y="-1408"/><nail x="-5440" y="-1664"/></transition></template><template><name>Host</name><parameter>const int local, const int remote, const int network</parameter><declaration>clock c;
 SEQ snd_nxt = 0;
@@ -85,17 +84,19 @@ void send(bool syn, bool ack) {
 void retransmit() {
 	target_address = remote;
 	to_network := retrans;
-}</declaration><location id="id4" x="-928" y="-1120"><name x="-976" y="-1144">Init</name><committed/></location><location id="id5" x="-448" y="-672"><committed/></location><location id="id6" x="-736" y="-768"><committed/></location><location id="id7" x="-992" y="-928"><committed/></location><location id="id8" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id9" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c &lt;= UBOUND</label></location><location id="id10" x="-448" y="-768"><name x="-512" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c &lt;= UBOUND</label></location><location id="id11" x="-736" y="-928"><name x="-752" y="-912">Listen</name></location><location id="id12" x="-736" y="-1120"><name x="-800" y="-1144">Closed</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id12"/><label kind="select" x="-896" y="-1120">i:SEQ</label><label kind="assignment" x="-896" y="-1104">snd_nxt := i</label></transition><transition><source ref="id6"/><target ref="id9"/><label kind="synchronisation" x="-920" y="-832">Packet[network]!</label><label kind="assignment" x="-920" y="-817">send(false, true),
-c := 0</label></transition><transition><source ref="id8"/><target ref="id8"/><nail x="-704" y="-704"/><nail x="-776" y="-704"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-1224" y="-768">c &gt; LBOUND</label><label kind="synchronisation" x="-1256" y="-784">Packet[network]!</label><label kind="assignment" x="-1224" y="-752">retransmit(),
-c:=0</label><nail x="-1120" y="-768"/><nail x="-1120" y="-744"/></transition><transition><source ref="id10"/><target ref="id10"/><label kind="guard" x="-312" y="-776">c &gt; LBOUND</label><label kind="synchronisation" x="-312" y="-792">Packet[network]!</label><label kind="assignment" x="-312" y="-760">retransmit(),
-c := 0</label><nail x="-320" y="-736"/><nail x="-320" y="-768"/></transition><transition><source ref="id12"/><target ref="id12"/><label kind="synchronisation" x="-872" y="-1192">Packet[local]?</label><label kind="assignment" x="-872" y="-1176">receive_packet()</label><nail x="-720" y="-1192"/><nail x="-752" y="-1192"/></transition><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-664" y="-672">Packet[network]!</label><label kind="assignment" x="-664" y="-656">send(false,true)</label></transition><transition><source ref="id7"/><target ref="id9"/><label kind="synchronisation" x="-1120" y="-872">Packet[network]!</label><label kind="assignment" x="-1120" y="-856">send(true,true),
-c := 0</label></transition><transition><source ref="id11"/><target ref="id7"/><label kind="guard" x="-944" y="-976">from_network.syn &amp;&amp;
-! from_network.ack</label><label kind="synchronisation" x="-944" y="-992">Packet[local]?</label><label kind="assignment" x="-944" y="-952">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id5"/><label kind="guard" x="-432" y="-712">from_network.ack &amp;&amp;
-from_network.syn</label><label kind="synchronisation" x="-432" y="-728">Packet[local]?</label><label kind="assignment" x="-432" y="-680">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="guard" x="-672" y="-816">from_network.syn&amp;&amp;
-! from_network.ack</label><label kind="synchronisation" x="-672" y="-832">Packet[local]?</label><label kind="assignment" x="-672" y="-792">receive_packet()</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="synchronisation" x="-664" y="-976">Packet[network]!</label><label kind="assignment" x="-664" y="-960">send(true, false),
-c := 0</label><nail x="-480" y="-928"/><nail x="-480" y="-800"/></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-984" y="-656">from_network.ack &amp;&amp;
-! from_network.syn</label><label kind="synchronisation" x="-984" y="-672">Packet[local]?</label><label kind="assignment" x="-984" y="-624">receive_packet()</label><nail x="-992" y="-672"/></transition><transition><source ref="id10"/><target ref="id12"/><nail x="-416" y="-800"/><nail x="-416" y="-1152"/><nail x="-704" y="-1152"/></transition><transition><source ref="id12"/><target ref="id10"/><label kind="synchronisation" x="-592" y="-1120">Packet[network]!</label><label kind="assignment" x="-592" y="-1104">send(true,false),
-c := 0</label><nail x="-448" y="-1120"/></transition><transition><source ref="id11"/><target ref="id12"/><nail x="-704" y="-960"/><nail x="-704" y="-1088"/></transition><transition><source ref="id12"/><target ref="id11"/><nail x="-768" y="-1088"/><nail x="-768" y="-960"/></transition></template><system>Network1 = Network(0);
+}</declaration><location id="id4" x="-736" y="-544"><committed/></location><location id="id5" x="-928" y="-1120"><name x="-976" y="-1144">Init</name><committed/></location><location id="id6" x="-448" y="-672"><committed/></location><location id="id7" x="-736" y="-768"><committed/></location><location id="id8" x="-992" y="-928"><committed/></location><location id="id9" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id10" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c &lt;= UBOUND</label></location><location id="id11" x="-448" y="-768"><name x="-520" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c &lt;= UBOUND</label></location><location id="id12" x="-736" y="-928"><name x="-760" y="-912">Listen</name></location><location id="id13" x="-736" y="-1120"><name x="-800" y="-1144">Closed</name></location><init ref="id5"/><transition><source ref="id11"/><target ref="id13"/><nail x="-416" y="-824"/><nail x="-416" y="-1144"/><nail x="-704" y="-1144"/></transition><transition><source ref="id12"/><target ref="id13"/><nail x="-704" y="-960"/><nail x="-704" y="-1088"/></transition><transition><source ref="id9"/><target ref="id4"/><label kind="synchronisation" x="-872" y="-592">Packet[local]?</label><nail x="-776" y="-608"/></transition><transition><source ref="id4"/><target ref="id9"/><label kind="synchronisation" x="-688" y="-592">Packet[network]!</label><label kind="assignment" x="-688" y="-576">send(false,true)</label><nail x="-696" y="-608"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="guard" x="-320" y="-832">! from_network.syn</label><label kind="synchronisation" x="-320" y="-848">Packet[local]?</label><nail x="-312" y="-800"/><nail x="-328" y="-840"/></transition><transition><source ref="id10"/><target ref="id10"/><label kind="guard" x="-1240" y="-688">! from_network.ack ||
+from_network.syn</label><label kind="synchronisation" x="-1208" y="-656">Packet[local]?</label><nail x="-1104" y="-704"/><nail x="-1072" y="-672"/></transition><transition><source ref="id12"/><target ref="id12"/><label kind="guard" x="-800" y="-896">! from_network.syn ||
+from_network.ack</label><label kind="synchronisation" x="-800" y="-872">Packet[local]?</label><nail x="-776" y="-896"/><nail x="-704" y="-896"/></transition><transition><source ref="id5"/><target ref="id13"/><label kind="select" x="-896" y="-1120">i:SEQ</label><label kind="assignment" x="-896" y="-1104">snd_nxt := i</label></transition><transition><source ref="id7"/><target ref="id10"/><label kind="synchronisation" x="-920" y="-832">Packet[network]!</label><label kind="assignment" x="-920" y="-817">send(false, true),
+c := 0</label></transition><transition><source ref="id10"/><target ref="id10"/><label kind="guard" x="-1224" y="-768">c &gt; LBOUND</label><label kind="synchronisation" x="-1248" y="-784">Packet[network]!</label><label kind="assignment" x="-1224" y="-752">retransmit(),
+c:=0</label><nail x="-1120" y="-768"/><nail x="-1120" y="-744"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="guard" x="-312" y="-776">c &gt; LBOUND</label><label kind="synchronisation" x="-312" y="-792">Packet[network]!</label><label kind="assignment" x="-312" y="-760">retransmit(),
+c := 0</label><nail x="-320" y="-736"/><nail x="-320" y="-768"/></transition><transition><source ref="id13"/><target ref="id13"/><label kind="synchronisation" x="-872" y="-1192">Packet[local]?</label><label kind="assignment" x="-872" y="-1176">receive_packet()</label><nail x="-720" y="-1192"/><nail x="-752" y="-1192"/></transition><transition><source ref="id6"/><target ref="id9"/><label kind="synchronisation" x="-664" y="-672">Packet[network]!</label><label kind="assignment" x="-664" y="-656">send(false,true)</label></transition><transition><source ref="id8"/><target ref="id10"/><label kind="synchronisation" x="-1120" y="-920">Packet[network]!</label><label kind="assignment" x="-1120" y="-904">send(true,true),
+c := 0</label></transition><transition><source ref="id12"/><target ref="id8"/><label kind="guard" x="-944" y="-976">from_network.syn &amp;&amp;
+! from_network.ack</label><label kind="synchronisation" x="-944" y="-992">Packet[local]?</label><label kind="assignment" x="-944" y="-952">receive_packet()</label></transition><transition><source ref="id11"/><target ref="id6"/><label kind="guard" x="-432" y="-712">from_network.ack &amp;&amp;
+from_network.syn</label><label kind="synchronisation" x="-432" y="-728">Packet[local]?</label><label kind="assignment" x="-432" y="-680">receive_packet()</label></transition><transition><source ref="id11"/><target ref="id7"/><label kind="guard" x="-672" y="-816">from_network.syn&amp;&amp;
+! from_network.ack</label><label kind="synchronisation" x="-672" y="-832">Packet[local]?</label><label kind="assignment" x="-672" y="-792">receive_packet()</label></transition><transition><source ref="id12"/><target ref="id11"/><label kind="synchronisation" x="-664" y="-976">Packet[network]!</label><label kind="assignment" x="-664" y="-960">send(true, false),
+c := 0</label><nail x="-480" y="-928"/><nail x="-480" y="-800"/></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="-984" y="-656">from_network.ack &amp;&amp;
+! from_network.syn</label><label kind="synchronisation" x="-984" y="-672">Packet[local]?</label><label kind="assignment" x="-984" y="-624">receive_packet()</label><nail x="-992" y="-672"/></transition><transition><source ref="id13"/><target ref="id11"/><label kind="synchronisation" x="-592" y="-1120">Packet[network]!</label><label kind="assignment" x="-592" y="-1104">send(true,false),
+c := 0</label><nail x="-448" y="-1120"/></transition><transition><source ref="id13"/><target ref="id12"/><nail x="-768" y="-1088"/><nail x="-768" y="-960"/></transition></template><system>Network1 = Network(0);
 Network2 = Network(0);
 Network3 = Network(0);
 Network4 = Network(0);