diff --git a/Model/model.xml b/Model/model.xml
index b7e1eb8..b5aabf9 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -3,6 +3,7 @@ const int HOSTS = 2;
// TIMEOUT Bounds
const int UBOUND = 600;
const int LBOUND = 10;
+const int TTL = 600;
// sequence bounds
const int MAX_SEQ = 3;
@@ -11,19 +12,24 @@ chan Packet[HOSTS+1];
int target_address; //Global variable to pass the target address to the network
typedef struct {
- int syn;
- int ack;
-} TCP_packet;
+ bool syn;
+ bool ack;
+ int seqNr;
+ int ackNr;
+} TCP_segment;
-void initialize(TCP_packet& p)
+void initialize(TCP_segment& p)
{
- p.syn := 0;
- p.ack := 0;
+ p.seqNr := 0;
+ p.ackNr := 0;
+ p.syn := false;
+ p.ack := false;
}
-TCP_packet to_network;
-TCP_packet from_network;Networkconst int networkint target; // the target for the current network packet
-TCP_packet transfer;
+TCP_segment to_network;
+TCP_segment from_network;Networkconst int networkint target; // the target for the current network packet
+TCP_segment transfer;
+clock c;
void set_target() {
target = target_address;
@@ -37,63 +43,68 @@ void receive_packet(){
void send_packet(){
from_network := transfer;
}
-PacketLostPacketInTransitReadyToReceiveHost_Handshakeconst int local, const int remote, const int networkclock c;
-int last_syn = 0;
+PacketLostPacketInTransitReadyToReceiveHost_Handshakeconst int local, const int remote, const int networkclock c;
+int last_seq = 0;
int last_ack = 0;
-int retrans_syn;
-int retrans_ack;
-TCP_packet received;
-
-void set_target(int syn, int ack) {
- target_address = remote;
- to_network.syn = syn;
- to_network.ack = ack;
-}
+TCP_segment retrans;
+TCP_segment received;
void receive_packet(){
- received = from_network;
+ received := from_network;
initialize(from_network);
}
-int update_syn(){
- last_syn = (last_syn % MAX_SEQ) +1;
- return last_syn;
+int update_seq(bool syn){
+ last_seq = (last_seq % MAX_SEQ) +1;
+ return last_seq;
}
-int update_ack(){
- last_ack = received.syn;
+int update_ack(bool ack){
+ if(!ack)
+ return 0;
+ last_ack = received.seqNr;
return last_ack;
}
-void initialize()
+void reset()
{
- last_syn := 0;
+ last_seq := 0;
last_ack := 0;
+ initialize(retrans);
+ initialize(received);
}
-void set_retrans(int syn, int ack) {
- retrans_syn = syn;
- retrans_ack = ack;
-}EstablishedSynRcvdSynSentListenClosedNetwork1 = Network(0);
+void send(bool syn, bool ack) {
+ target_address = remote;
+ retrans.syn := syn;
+ retrans.ack := ack;
+ retrans.seqNr := update_seq(syn);
+ retrans.ackNr := update_ack(ack);
+ to_network := retrans;
+}
+
+void retransmit() {
+ target_address = remote;
+ to_network := retrans;
+}EstablishedSynRcvdSynSentListenClosedNetwork1 = 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, Network3, Network4, Host1Handshake,Host2Handshake;
+system Network1, Network2, Network3, Host1Handshake,Host2Handshake;
\ No newline at end of file