From 6b96f804faa4470156970f8402cc500617c2512b Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <j.dekker@recondor.com>
Date: Thu, 2 Jan 2014 17:05:53 +0100
Subject: [PATCH] Twee paketten.

---
 Model/model.xml | 45 ++++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 21 deletions(-)

diff --git a/Model/model.xml b/Model/model.xml
index bcc5f0e..fc079b7 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -21,7 +21,8 @@ void initialize(TCP_packet&amp; p)
  p.ack := 0;
 }
 
-TCP_packet packet;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
+TCP_packet to_network;
+TCP_packet from_network;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
 TCP_packet transfer;
 
 void set_target() {
@@ -29,13 +30,14 @@ void set_target() {
 }
 
 void receive_packet(){
-	transfer := packet;
+	transfer := to_network;
+	initialize(to_network);
 }
 
 void send_packet(){
-	packet := transfer;
+	from_network := transfer;
 }
-</declaration><location id="id0" x="-672" y="-736"><name x="-682" y="-766">PacketLost</name><committed/></location><location id="id1" x="-864" y="-864"><name x="-1008" y="-888">PacketInTransit</name></location><location id="id2" x="-864" y="-608"><name x="-912" y="-584">ReadyToReceive</name></location><init ref="id2"/><transition><source ref="id1"/><target ref="id0"/></transition><transition><source ref="id0"/><target ref="id2"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="synchronisation" x="-976" y="-768">Packet[target]!</label><label kind="assignment" x="-968" y="-752">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="-1120" y="-784">Packet[network]?</label><label kind="assignment" x="-1120" y="-768">set_target(),
+</declaration><location id="id0" x="-864" y="-736"><committed/></location><location id="id1" x="-672" y="-736"><name x="-682" y="-766">PacketLost</name><committed/></location><location id="id2" x="-864" y="-864"><name x="-1008" y="-888">PacketInTransit</name></location><location id="id3" x="-864" y="-608"><name x="-912" y="-584">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-848" y="-760">initialize(from_network)</label><nail x="-832" y="-792"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-976" y="-688">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="assignment" x="-968" y="-792">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/></transition><transition><source ref="id1"/><target ref="id3"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-1120" y="-784">Packet[network]?</label><label kind="assignment" x="-1120" y="-768">set_target(),
 receive_packet()</label><nail x="-992" y="-608"/><nail x="-992" y="-864"/><nail x="-992" y="-864"/></transition></template><template><name>Host_Handshake</name><parameter>const int local, const int remote, const int network</parameter><declaration>clock c;
 int last_syn = 0;
 int last_ack = 0;
@@ -43,12 +45,13 @@ TCP_packet received;
 
 void set_target(int syn, int ack) {
 	target_address = remote;
-	packet.syn = syn;
-	packet.ack = ack;
+	to_network.syn = syn;
+	to_network.ack = ack;
 }
 
 void receive_packet(){
-	received = packet;
+	received = from_network;
+	initialize(from_network);
 }
 
 int update_syn(){
@@ -65,25 +68,25 @@ void initialize()
 {
 	last_syn := 0;
 	last_ack := 0;
-}</declaration><location id="id3" x="-520" y="-672"><name x="-528" y="-656">SynRcvd1</name><label kind="invariant" x="-536" y="-640">c &lt;= UBOUND</label></location><location id="id4" x="-104" y="-448"><committed/></location><location id="id5" x="-392" y="-544"><committed/></location><location id="id6" x="-880" y="-872"><committed/></location><location id="id7" x="-392" y="-448"><name x="-424" y="-432">Established</name></location><location id="id8" x="-880" y="-544"><name x="-976" y="-576">SynRcvd2</name><label kind="invariant" x="-1000" y="-560">c &lt;= UBOUND</label></location><location id="id9" x="-104" y="-544"><name x="-64" y="-584">SynSent</name><label kind="invariant" x="-72" y="-568">c &lt;= UBOUND</label></location><location id="id10" x="-392" y="-872"><name x="-408" y="-912">Listen</name></location><location id="id11" x="-392" y="-1064"><name x="-464" y="-1064">Closed</name></location><init ref="id11"/><transition><source ref="id7"/><target ref="id7"/><nail x="-400" y="-480"/><nail x="-432" y="-480"/></transition><transition><source ref="id7"/><target ref="id7"/><label kind="synchronisation" x="-328" y="-384">Packet[network]!</label><label kind="assignment" x="-328" y="-368">set_target(0, last_ack)</label><nail x="-328" y="-352"/><nail x="-464" y="-352"/></transition><transition><source ref="id3"/><target ref="id7"/><label kind="guard" x="-632" y="-584">packet.ack == last_syn &amp;&amp;
-packet.syn == 0</label><label kind="synchronisation" x="-632" y="-600">Packet[local]?</label><label kind="assignment" x="-632" y="-552">receive_packet()</label><nail x="-648" y="-672"/><nail x="-648" y="-512"/><nail x="-392" y="-512"/></transition><transition><source ref="id3"/><target ref="id3"/><label kind="guard" x="-552" y="-792">c &gt; LBOUND</label><label kind="synchronisation" x="-552" y="-808">Packet[network]!</label><label kind="assignment" x="-552" y="-776">set_target(0, last_ack),
-c:=0</label><nail x="-484" y="-738"/><nail x="-556" y="-738"/></transition><transition><source ref="id5"/><target ref="id3"/><label kind="synchronisation" x="-384" y="-679">Packet[network]!</label><label kind="assignment" x="-384" y="-664">set_target(0, update_ack()),
-c := 0</label><nail x="-392" y="-672"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="-1216" y="-544">c &gt; LBOUND</label><label kind="synchronisation" x="-1216" y="-560">Packet[network]!</label><label kind="assignment" x="-1216" y="-528">set_target(last_syn, last_ack),
-c:=0</label><nail x="-1008" y="-544"/><nail x="-1008" y="-512"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="32" y="-552">c &gt; LBOUND</label><label kind="synchronisation" x="32" y="-536">Packet[network]!</label><label kind="assignment" x="32" y="-520">set_target(last_syn, 0),
-c := 0</label><nail x="24" y="-512"/><nail x="24" y="-544"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-488" y="-1192">Packet[local]?</label><nail x="-376" y="-1176"/><nail x="-408" y="-1176"/></transition><transition><source ref="id4"/><target ref="id7"/><label kind="synchronisation" x="-296" y="-488">Packet[network]!</label><label kind="assignment" x="-336" y="-472">set_target(0, update_ack())</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-1160" y="-824">Packet[network]!</label><label kind="assignment" x="-1160" y="-808">set_target(update_syn(), update_ack()),
-c := 0</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="guard" x="-592" y="-920">packet.syn != 0 &amp;&amp;
-packet.ack == 0</label><label kind="synchronisation" x="-592" y="-936">Packet[local]?</label><label kind="assignment" x="-592" y="-896">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="guard" x="-96" y="-488">packet.ack == last_syn &amp;&amp;
-packet.syn != 0</label><label kind="synchronisation" x="-96" y="-504">Packet[local]?</label><label kind="assignment" x="-80" y="-456">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="guard" x="-296" y="-592">packet.syn != 0 &amp;&amp;
-packet.ack == 0</label><label kind="synchronisation" x="-296" y="-608">Packet[local]?</label><label kind="assignment" x="-296" y="-568">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-320" y="-920">Packet[network]!</label><label kind="assignment" x="-320" y="-904">set_target(update_syn(), 0),
-c := 0</label><nail x="-136" y="-872"/><nail x="-136" y="-576"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="-872" y="-432">packet.ack == last_syn &amp;&amp;
-packet.syn == 0</label><label kind="synchronisation" x="-872" y="-448">Packet[local]?</label><label kind="assignment" x="-872" y="-400">receive_packet()</label><nail x="-880" y="-448"/></transition><transition><source ref="id9"/><target ref="id11"/><nail x="-72" y="-576"/><nail x="-72" y="-1096"/><nail x="-360" y="-1096"/></transition><transition><source ref="id11"/><target ref="id9"/><label kind="synchronisation" x="-248" y="-1064">Packet[network]!</label><label kind="assignment" x="-248" y="-1048">initialize(),
+}</declaration><location id="id4" x="-520" y="-672"><name x="-528" y="-656">SynRcvd1</name><label kind="invariant" x="-536" y="-640">c &lt;= UBOUND</label></location><location id="id5" x="-104" y="-448"><committed/></location><location id="id6" x="-392" y="-544"><committed/></location><location id="id7" x="-880" y="-872"><committed/></location><location id="id8" x="-392" y="-448"><name x="-424" y="-432">Established</name></location><location id="id9" x="-880" y="-544"><name x="-976" y="-576">SynRcvd2</name><label kind="invariant" x="-1000" y="-560">c &lt;= UBOUND</label></location><location id="id10" x="-104" y="-544"><name x="-64" y="-584">SynSent</name><label kind="invariant" x="-72" y="-568">c &lt;= UBOUND</label></location><location id="id11" x="-392" y="-872"><name x="-408" y="-912">Listen</name></location><location id="id12" x="-392" y="-1064"><name x="-464" y="-1064">Closed</name></location><init ref="id12"/><transition><source ref="id8"/><target ref="id8"/><nail x="-400" y="-480"/><nail x="-432" y="-480"/></transition><transition><source ref="id4"/><target ref="id8"/><label kind="guard" x="-632" y="-584">from_network.ack == last_syn &amp;&amp;
+from_network.syn == 0</label><label kind="synchronisation" x="-632" y="-600">Packet[local]?</label><label kind="assignment" x="-632" y="-552">receive_packet()</label><nail x="-648" y="-672"/><nail x="-648" y="-512"/><nail x="-392" y="-512"/></transition><transition><source ref="id4"/><target ref="id4"/><label kind="guard" x="-552" y="-792">c &gt; LBOUND</label><label kind="synchronisation" x="-552" y="-808">Packet[network]!</label><label kind="assignment" x="-552" y="-776">set_target(0, last_ack),
+c:=0</label><nail x="-484" y="-738"/><nail x="-556" y="-738"/></transition><transition><source ref="id6"/><target ref="id4"/><label kind="synchronisation" x="-384" y="-679">Packet[network]!</label><label kind="assignment" x="-384" y="-664">set_target(0, update_ack()),
+c := 0</label><nail x="-392" y="-672"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-1216" y="-544">c &gt; LBOUND</label><label kind="synchronisation" x="-1216" y="-560">Packet[network]!</label><label kind="assignment" x="-1216" y="-528">set_target(last_syn, last_ack),
+c:=0</label><nail x="-1008" y="-544"/><nail x="-1008" y="-512"/></transition><transition><source ref="id10"/><target ref="id10"/><label kind="guard" x="32" y="-552">c &gt; LBOUND</label><label kind="synchronisation" x="32" y="-536">Packet[network]!</label><label kind="assignment" x="32" y="-520">set_target(last_syn, 0),
+c := 0</label><nail x="24" y="-512"/><nail x="24" y="-544"/></transition><transition><source ref="id12"/><target ref="id12"/><label kind="synchronisation" x="-528" y="-1192">Packet[local]?</label><label kind="assignment" x="-528" y="-1176">receive_packet()</label><nail x="-376" y="-1176"/><nail x="-408" y="-1176"/></transition><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-296" y="-488">Packet[network]!</label><label kind="assignment" x="-336" y="-472">set_target(0, update_ack())</label></transition><transition><source ref="id7"/><target ref="id9"/><label kind="synchronisation" x="-1160" y="-824">Packet[network]!</label><label kind="assignment" x="-1160" y="-808">set_target(update_syn(), update_ack()),
+c := 0</label></transition><transition><source ref="id11"/><target ref="id7"/><label kind="guard" x="-592" y="-920">from_network.syn != 0 &amp;&amp;
+from_network.ack == 0</label><label kind="synchronisation" x="-592" y="-936">Packet[local]?</label><label kind="assignment" x="-592" y="-896">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id5"/><label kind="guard" x="-96" y="-488">from_network.ack == last_syn &amp;&amp;
+from_network.syn != 0</label><label kind="synchronisation" x="-96" y="-504">Packet[local]?</label><label kind="assignment" x="-80" y="-456">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="guard" x="-296" y="-592">from_network.syn != 0 &amp;&amp;
+from_network.ack == 0</label><label kind="synchronisation" x="-296" y="-608">Packet[local]?</label><label kind="assignment" x="-296" y="-568">receive_packet()</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="synchronisation" x="-320" y="-920">Packet[network]!</label><label kind="assignment" x="-320" y="-904">set_target(update_syn(), 0),
+c := 0</label><nail x="-136" y="-872"/><nail x="-136" y="-576"/></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-872" y="-432">from_network.ack == last_syn &amp;&amp;
+from_network.syn == 0</label><label kind="synchronisation" x="-872" y="-448">Packet[local]?</label><label kind="assignment" x="-872" y="-400">receive_packet()</label><nail x="-880" y="-448"/></transition><transition><source ref="id10"/><target ref="id12"/><nail x="-72" y="-576"/><nail x="-72" y="-1096"/><nail x="-360" y="-1096"/></transition><transition><source ref="id12"/><target ref="id10"/><label kind="synchronisation" x="-248" y="-1064">Packet[network]!</label><label kind="assignment" x="-248" y="-1048">initialize(),
 set_target(update_syn(), 0),
-c := 0</label><nail x="-104" y="-1064"/></transition><transition><source ref="id10"/><target ref="id11"/><nail x="-360" y="-904"/><nail x="-360" y="-1032"/></transition><transition><source ref="id11"/><target ref="id10"/><label kind="assignment" x="-496" y="-976">initialize()</label><nail x="-424" y="-1032"/><nail x="-424" y="-904"/></transition></template><system>Network1 = Network(0);
+c := 0</label><nail x="-104" y="-1064"/></transition><transition><source ref="id11"/><target ref="id12"/><nail x="-360" y="-904"/><nail x="-360" y="-1032"/></transition><transition><source ref="id12"/><target ref="id11"/><label kind="assignment" x="-496" y="-976">initialize()</label><nail x="-424" y="-1032"/><nail x="-424" y="-904"/></transition></template><system>Network1 = Network(0);
 Network2 = Network(0);
 Network3 = Network(0);
 Network4 = Network(0);
 Host1Handshake = Host_Handshake(1,2,0);
 Host2Handshake = Host_Handshake(2,1,0);
 
-system Network1, Network2 ,Host1Handshake,Host2Handshake;
+system Network1, Network2, Network3,Host1Handshake,Host2Handshake;
 </system></nta>
\ No newline at end of file