Reading in file: "test4.maude"
==========================================

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST4
==========================================
search in TEST4 : start1 =>! state:State .

Solution 1 (state 3214)
states: 3215  rewrites: 152608 in 1210ms cpu (1240ms real) (126122 rewrites/second)
state:State --> network(sProcSet(proc("a")) sProcSet(proc("b")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
freshseq(0)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4))
localconf(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4))
delivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))) sMessageList(transmsg(transconf(
    sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)))) sMessageList(confmsg(regconf(sProcSet(proc("a"))
    sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))) sMessageList(transmsg(transconf(
    sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)))) sMessageList(confmsg(regconf(sProcSet(proc("a"))
    sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))) sMessageList(transmsg(
    transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)))) sMessageList(confmsg(regconf(sProcSet(
    proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))) sMessageList(transmsg(
    transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)))) sMessageList(confmsg(regconf(sProcSet(
    proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")))
reachable(proc("b"), sProcSet(proc("a")) sProcSet(proc("b")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eConstraintSet)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eEventList)
totalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eEventList)
totalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eEventList)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
localmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
localmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
knownmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2)), eNatSet)

No more solutions.
states: 3215  rewrites: 152608 in 1220ms cpu (1660ms real) (125088 rewrites/second)
==========================================
search in TEST4 : start2 =>! state:State .

Solution 1 (state 1302)
states: 1303  rewrites: 51604 in 410ms cpu (430ms real) (125863 rewrites/second)
state:State --> network(sProcSet(proc("a")) sProcSet(proc("b")))
freshconf(3)
operational(proc("a"))
operational(proc("b"))
freshseq(0)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2))
localconf(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2))
delivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")))
reachable(proc("b"), sProcSet(proc("a")) sProcSet(proc("b")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eConstraintSet)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eEventList)
totalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eEventList)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)

No more solutions.
states: 1303  rewrites: 51604 in 410ms cpu (810ms real) (125863 rewrites/second)
==========================================
search in TEST4 : start3 =>! state:State .

Solution 1 (state 1302)
states: 1303  rewrites: 51604 in 390ms cpu (440ms real) (132317 rewrites/second)
state:State --> network(sProcSet(proc("a")) sProcSet(proc("b")))
freshconf(3)
operational(proc("a"))
operational(proc("b"))
freshseq(0)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2))
localconf(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2))
delivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")),
    0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), sProcSet(proc("a")) sProcSet(proc("b")))))
reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")))
reachable(proc("b"), sProcSet(proc("a")) sProcSet(proc("b")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eConstraintSet)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eEventList)
totalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eEventList)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 2), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")), 0)), eNatSet)

No more solutions.
states: 1303  rewrites: 51604 in 390ms cpu (1050ms real) (132317 rewrites/second)
Done reading in file: "test4.maude"