From 18755cebf4b01a01b8c68c2fba795bce9702e938 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <admin@recondor.com>
Date: Sun, 2 Feb 2014 13:54:42 +0100
Subject: [PATCH] Added the query from frits

---
 Model/model.q   | 5 +++++
 Model/model.xml | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Model/model.q b/Model/model.q
index bf8c298..daaead1 100644
--- a/Model/model.q
+++ b/Model/model.q
@@ -2,6 +2,11 @@
 
 /*
 
+*/
+(not Host1.Init and not Host1.Closed) --> (Host1.Established && Host2.Established)
+
+/*
+
 */
 (not Host1.Closed and not Host2.Closed) --> Host1.Established
 
diff --git a/Model/model.xml b/Model/model.xml
index 7f6081b..6e47453 100644
--- a/Model/model.xml
+++ b/Model/model.xml
@@ -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),