diff --git a/Model/model.q b/Model/model.q index f9386ef..bf8c298 100644 --- a/Model/model.q +++ b/Model/model.q @@ -2,15 +2,20 @@ /* +*/ +(not Host1.Closed and not Host2.Closed) --> Host1.Established + +/* + */ A[] not deadlock /* */ -E<> (Host1Handshake.Established and Host2Handshake.Established) +E<> (Host1.Established and Host2.Established) /* */ -A[] not (Host1Handshake.Closed and Host2Handshake.Established) +A[] not (Host1.Closed and Host2.Established) diff --git a/Model/model.xml b/Model/model.xml index 600ea3c..7f6081b 100644 --- a/Model/model.xml +++ b/Model/model.xml @@ -48,7 +48,7 @@ void send_packet(){ } PacketLostPacketInTransitReadyToReceive