module odp is

------------------------------------------------------------------------------
-- type definitions
------------------------------------------------------------------------------

type Object is
    O1, O2, O3, O4
    with ==, <
end type

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

type Service is
    S1, S2, S3, S4, S5
    with ==, <
end type

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

type DataBase is
   nil, cons (s: Service, o: Object, d: Database)
end type

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

function Add (db: DataBase, z: Service, x: Object): DataBase is
   var y: Object, t: Service, d: DataBase in
      case db in
         nil ->
            return cons (z, x, nil)
      |  cons (t, y, d) ->
            if (z < t) or ((z == t) and (x < y)) then
               return cons (z, x, cons (t, y, d))
            else if (z == t) and (x == y) then
               return cons (t, y, d)
            else
               return cons (t, y, Add (d, z, x))
            end if
         end if
      end case
   end var
end function

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

function Is_in (db: DataBase, z: Service, x: Object): Bool is
   var y: Object, t: Service, d: DataBase in
      case db in
         nil ->
            return false
      |  cons (t, y, d) ->
            if (z == t) and (x == y) then
               return true
            else
               return Is_in (d, z, x)
            end if
      end case
   end var
end function

------------------------------------------------------------------------------
-- channel definitions
------------------------------------------------------------------------------

channel ExportChannel is
   (o1: Object, s: Service)
end channel

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

channel ImportChannel is
   (o1: Object, s: Service, o2: Object)
end channel

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

channel WorkChannel is
   (o1: Object, o2: Object, s: Service),
   (s: Service)
end channel

------------------------------------------------------------------------------
-- process definitions
------------------------------------------------------------------------------

process Main [Export: ExportChannel, Import: ImportChannel, Work: WorkChannel] is
   access Export, Import, Work;
   (*
    * the specification has three gates, named Export, Import, and Work:
    *
    *    - communication on Export (between the trader and an object) is used
    *      to signal that the object is server for a given service; Export
    *      has two offers (in this order): the identity of the server object
    *      and the exported service
    *
    *    - communication on Import (between the trader and an object) is used
    *      to signal that the object (client) can use some server to get a
    *      given service; Import has three offers (in this order): the
    *      identity of the client object, the name of the service, and the
    *      identity of the server object
    *
    *    - communication on Work (between two objects) models the execution of
    *      some service between a client object and a server object; Work has
    *      three offers (in this order): the identity of the server, the
    *      identity of the client, and the name of the service
    *)
   stop
   (*
    * the actual behaviour is the following:
    *
    * hide all but WORK in
    *    par EXPORT, IMPORT in
    *       Trader
    *    ||
    *       par WORK #2 in 
    *          Object_1
    *       || Object_2
    *       || Object_3
    *       || Object_4
    *       end par
    *    end par
    * end hide
    *
    * it is described compositionally in file demo.svl because ``m among n''
    * synchronization is not yet available in LNT
    *)
end process

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

process Trader [Export: ExportChannel, Import: ImportChannel] is
   var d: DataBase, server: Object, s: Service, client: Object in
      d := nil;
      loop
         alt
            -- some server exports the service s
            Export (?server, ?s);
            d := Add (d, s, server)
         []
            -- some client imports service s, which is provided by server
            Import (?client, ?s, ?server) where Is_in (d, s, server);
            use client
         end alt
      end loop
   end var
end process

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

process Trader_Alphabet [Export: ExportChannel, Import: ImportChannel] is
   loop
      alt
         Export (?any Object, ?any Service)
      []
         Import (?any Object, ?any Service, ?any Object)
      end alt
   end loop
end process

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

process Client [Import: ImportChannel, Work: WorkChannel]
               (o: Object, s: Service) is
   -- generic client of identity o requiring service s
   var server: Object in
      Import (o, s, ?server);
      Work (server, o, s)
   end var
end process

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

process Server [Export: ExportChannel, Work: WorkChannel]
               (o: Object, s: Service) is
   -- generic server of identity o providing service s
   Export (o, s);
   loop
      var client: Object in
         Work (o, ?client, s);
         use client
      end var
   end loop
end process

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

process Object_1 [Export: ExportChannel, Import: ImportChannel, Work: WorkChannel] is
   -- Object_1 is server for S2, S3, and S5 and executes service S1 forever
   par
      Server [Export, Work] (O1, S2)
   ||
      Server [Export, Work] (O1, S3)
   ||
      Server [Export, Work] (O1, S5)
   ||
      Object_1_Client [Import, Work]
   end par
end process

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

process Object_1_Client [Import: ImportChannel, Work: WorkChannel] is
   loop
      Client [Import, Work] (O1, S1);
      i -- former LOTOS operator ">>"
   end loop
end process

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

process Object_2 [Export: ExportChannel, Import: ImportChannel, Work: WorkChannel] is
   -- Object_2 is server for both S1 and S2 and executes service S3 forever
   par
      Server [Export, Work] (O2, S1)
   ||
      Server [Export, Work] (O2, S2)
   ||
      Object_2_Client [Import, Work]
   end par
end process

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

process Object_2_Client [Import: ImportChannel, Work: WorkChannel] is
   loop
      Client [Import, Work] (O2, S3);
      i -- former LOTOS operator ">>"
   end loop
end process

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

process Object_3 [Export: ExportChannel, Import: ImportChannel, Work: WorkChannel] is
   -- Object_3 is server for S3 and S4 and runs services S1 and S2 in alternance
   par
      Server [Export, Work] (O3, S3)
   ||
      Server [Export, Work] (O3, S4)
   ||
      Object_3_Client [Import, Work]
   end par
end process

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

process Object_3_Client [Import: ImportChannel, Work: WorkChannel] is
   loop
      Client [Import, Work] (O3, S1);
      i; -- former LOTOS operator ">>"
      Client [Import, Work] (O3, S2);
      i -- former LOTOS operator ">>"
   end loop
end process

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

process Object_4 [Export: ExportChannel, Import: ImportChannel, Work: WorkChannel] is
   -- Object_4 is server for S1 and runs services S2 to S5 in alternance
   par
      Server [Export, Work] (O4, S1)
   ||
      Object_4_Client [Import, Work]
   end par
end process

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

process Object_4_Client [Import: ImportChannel, Work: WorkChannel] is
   loop
      Client [Import, Work] (O4, S2);	
      i; -- former LOTOS operator ">>"
      Client [Import, Work] (O4, S3);
      i; -- former LOTOS operator ">>"
      Client [Import, Work] (O4, S4);
      i; -- former LOTOS operator ">>"
      Client [Import, Work] (O4, S5);
      i -- former LOTOS operator ">>"
   end loop
end process

------------------------------------------------------------------------------
-- the following processes represent the services that should be executed   --
-- by the different objects; these processes are used in demo.svl to verify --
-- the good behaviour of the trader                                         --
------------------------------------------------------------------------------

process Object_1_Service [Work: WorkChannel] is
   loop
      Work (S1)
   end loop
end process

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

process Object_2_Service [Work: WorkChannel] is
   loop
      Work (S3)
   end loop
end process

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

process Object_3_Service [Work: WorkChannel] is
   loop
      Work (S1);
      Work (S2)
   end loop
end process

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

process Object_4_Service [Work: WorkChannel] is
   loop
      Work (S2);
      Work (S3);
      Work (S4);
      Work (S5)
   end loop
end process

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

end module