mod STEST is

protecting SECURESPREAD .

var agent : Agent .
var smessage : SMessage .
var smessagelist smessagelist' : SMessageList .

op sdelivered : Agent SMessageList -> State .
op sdelivered' : Agent SMessageList -> State .

op  FLUSHOK : Agent -> Action .
op  DELIVERCHANGE : Agent -> Action .

--- keep on requesting messages and put into deliver buffer
rl  ssp-receive-ack(agent,smessage) 
    sdelivered(agent, smessagelist) =>
    ssp-receive-req(agent)
    sdelivered(agent, smessagelist sSMessageList(smessage)) .

--- if agent gets freq, it answers immediately with fok
--- delivered' =  history of all processed messages
--- delivered = list of all received messages
crl ENABLED(FLUSHOK(agent))
    sdelivered'(agent,smessagelist')
    sdelivered(agent, sSMessageList(smessage) smessagelist) =>
    PERFORMED(FLUSHOK(agent))
    sdelivered'(agent,smessagelist' sSMessageList(smessage))
    sdelivered(agent, smessagelist)
    ssp-flushok-req(agent,group(smessage))
    if issfreq(smessage) .

--- get rid of flushok-ack
rl  ssp-flushok-ack(agent) => eState .

--- 

crl sdelivered'(agent,smessagelist')
    sdelivered(agent, sSMessageList(smessage) smessagelist) =>
    sdelivered'(agent,smessagelist' sSMessageList(smessage))
    sdelivered(agent, smessagelist)
    if issdata(smessage) .

crl ENABLED(DELIVERCHANGE(agent))
    sdelivered'(agent,smessagelist')
    sdelivered(agent, sSMessageList(smessage) smessagelist) =>
    PERFORMED(DELIVERCHANGE(agent))
    sdelivered'(agent,smessagelist' sSMessageList(smessage))
    sdelivered(agent, smessagelist)
    if issjoin(smessage) or
       issleave(smessage) or issselfleave(smessage) or
       issdisconnect(smessage) or
       isstrans(smessage) or issconf(smessage) .

endm