fmod GAPI is

--- Spread group layer API (official API)
--- used by applications directly or by Flush Spread layer

protecting GMESSAGE .
including STATE .

subsort Agent < Proc . 
--- assume each agent is running as an individual process

----------------------------------------------
---  group layer interface towards upper layer
----------------------------------------------

sort Error . --- has several subsorts, see below

sort IllegalAgentError .
op IllegalAgent : -> IllegalAgentError .

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

sort ConnectError .
subsort ConnectError < Error .
op AgentNotUnique : -> ConnectError .

op sp-connect-req        --- client requests connection to spread server
    : Agent              --- client
   -> State .

op sp-connect-ack        --- server acknowledges established connection
    : Agent              --- client
   -> State .

op sp-connect-err        --- server rejects request
    : Agent              --- client
      ConnectError       --- error status
   -> State .

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

sort DisconnectError .
subsort DisconnectError < Error .
subsort IllegalAgentError < DisconnectError .

op sp-disconnect-req     --- client requests to disconnect from spread server
    : Agent              --- client
   -> State .

op sp-disconnect-ack     --- server acknowledges disconnect
    : Agent              --- client
   -> State .

op sp-disconnect-err     --- server rejects request
    : Agent              --- client
      DisconnectError    --- error status
   -> State .

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

sort JoinError .
subsort JoinError < Error .
subsort IllegalAgentError < JoinError .

op sp-join-req           --- client requests to join a group
    : Agent              --- client
      Group              --- group to join
   -> State .

op sp-join-ack           --- server acknowledges group join
    : Agent              --- client
   -> State .

op sp-join-err           --- server rejects request
    : Agent              --- client
      JoinError          --- error status 
   -> State .

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

sort LeaveError .
subsort LeaveError < Error .
subsort IllegalAgentError < LeaveError .

op sp-leave-req          --- client requests to leave a group
    : Agent              --- client
      Group              --- group to leave
   -> State .

op sp-leave-ack          --- server acknowledges group leave
    : Agent              --- client
   -> State .

op sp-leave-err          --- server rejects request
    : Agent              --- client
      LeaveError         --- error status
   -> State .

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

sort MulticastError .
subsort MulticastError < Error .
subsort IllegalAgentError < MulticastError .

op sp-multicast-req      --- client requests multicast to a group
    : Agent              --- client
      Mode               --- message type
      Group              --- destination
      GData	         --- contents
   -> State .

op sp-multicast-ack      --- server acknowledges multicast
    : Agent              --- client
   -> State .

op sp-multicast-err      --- server rejects multicast
    : Agent              --- client
      MulticastError     --- error status
   -> State .

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

sort ReceiveError .
subsort ReceiveError < Error .
subsort IllegalAgentError < ReceiveError .

op sp-receive-req          --- client requests next gmessage from server
    : Agent                --- client = intended receiver
   -> State .

op sp-receive-ack          --- received gmessage
    : Agent                --- client = receiver
      GMessage
   -> State .

op sp-receive-err          --- receive failed
    : Agent                --- client = intended receiver
      ReceiveError         --- error status
   -> State .

--------------------------------------------
--- group layer interface towards controller
--------------------------------------------

--- the following state compoments are only used to have a fine
--- control over the execution and to generate specific scenarios
--- (note that there are more actions defined in CAPI)

op MULTICAST : Agent Group -> Action .  
op JOIN : Agent Group -> Action .  
op LEAVE : Agent Group -> Action .
op DISCONNECT : Agent -> Action .
op SENDGROUPMSG : Agent -> Action .
op FAIL : Proc -> Action .
op RECOVER : Proc -> Action .

endfm