Makefile

@@ -42,3 +42,7 @@ otrv4.disk.cpp: otrv4.m
 
 clean:
 	rm -f *.cpp otrv4 otrv4.cache otrv4.disk otrv4.cache.splitfile otrv4.disk.splitfile
+
+runake:
+	make otrv4
+	./otrv4 -tv -ndl

notes.md

@@ -17,7 +17,6 @@
 
 ### Take into account:
 
-- Whitespace tags should not be sent in ENCRYPTED_MESSAGES state.
 - Whitespace tags are not be sent in ENCRYPTED_MESSAGES state.
 - Transition between interactive and non-interactive.
 - Receiving v3 messages at any point.
@@ -25,3 +24,10 @@
 - Receiving a identity message at any point.
 - Receiving a auth-r message at any point.
 - Receiving a auth-i message at any point.
+
+### Add to the protocol
+
+- Whitespace tags are not be sent in ENCRYPTED_MESSAGES state.
+- Are we going to allow receiving query messages in any state?
+- Are we going to allow receiving identity messages in encrypted state?
+- Are we going to allow receiving non-interactive-auth messages in encrypted state?

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