diff --git a/Model/model.xml b/Model/model.xml
index be6308a..bcc5f0e 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -24,7 +24,6 @@ void initialize(TCP_packet& p)
TCP_packet packet;Networkconst int networkint target; // the target for the current network packet
TCP_packet transfer;
-
void set_target() {
target = target_address;
}
@@ -36,7 +35,7 @@ void receive_packet(){
void send_packet(){
packet := transfer;
}
-PacketLostPacketInTransitReadyToReceiveHost_Handshakeconst int local, const int remote, const int networkclock c;
int last_syn = 0;
int last_ack = 0;
@@ -66,16 +65,20 @@ void initialize()
{
last_syn := 0;
last_ack := 0;
-}EstablishedSynRcvdSynSentc <= UBOUNDListenClosedc > LBOUNDPacket[network]!set_target(last_syn, 0),
-c := 0Packet[local]?Packet[network]!set_target(0, update_ack())Packet[network]!set_target(0, update_ack()),
-c := 0Packet[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)packet.ack == last_syn &&
-packet.syn == 0Packet[local]?receive_packet()Packet[network]!initialize(),
+}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(),
set_target(update_syn(), 0),
-c := 0initialize()Network1 = Network(0);
+c := 0initialize()Network1 = Network(0);
Network2 = Network(0);
Network3 = Network(0);
Network4 = Network(0);