module CO4_PROCESSES (CO4_DATATYPES) is

-------------------------------------------------------------------------------

channel MessageChannel is
   (b1: BaseId, b2: BaseId, m: Message)
end channel

channel UserActionChannel is
   (dest: BaseId, u: UserAction, b: BaseId),
   (dest: BaseId, u: UserAction, p: Proposal),
   (dest: BaseId, u: UserAction, r: Request),
   (dest: BaseId, u: UserAction, r: Request, p: Proposal)
end channel

channel SignalValChannel is
   (sender: BaseId, s: SignalVal, m: Message),
   (sender: BaseId, s: SignalVal, p: Proposal, b: Bool),
   (sender: BaseId, s: SignalVal, from: BaseId),
   (sender: BaseId, s: SignalVal, p: Proposal)
end channel

-------------------------------------------------------------------------------

process InitIndividualKB [user: UserActionChannel, parentin: MessageChannel,
        parentout: MessageChannel, signal: SignalValChannel] (B: BaseId) is
   IndividualKB [user, parentin, parentout, signal] (B, None of ParentBase,
   {} of SubmittedTbl, First of Id, {} of PendingTbl)
end process

process IdleIndividualKB [user: UserActionChannel, parentin: MessageChannel,
        parentout: MessageChannel, signal: SignalValChannel] (B: BaseId,
        G: ParentBase) is
   IndividualKB [user, parentin, parentout, signal] (B, G, {} of SubmittedTbl,
   First of Id, {} of PendingTbl)
end process

process IndividualKB [user: UserActionChannel, parentin: MessageChannel,
        parentout: MessageChannel, signal: SignalValChannel] (B: BaseId,
        in var G: ParentBase, in var A: SubmittedTbl, in var NA: Id,
        in var P: PendingTbl) is
   loop L in
      alt
         only if (A == {} of SubmittedTbl) and (P == {} of PendingTbl) then
            break L
         end if
      []
         only if (G == None) and (A == {} of SubmittedTbl) then
            var b1: BaseId in
               user (B, doregister, ?b1);
               parentout (B, b1, register (NA, b1));
               A := insert (submitted (NA, reqregister (b1)), A);
               NA := next (NA)
            end var
         end if
      []
         only if issome (G) then
            var p1: Proposal in
               user (B, doevaluate, ?p1);
               parentout (B, the (G), evaluate (NA, p1));
               A := insert (submitted (NA, reqevaluate (p1)), A);
               NA := next (NA)
            end var
         end if
      []
         only if issome (G) then
            var p1: Proposal in
               user (B, doachieve, ?p1);
               parentout (B, the (G), achieve (NA, p1));
               A := insert (submitted (NA, reqachieve (p1)), A);
               NA := next (NA)
            end var
         end if
      []
         only if issome (G) then
            var r1: Request in
               user (B, doforward, ?r1);
               parentout (B, the (G), forward (NA, r1));
               A := insert (submitted (NA, reqforward (r1)), A);
               NA := next (NA)
            end var
         end if
      []
         only if issome (G) then
            var m1: Id in
               m1 := any Id;
               only if m1 isin A then
                  user (B, dodeny, req (Get (m1, A)));
                  parentout (B, the (G), deny (m1));
                  A := Remove (m1, A)
               end if
            end var
         end if
      []
         only if issome (G) then
            var n1: Id, r1: Request in
               n1 := any Id;
               only if (n1 isin P) and then (status (Get (n1, P)) == new) then
                  r1 := req (Get (n1, P));
                  alt
                     user (B, doaccept, r1);
                     parentout (B, the (G), reply (n1, acceptx));
                     P := insert (set_status (accepted, Get (n1, P)), P)
                  []
                     user (B, doreject, r1);
                     parentout (B, the (G), reply (n1, reject));
                     P := insert (set_status (rejected, Get (n1, P)), P)
                  []
                     only if Is_reqachieve (r1) then
                        (*** should apply to forward* (achieve (...)) too ***)
                        var p1: Proposal in
                           user (B, dochallenge, r1, ?p1);
                           parentout (B, the (G), reply (n1, challenge (NA, p1)));
                           A := insert (submitted (NA, reqchallenge (p1)), A);
                           NA := next (NA);
                           P := insert (set_status (challenged, Get (n1, P)), P)
                        end var
                     end if
                  end alt
               end if
            end var
         end if
      []
         var from: BaseId, msg: Message in
            parentin (?from, B, ?msg);
            alt
               only if Is_notify (msg) then
                  var m1: Id, a1: Answer in
                     m1 := inreplyto (msg);
                     a1 := content (msg);
                     if m1 isin A then
                        if Is_reqregister (req (Get (m1, A))) then
                           only if content (req (Get (m1, A))) of BaseId == from then
                              if isNone (G) then
                                 if Is_acceptx (a1) then
                                    G := some (from)
                                  end if
                              else
                                 assert isSome (G)
                              end if;
                              A := Remove (m1, A)
                           end if
                        else
                           A := Remove (m1, A)
                        end if
                     else
                        signal (B, signotinA, msg)
                     end if
                  end var
               end if
            []
               only if Is_askall (msg) and (G == some (from)) then
                  var n1: Id, r1: Request in
                     n1 := replywith (msg);
                     r1 := content (msg);
                     P := insert (pending (n1, r1, new), P)
                  end var
               end if
            []
               only if Is_tell (msg) and (G == some (from)) then
                  (*** handling of knowledge in user KB: unspecified ***)
                  null
               end if
            []
               only if Is_error (msg) and (G == some (from)) then
                  var m1: Id in
                     m1 := inreplyto (msg);
                     if m1 isin A then
                        A := Remove (m1, A)
                     else
                        signal (B, signotinA, msg)
                     end if
                  end var
               end if
            []
               only if Is_poolnotify (msg) and (G == some (from)) then
                  var n1: Id in
                     n1 := inreplyto (msg);
                     if n1 isin P then
                        P := Remove (n1, P)
                     else
                        signal (B, signotinP, msg)
                     end if
                  end var
               end if
            []
               only if Is_pooldeny (msg) and (G == some (from)) then
                  var n1: Id in
                     n1 := inreplyto (msg);
                     if n1 isin P then
                        P := Remove (n1, P)
                     else
                        signal (B, signotinP, msg)
                     end if
                  end var
               end if
            end alt
         end var
      end alt
   end loop
end process

process SerializeIndividualKB [user: UserActionChannel,
        parentin, parentout: MessageChannel] is
   loop L in
      var b: BaseId in
         alt
            break L
         []
            user (?b, ?any UserAction, ?any BaseId);
            parentout (b, ?any BaseId, ?any Message)
         []
            user (?b, ?any UserAction, ?any Proposal);
            parentout (b, ?any BaseId, ?any Message)
         []
            user (?b, ?any UserAction, ?any Request);
            parentout (b, ?any BaseId, ?any Message)
         []
            user (?b, ?any UserAction, ?any Request, ?any Proposal);
            parentout (b, ?any BaseId, ?any Message)
         []
            parentin (?any BaseId, ?any BaseId, ?any Message)
         end alt
      end var
   end loop
end process

-------------------------------------------------------------------------------
-- Group KBs

process InitGroupKB [childrenin, childrenout, parentin, parentout: MessageChannel,
        signal: SignalValChannel] (B: BaseId) is
   GroupKB [childrenin, childrenout, parentin, parentout, signal] (B,
   none of ParentBase, {} of GrpSubmittedTbl, First of Id, {} of PendingTbl,
   {} of CfcTbl, First of Id, {} of SubscriberSet, {} of Knowledge)
end process

process IdleGroupKB [childrenin, childrenout, parentin, parentout: MessageChannel,
        signal: SignalValChannel] (B: BaseId, G: ParentBase, S: SubscriberSet) is
   GroupKB [childrenin, childrenout, parentin, parentout, signal] (B, G,
   {} of GrpSubmittedTbl, First of Id, {} of PendingTbl, {} of CfcTbl,
   First of Id, S, {} of Knowledge)
end process

process GroupKB [childrenin, childrenout, parentin, parentout: MessageChannel,
        signal: SignalValChannel] (B: BaseId, in var G: Parentbase,
        in var A: GrpSubmittedTbl, in var NA: Id, in var P: PendingTbl,
        in var C: CfcTbl, in var NC: Id, in var S: SubscriberSet,
        in var K: Knowledge) is
   loop L in
      alt
         only if (A == {} of GrpSubmittedTbl) and (P == {} of PendingTbl) then
            break L
         end if
      []
         var from: BaseId, msg: Message in
            childrenin (?from, B, ?msg);
            alt
               only if Is_register (msg) then
                  var b2: BaseId, m1: Id, req: Request in
                     b2 := content (msg);
                     m1 := replywith (msg);
                     req := reqregister (b2);
                     only if b2 == B then
                        if S <> {} then
                           Broadcast [childrenout] (B, askall (NC, req), S);
                           C := Insert (cfc (NC, from, m1, req, Card (S)), C);
                           NC := Next (NC)
                        else
                           childrenout (B, from, notify (m1, acceptx));
                           childrenout (B, from, tell (Assert (K)));
                           signal (B, sigregistered, from);
                           S := Insert (from, S)
                        end if
                     end if
                  end var
               end if
            []
               only if Is_evaluate (msg) then
                  var p1: Proposal, m1: Id in
                     p1 := content (msg);
                     m1 := replywith (msg);
                     childrenout (B, from, notify (m1, answer (query (K, p1))))
                  end var
               end if
            []
               only if Is_achieve (msg) then
                  var p1: Proposal, m1: Id, req: Request in
                     p1 := content (msg);
                     m1 := replywith (msg);
                     req := reqachieve (p1);
                     if query (K, p1) then
                        Broadcast [childrenout] (B, askall (NC, req), S);
                        C := insert (cfc (NC, from, m1, req, card (S)), C);
                        NC := Next (NC)
                     else
                        childrenout (B, from, error (m1))
                     end if
                  end var
               end if
            []
               only if Is_forward (msg) then
                  var m1: Id, r1, req: Request in
                     r1 := content (msg);
                     m1 := replywith (msg);
                     req := reqforward (r1);
                     if isSome (G) or (isNone (G) and Is_reqregister (r1)) then
                        Broadcast [childrenout] (B, askall (NC, req), S);
                        C := insert (cfc (NC, from, m1, req, card (S)), C);
                        NC := Next (NC)
                     else
                        assert isNone (G) and not (Is_reqregister (r1));
                        childrenout (B, from, error (m1))
                     end if
                  end var
               end if
            []
               only if Is_deny (msg) then
                  var m1: Id in
                     m1 := inreplyto (msg);
                     if searchrequest (from, m1, C) then
                        var n1: Id in
                           n1 := id (getrequest (from, m1, C));
                           Broadcast [childrenout] (B, pooldeny (n1), S);
                           C := Remove (n1, C)
                        end var
                     else
                        signal (B, signotinC, msg)
                     end if
                  end var
               end if
            []
               only if Is_reply (msg) then
                  var n1: Id, a1: Answer in
                     n1 := inreplyto (msg);
                     a1 := content (msg);
                     if n1 isin C then
                        var entry: CfcEntry, x1: Nat, r1: Request, b2: BaseId, m2: Id in
                           entry := Get (n1, C);
                           x1 := count (entry);
                           r1 := req (entry);
                           b2 := sender (entry);
                           m2 := senderid (entry);
                           alt
                              only if Is_acceptx (a1) then
                                 if x1 == 1 then
                                    alt
                                       only if Is_reqregister (r1) then
                                          childrenout (B, b2, notify (m2, acceptx));
                                          childrenout (B, b2, tell (Assert (K)));
                                          Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                          EnumerateAskall [childrenout] (B, Remove (n1, C), b2);
                                          signal (B, sigregistered, b2);
                                          C := incallcount (Remove (n1, C));
                                          S := insert (b2, S)
                                       end if
                                    []
                                       only if Is_reqachieve (r1) then
                                          childrenout (B, b2, notify (m2, acceptx));
                                          var p1: Proposal in
                                             p1 := content (r1);
                                             Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                             Broadcast [childrenout] (B, tell (p1), S);
                                             signal (B, sigstored, p1, query (K, p1));
                                             C := remove (n1, C);
                                             K := K + p1
                                          end var
                                       end if
                                    []
                                       only if Is_reqforward (r1) then
                                          if not (G == some (b2)) then
                                             var r2: Request in
                                                r2 := content (r1);
                                                Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                                alt
                                                   only if Is_reqregister (r2) then
                                                      var b3: BaseId in
                                                         b3 := content (r2);
                                                         parentout (B, b3, register (NA, b3));
                                                         A := Insert (submitted (NA, r2, b2, m2), A);
                                                         NA := next (NA);
                                                         C := Remove (n1, C)
                                                      end var
                                                   end if
                                                []
                                                   only if Is_reqevaluate (r2) and issome (G) then
                                                      parentout (B, the (G), evaluate (NA, content (r2)));
                                                      A := Insert (submitted (NA, r2, b2, m2), A);
                                                      NA := next (NA);
                                                      C := Remove (n1, C)
                                                   end if
                                                []
                                                   only if Is_reqachieve (r2) and issome (G) then
                                                      parentout (B, the (G), achieve (NA, content (r2)));
                                                      A := insert (submitted (NA, r2, b2, m2), A);
                                                      NA := next (NA);
                                                      C := Remove (n1, C)
                                                   end if
                                                []
                                                   only if Is_reqforward (r2) and issome (G) then
                                                      parentout (B, the (G), forward (NA, content (r2)));
                                                      A := insert (submitted (NA, r2, b2, m2), A);
                                                      NA := next (NA);
                                                      C := Remove (n1, C)
                                                   end if
                                                end alt
                                             end var
                                          elsif m2 isin P then
                                             only if status (Get (m2, P)) == new then
                                                parentout (B, the (G), reply (m2, acceptx));
                                                Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                                P := Insert (set_status (accepted, Get (m2, P)), P);
                                                C := Remove (n1, C)
                                             end if
                                          else
                                              signal (B, signotinP, msg);
                                              Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                              C := Remove (n1, C)
                                          end if
                                       end if
                                    []
                                       only if Is_reqtell (r1) and (G == some (b2)) then
                                          var p1: Proposal in
                                             p1 := content (r1);
                                             Broadcast [childrenout] (B, poolnotify (n1, acceptx), S);
                                             Broadcast [childrenout] (B, tell (p1), S);
                                             signal (B, sigstored, p1, query (K, p1));
                                             C := Remove (n1, C);
                                             K := K + p1
                                          end var
                                       end if
                                    end alt
                                 else
                                    assert x1 > 1;
                                    C := Insert (set_count (x1 - 1, entry), C)
                                 end if
                              end if
                           []
                              only if Is_reject (a1) then
                                 if not (G == some (b2)) then
                                    childrenout (B, b2, notify (m2, a1));
                                    Broadcast [childrenout] (B, pooldeny (n1), S);
                                    C := Remove (n1, C)
                                 else
                                    alt
                                       only if Is_reqforward (r1) then
                                          if m2 isin P then
                                             only if status (Get (m2, P)) == new then
                                                parentout (B, the (G), reply (m2, reject));
                                                Broadcast [childrenout] (B, pooldeny (n1), S);
                                                P := insert (set_status (rejected, Get (m2, P)), P);
                                                C := Remove (n1, C)
                                             end if
                                          else
                                             signal (B, signotinP, msg);
                                             Broadcast [childrenout] (B, pooldeny (n1), S);
                                             C := Remove (n1, C)
                                          end if
                                       end if
                                    []
                                       only if Is_reqtell (r1) then
                                          Broadcast [childrenout] (B, pooldeny (n1), S);
                                          C := Remove (n1, C)
                                       end if
                                    end alt
                                 end if
                              end if
                           []
                              only if Is_challenge (a1) and Is_reqachieve (r1) then
                                 (*** should apply to forward* (achieve (...)) too ***)
                                 if not (G == some (b2)) then
                                    var m1: Id, p1, p2: Proposal, r2: Request in
                                       m1 := replywith (a1);
                                       p1 := content (a1);
                                       p2 := content (r1);
                                       r2 := reqachieve (p2*p1);
                                       childrenout (B, b2, notify (m2, a1));
                                       Broadcast [childrenout] (B, pooldeny (n1), S);
                                       Broadcast [childrenout] (B, askall (NC, r2), S);
                                       C := Insert (cfc (NC, from, m1, r2, card (S)), remove (n1, C));
                                       NC := Next (NC)
                                    end var
                                 else
                                    stop (*** should not be reached ***)
                                 end if
                              end if
                           end alt
                        end var
                     else
                        signal (B, signotinC, msg)
                     end if
                  end var
               end if
            end alt
         end var
      []
         var from: BaseId, msg: Message in
            parentin (?from, B, ?msg);
            alt
               only if Is_notify (msg) then
                  var m1: Id, a1: Answer in
                     m1 := inreplyto (msg);
                     a1 := content (msg);
                     if m1 isin A then
                        var entry: GrpSubmittedEntry, r1: Request, b2: BaseId, m2: Id in
                           entry := Get (m1, A);
                           r1 := req (entry);
                           b2 := sender (entry);
                           m2 := senderid (entry);
                           childrenout (B, b2, notify (m2, a1));
                           if Is_reqregister (r1) then
                              only if content (r1) of BaseId == from then
                                 if Is_acceptx (a1) then
                                    G := Some (from)
                                 end if;
                                 A := Remove (m1, A)
                              end if
                           else
                              only if G == some (from) then
                                 A := Remove (m1, A)
                              end if
                           end if
                        end var
                     else
                        signal (B, signotinA, msg)
                     end if
                  end var
               end if
            []
               only if Is_askall (msg) and (G == some (from)) then
                  var n1: Id, r1: Request in
                     n1 := replywith (msg);
                     r1 := content (msg);
                     Broadcast [childrenout] (B, askall (NC, reqforward (r1)), S);
                     P := insert (pending (n1, r1, new), P);
                     C := insert (cfc (NC, from, n1, reqforward (r1), card (S)), C);
                     NC := Next (NC)
                  end var
               end if
            []
               only if Is_error (msg) and (G == some (from)) then
                  var m1: Id in
                     m1 := inreplyto (msg);
                     if m1 isin A then
                        var entry: GrpSubmittedEntry, b2: BaseId, m2: Id in
                           entry := Get (m1, A);
                           b2 := sender (entry);
                           m2 := senderid (entry);
                           childrenout (B, b2, error (m2));
                           A := Remove (m1, A)
                        end var
                     else
                        signal (B, signotinA, msg)
                     end if
                  end var
               end if
            []
               only if Is_poolnotify (msg) and (G == some (from)) then
                  var n1: Id in
                     n1 := inreplyto (msg);
                     if n1 isin P then
                        if searchrequest (from, n1, C) then
                           var n2: Id in
                              n2 := id (getrequest (from, n1, C));
                              Broadcast [childrenout] (B, poolnotify (n2, acceptx), S);
                              C := Remove (n2, C)
                           end var
                        end if;
                        P := Remove (n1, P)
                     else
                        signal (B, signotinP, msg)
                     end if
                  end var
               end if
            []
               only if Is_pooldeny (msg) and (G == some (from)) then
                  var n1: Id in
                     n1 := inreplyto (msg);
                     if n1 isin P then
                        if searchrequest (from, n1, C) then
                           var n2: Id in
                              n2 := id (getrequest (from, n1, C));
                              Broadcast [childrenout] (B, pooldeny (n2), S);
                              C := Remove (n2, C)
                           end var
                        end if;
                        P := Remove (n1, P)
                     else
                        signal (B, signotinP, msg)
                     end if
                  end var
               end if
            []
               only if Is_tell (msg) and (G == some (from)) then
                  var p1: Proposal, req: Request in
                     p1 := content (msg);
                     req := reqtell (p1);
                     if query (K, p1) then
                        Broadcast [childrenout] (B, askall (NC, req), S);
                        C := Insert (cfc (NC, from, First, req, Card (S)), C);
                        NC := Next (NC)
                     else
                        signal (B, signotconsistent, p1)
                     end if
                  end var
               end if
            end alt
         end var
      end alt
   end loop
end process

-------------------------------------------------------------------------------

process Broadcast [broadcastout: MessageChannel] (B: BaseId, msg: Message,
        in var S: SubscriberSet) is
   while S <> {} loop
      var b1: BaseId in
         b1 := pick (S);
         broadcastout (B, b1, msg);
         S := remove (b1, S)
       end var
   end loop;
   i -- to model the "exit" that existed in the original LOTOS specification
end process

process EnumerateAskall [childrenout: MessageChannel] (B: BaseId,
        in var C: CfcTbl, b1: BaseId) is
   while C <> {} loop
      var entry: CfcEntry in
         entry := pick (C);
         childrenout (B, b1, askall (id (entry), req (entry)));
         C := Remove (id (entry), C)
         end var
   end loop;
   i -- to model the "exit" that existed in the original LOTOS specification
end process

process InitQueue [input, output: MessageChannel] is
   var pktq: PacketQueue in
      pktq := {};
      loop L in -- %%% WHILE LOOP impprobable
         alt
            var b1, b2: BaseId, msg: Message in
               input (?b1, ?b2, ?msg);
               pktq := pktq + packet (b1, b2, msg)
            end var
         []
            if pktq == {} then
               break L
            else
               var p: Packet in
                  p := First (pktq);
                  output (sender (p), receiver (p), message (p));
                  pktq := butfirst (pktq)
               end var
            end if
         end alt
      end loop
   end var
end process

process Ring [g: none] is
   g; Ring [g]
end process

process AllUserAccept [user: UserActionChannel] is
   loop
      user (?any BaseId, doaccept, ?any Request)
   end loop
end process

process AllUserReply [user: UserActionChannel] is
   loop
      alt
         user (?any BaseId, doaccept, ?any Request)
         []
         user (?any BaseId, doreject, ?any Request)
         []
         user (?any BaseId, dodeny, ?any Request)
      end alt
   end loop
end process

-------------------------------------------------------------------------------

end module