dekker.one
An Uppaal analysis of the connection setup of the TCP protocol.
Updated sequence number stuff
+25
-22
Model/model.xml
+25
-22
Model/model.xml
···
50
50
c:=0</label><nail x="-5440" y="-1408"/><nail x="-5440" y="-1664"/></transition></template><template><name>Host_Handshake</name><parameter>const int local, const int remote, const int network</parameter><declaration>clock c;
51
51
meta int snd_una = 0;
52
52
meta int snd_nxt = 0;
53
-
meta int seg_ack = 0;
54
-
meta int seg_len = 0;
53
+
meta int snd_ack = 0;
55
54
meta int rcv_nxt = 0;
55
+
const int seg_len = 0;
56
+
const int window = 1;
56
57
meta TCP_segment retrans;
57
58
meta TCP_segment received;
58
59
59
60
bool receive_packet(){
60
-
received := from_network;
61
-
snd_nxt = received.ackNr;
62
-
seg_ack = (received.seqNr + 1 + len)%MAX_SEQ;
63
-
64
-
initialize(from_network);
65
-
}
66
-
67
-
int update_win(){
68
-
//TODO: do something usefull.
69
-
return 0;
70
-
}
71
-
72
-
void reset()
73
-
{
74
-
last_seq := 0;
75
-
last_ack := 0;
76
-
initialize(retrans);
77
-
initialize(received);
61
+
if (from_network.syn) {
62
+
rcv_nxt = from_network.seqNr;
63
+
}
64
+
if (rcv_nxt == from_network.seqNr) {
65
+
if (received.ack && snd_una < from_network.ackNr) {
66
+
snd_una = from_network.ackNr;
67
+
}
68
+
else if (received.ack) {
69
+
return false;
70
+
}
71
+
received := from_network;
72
+
snd_nxt = received.ackNr + 1;
73
+
snd_ack = (received.seqNr + 1 + seg_len)%MAX_SEQ;
74
+
initialize(from_network);
75
+
return true;
76
+
}
77
+
return false;
78
78
}
79
79
80
80
void send(bool syn, bool ack) {
81
+
if (syn) {
82
+
snd_una := snd_nxt;
83
+
}
81
84
target_address = remote;
82
85
retrans.syn := syn;
83
86
retrans.ack := ack;
84
87
retrans.seqNr := snd_nxt;
85
-
retrans.ackNr := seq_ack;
86
-
retrans.win := update_win();
88
+
retrans.ackNr := snd_ack;
89
+
retrans.win := window;
87
90
to_network := retrans;
88
91
}
89
92