--------------------------------------------------------------------------
--                                                                      --
-- Système de messagerie instantannée: spécification lfp.               --
--                                                                      --
-- Cette spécification est exactement identique à la spécification      --
-- définie dans le chapitre "Etude de cas" de la thèse.                 --
-- Elle doit permettre de comparer les deux syntaxes et de valider la   --
-- syntaxe textuelle                                                    --
--                                                                      --
--------------------------------------------------------------------------



------------------| DECLARATION GLOBALES DU MODELE |------------------

type t_msg_type is enum (diffuse, quit, join);
type t_message is opaque
   function get_type () return boolean;
   function is_equal (msg : in t_message) return boolean;
end;

type GUI is opaque
   function get_message () return t_message;
   procedure display_message (msg : in t_message);
end;

type t_port is port (t_port);


-- nombre max de client par groupe de discution
const max_number_of_client : integer :=  255;
-- nombre max de groupe gérable par un serveur.
const max_nb_group : integer := 128;

-- déclaration "en avance" des classes du système.
class sender;
class receiver;
class group;
class server;

-- déclaration "en avance" des médias du système
media rpc;
media message_sender;

-- déclaration de l'instance statique du serveur.
s1 : server with();

--------------------| DECLARATION DES INTERFACES |--------------------

-- declarer tous les attributs qui apparaissent dans une instruction 
-- d'instanciation dynamique avant que le composant ait été défini. 
--
-- dans ce modèle on aurait peut être pu s'en sortir en délcarant les 
-- composants dans le bon ordre, mais c'est plus simple en utilisant une
-- interface explicite. 

media rpc is 
   input : t_port;
end;


media msg_sender is
   input : t_port;
end;

class group is
   first_user : receiver;
   itf, server_itf : t_port;
   asynchronous procedure diffuse (msg : in t_message) -> itf;
   function remove (client : in receiver) return integer -> server_itf;
   asynchronous procedure register (client : in receiver) -> server_itf;
end;

class server is
   itf, group_itf : t_port;
end;

class receiver is 
   itf : t_port;
end;


--------------------------| CLASSE SENDER |--------------------------
--
-- afin de tester les instructions de saut de type "goto" la boucle
-- principale de la classe est implémentée à l'aide d'un label et
-- d'instructions goto afin de fournir un exemple de l'utilisation de
-- ces instructions dans la syntaxe textuelle. 
class sender is
   itf : t_port ;
   next_msg : t_message ;
   user_itf : GUI ;
   connected : boolean := false;
   current_group : group ;
   recep : receiver ;
   msg_kind : t_msg_type ;
   my_rpc : rpc ;
   snd : msg_sender;
begin
   recep := new receiver (interface => user_itf);

   -- début de la boucle : label de l'état start_loop.
:start_loop:
   next_msg := user_itf@get_message();
   msg_kind := next_msg@get_type();

   if msg_kind = join
   then
      if connected = true
      then
         snd := new msg_sender(input => itf);
         [s1.itf] quit_group (current_group, recep) -> itf;
      end; -- if connected = true

      my_rpc := new rpc (input => itf);
      current_group := [s1.itf] join (recep, next_msg) <=> itf;
      connected := true;
      goto start_loop;
   elsif msg_kind = diffuse
   then
      snd := new msg_sender(input =>itf);
      [current_group.itf] diffuse(next_msg) -> itf;
      goto start_loop;
   elsif msg_kind = quit
   then
      connected := false;
      snd := new msg_sender(input => itf);
      [s1.itf] quit_group (current_group, recep) -> itf;
      goto start_loop;
   end;

end; -- class sender.


--------------------------| CLASSE RECEIVER |--------------------------
--
-- réception et affichage des messages en provenance du groupe.
class receiver is
   msg : t_message;
   interface : GUI;
   itf : t_port;
begin
   while true
   begin
      (msg) <- itf;
      interface@display_message(msg);
   end;
end;


---------------------------| CLASSE SERVER |---------------------------
--
-- gestion des groupes et de leurs abonnés.

class server is
   itf : t_port ; 
   group_itf : t_port ;
   type t_group is record
       name : t_message ;
       reference : group ; 
   end ;

   type t_group_list is array (1..max_nb_group) of t_group ;
   group_list : t_group_list ; 
   nbr_of_groups : integer := 0 ;



   function join (user       : in receiver ; 
                  group_name : in t_message) return group -> itf
   is
      group_exists : boolean := false; 
      group_index : integer := 0;
      new_group : group;
      send : msg_sender;
   begin
      for i in 1..nbr_of_groups
      begin
         if group_name@is_equal(group_list(i).name)
         then
            group_index := i;
            group_exists := true;
         end;
      end;

      if group_exists = false
      then
         new_group := new group (first_user => user);
         nbr_of_groups := nbr_of_groups + 1;
         group_list (nbr_of_groups).reference := new_group;
         group_list(nbr_of_groups).name := group_name;
         group_index := 1;
      elsif group_exists = true 
      then
         new_group := group_list(group_index).reference;
         send := new msg_sender(input => group_itf);
         [new_group.server_itf] group:register(user) -> itf;
      end;

      return (new_group);
      
   end; -- join 


   procedure quit_group (group_ref : in group; 
                         user : in receiver) -> itf
   is
      comm : rpc;
      nbr : integer;
      index :  integer := 0;
   begin
      comm := new rpc (input => group_itf);
      nbr := [group_ref.server_itf] remove (user) <=> group_itf;

      if nbr = 0
         then
         for i in 1..nbr_of_groups
         begin
            if group_list(i).reference = group_ref
            then 
               index := i ; 
            end ;
         end ;
   
         nbr_of_groups := nbr_of_groups - 1 ; 
   
         for i in index..nbr_of_groups
         begin
            group_list(i) := group_list(i+1) ;  
         end ; 
      end;
   end; -- quit_group

begin
   while true
   begin
      accept 
         join <- (), 
         quit_group <- ()
      end;
   end;
end; -- class server. 

---------------------------| CLASSE GROUP |---------------------------
--
-- diffuser les messages et gérer la liste des abonnés. 
class group is 
   itf, server_itf : t_port ; 
   type t_user_list is array (1..max_number_of_client) of receiver;
   
   client_list : t_user_list;

   nbr_of_clients : integer := 1;

   asynchronous procedure diffuse (msg : in t_message) -> itf
   is
      i : integer := 0;
      snd : msg_sender ;
   begin
      while i < nbr_of_clients
      begin
         i := i + 1;
         snd := new msg_sender(input => itf);
         [client_list(i).itf] (msg) -> itf;
      end;
   end; -- diffuse

   function remove (client : in receiver) return integer -> server_itf 
   is
   begin
      for i in 1..nbr_of_clients
      begin
         if client_list(i) = client
         then
            index := i;
         end ;
      end;

      nbr_of_clients := integer'pred(nbr_of_clients);
      for i in index..nbr_of_clients
      begin 
       client_list(i) := client_list(i+1);
      end ;

      return (nbr_of_clients);
   end; -- remove

   asynchronous procedure register (client : in receiver) -> server_itf
   is
   begin
      nbr_of_clients := nbr_of_clients + 1;
      client_list (nbr_of_clients) := client;
   end; -- register

   --id of the user that creates the group
   first_user : receiver; 
begin
   client_list(1) := first_user;

   while nbr_of_clients >0
   begin
      accept
         diffuse <- (),
         register <- (),
         remove <- ()
      end;
   end;
end;

----------------------------| MEDIA RPC |----------------------------
--
media rpc is
   target : t_port;
   input : t_port;
   msg : message;
begin
   [target] (msg) <- input;
   (msg) -> target;
   (msg) <- target;
   (msg) -> input;
end;


-------------------------| MEDIA MSG_SENDER |-------------------------
--
media msg_sender is
   msg : message;
   target : t_port;
   input : t_port;
begin
    [target] (msg) <- input;
   (msg) -> target;
end;

---------------------| DIAGRAMME D'ARCHITECTURE |---------------------

-- diagramme d'architecture, on reprend exactement ce qui existe dans
-- la thèse même si ce n'est pas optimal.
binder sender.itf is FIFO (3)
   itf |-> rpc, msg_sender;
   itf <-| rpc, msg_sender, sender;
end;

binder receiver.itf is FIFO (3)
   itf |-> msg_sender;
   itf <-| receiver, msg_sender;
end;

binder server.itf is FIFO (3)
   itf |-> server, rpc;
   itf <-| server, rpc;
end;

binder group.itf is fifo (3)
   itf |-> group, msg_sender;
   itf <-| msg_sender, group;
end;

binder server.group_itf is fifo (1)
   group_itf |-> server, msg_sender, rpc;
   group_itf <-| server, msg_sender, rpc;
end;

binder group.server_itf is fifo (1)
   server_itf |-> group, msg_sender, rpc;
   server_itf <-| group, msg_sender, rpc;
end;


media rpc (sender, server);
media rpc (group, server);
media msg_sender ( (group, server), 
                   (sender, group), 
                   (group, receiver));

-----------------| FIN DU DIAGRAMME D'ARCHITECTURE |-----------------