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 .

var forceka, kainprogress : GroupSet .

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) .


--- if force flush, set flags

crl ENABLED(FLUSHOK(agent))
    sdelivered'(agent,smessagelist')
    sdelivered(agent, sSMessageList(smessage) smessagelist)
    sforceka(agent,forceka)
    skainprogress(agent,kainprogress)
    =>
    PERFORMED(FLUSHOK(agent))
    sdelivered'(agent,smessagelist' sSMessageList(smessage))
    sdelivered(agent, smessagelist)
    sforceka(agent,add'(forceka,group(smessage)))
    skainprogress(agent,add'(kainprogress,group(smessage)))
    ssp-flushok-req(agent,group(smessage))
    if issffreq(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