Dekker1/TCP-setup-uppaal
Archived
1
0
Fork 0
Code

Added all variables for real sequence numbers

Browse Source
This commit is contained in:
Jip Dekker 2014-01-06 16:41:47 +01:00
parent f5eb2660a1
commit ae7db80d9b
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Model/model.xml
View File

@ -14,12 +14,14 @@ int target_address; //Global variable to pass the target address to the network
typedef struct { typedef struct {
bool syn; bool syn;
bool ack; bool ack;
int win;
int seqNr; int seqNr;
int ackNr; int ackNr;
} TCP_segment; } TCP_segment;
void initialize(TCP_segment& p) void initialize(TCP_segment& p)
{ {
p.win := 0;
p.seqNr := 0; p.seqNr := 0;
p.ackNr := 0; p.ackNr := 0;
p.syn := false; p.syn := false;
@ -46,8 +48,10 @@ void send_packet(){
</declaration><location id="id0" x="-5312" y="-1536"><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5160" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-5296" y="-1560">initialize(from_network)</label><nail x="-5280" y="-1592"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="-5384" y="-1624">c &lt;= TTL</label><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5432" y="-1560">Packet[network]?</label><label kind="assignment" x="-5432" y="-1544">set_target(), </declaration><location id="id0" x="-5312" y="-1536"><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5160" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-5296" y="-1560">initialize(from_network)</label><nail x="-5280" y="-1592"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="-5384" y="-1624">c &lt;= TTL</label><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5432" y="-1560">Packet[network]?</label><label kind="assignment" x="-5432" y="-1544">set_target(),
receive_packet(), receive_packet(),
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; 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;
meta int last_seq = 0; meta int una = 0;
meta int last_ack = 0; meta int snd_nxt = 0;
meta int len = 0;
meta int rcv_nxt = 0;
meta TCP_segment retrans; meta TCP_segment retrans;
meta TCP_segment received; meta TCP_segment received;
@ -57,6 +61,7 @@ void receive_packet(){
} }
int update_seq(bool syn){ int update_seq(bool syn){
last_seq = (last_seq % MAX_SEQ) +1; last_seq = (last_seq % MAX_SEQ) +1;
return last_seq; return last_seq;
} }