in sectrace.maude

***(
			a     a   b	a   b	  a
		       C ----- SG1 ----- SG2 ----- S
)

search
    shost(node("C"))
    shost(node("SG1"))
    shost(node("SG2"))
    shost(node("S"))

    sgw(node("SG1"))
    sgw(node("SG2"))

    sectraced(node("C"))
    sectraced(node("SG1"))
    sectraced(node("SG2"))
    sectraced(node("S"))

    subnet(sAddrSet(addr("Ca")) sAddrSet(addr("SG1a"))) 
    subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) 
    subnet(sAddrSet(addr("SG2b")) sAddrSet(addr("Sa"))) 

    interfaces(node("C"),sAddrSet(addr("Ca")))
    interfaces(node("S"),sAddrSet(addr("Sa")))
    interfaces(node("SG1"),sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
    interfaces(node("SG2"),sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")))

    routetab(node("C"),
       sRouteList(route(addr("Ca"), addr("Ca"),addr("Ca")))
       sRouteList(route(addr("SG1a"), addr("Ca"),addr("SG1a")))
       sRouteList(route(addr("SG1b"), addr("Ca"),addr("SG1a")))
       sRouteList(route(addr("SG2a"), addr("Ca"),addr("SG1a")))
       sRouteList(route(addr("SG2b"), addr("Ca"),addr("SG1a")))
       sRouteList(route(addr("Sa"), addr("Ca"),addr("SG1a"))))

    routetab(node("SG1"),
       sRouteList(route(addr("SG1a"), addr("SG1a"),addr("SG1a")))
       sRouteList(route(addr("SG1b"), addr("SG1b"),addr("SG1b")))
       sRouteList(route(addr("SG2a"), addr("SG1b"),addr("SG2a")))
       sRouteList(route(addr("SG2b"), addr("SG1b"),addr("SG2a")))
       sRouteList(route(addr("Ca"), addr("SG1a"),addr("Ca")))
       sRouteList(route(addr("Sa"), addr("SG1b"),addr("SG2a"))))

    routetab(node("SG2"),
       sRouteList(route(addr("SG2a"), addr("SG2a"),addr("SG2a")))
       sRouteList(route(addr("SG2b"), addr("SG2b"),addr("SG2b")))
       sRouteList(route(addr("SG1a"), addr("SG2a"),addr("SG1b")))
       sRouteList(route(addr("SG1b"), addr("SG2a"),addr("SG1b")))
       sRouteList(route(addr("Ca"), addr("SG2a"),addr("SG1b")))
       sRouteList(route(addr("Sa"), addr("SG2b"),addr("Sa"))))

    routetab(node("S"),
       sRouteList(route(addr("Sa"), addr("Sa"),addr("Sa")))
       sRouteList(route(addr("Ca"), addr("Sa"),addr("SG2b")))
       sRouteList(route(addr("SG1b"), addr("Sa"),addr("SG2b")))
       sRouteList(route(addr("SG1a"), addr("Sa"),addr("SG2b")))
       sRouteList(route(addr("SG2a"), addr("Sa"),addr("SG2b")))
       sRouteList(route(addr("SG2b"), addr("Sa"),addr("SG2b"))))

    rootinfo(node("C"),addr("CA1"),sAddrSet(addr("CA1")))
    rootinfo(node("SG1"),addr("CA2"),sAddrSet(addr("CA2")) sAddrSet(addr("CA1")))
    rootinfo(node("SG2"),addr("CA1"),sAddrSet(addr("CA1")))
    rootinfo(node("S"),addr("CA1"),sAddrSet(addr("CA1")))

    sadb(node("C"),eSASet)
    sadb(node("SG1"),eSASet)
    sadb(node("SG2"),eSASet)
    sadb(node("S"),eSASet)

    spdb(node("C"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG1"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG2"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("S"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))

    sectrace-start(node("C"), addr("Ca"), addr("Sa"))

    =>! state:State .