Changed from packets to segments
This commit is contained in:
Jip Dekker
parent
dfd2907041
commit
ce9ac9ea6a
105
Model/model.xml
105
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;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
|
||||
TCP_packet transfer;
|
||||
TCP_segment to_network;
|
||||
TCP_segment from_network;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int 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;
|
||||
}
|
||||
</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="-5400" y="-1480">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="assignment" x="-5400" 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()</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;
|
||||
int last_syn = 0;
|
||||
</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 <= 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(),
|
||||
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;
|
||||
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;
|
||||
}</declaration><location id="id4" x="-448" y="-672"><committed/></location><location id="id5" x="-736" y="-768"><committed/></location><location id="id6" x="-992" y="-928"><committed/></location><location id="id7" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id8" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c <= UBOUND</label></location><location id="id9" x="-448" y="-768"><name x="-512" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c <= UBOUND</label></location><location id="id10" x="-736" y="-928"><name x="-752" y="-912">Listen</name></location><location id="id11" x="-736" y="-1120"><name x="-800" y="-1128">Closed</name></location><init ref="id11"/><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-920" y="-832">Packet[network]!</label><label kind="assignment" x="-920" y="-817">set_target(0, update_ack()),
|
||||
set_retrans(0, last_ack),
|
||||
c := 0</label></transition><transition><source ref="id7"/><target ref="id7"/><nail x="-704" y="-704"/><nail x="-776" y="-704"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="-1232" y="-720">c > LBOUND</label><label kind="synchronisation" x="-1232" y="-736">Packet[network]!</label><label kind="assignment" x="-1232" y="-704">set_target(retrans_syn, retrans_ack),
|
||||
c:=0</label><nail x="-1120" y="-768"/><nail x="-1120" y="-736"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-312" y="-776">c > LBOUND</label><label kind="synchronisation" x="-312" y="-792">Packet[network]!</label><label kind="assignment" x="-312" y="-760">set_target(last_syn, 0),
|
||||
c := 0</label><nail x="-320" y="-736"/><nail x="-320" y="-768"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-856" y="-1192">Packet[local]?</label><label kind="assignment" x="-856" y="-1176">receive_packet()</label><nail x="-720" y="-1192"/><nail x="-752" y="-1192"/></transition><transition><source ref="id4"/><target ref="id7"/><label kind="synchronisation" x="-664" y="-672">Packet[network]!</label><label kind="assignment" x="-664" y="-656">set_target(0, update_ack())</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-1240" y="-888">Packet[network]!</label><label kind="assignment" x="-1240" y="-872">set_target(update_syn(), update_ack()),
|
||||
set_retrans(last_syn, last_ack),
|
||||
c := 0</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="guard" x="-944" y="-976">from_network.syn != 0 &&
|
||||
from_network.ack == 0</label><label kind="synchronisation" x="-944" y="-992">Packet[local]?</label><label kind="assignment" x="-944" y="-952">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="guard" x="-432" y="-712">from_network.ack == last_syn &&
|
||||
from_network.syn != 0</label><label kind="synchronisation" x="-432" y="-728">Packet[local]?</label><label kind="assignment" x="-432" y="-680">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="guard" x="-672" y="-816">from_network.syn != 0 &&
|
||||
from_network.ack == 0</label><label kind="synchronisation" x="-672" y="-832">Packet[local]?</label><label kind="assignment" x="-672" y="-792">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-664" y="-976">Packet[network]!</label><label kind="assignment" x="-664" y="-960">set_target(update_syn(), 0),
|
||||
c := 0</label><nail x="-480" y="-928"/><nail x="-480" y="-800"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="-984" y="-656">from_network.ack == last_syn &&
|
||||
from_network.syn == 0</label><label kind="synchronisation" x="-984" y="-672">Packet[local]?</label><label kind="assignment" x="-984" y="-624">receive_packet()</label><nail x="-992" y="-672"/></transition><transition><source ref="id9"/><target ref="id11"/><nail x="-416" y="-800"/><nail x="-416" y="-1152"/><nail x="-704" y="-1152"/></transition><transition><source ref="id11"/><target ref="id9"/><label kind="synchronisation" x="-592" y="-1120">Packet[network]!</label><label kind="assignment" x="-592" y="-1104">initialize(),
|
||||
set_target(update_syn(), 0),
|
||||
c := 0</label><nail x="-448" y="-1120"/></transition><transition><source ref="id10"/><target ref="id11"/><nail x="-704" y="-960"/><nail x="-704" y="-1088"/></transition><transition><source ref="id11"/><target ref="id10"/><label kind="assignment" x="-840" y="-1032">initialize()</label><nail x="-768" y="-1088"/><nail x="-768" y="-960"/></transition></template><system>Network1 = 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;
|
||||
}</declaration><location id="id4" x="-448" y="-672"><committed/></location><location id="id5" x="-736" y="-768"><committed/></location><location id="id6" x="-992" y="-928"><committed/></location><location id="id7" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id8" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c <= UBOUND</label></location><location id="id9" x="-448" y="-768"><name x="-512" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c <= UBOUND</label></location><location id="id10" x="-736" y="-928"><name x="-752" y="-912">Listen</name></location><location id="id11" x="-736" y="-1120"><name x="-800" y="-1128">Closed</name></location><init ref="id11"/><transition><source ref="id5"/><target ref="id8"/><label kind="synchronisation" x="-920" y="-832">Packet[network]!</label><label kind="assignment" x="-920" y="-817">send(false, true),
|
||||
c := 0</label></transition><transition><source ref="id7"/><target ref="id7"/><nail x="-704" y="-704"/><nail x="-776" y="-704"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="-1224" y="-768">c > LBOUND</label><label kind="synchronisation" x="-1256" y="-784">Packet[network]!</label><label kind="assignment" x="-1224" y="-752">retransmit(),
|
||||
c:=0</label><nail x="-1120" y="-768"/><nail x="-1120" y="-744"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-312" y="-776">c > LBOUND</label><label kind="synchronisation" x="-312" y="-792">Packet[network]!</label><label kind="assignment" x="-312" y="-760">retransmit(),
|
||||
c := 0</label><nail x="-320" y="-736"/><nail x="-320" y="-768"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="-872" y="-1192">Packet[local]?</label><label kind="assignment" x="-872" y="-1176">receive_packet()</label><nail x="-720" y="-1192"/><nail x="-752" y="-1192"/></transition><transition><source ref="id4"/><target ref="id7"/><label kind="synchronisation" x="-664" y="-672">Packet[network]!</label><label kind="assignment" x="-664" y="-656">send(false,true)</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="-1120" y="-872">Packet[network]!</label><label kind="assignment" x="-1120" y="-856">send(true,true),
|
||||
c := 0</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="guard" x="-944" y="-976">from_network.syn &&
|
||||
! from_network.ack</label><label kind="synchronisation" x="-944" y="-992">Packet[local]?</label><label kind="assignment" x="-944" y="-952">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="guard" x="-432" y="-712">from_network.ack &&
|
||||
from_network.syn</label><label kind="synchronisation" x="-432" y="-728">Packet[local]?</label><label kind="assignment" x="-432" y="-680">receive_packet()</label></transition><transition><source ref="id9"/><target ref="id5"/><label kind="guard" x="-672" y="-816">from_network.syn&&
|
||||
! from_network.ack</label><label kind="synchronisation" x="-672" y="-832">Packet[local]?</label><label kind="assignment" x="-672" y="-792">receive_packet()</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-664" y="-976">Packet[network]!</label><label kind="assignment" x="-664" y="-960">send(true, false),
|
||||
c := 0</label><nail x="-480" y="-928"/><nail x="-480" y="-800"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="-984" y="-656">from_network.ack &&
|
||||
! from_network.syn</label><label kind="synchronisation" x="-984" y="-672">Packet[local]?</label><label kind="assignment" x="-984" y="-624">receive_packet()</label><nail x="-992" y="-672"/></transition><transition><source ref="id9"/><target ref="id11"/><nail x="-416" y="-800"/><nail x="-416" y="-1152"/><nail x="-704" y="-1152"/></transition><transition><source ref="id11"/><target ref="id9"/><label kind="synchronisation" x="-592" y="-1120">Packet[network]!</label><label kind="assignment" x="-592" y="-1104">reset(),
|
||||
send(true,false),
|
||||
c := 0</label><nail x="-448" y="-1120"/></transition><transition><source ref="id10"/><target ref="id11"/><nail x="-704" y="-960"/><nail x="-704" y="-1088"/></transition><transition><source ref="id11"/><target ref="id10"/><label kind="assignment" x="-816" y="-1056">reset()</label><nail x="-768" y="-1088"/><nail x="-768" y="-960"/></transition></template><system>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, Network3, Network4, Host1Handshake,Host2Handshake;
|
||||
system Network1, Network2, Network3, Host1Handshake,Host2Handshake;
|
||||
</system></nta>
|
||||
Reference in New Issue
Block a user