Reading in file: "gtest5.maude"
==========================================
 
Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================

Reading in file: "gtest.maude"
==========================================
fmod GTEST
Advisory: redefining module GTEST.
Done reading in file: "gtest.maude"
==========================================
mod TEST-SPREAD
Advisory: redefining module TEST-SPREAD.
==========================================
rewrite in TEST-SPREAD : init .
rewrites: 720 in 20ms cpu (20ms real) (36000 rewrites/second)
result State: network(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
freshconf(1)
operational(agent("a"))
operational(agent("b"))
operational(agent("c"))
freshseq(1)
gclients(sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
CONTROLLER(eController)
a(5)
b(3)
c(3)
localconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
localconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
localconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
delivered(agent("a"), eMessageList)
delivered(agent("b"), eMessageList)
delivered(agent("c"), eMessageList)
alldelivered(agent("a"), sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gdatamsg(agent("a"), privategroup(agent("c")), gdata("TEST")))))
alldelivered(agent("b"), sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gdatamsg(agent("a"), privategroup(agent("c")), gdata("TEST")))))
alldelivered(agent("c"), sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gdatamsg(agent("a"), privategroup(agent("c")), gdata("TEST")))))
reachable(agent("a"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
reachable(agent("b"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
reachable(agent("c"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
sent(agent("a"), eBroadcastSet)
sent(agent("b"), eBroadcastSet)
sent(agent("c"), eBroadcastSet)
received(agent("a"), eMessageSet)
received(agent("b"), eMessageSet)
received(agent("c"), eMessageSet)
acked(agent("a"), eMessageSet)
acked(agent("b"), eMessageSet)
acked(agent("c"), eMessageSet)
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), eConstraintSet)
totalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sEventList(event(agent("a"), 0)) sEventList(event(agent("a"), 0))
    sEventList(event(agent("a"), 0)))
gjoined(agent("a"), eGroupList)
gjoined(agent("b"), eGroupList)
gjoined(agent("c"), eGroupList)
gview(agent("a"), eViewSet)
gview(agent("b"), eViewSet)
gview(agent("c"), eViewSet)
glocalconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
glocalconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
glocalconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
gdelivered(agent("a"), eGMessageList)
gdelivered(agent("b"), eGMessageList)
gdelivered(agent("c"), sGMessageList(gdatamsg(agent("a"), privategroup(agent("c")), gdata("TEST"))))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0))
localmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), eNatSet)
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), eNatSet)
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0))
gstate(goperational(agent("a"))
goperational(agent("b"))
goperational(agent("c")), eState, eState, eState)
Done reading in file: "gtest5.maude"