mod FTEST is

protecting FLUSHSPREAD .

var agent : Agent .
var fmessage : FMessage .
var fmessagelist fmessagelist' : FMessageList .

op fdelivered : Agent FMessageList -> State .
op fdelivered' : Agent FMessageList -> State .

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

rl  f-receive-ack(agent,fmessage) 
    fdelivered(agent, fmessagelist) =>
    f-receive-req(agent)
    fdelivered(agent, fmessagelist sFMessageList(fmessage)) .

crl ENABLED(FLUSHOK(agent))
    fdelivered'(agent,fmessagelist')
    fdelivered(agent, sFMessageList(fmessage) fmessagelist) =>
    PERFORMED(FLUSHOK(agent))
    fdelivered'(agent,fmessagelist' sFMessageList(fmessage))
    fdelivered(agent, fmessagelist)
    f-flushok-req(agent,group(fmessage))
    if isfreq(fmessage) .

rl  f-flushok-ack(agent) => eState .

crl fdelivered'(agent,fmessagelist')
    fdelivered(agent, sFMessageList(fmessage) fmessagelist) =>
    fdelivered'(agent,fmessagelist' sFMessageList(fmessage))
    fdelivered(agent, fmessagelist)
    if isfdata(fmessage) .

crl ENABLED(DELIVERCHANGE(agent))
    fdelivered'(agent,fmessagelist')
    fdelivered(agent, sFMessageList(fmessage) fmessagelist) =>
    PERFORMED(DELIVERCHANGE(agent))
    fdelivered'(agent,fmessagelist' sFMessageList(fmessage))
    fdelivered(agent, fmessagelist)
    if isfjoin(fmessage) or
       isfleave(fmessage) or isfselfleave(fmessage) or
       isfdisconnect(fmessage) or
       isftrans(fmessage) or isfconf(fmessage) .

endm