in full-maude.maude

(omod BROADCAST is protecting STRING . 
    subsort String < Oid . 
    ops m1 m2 m3 m4 m5 : -> Msg . 
    msg broadcast : Msg Oid -> Msg . 
    
    sort OidSet . subsort Oid < OidSet . 
    op none : -> OidSet [ctor] . 
    op _;_ : OidSet OidSet -> OidSet 
	[ctor assoc comm id: none] .



    op msg_from_to_ : Msg Oid Oid -> Msg [ctor] .
    op multimsg_from_to_ : Msg Oid OidSet -> Msg [ctor] .
    var M : Msg . vars SENDER ARECEIVER : Oid .
    var OTHER-RECEIVERS : OidSet .
    eq multimsg M from SENDER to none = none .
    eq multimsg M from SENDER to ARECEIVER ; OTHER-RECEIVERS =
	  (msg M from SENDER to ARECEIVER)
	  (multimsg M from SENDER to OTHER-RECEIVERS) .



    class Node | neighbors : OidSet, msgRead : Configuration .

    vars O O' : Oid .
    var OS : OidSet .
    var M : Msg .
    rl [startBroadcast] :
	broadcast(M, O)
	< O : Node | neighbors : OS, msgRead : none > =>
	< O : Node | msgRead : M > 
	multimsg M from O to OS .
    
    rl [readAndForward] :
	(msg M from O to O')
	< O' : Node | neighbors : O ; OS, msgRead : none > =>
	< O' : Node | msgRead : M > multimsg M from O' to OS .
 
    rl [readSeenMsg] :
	(msg M from O to O')
	< O' : Node | neighbors : OS, msgRead : M > => 
	< O' : Node | > .


    op initState : -> Configuration .
    eq initState =
	broadcast(m4, "b")
	< "a" : Node | neighbors : "b" ; "e", msgRead : none > 
	< "b" : Node | neighbors : "a" ; "d", msgRead : none >
	< "c" : Node | neighbors : "d", msgRead : none >
	< "d" : Node | neighbors : "b" ; "c" ; "e", msgRead : none >
	< "e" : Node | neighbors : "a" ; "d", msgRead : none > .
endom)

(rew initState .)
(search initState =>! C:Configuration .)