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

Added the query from frits

Browse Source
This commit is contained in:
Jip J. Dekker 2014-02-02 13:54:42 +01:00
parent 0d1cd6f24b
commit 18755cebf4
2 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Model/model.q
View File

@ -2,6 +2,11 @@
/*
*/
(not Host1.Init and not Host1.Closed) --> (Host1.Established && Host2.Established)
/*
*/
(not Host1.Closed and not Host2.Closed) --> Host1.Established

2
Model/model.xml
View File

@ -85,7 +85,7 @@ void send(bool syn, bool ack) {
void retransmit() {
target_address = remote;
to_network := retrans;
}</declaration><location id="id4" x="-928" y="-1120"><committed/></location><location id="id5" x="-448" y="-672"><committed/></location><location id="id6" x="-736" y="-768"><committed/></location><location id="id7" x="-992" y="-928"><committed/></location><location id="id8" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id9" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c &lt;= UBOUND</label></location><location id="id10" x="-448" y="-768"><name x="-512" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c &lt;= UBOUND</label></location><location id="id11" x="-736" y="-928"><name x="-752" y="-912">Listen</name></location><location id="id12" x="-736" y="-1120"><name x="-800" y="-1144">Closed</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id12"/><label kind="select" x="-896" y="-1120">i:SEQ</label><label kind="assignment" x="-896" y="-1104">snd_nxt := i</label></transition><transition><source ref="id6"/><target ref="id9"/><label kind="synchronisation" x="-920" y="-832">Packet[network]!</label><label kind="assignment" x="-920" y="-817">send(false, true),
}</declaration><location id="id4" x="-928" y="-1120"><name x="-976" y="-1144">Init</name><committed/></location><location id="id5" x="-448" y="-672"><committed/></location><location id="id6" x="-736" y="-768"><committed/></location><location id="id7" x="-992" y="-928"><committed/></location><location id="id8" x="-736" y="-672"><name x="-768" y="-656">Established</name></location><location id="id9" x="-992" y="-768"><name x="-984" y="-768">SynRcvd</name><label kind="invariant" x="-984" y="-752">c &lt;= UBOUND</label></location><location id="id10" x="-448" y="-768"><name x="-512" y="-768">SynSent</name><label kind="invariant" x="-552" y="-752">c &lt;= UBOUND</label></location><location id="id11" x="-736" y="-928"><name x="-752" y="-912">Listen</name></location><location id="id12" x="-736" y="-1120"><name x="-800" y="-1144">Closed</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id12"/><label kind="select" x="-896" y="-1120">i:SEQ</label><label kind="assignment" x="-896" y="-1104">snd_nxt := i</label></transition><transition><source ref="id6"/><target ref="id9"/><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="id8"/><target ref="id8"/><nail x="-704" y="-704"/><nail x="-776" y="-704"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-1224" y="-768">c &gt; 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="id10"/><target ref="id10"/><label kind="guard" x="-312" y="-776">c &gt; 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="id12"/><target ref="id12"/><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="id5"/><target ref="id8"/><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="id7"/><target ref="id9"/><label kind="synchronisation" x="-1120" y="-872">Packet[network]!</label><label kind="assignment" x="-1120" y="-856">send(true,true),