Receive query message

otrv4.m

@@ -129,7 +129,13 @@ begin
   clients[src].msgCount := clients[src].msgCount + 1
 endprocedure;
 
-
+procedure receiveMessage(src, dst: InstanceTag; var msg: Message);
+begin
+  msg.src := src;
+  msg.dst := dst;
+  multisetadd(msg, net);
+  clients[src].msgCount := clients[src].msgCount + 1
+endprocedure;
 
 
 --------------------------------------------------------------------------------
@@ -162,6 +168,22 @@ ruleset a : InstanceTag; b : InstanceTag do
   endrule;
 endruleset;
 
+ruleset a : InstanceTag; b : InstanceTag do
+  rule "User reacts to a Query message and sends Identity message"
+      transmittable(a, b)
+      & (clients[a].conv[b].protoState = S_Start
+      | clients[a].conv[b].protoState = S_WaitingAuthR
+      | clients[a].conv[b].protoState = S_WaitingAuthI
+      | clients[a].conv[b].protoState = S_EncryptedMessages
+      | clients[a].conv[b].protoState = S_Finished)
+    ==>
+    var msg: Message;
+    begin
+      undefine msg;
+      msg.msgType := M_QueryMessage;
+      receiveMessage(a, b, msg)
+  endrule;
+endruleset;
 
 --------------------------------------------------------------------------------
 -- Starting state