Fix first bug found by McErlang, I think.

Sequence with client c1 and server s1::

1. Client c1 sets up a watch but times out.
  * Server s1's reply is dropped.
2. Client c1's watch request times out
3. Client c1 starts a counter_op and gets as far as `client_ph2_waiting`.
4. Server s1's response is dropped.
   * Client c1 is still waiting for a `{ph2_ok,...}` message
5. Server s1 times out waiting for c1's `{watch_notifies_delivered,...}`
   message.
6. Server s1 sends a `{watch_notify_maybe_req,...}` message to c1.
7. Client c1 isn't expecting a `{watch_notify_maybe_req,...}` message
   and therefore never replies.
8. Server s1 times out waiting for `{watch_notify_maybe_resp,...}` from
   client c1.  Goto step #6, looping forever.

src/distrib_counter_2phase_vclocksetwatch_sim.erl

@@ -471,6 +471,18 @@ client_ph2_waiting({ph1_ask_ok, ClOp, Server, Cookie, _Z} = Msg,
                    C = #c{clop = ClOp, ph1_oks = Oks, ph2_val = Z}) ->
     slf_msgsim:bang(Server, {ph2_do_set, slf_msgsim:self(), ClOp, Cookie, Z}),
     {recv_timeout, same, C#c{ph1_oks = [Msg|Oks]}};
+%% next 2 clauses, first bugfix for McErlang??
+client_ph2_waiting({watch_notify_req, ClOp, From, Z}, C) ->
+    %% Race: this arrived late, need to respond to it, though.
+    slf_msgsim:add_utrace({late_watch_notify_req, ClOp, Z}),
+    slf_msgsim:bang(From, {watch_notify_resp, slf_msgsim:self(), ClOp, ok}),
+    {recv_general, same, C};
+client_ph2_waiting({watch_notify_maybe_req, ClOp, From, Z}, C) ->
+    %% Race: this arrived late, need to respond to it, though.
+    slf_msgsim:add_utrace({late_watch_notify_maybe_req, Z}),
+    slf_msgsim:bang(From, {watch_notify_maybe_resp,
+                           slf_msgsim:self(), ClOp, ok}),
+    {recv_general, same, C};
 client_ph2_waiting(timeout, C = #c{num_responses = NumResps, ph2_val = Z,
                                    watchers = Ws}) ->
     Q = calc_q(C),
@@ -976,7 +988,18 @@ e_client_ph2_waiting(C = #c{clop = ClOp,
             end;
         {ph1_ask_ok, ClOp, Server, Cookie, _Z} = Msg ->
             mc_bang(Server, {ph2_do_set, mc_self(), ClOp, Cookie, Z}),
-            e_client_ph2_waiting(C#c{ph1_oks = [Msg|Oks]})
+            e_client_ph2_waiting(C#c{ph1_oks = [Msg|Oks]});
+        %% next 2 clauses, first bugfix for McErlang??
+        {watch_notify_req, _ClOp, From, _Z} ->
+            %% Race: this arrived late, need to respond to it, though.
+            mc_probe({late_watch_notify_req, ClOp, Z}),
+            mc_bang(From, {watch_notify_resp, mc_self(), ClOp, ok}),
+            e_client_ph2_waiting(C);
+        {watch_notify_maybe_req, _ClOp, From, _Z} ->
+            %% Race: this arrived late, need to respond to it, though.
+            mc_probe({late_watch_notify_maybe_req, Z}),
+            mc_bang(From, {watch_notify_maybe_resp, mc_self(), ClOp, ok}),
+            e_client_ph2_waiting(C)
     after ?TIMEOUT ->
             Q = calc_q(C),
             if NumResps >= Q ->