fmod SMESSAGE is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting FLUSHSPREAD .
protecting CLIQUES .

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

var client agent : Agent .
var group group' : Group .
var agentset agentset' : AgentSet .
var token : Token .
var view : View .
var transset transset' : AgentSet .
var fdata : FData .
var error : Error .
var key : PartialKey .

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

sort SMessage .  --- secure spread messages

var smessage smessage' : SMessage .

sort SData .     --- contents of secure spread data messages 
op sdata : String -> SData . 

var sdata : SData . 

--- secure spread messages

subsort SMessage < FData . --- some secure layer messages are flush layer data

--- messages visible to the upper layer

op sdatamsg         --- regular message
    : Agent         --- sender
      Group         --- all receivers 
      SData         --- contents
      View          --- sending view
   -> SMessage .
    
op sfreqmsg         --- secure flush request message
    : Agent         --- sender
      Group         --- affected group
   -> SMessage .
   
op stransmsg        --- secure transitional view message
    : Group         --- affected group
   -> SMessage .

op sjoinmsg         --- regular secure view message caused by join
    : Agent         --- joining agent
      Group         --- affected group
      View          --- new view
   -> SMessage .

op sleavemsg        --- regular secure view message caused by leave
    : Agent         --- joining agent
      Group         --- affected group
      View          --- new view
   -> SMessage .

op sdisconnectmsg   --- regular secure view message caused by disconnect
    : Agent         --- disconnecting agent
      Group         --- affected group
      View          --- new view
   -> SMessage .

op sconfmsg         --- regular secure view message caused by network
    : Group         --- affected group
      View          --- new view
      AgentSet      --- transitional set of agents 
   -> SMessage .    --- (i.e. agents that came with client into the new view)

op sselfleavemsg    --- selfleavemsg message
    : Agent         --- leaving agent
      Group         --- affected group
   -> SMessage .

--- internal messages (not visible to the upper layer)

op sdatamsg         --- internal data message
    : PartialKey    --- encrypted with
      SData         --- contents
   -> SMessage .

op stokenmsg        --- internal cliques message
    : Token         --- contents
   -> SMessage .

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

op issdata : SMessage ~> Bool .
eq issdata(sdatamsg(client,group,sdata,view)) = true .
eq issdata(stokenmsg(token)) = false .
eq issdata(sfreqmsg(client,group)) = false .
eq issdata(sjoinmsg(client,group,view)) = false .
eq issdata(sleavemsg(client,group,view)) = false .
eq issdata(stransmsg(group)) = false .
eq issdata(sconfmsg(group,view,transset)) = false .
eq issdata(sselfleavemsg(client,group)) = false .
eq issdata(sdisconnectmsg(client,group,view)) = false .

op issfreq : SMessage ~> Bool .
eq issfreq(sdatamsg(client,group,sdata,view)) = false .
eq issfreq(sfreqmsg(client,group)) = true .
eq issfreq(sjoinmsg(client,group,view)) = false .
eq issfreq(sleavemsg(client,group,view)) = false .
eq issfreq(stransmsg(group)) = false .
eq issfreq(sconfmsg(group,view,transset)) = false .
eq issfreq(sselfleavemsg(client,group)) = false .
eq issfreq(sdisconnectmsg(client,group,view)) = false .

op issjoin : SMessage ~> Bool .
eq issjoin(sdatamsg(client,group,sdata,view)) = false .
eq issjoin(sfreqmsg(client,group)) = false .
eq issjoin(sjoinmsg(client,group,view)) = true .
eq issjoin(sleavemsg(client,group,view)) = false .
eq issjoin(stransmsg(group)) = false .
eq issjoin(sconfmsg(group,view,transset)) = false .
eq issjoin(sselfleavemsg(client,group)) = false .
eq issjoin(sdisconnectmsg(client,group,view)) = false .

op issleave : SMessage ~> Bool .
eq issleave(sdatamsg(client,group,sdata,view)) = false .
eq issleave(sfreqmsg(client,group)) = false .
eq issleave(sjoinmsg(client,group,view)) = false .
eq issleave(sleavemsg(client,group,view)) = true .
eq issleave(stransmsg(group)) = false .
eq issleave(sconfmsg(group,view,transset)) = false .
eq issleave(sselfleavemsg(client,group)) = false .
eq issleave(sdisconnectmsg(client,group,view)) = false .

op issselfleave : SMessage ~> Bool .
eq issselfleave(sdatamsg(client,group,sdata,view)) = false .
eq issselfleave(sfreqmsg(client,group)) = false .
eq issselfleave(sjoinmsg(client,group,view)) = false .
eq issselfleave(sleavemsg(client,group,view)) = false .
eq issselfleave(stransmsg(group)) = false .
eq issselfleave(sconfmsg(group,view,transset)) = false .
eq issselfleave(sselfleavemsg(client,group)) = true .
eq issselfleave(sdisconnectmsg(client,group,view)) = false .

op isstrans : SMessage ~> Bool .
eq isstrans(sdatamsg(client,group,sdata,view)) = false .
eq isstrans(sfreqmsg(client,group)) = false .
eq isstrans(sjoinmsg(client,group,view)) = false .
eq isstrans(sleavemsg(client,group,view)) = false .
eq isstrans(stransmsg(group)) = true .
eq isstrans(sconfmsg(group,view,transset)) = false .
eq isstrans(sselfleavemsg(client,group)) = false .
eq isstrans(sdisconnectmsg(client,group,view)) = false .

op issconf : SMessage ~> Bool .
eq issconf(sdatamsg(client,group,sdata,view)) = false .
eq issconf(sfreqmsg(client,group)) = false .
eq issconf(sjoinmsg(client,group,view)) = false .
eq issconf(sleavemsg(client,group,view)) = false .
eq issconf(stransmsg(group)) = false .
eq issconf(sconfmsg(group,view,transset)) = true .
eq issconf(sselfleavemsg(client,group)) = false .
eq issconf(sdisconnectmsg(client,group,view)) = false .

op issdisconnect : SMessage ~> Bool .
eq issdisconnect(sdatamsg(client,group,sdata,view)) = false .
eq issdisconnect(sfreqmsg(client,group)) = false .
eq issdisconnect(sjoinmsg(client,group,view)) = false .
eq issdisconnect(sleavemsg(client,group,view)) = false .
eq issdisconnect(stransmsg(group)) = false .
eq issdisconnect(sconfmsg(group,view,transset)) = false .
eq issdisconnect(sselfleavemsg(client,group)) = false .
eq issdisconnect(sdisconnectmsg(client,group,view)) = true .

op view : SMessage ~> View .
eq view(sdatamsg(client,group,sdata,view)) = view .

op group : SMessage ~> Group .
eq group(sdatamsg(client,group,sdata,view)) = group .
eq group(sfreqmsg(client,group)) = group .
eq group(sjoinmsg(client,group,view)) = group .
eq group(sleavemsg(client,group,view)) = group .
eq group(stransmsg(group)) = group .
eq group(sconfmsg(group,view,transset)) = group .
eq group(sselfleavemsg(client,group)) = group .
eq group(sdisconnectmsg(client,group,view)) = group .

op update-transset : SMessage AgentSet ~> SMessage .
eq update-transset(sdatamsg(client,group,sdata,view),transset') = sdatamsg(client,group,sdata,view) .
eq update-transset(stokenmsg(token),transset') = stokenmsg(token) .
eq update-transset(sfreqmsg(client,group),transset') = sfreqmsg(client,group) .
eq update-transset(sjoinmsg(client,group,view),transset') = sjoinmsg(client,group,view) .
eq update-transset(sleavemsg(client,group,view),transset') = sleavemsg(client,group,view) .
eq update-transset(stransmsg(group),transset') = stransmsg(group) .
eq update-transset(sconfmsg(group,view,transset),transset') = sconfmsg(group,view,transset') .
eq update-transset(sselfleavemsg(client,group),transset') = sselfleavemsg(client,group) .
eq update-transset(sdisconnectmsg(client,group,view),transset') = sdisconnectmsg(client,group,view) .

---- two kinds of internal messages

op isidata : SMessage ~> Bool .
eq isidata(sdatamsg(key,sdata)) = true .
eq isidata(stokenmsg(token)) = false .

op isitoken : SMessage ~> Bool .
eq isitoken(sdatamsg(key,sdata)) = false .
eq isitoken(stokenmsg(token)) = true .

op token : SMessage ~> Token .
eq token(stokenmsg(token)) = token .

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

sort SMessageList .
op eSMessageList : -> SMessageList .
op sSMessageList : SMessage -> SMessageList .
op __ : SMessageList SMessageList -> SMessageList 
        [assoc id: eSMessageList] .

var smessagelist smessagelist' : SMessageList .
	

endfm