rpc added by megane on Wed Feb 27 16:50:57 2019
---- MODULE simple_rpc_threads_flushing ----
EXTENDS TLC, Sequences, Integers
\* Version that handles pending requests before closing the connection
(* Connection is cut at arbitrary times: connection-breaker *)
(* Checked properties: *)
\* check_query_responses: Check responses ok or queries marked FAILED
\* ghost_got_close_ack: if server closes first, and there's no connection cut, the
\* remote end should get (close), and server should get (ack-close)
(* TODO: check threads eventually always stopped. strange error while checking Termination *)
(* TODO: Feature: Fail queries when connection is not cut, but remote
end just doesn't reply *)
(* TODO: Feature: Handle invalid messages. conn-in *)
EMPTY_QUEUE == <<>>
WAITING_RESPONSE == "WAITING_RESPONSE"
FAILED == "FAILED"
CLOSE == -1
CLOSE_CLEAN == -2
BrokenSocket(s) == s = <<"connection-cut">>
CliResponses == [sq1 |-> "cr1", sq2 |-> "cr2", sq3 |-> "cr3", sq4 |-> "cr4"]
SrvQueries == DOMAIN CliResponses
SrvQueryResults == {CliResponses[q]: q \in SrvQueries}
SrvResponses == [q1 |-> "r1", q2 |-> "r2", q3 |-> "r3", q4 |-> "r4"]
CliQueries == DOMAIN SrvResponses
CliQueryResults == {SrvResponses[q]: q \in CliQueries}
WireMsgs == {"(close)", "(ack-close)"} \cup SrvQueries \cup SrvQueryResults \cup CliQueries \cup CliQueryResults
QueryStates == [q: SrvQueries, res: SrvQueryResults \union {WAITING_RESPONSE, FAILED}]
Min(a,b) == IF a < b THEN a ELSE b
Prefixes(max, s) == {<<>>} \union {SubSeq(s, 1, l): l \in 1..Min(max, Len(s))}
SeqOf(seq, set) == \A i \in DOMAIN seq: seq[i] \in set \/ Print(<<"SeqOf", i, seq[i], set >>, FALSE )
(* --algorithm simple_rpc_threads_flushing
\* Variables
variables
WaitForServerQueriesBeforeClosing \in BOOLEAN,
flag_serverTriesToClose \in BOOLEAN,
flag_remote_waits_for_close \in BOOLEAN,
IncomingQueries \in Prefixes(3, << "q1", "q2", "q3", "q4" >> ),
OutgoingQueries \in Prefixes(3, << "sq1", "sq2", "sq3" >> ),
sockIn = EMPTY_QUEUE,
sockOut = EMPTY_QUEUE,
mbQueryRes = EMPTY_QUEUE,
mbQuery = EMPTY_QUEUE,
mbQueryCopy = EMPTY_QUEUE,
mbOut = EMPTY_QUEUE,
mbRequests = EMPTY_QUEUE,
queriesToSend = OutgoingQueries,
sentQueries = <<>>,
send_ack_close = FALSE,
send_close = FALSE,
ghost_droppedQueries = <<>>, (* Queries that don't get responses due to closed connection *)
ghost_received_sockOut_msgs = <<>>,
ghost_received_sockIn_msgs = <<>>,
ghost_got_close_ack = FALSE,
\* Definitions
define
QueryIds == DOMAIN sentQueries
TypeInvariant ==
/\ SeqOf(sentQueries, QueryStates)
/\ SeqOf(mbOut, SrvQueries
\cup CliQueryResults
\union {"(close)", "(ack-close)", "close", "flush-and-ack-close"})
/\ SeqOf(mbQuery, QueryIds \union {CLOSE, CLOSE_CLEAN})
/\ SeqOf(mbQueryCopy, QueryIds \union {CLOSE, CLOSE_CLEAN})
/\ SeqOf(mbQueryRes, SrvQueryResults \union {"close", "fail"})
/\ BrokenSocket(sockIn) \/ SeqOf(sockIn, WireMsgs)
/\ BrokenSocket(sockOut) \/ SeqOf(sockOut, WireMsgs)
QueueEmpty(q) == q = EMPTY_QUEUE
QueuePeek(q) == Head(q)
ConnThreads == {"conn-out", "conn-in", "query-joiner", "query-send"}
ConnThreadsStopped == \A t \in ConnThreads: pc[t] = "Done"
NoThreadsStopped == \A t \in ConnThreads: pc[t] /= "Done"
ConnectionTermination == <>(ConnThreadsStopped)
ghost_HavePendingRequests == \E i \in DOMAIN sentQueries: sentQueries[i].res = WAITING_RESPONSE
Query(query, response) == [q |-> query, res |-> response]
SeqMap(s, Op(_)) == [i \in DOMAIN s |-> Op(s[i])]
WaitingQueries == SeqMap(SelectSeq(sentQueries, LAMBDA q: q.res = WAITING_RESPONSE),
LAMBDA q: q.q)
AllQueriesDone == Len(sentQueries) = Len(OutgoingQueries) /\ WaitingQueries = <<>>
end define
\* Macros
macro QueuePop(q) begin
q := Tail(q);
end macro;
macro QueuePush(q, v) begin
q := Append(q, v);
end macro;
macro QueueReceive(q, v) begin
await ~QueueEmpty(q);
v := QueuePeek(q);
q := Tail(q);
end macro;
macro SocketSend(s, v) begin
if ~BrokenSocket(s) then
QueuePush(s, v);
end if;
end macro;
macro SocketReceive(s, v) begin
await ~QueueEmpty(s);
if BrokenSocket(s) then
v := "connection-cut";
else
v := QueuePeek(s);
s := Tail(s);
end if;
end macro;
macro MarkDroppedQueries() begin
if ghost_droppedQueries = <<>> then
ghost_droppedQueries := WaitingQueries \o queriesToSend;
end if;
end macro;
macro error(msg) begin
assert Print(msg, FALSE);
end macro;
\* API operations
macro SendQuery(query) begin
QueuePush(sentQueries, Query(query, WAITING_RESPONSE));
QueuePush(mbQuery, Len(sentQueries));
end macro;
macro SetQueryResult(id, val) begin
assert sentQueries[id].res = WAITING_RESPONSE;
sentQueries := id :> [q |-> sentQueries[id].q, res |-> val]
@@ [i \in DOMAIN sentQueries \ {id} |-> sentQueries[i]];
end macro;
procedure CleanShutdown() (* remote-conn-close! *)
(* Wait pending requests have received responses / failed *)
(* Completely abort / ignore pending incoming requests *)
begin CleanShutdown_entry:
send_close := TRUE;
QueuePush(mbQuery, CLOSE_CLEAN);
shutdown_loop:
await ConnThreadsStopped \/ ~QueueEmpty(mbRequests);
if ~QueueEmpty(mbRequests) then
mbRequests := EMPTY_QUEUE;
goto shutdown_loop;
else
return;
end if;
end procedure;
\* Processes
process tOut="conn-out"
variables tOut_msg = FALSE, tOut_flush = FALSE;
begin
(* IN: mbOut *)
(* OUT: sockOut, mbQuery (close) *)
conn_out:
QueueReceive( mbOut, tOut_msg);
if BrokenSocket(sockOut) then
skip;
elsif tOut_msg = "(close)" then
SocketSend( sockOut, tOut_msg); (* Server requests close *)
goto notify_sender;
elsif tOut_msg = "flush-and-ack-close" then
tOut_flush := TRUE;
else
SocketSend( sockOut, tOut_msg);
goto conn_out;
end if;
flush_out_queue:
if tOut_flush /\ ~( QueueEmpty(mbOut) /\ QueueEmpty(mbRequests)) then
QueueReceive(mbOut, tOut_msg);
if tOut_msg = "close" then
skip;
elsif tOut_msg = "(close)" then
SocketSend(sockOut, tOut_msg);
goto notify_sender;
else
SocketSend(sockOut, tOut_msg);
end if;
flush_out_queue_loop:
goto flush_out_queue;
end if;
notify_sender:
QueuePush( mbQuery, CLOSE );
end process;
process tIn="conn-in"
variables tIn_msg = FALSE;
begin
(* IN: sockIn *)
(* OUT: mbQueryRes, mbRequests, (mbQuery on failure), mbOut (flush-and-ack-close) *)
conn_in:
SocketReceive(sockIn, tIn_msg);
ghost_received_sockIn_msgs := Append(ghost_received_sockIn_msgs, tIn_msg);
if tIn_msg = "(close)" then
(* Start shutdown *)
send_ack_close := TRUE;
QueuePush(mbOut, "flush-and-ack-close");
QueuePush(mbQueryRes, "close");
elsif tIn_msg = "(ack-close)" then
ghost_got_close_ack := TRUE;
elsif tIn_msg \in CliQueries then (* Received a request *)
QueuePush( mbRequests, tIn_msg);
goto conn_in;
elsif tIn_msg \in SrvQueryResults then
QueuePush(mbQueryRes, tIn_msg);
goto conn_in;
elsif tIn_msg = "connection-cut" then
(* Fail *)
QueuePush(mbQueryRes, "fail");
QueuePush(mbQuery, CLOSE);
else
error("Invalid message");
end if;
end process;
process tJoin="query-joiner"
variables tJoin_q = FALSE, tJoin_res = FALSE, tJoin_fail_remaining = FALSE;
begin
(* IN: mbQueryCopy, mbQueryRes, (mbQuery during fail_remaining) *)
(* OUT: ( mbQuery <- CLOSE during fail_remaining) *)
query_joiner:
QueueReceive(mbQueryCopy, tJoin_q);
if tJoin_q = CLOSE then
tJoin_fail_remaining := TRUE;
elsif tJoin_q = CLOSE_CLEAN then
skip;
else
join_get_resp: (* Get response *)
QueueReceive(mbQueryRes, tJoin_res);
if tJoin_res \in {"close", "fail"} then
SetQueryResult(tJoin_q, FAILED);
tJoin_fail_remaining := TRUE;
else
set_query_result:
SetQueryResult(tJoin_q, tJoin_res);
goto query_joiner;
end if;
end if;
fail_remaining:
if tJoin_fail_remaining then
fail_remaining_loop:
if ~QueueEmpty(mbQueryCopy) then
if QueuePeek(mbQueryCopy) \notin {CLOSE, CLOSE_CLEAN} then
SetQueryResult(QueuePeek(mbQueryCopy), FAILED);
end if;
QueuePop(mbQueryCopy);
goto fail_remaining_loop;
elsif ~QueueEmpty(mbQuery) then
(* peek&pop requires disable-interrupts, because mbQuery is read
from multiple threads *)
if QueuePeek(mbQuery) \notin {CLOSE, CLOSE_CLEAN} then
SetQueryResult(QueuePeek(mbQuery), FAILED);
QueuePop(mbQuery);
goto fail_remaining_loop;
else
(* Stop *)
QueuePop(mbQuery);
replace_close:
QueuePush(mbQuery, CLOSE);
end if;
end if;
end if;
end process;
process tSend="query-send"
variables tSend_q = FALSE;
begin
(* IN: mbQuery *)
(* OUT: mbQueryCopy, mbOut *)
query_send:
QueueReceive( mbQuery, tSend_q );
QueuePush( mbQueryCopy, tSend_q );
if tSend_q = CLOSE then
QueuePush( mbOut, "close" );
elsif tSend_q = CLOSE_CLEAN then
QueuePush( mbOut, "(close)" );
else
QueuePush( mbOut, sentQueries[tSend_q].q );
goto query_send;
end if;
end process;
\* Connection breaker
process tBreaker = "connection-breaker" begin
maybe_break_connection:
either
sockIn := <<"connection-cut">>;
sockOut := <<"connection-cut">>;
MarkDroppedQueries();
or
skip;
end either;
end process;
\* The server
\* Creates responses for the received queries.
process tServer="server"
variables tServer_req = FALSE, checkId = 0;
begin
server:
await \/ ConnThreadsStopped
\/ ~QueueEmpty(mbRequests)
\/ ~QueueEmpty(queriesToSend)
\/ flag_serverTriesToClose;
if ConnThreadsStopped then
skip;
elsif QueueEmpty(queriesToSend) /\ flag_serverTriesToClose then
call CleanShutdown();
else
either (* Handle a request *)
(* in maybe-do-request *)
QueueReceive(mbRequests, tServer_req );
(* Send response *)
QueuePush(mbOut, SrvResponses[tServer_req]);
or (* Send a query *)
await NoThreadsStopped /\ ~QueueEmpty(queriesToSend);
SendQuery(QueuePeek(queriesToSend));
QueuePop(queriesToSend);
end either;
server_loopy:
goto server;
end if;
send_ack_close:
(* Order is important *)
if send_close then
assert ConnThreadsStopped;
(* in create-remote-connection *)
SocketSend(sockOut, "(close)");
elsif send_ack_close then
assert ConnThreadsStopped;
(* in create-remote-connection *)
SocketSend(sockOut, "(ack-close)");
end if;
check_query_responses:
\* Check each query is either marked FAILED or has a correct reply
\* This is NOT part of the implementation
if checkId < Len(sentQueries) then
checkId := checkId + 1;
if LET query == sentQueries[checkId]
IN query.res = CliResponses[query.q] then
(* Ok response *)
(* ghost_droppedQueries is just a heuristic, drop the entry if
it was marked to be dropped *)
if /\ ghost_droppedQueries /= <<>>
/\ sentQueries[checkId].q = Head(ghost_droppedQueries) then
ghost_droppedQueries := Tail(ghost_droppedQueries);
end if;
goto check_query_responses;
elsif (* Remote end closed before queries were replied to *)
/\ ghost_droppedQueries /= <<>>
/\ sentQueries[checkId].q = Head(ghost_droppedQueries) then
(* Queries must be marked failed *)
assert sentQueries[checkId].res = FAILED;
ghost_droppedQueries := Tail(ghost_droppedQueries);
goto check_query_responses;
else
error( <<"Query result wrong", checkId, sentQueries[checkId] >> );
end if;
end if;
server_stop:
if ~BrokenSocket(sockIn) then (* TODO: remove this hack *)
assert ~WaitForServerQueriesBeforeClosing \/ queriesToSend = <<>>;
end if;
(* Should receive (ack-close) when "conditions" *)
assert ( /\ flag_serverTriesToClose
/\ WaitForServerQueriesBeforeClosing
/\ flag_remote_waits_for_close
/\ ~BrokenSocket(sockIn))
=> ghost_got_close_ack;
end process;
\*
\* Remote end
\*
process tRemote = "remote-end"
variables remoteMsgs = IncomingQueries \o << "(close)" >> , rmsg = FALSE,
expResps = EMPTY_QUEUE, tRemote_received = FALSE;
begin
other:
either (* Send message *)
await <<>> /= remoteMsgs;
await \/ ~WaitForServerQueriesBeforeClosing
\/ Head(remoteMsgs) /= "(close)"
\/ AllQueriesDone;
QueueReceive(remoteMsgs, rmsg);
if rmsg = "(close)" then
if flag_remote_waits_for_close /\ flag_serverTriesToClose then
goto handle_query;
else
SocketSend(sockIn, rmsg);
QueuePush(expResps, "(ack-close)");
MarkDroppedQueries();
goto other;
end if;
else (* Send query *)
SocketSend(sockIn, rmsg);
QueuePush(expResps, SrvResponses[rmsg]);
goto other;
end if;
or (* Handle message from server *)
await ~QueueEmpty(sockOut);
handle_query:
SocketReceive(sockOut, tRemote_received);
ghost_received_sockOut_msgs := Append(ghost_received_sockOut_msgs, tRemote_received);
if tRemote_received = "connection-cut" \/ BrokenSocket(sockIn) then
goto other_stop;
elsif tRemote_received \in SrvQueries then
(* Respond to query from server *)
SocketSend(sockIn, CliResponses[tRemote_received]);
elsif tRemote_received = "(close)" then
SocketSend(sockIn, "(ack-close)");
remoteMsgs := <<>>;
goto other_stop;
else
(* Check result to our query was as expected *)
assert tRemote_received = QueuePeek(expResps);
QueuePop(expResps);
if tRemote_received = "(ack-close)" then
goto other_stop;
end if;
end if;
other_loopy:
goto other;
or (* Nothing more to send *) (* TODO: never-triggers *)
await QueueEmpty(remoteMsgs) /\ QueueEmpty(expResps) /\ ~flag_serverTriesToClose;
end either;
other_stop:
skip;
end process;
end algorithm;*)
\* BEGIN TRANSLATION
\* Label send_ack_close of process tServer at line 350 col 1 changed to send_ack_close_
VARIABLES WaitForServerQueriesBeforeClosing, flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut,
mbRequests, queriesToSend, sentQueries, send_ack_close, send_close,
ghost_droppedQueries, ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack, pc, stack
(* define statement *)
QueryIds == DOMAIN sentQueries
TypeInvariant ==
/\ SeqOf(sentQueries, QueryStates)
/\ SeqOf(mbOut, SrvQueries
\cup CliQueryResults
\union {"(close)", "(ack-close)", "close", "flush-and-ack-close"})
/\ SeqOf(mbQuery, QueryIds \union {CLOSE, CLOSE_CLEAN})
/\ SeqOf(mbQueryCopy, QueryIds \union {CLOSE, CLOSE_CLEAN})
/\ SeqOf(mbQueryRes, SrvQueryResults \union {"close", "fail"})
/\ BrokenSocket(sockIn) \/ SeqOf(sockIn, WireMsgs)
/\ BrokenSocket(sockOut) \/ SeqOf(sockOut, WireMsgs)
QueueEmpty(q) == q = EMPTY_QUEUE
QueuePeek(q) == Head(q)
ConnThreads == {"conn-out", "conn-in", "query-joiner", "query-send"}
ConnThreadsStopped == \A t \in ConnThreads: pc[t] = "Done"
NoThreadsStopped == \A t \in ConnThreads: pc[t] /= "Done"
ConnectionTermination == <>(ConnThreadsStopped)
ghost_HavePendingRequests == \E i \in DOMAIN sentQueries: sentQueries[i].res = WAITING_RESPONSE
Query(query, response) == [q |-> query, res |-> response]
SeqMap(s, Op(_)) == [i \in DOMAIN s |-> Op(s[i])]
WaitingQueries == SeqMap(SelectSeq(sentQueries, LAMBDA q: q.res = WAITING_RESPONSE),
LAMBDA q: q.q)
AllQueriesDone == Len(sentQueries) = Len(OutgoingQueries) /\ WaitingQueries = <<>>
VARIABLES tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs,
rmsg, expResps, tRemote_received
vars == << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut,
mbRequests, queriesToSend, sentQueries, send_ack_close, send_close,
ghost_droppedQueries, ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack, pc, stack,
tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs,
rmsg, expResps, tRemote_received >>
ProcSet == {"conn-out"} \cup {"conn-in"} \cup {"query-joiner"} \cup {"query-send"} \cup {"connection-breaker"} \cup {"server"} \cup {"remote-end"}
Init == (* Global variables *)
/\ WaitForServerQueriesBeforeClosing \in BOOLEAN
/\ flag_serverTriesToClose \in BOOLEAN
/\ flag_remote_waits_for_close \in BOOLEAN
/\ IncomingQueries \in Prefixes(3, << "q1", "q2", "q3", "q4" >> )
/\ OutgoingQueries \in Prefixes(3, << "sq1", "sq2", "sq3" >> )
/\ sockIn = EMPTY_QUEUE
/\ sockOut = EMPTY_QUEUE
/\ mbQueryRes = EMPTY_QUEUE
/\ mbQuery = EMPTY_QUEUE
/\ mbQueryCopy = EMPTY_QUEUE
/\ mbOut = EMPTY_QUEUE
/\ mbRequests = EMPTY_QUEUE
/\ queriesToSend = OutgoingQueries
/\ sentQueries = <<>>
/\ send_ack_close = FALSE
/\ send_close = FALSE
/\ ghost_droppedQueries = <<>>
/\ ghost_received_sockOut_msgs = <<>>
/\ ghost_received_sockIn_msgs = <<>>
/\ ghost_got_close_ack = FALSE
(* Process tOut *)
/\ tOut_msg = FALSE
/\ tOut_flush = FALSE
(* Process tIn *)
/\ tIn_msg = FALSE
(* Process tJoin *)
/\ tJoin_q = FALSE
/\ tJoin_res = FALSE
/\ tJoin_fail_remaining = FALSE
(* Process tSend *)
/\ tSend_q = FALSE
(* Process tServer *)
/\ tServer_req = FALSE
/\ checkId = 0
(* Process tRemote *)
/\ remoteMsgs = IncomingQueries \o << "(close)" >>
/\ rmsg = FALSE
/\ expResps = EMPTY_QUEUE
/\ tRemote_received = FALSE
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self = "conn-out" -> "conn_out"
[] self = "conn-in" -> "conn_in"
[] self = "query-joiner" -> "query_joiner"
[] self = "query-send" -> "query_send"
[] self = "connection-breaker" -> "maybe_break_connection"
[] self = "server" -> "server"
[] self = "remote-end" -> "other"]
CleanShutdown_entry(self) == /\ pc[self] = "CleanShutdown_entry"
/\ send_close' = TRUE
/\ mbQuery' = Append(mbQuery, CLOSE_CLEAN)
/\ pc' = [pc EXCEPT ![self] = "shutdown_loop"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes,
mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries,
send_ack_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack,
tOut_msg, tOut_flush, tIn_msg,
tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs,
rmsg, expResps, tRemote_received >>
shutdown_loop(self) == /\ pc[self] = "shutdown_loop"
/\ ConnThreadsStopped \/ ~QueueEmpty(mbRequests)
/\ IF ~QueueEmpty(mbRequests)
THEN /\ mbRequests' = EMPTY_QUEUE
/\ pc' = [pc EXCEPT ![self] = "shutdown_loop"]
/\ stack' = stack
ELSE /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED mbRequests
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbQuery,
mbQueryCopy, mbOut, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
CleanShutdown(self) == CleanShutdown_entry(self) \/ shutdown_loop(self)
conn_out == /\ pc["conn-out"] = "conn_out"
/\ ~QueueEmpty(mbOut)
/\ tOut_msg' = QueuePeek(mbOut)
/\ mbOut' = Tail(mbOut)
/\ IF BrokenSocket(sockOut)
THEN /\ TRUE
/\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"]
/\ UNCHANGED << sockOut, tOut_flush >>
ELSE /\ IF tOut_msg' = "(close)"
THEN /\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, tOut_msg')
ELSE /\ TRUE
/\ UNCHANGED sockOut
/\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"]
/\ UNCHANGED tOut_flush
ELSE /\ IF tOut_msg' = "flush-and-ack-close"
THEN /\ tOut_flush' = TRUE
/\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"]
/\ UNCHANGED sockOut
ELSE /\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, tOut_msg')
ELSE /\ TRUE
/\ UNCHANGED sockOut
/\ pc' = [pc EXCEPT !["conn-out"] = "conn_out"]
/\ UNCHANGED tOut_flush
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, mbQueryRes, mbQuery,
mbQueryCopy, mbRequests, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries, ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
flush_out_queue == /\ pc["conn-out"] = "flush_out_queue"
/\ IF tOut_flush /\ ~( QueueEmpty(mbOut) /\ QueueEmpty(mbRequests))
THEN /\ ~QueueEmpty(mbOut)
/\ tOut_msg' = QueuePeek(mbOut)
/\ mbOut' = Tail(mbOut)
/\ IF tOut_msg' = "close"
THEN /\ TRUE
/\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue_loop"]
/\ UNCHANGED sockOut
ELSE /\ IF tOut_msg' = "(close)"
THEN /\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, tOut_msg')
ELSE /\ TRUE
/\ UNCHANGED sockOut
/\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"]
ELSE /\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, tOut_msg')
ELSE /\ TRUE
/\ UNCHANGED sockOut
/\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue_loop"]
ELSE /\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"]
/\ UNCHANGED << sockOut, mbOut, tOut_msg >>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries, sockIn,
mbQueryRes, mbQuery, mbQueryCopy,
mbRequests, queriesToSend, sentQueries,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_flush,
tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
flush_out_queue_loop == /\ pc["conn-out"] = "flush_out_queue_loop"
/\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbQuery,
mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining,
tSend_q, tServer_req, checkId,
remoteMsgs, rmsg, expResps,
tRemote_received >>
notify_sender == /\ pc["conn-out"] = "notify_sender"
/\ mbQuery' = Append(mbQuery, CLOSE)
/\ pc' = [pc EXCEPT !["conn-out"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQueryCopy, mbOut, mbRequests, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
tOut == conn_out \/ flush_out_queue \/ flush_out_queue_loop
\/ notify_sender
conn_in == /\ pc["conn-in"] = "conn_in"
/\ ~QueueEmpty(sockIn)
/\ IF BrokenSocket(sockIn)
THEN /\ tIn_msg' = "connection-cut"
/\ UNCHANGED sockIn
ELSE /\ tIn_msg' = QueuePeek(sockIn)
/\ sockIn' = Tail(sockIn)
/\ ghost_received_sockIn_msgs' = Append(ghost_received_sockIn_msgs, tIn_msg')
/\ IF tIn_msg' = "(close)"
THEN /\ send_ack_close' = TRUE
/\ mbOut' = Append(mbOut, "flush-and-ack-close")
/\ mbQueryRes' = Append(mbQueryRes, "close")
/\ pc' = [pc EXCEPT !["conn-in"] = "Done"]
/\ UNCHANGED << mbQuery, mbRequests, ghost_got_close_ack >>
ELSE /\ IF tIn_msg' = "(ack-close)"
THEN /\ ghost_got_close_ack' = TRUE
/\ pc' = [pc EXCEPT !["conn-in"] = "Done"]
/\ UNCHANGED << mbQueryRes, mbQuery,
mbRequests >>
ELSE /\ IF tIn_msg' \in CliQueries
THEN /\ mbRequests' = Append(mbRequests, tIn_msg')
/\ pc' = [pc EXCEPT !["conn-in"] = "conn_in"]
/\ UNCHANGED << mbQueryRes,
mbQuery >>
ELSE /\ IF tIn_msg' \in SrvQueryResults
THEN /\ mbQueryRes' = Append(mbQueryRes, tIn_msg')
/\ pc' = [pc EXCEPT !["conn-in"] = "conn_in"]
/\ UNCHANGED mbQuery
ELSE /\ IF tIn_msg' = "connection-cut"
THEN /\ mbQueryRes' = Append(mbQueryRes, "fail")
/\ mbQuery' = Append(mbQuery, CLOSE)
ELSE /\ Assert(Print("Invalid message", FALSE),
"Failure of assertion at line 139, column 3 of macro called at line 235, column 5.")
/\ UNCHANGED << mbQueryRes,
mbQuery >>
/\ pc' = [pc EXCEPT !["conn-in"] = "Done"]
/\ UNCHANGED mbRequests
/\ UNCHANGED ghost_got_close_ack
/\ UNCHANGED << mbOut, send_ack_close >>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockOut, mbQueryCopy,
queriesToSend, sentQueries, send_close,
ghost_droppedQueries, ghost_received_sockOut_msgs,
stack, tOut_msg, tOut_flush, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req, checkId,
remoteMsgs, rmsg, expResps, tRemote_received >>
tIn == conn_in
query_joiner == /\ pc["query-joiner"] = "query_joiner"
/\ ~QueueEmpty(mbQueryCopy)
/\ tJoin_q' = QueuePeek(mbQueryCopy)
/\ mbQueryCopy' = Tail(mbQueryCopy)
/\ IF tJoin_q' = CLOSE
THEN /\ tJoin_fail_remaining' = TRUE
/\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"]
ELSE /\ IF tJoin_q' = CLOSE_CLEAN
THEN /\ TRUE
/\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"]
ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "join_get_resp"]
/\ UNCHANGED tJoin_fail_remaining
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbOut, mbRequests, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_res, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
join_get_resp == /\ pc["query-joiner"] = "join_get_resp"
/\ ~QueueEmpty(mbQueryRes)
/\ tJoin_res' = QueuePeek(mbQueryRes)
/\ mbQueryRes' = Tail(mbQueryRes)
/\ IF tJoin_res' \in {"close", "fail"}
THEN /\ Assert(sentQueries[tJoin_q].res = WAITING_RESPONSE,
"Failure of assertion at line 150, column 3 of macro called at line 254, column 7.")
/\ sentQueries' = (tJoin_q :> [q |-> sentQueries[tJoin_q].q, res |-> FAILED]
@@ [i \in DOMAIN sentQueries \ {tJoin_q} |-> sentQueries[i]])
/\ tJoin_fail_remaining' = TRUE
/\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"]
ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "set_query_result"]
/\ UNCHANGED << sentQueries, tJoin_fail_remaining >>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQuery,
mbQueryCopy, mbOut, mbRequests, queriesToSend,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
set_query_result == /\ pc["query-joiner"] = "set_query_result"
/\ Assert(sentQueries[tJoin_q].res = WAITING_RESPONSE,
"Failure of assertion at line 150, column 3 of macro called at line 258, column 7.")
/\ sentQueries' = (tJoin_q :> [q |-> sentQueries[tJoin_q].q, res |-> tJoin_res]
@@ [i \in DOMAIN sentQueries \ {tJoin_q} |-> sentQueries[i]])
/\ pc' = [pc EXCEPT !["query-joiner"] = "query_joiner"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries, sockIn,
sockOut, mbQueryRes, mbQuery, mbQueryCopy,
mbOut, mbRequests, queriesToSend,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
fail_remaining == /\ pc["query-joiner"] = "fail_remaining"
/\ IF tJoin_fail_remaining
THEN /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"]
ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
fail_remaining_loop == /\ pc["query-joiner"] = "fail_remaining_loop"
/\ IF ~QueueEmpty(mbQueryCopy)
THEN /\ IF QueuePeek(mbQueryCopy) \notin {CLOSE, CLOSE_CLEAN}
THEN /\ Assert(sentQueries[(QueuePeek(mbQueryCopy))].res = WAITING_RESPONSE,
"Failure of assertion at line 150, column 3 of macro called at line 267, column 7.")
/\ sentQueries' = ((QueuePeek(mbQueryCopy)) :> [q |-> sentQueries[(QueuePeek(mbQueryCopy))].q, res |-> FAILED]
@@ [i \in DOMAIN sentQueries \ {(QueuePeek(mbQueryCopy))} |-> sentQueries[i]])
ELSE /\ TRUE
/\ UNCHANGED sentQueries
/\ mbQueryCopy' = Tail(mbQueryCopy)
/\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"]
/\ UNCHANGED mbQuery
ELSE /\ IF ~QueueEmpty(mbQuery)
THEN /\ IF QueuePeek(mbQuery) \notin {CLOSE, CLOSE_CLEAN}
THEN /\ Assert(sentQueries[(QueuePeek(mbQuery))].res = WAITING_RESPONSE,
"Failure of assertion at line 150, column 3 of macro called at line 275, column 7.")
/\ sentQueries' = ((QueuePeek(mbQuery)) :> [q |-> sentQueries[(QueuePeek(mbQuery))].q, res |-> FAILED]
@@ [i \in DOMAIN sentQueries \ {(QueuePeek(mbQuery))} |-> sentQueries[i]])
/\ mbQuery' = Tail(mbQuery)
/\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"]
ELSE /\ mbQuery' = Tail(mbQuery)
/\ pc' = [pc EXCEPT !["query-joiner"] = "replace_close"]
/\ UNCHANGED sentQueries
ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "Done"]
/\ UNCHANGED << mbQuery,
sentQueries >>
/\ UNCHANGED mbQueryCopy
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbOut,
mbRequests, queriesToSend,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
replace_close == /\ pc["query-joiner"] = "replace_close"
/\ mbQuery' = Append(mbQuery, CLOSE)
/\ pc' = [pc EXCEPT !["query-joiner"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQueryCopy, mbOut, mbRequests, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
tJoin == query_joiner \/ join_get_resp \/ set_query_result
\/ fail_remaining \/ fail_remaining_loop \/ replace_close
query_send == /\ pc["query-send"] = "query_send"
/\ ~QueueEmpty(mbQuery)
/\ tSend_q' = QueuePeek(mbQuery)
/\ mbQuery' = Tail(mbQuery)
/\ mbQueryCopy' = Append(mbQueryCopy, tSend_q')
/\ IF tSend_q' = CLOSE
THEN /\ mbOut' = Append(mbOut, "close")
/\ pc' = [pc EXCEPT !["query-send"] = "Done"]
ELSE /\ IF tSend_q' = CLOSE_CLEAN
THEN /\ mbOut' = Append(mbOut, "(close)")
/\ pc' = [pc EXCEPT !["query-send"] = "Done"]
ELSE /\ mbOut' = Append(mbOut, (sentQueries[tSend_q'].q))
/\ pc' = [pc EXCEPT !["query-send"] = "query_send"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbRequests, queriesToSend, sentQueries,
send_ack_close, send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
tSend == query_send
maybe_break_connection == /\ pc["connection-breaker"] = "maybe_break_connection"
/\ \/ /\ sockIn' = <<"connection-cut">>
/\ sockOut' = <<"connection-cut">>
/\ IF ghost_droppedQueries = <<>>
THEN /\ ghost_droppedQueries' = WaitingQueries \o queriesToSend
ELSE /\ TRUE
/\ UNCHANGED ghost_droppedQueries
\/ /\ TRUE
/\ UNCHANGED <>
/\ pc' = [pc EXCEPT !["connection-breaker"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
mbQueryRes, mbQuery, mbQueryCopy,
mbOut, mbRequests, queriesToSend,
sentQueries, send_ack_close,
send_close,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining,
tSend_q, tServer_req, checkId,
remoteMsgs, rmsg, expResps,
tRemote_received >>
tBreaker == maybe_break_connection
server == /\ pc["server"] = "server"
/\ \/ ConnThreadsStopped
\/ ~QueueEmpty(mbRequests)
\/ ~QueueEmpty(queriesToSend)
\/ flag_serverTriesToClose
/\ IF ConnThreadsStopped
THEN /\ TRUE
/\ pc' = [pc EXCEPT !["server"] = "send_ack_close_"]
/\ UNCHANGED << mbQuery, mbOut, mbRequests, queriesToSend,
sentQueries, stack, tServer_req >>
ELSE /\ IF QueueEmpty(queriesToSend) /\ flag_serverTriesToClose
THEN /\ stack' = [stack EXCEPT !["server"] = << [ procedure |-> "CleanShutdown",
pc |-> "send_ack_close_" ] >>
\o stack["server"]]
/\ pc' = [pc EXCEPT !["server"] = "CleanShutdown_entry"]
/\ UNCHANGED << mbQuery, mbOut, mbRequests,
queriesToSend, sentQueries,
tServer_req >>
ELSE /\ \/ /\ ~QueueEmpty(mbRequests)
/\ tServer_req' = QueuePeek(mbRequests)
/\ mbRequests' = Tail(mbRequests)
/\ mbOut' = Append(mbOut, (SrvResponses[tServer_req']))
/\ UNCHANGED <>
\/ /\ NoThreadsStopped /\ ~QueueEmpty(queriesToSend)
/\ sentQueries' = Append(sentQueries, (Query((QueuePeek(queriesToSend)), WAITING_RESPONSE)))
/\ mbQuery' = Append(mbQuery, (Len(sentQueries')))
/\ queriesToSend' = Tail(queriesToSend)
/\ UNCHANGED <>
/\ pc' = [pc EXCEPT !["server"] = "server_loopy"]
/\ stack' = stack
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose, flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries, sockIn, sockOut,
mbQueryRes, mbQueryCopy, send_ack_close, send_close,
ghost_droppedQueries, ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, checkId, remoteMsgs,
rmsg, expResps, tRemote_received >>
server_loopy == /\ pc["server"] = "server_loopy"
/\ pc' = [pc EXCEPT !["server"] = "server"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
send_ack_close_ == /\ pc["server"] = "send_ack_close_"
/\ IF send_close
THEN /\ Assert(ConnThreadsStopped,
"Failure of assertion at line 351, column 3.")
/\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, "(close)")
ELSE /\ TRUE
/\ UNCHANGED sockOut
ELSE /\ IF send_ack_close
THEN /\ Assert(ConnThreadsStopped,
"Failure of assertion at line 355, column 3.")
/\ IF ~BrokenSocket(sockOut)
THEN /\ sockOut' = Append(sockOut, "(ack-close)")
ELSE /\ TRUE
/\ UNCHANGED sockOut
ELSE /\ TRUE
/\ UNCHANGED sockOut
/\ pc' = [pc EXCEPT !["server"] = "check_query_responses"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries, sockIn,
mbQueryRes, mbQuery, mbQueryCopy, mbOut,
mbRequests, queriesToSend, sentQueries,
send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
check_query_responses == /\ pc["server"] = "check_query_responses"
/\ IF checkId < Len(sentQueries)
THEN /\ checkId' = checkId + 1
/\ IF LET query == sentQueries[checkId']
IN query.res = CliResponses[query.q]
THEN /\ IF /\ ghost_droppedQueries /= <<>>
/\ sentQueries[checkId'].q = Head(ghost_droppedQueries)
THEN /\ ghost_droppedQueries' = Tail(ghost_droppedQueries)
ELSE /\ TRUE
/\ UNCHANGED ghost_droppedQueries
/\ pc' = [pc EXCEPT !["server"] = "check_query_responses"]
ELSE /\ IF /\ ghost_droppedQueries /= <<>>
/\ sentQueries[checkId'].q = Head(ghost_droppedQueries)
THEN /\ Assert(sentQueries[checkId'].res = FAILED,
"Failure of assertion at line 381, column 7.")
/\ ghost_droppedQueries' = Tail(ghost_droppedQueries)
/\ pc' = [pc EXCEPT !["server"] = "check_query_responses"]
ELSE /\ Assert(Print((<<"Query result wrong", checkId', sentQueries[checkId'] >>), FALSE),
"Failure of assertion at line 139, column 3 of macro called at line 386, column 7.")
/\ pc' = [pc EXCEPT !["server"] = "server_stop"]
/\ UNCHANGED ghost_droppedQueries
ELSE /\ pc' = [pc EXCEPT !["server"] = "server_stop"]
/\ UNCHANGED << ghost_droppedQueries,
checkId >>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries,
sockIn, sockOut, mbQueryRes, mbQuery,
mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries,
send_ack_close, send_close,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining,
tSend_q, tServer_req, remoteMsgs,
rmsg, expResps, tRemote_received >>
server_stop == /\ pc["server"] = "server_stop"
/\ IF ~BrokenSocket(sockIn)
THEN /\ Assert(~WaitForServerQueriesBeforeClosing \/ queriesToSend = <<>>,
"Failure of assertion at line 391, column 3.")
ELSE /\ TRUE
/\ Assert(( /\ flag_serverTriesToClose
/\ WaitForServerQueriesBeforeClosing
/\ flag_remote_waits_for_close
/\ ~BrokenSocket(sockIn))
=> ghost_got_close_ack,
"Failure of assertion at line 394, column 1.")
/\ pc' = [pc EXCEPT !["server"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
tServer == server \/ server_loopy \/ send_ack_close_
\/ check_query_responses \/ server_stop
other == /\ pc["remote-end"] = "other"
/\ \/ /\ <<>> /= remoteMsgs
/\ \/ ~WaitForServerQueriesBeforeClosing
\/ Head(remoteMsgs) /= "(close)"
\/ AllQueriesDone
/\ ~QueueEmpty(remoteMsgs)
/\ rmsg' = QueuePeek(remoteMsgs)
/\ remoteMsgs' = Tail(remoteMsgs)
/\ IF rmsg' = "(close)"
THEN /\ IF flag_remote_waits_for_close /\ flag_serverTriesToClose
THEN /\ pc' = [pc EXCEPT !["remote-end"] = "handle_query"]
/\ UNCHANGED << sockIn,
ghost_droppedQueries,
expResps >>
ELSE /\ IF ~BrokenSocket(sockIn)
THEN /\ sockIn' = Append(sockIn, rmsg')
ELSE /\ TRUE
/\ UNCHANGED sockIn
/\ expResps' = Append(expResps, "(ack-close)")
/\ IF ghost_droppedQueries = <<>>
THEN /\ ghost_droppedQueries' = WaitingQueries \o queriesToSend
ELSE /\ TRUE
/\ UNCHANGED ghost_droppedQueries
/\ pc' = [pc EXCEPT !["remote-end"] = "other"]
ELSE /\ IF ~BrokenSocket(sockIn)
THEN /\ sockIn' = Append(sockIn, rmsg')
ELSE /\ TRUE
/\ UNCHANGED sockIn
/\ expResps' = Append(expResps, (SrvResponses[rmsg']))
/\ pc' = [pc EXCEPT !["remote-end"] = "other"]
/\ UNCHANGED ghost_droppedQueries
\/ /\ ~QueueEmpty(sockOut)
/\ pc' = [pc EXCEPT !["remote-end"] = "handle_query"]
/\ UNCHANGED <>
\/ /\ QueueEmpty(remoteMsgs) /\ QueueEmpty(expResps) /\ ~flag_serverTriesToClose
/\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"]
/\ UNCHANGED <>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose, flag_remote_waits_for_close,
IncomingQueries, OutgoingQueries, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req,
checkId, tRemote_received >>
handle_query == /\ pc["remote-end"] = "handle_query"
/\ ~QueueEmpty(sockOut)
/\ IF BrokenSocket(sockOut)
THEN /\ tRemote_received' = "connection-cut"
/\ UNCHANGED sockOut
ELSE /\ tRemote_received' = QueuePeek(sockOut)
/\ sockOut' = Tail(sockOut)
/\ ghost_received_sockOut_msgs' = Append(ghost_received_sockOut_msgs, tRemote_received')
/\ IF tRemote_received' = "connection-cut" \/ BrokenSocket(sockIn)
THEN /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"]
/\ UNCHANGED << sockIn, remoteMsgs, expResps >>
ELSE /\ IF tRemote_received' \in SrvQueries
THEN /\ IF ~BrokenSocket(sockIn)
THEN /\ sockIn' = Append(sockIn, (CliResponses[tRemote_received']))
ELSE /\ TRUE
/\ UNCHANGED sockIn
/\ pc' = [pc EXCEPT !["remote-end"] = "other_loopy"]
/\ UNCHANGED << remoteMsgs, expResps >>
ELSE /\ IF tRemote_received' = "(close)"
THEN /\ IF ~BrokenSocket(sockIn)
THEN /\ sockIn' = Append(sockIn, "(ack-close)")
ELSE /\ TRUE
/\ UNCHANGED sockIn
/\ remoteMsgs' = <<>>
/\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"]
/\ UNCHANGED expResps
ELSE /\ Assert(tRemote_received' = QueuePeek(expResps),
"Failure of assertion at line 445, column 7.")
/\ expResps' = Tail(expResps)
/\ IF tRemote_received' = "(ack-close)"
THEN /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"]
ELSE /\ pc' = [pc EXCEPT !["remote-end"] = "other_loopy"]
/\ UNCHANGED << sockIn,
remoteMsgs >>
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, mbQueryRes, mbQuery,
mbQueryCopy, mbOut, mbRequests, queriesToSend,
sentQueries, send_ack_close, send_close,
ghost_droppedQueries,
ghost_received_sockIn_msgs,
ghost_got_close_ack, stack, tOut_msg,
tOut_flush, tIn_msg, tJoin_q, tJoin_res,
tJoin_fail_remaining, tSend_q, tServer_req,
checkId, rmsg >>
other_loopy == /\ pc["remote-end"] = "other_loopy"
/\ pc' = [pc EXCEPT !["remote-end"] = "other"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg,
expResps, tRemote_received >>
other_stop == /\ pc["remote-end"] = "other_stop"
/\ TRUE
/\ pc' = [pc EXCEPT !["remote-end"] = "Done"]
/\ UNCHANGED << WaitForServerQueriesBeforeClosing,
flag_serverTriesToClose,
flag_remote_waits_for_close, IncomingQueries,
OutgoingQueries, sockIn, sockOut, mbQueryRes,
mbQuery, mbQueryCopy, mbOut, mbRequests,
queriesToSend, sentQueries, send_ack_close,
send_close, ghost_droppedQueries,
ghost_received_sockOut_msgs,
ghost_received_sockIn_msgs, ghost_got_close_ack,
stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q,
tJoin_res, tJoin_fail_remaining, tSend_q,
tServer_req, checkId, remoteMsgs, rmsg, expResps,
tRemote_received >>
tRemote == other \/ handle_query \/ other_loopy \/ other_stop
Next == tOut \/ tIn \/ tJoin \/ tSend \/ tBreaker \/ tServer \/ tRemote
\/ (\E self \in ProcSet: CleanShutdown(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
================================================================================