fmod FAPI is

--- Flush Spread layr API
--- used by Secure Spread or directly by applications

protecting FMESSAGE .
including STATE .

--- additional errors generated by flush layer

sort IllegalStateError .
op IllegalState : -> IllegalStateError .

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

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

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

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

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

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

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

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

-----------------------
--- Seguti
op f-join-req            --- client requests to join a group
    : Agent              --- client
      Group              --- group to join
      GroupType		 --- group type tag (either VS or EVS)
   -> State .

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

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

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

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

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

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

subsort IllegalStateError < MulticastError .

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

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

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

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

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

op f-receive-ack         --- received message
    : Agent              --- client = receiver
      FMessage
   -> State .

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

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

sort FlushError .
subsort FlushError < Error .
subsort IllegalAgentError < FlushError .
subsort IllegalStateError < FlushError .

op f-flushok-req         --- client sends flushok
    : Agent              --- client
      Group              --- group to flush
   -> State .

op f-flushok-ack         --- server acknowledges flushok
    : Agent              --- client
   -> State .

op f-flushok-err         --- server rejects flushok
    : Agent              --- client
      FlushError         --- error status
   -> State .

endfm