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& p)
p.ack := 0;
}
-TCP_packet packet;Networkconst int networkint target; // the target for the current network packet
+TCP_packet to_network;
+TCP_packet from_network;Networkconst int networkint 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;
}
-PacketLostPacketInTransitReadyToReceiveHost_Handshakeconst int local, const int remote, const int networkclock 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;
-}SynRcvd1c <= UBOUNDEstablishedSynRcvd2c <= UBOUNDSynSentc <= UBOUNDListenClosedPacket[network]!set_target(0, last_ack)packet.ack == last_syn &&
-packet.syn == 0Packet[local]?receive_packet()c > LBOUNDPacket[network]!set_target(0, last_ack),
-c:=0Packet[network]!set_target(0, update_ack()),
-c := 0c > LBOUNDPacket[network]!set_target(last_syn, last_ack),
-c:=0c > LBOUNDPacket[network]!set_target(last_syn, 0),
-c := 0Packet[local]?Packet[network]!set_target(0, update_ack())Packet[network]!set_target(update_syn(), update_ack()),
-c := 0packet.syn != 0 &&
-packet.ack == 0Packet[local]?receive_packet()packet.ack == last_syn &&
-packet.syn != 0Packet[local]?receive_packet()packet.syn != 0 &&
-packet.ack == 0Packet[local]?receive_packet()Packet[network]!set_target(update_syn(), 0),
-c := 0packet.ack == last_syn &&
-packet.syn == 0Packet[local]?receive_packet()Packet[network]!initialize(),
+}SynRcvd1c <= UBOUNDEstablishedSynRcvd2c <= UBOUNDSynSentc <= UBOUNDListenClosedfrom_network.ack == last_syn &&
+from_network.syn == 0Packet[local]?receive_packet()c > LBOUNDPacket[network]!set_target(0, last_ack),
+c:=0Packet[network]!set_target(0, update_ack()),
+c := 0c > LBOUNDPacket[network]!set_target(last_syn, last_ack),
+c:=0c > LBOUNDPacket[network]!set_target(last_syn, 0),
+c := 0Packet[local]?receive_packet()Packet[network]!set_target(0, update_ack())Packet[network]!set_target(update_syn(), update_ack()),
+c := 0from_network.syn != 0 &&
+from_network.ack == 0Packet[local]?receive_packet()from_network.ack == last_syn &&
+from_network.syn != 0Packet[local]?receive_packet()from_network.syn != 0 &&
+from_network.ack == 0Packet[local]?receive_packet()Packet[network]!set_target(update_syn(), 0),
+c := 0from_network.ack == last_syn &&
+from_network.syn == 0Packet[local]?receive_packet()Packet[network]!initialize(),
set_target(update_syn(), 0),
-c := 0initialize()Network1 = Network(0);
+c := 0initialize()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;
\ No newline at end of file