in sectrace.maude

mod EXT-TEST-SEQ-C1-C2 is

protecting SECTRACE .

***(

   Configuration:
   
			   a
			 C1 -----|
				 |b
	       a     a	 b     a | c	 a   b	   a   b    a
	     C2 ----- SG1 ----- SG2 ----- SG3 ----- SG4 ---- S

   C1 << SG2,SG3,S
   C2 << SG1,SG3,S
   SG1 << SG2
   SG3 << SG4,S
   SG4 << S

   Expected result:
      
		  C1 ----- SG2 ----- SG3 ----- SG4 ----- S
		     =====               =====     =====
		     ===============

	     C2 ----- SG1 ----- SG2 ----- SG3 ----- SG4 ----- S
		=====     =====               =====     =====
		=========================

)

op network : -> State .

eq network = 
    shost(node("C1"))
    shost(node("C2"))
    shost(node("SG1"))
    shost(node("SG2"))
    shost(node("SG3"))
    shost(node("SG4"))
    shost(node("S"))

    sgw(node("SG1"))
    sgw(node("SG2"))
    sgw(node("SG3"))
    sgw(node("SG4"))

    sectraced(node("C1"))
    sectraced(node("C2"))
    sectraced(node("SG1"))
    sectraced(node("SG2"))
    sectraced(node("SG3"))
    sectraced(node("SG4"))
    sectraced(node("S"))

    subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b")))
    subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a")))
    subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a")))
    subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a")))
    subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a")))
    subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa")))

    interfaces(node("C1"),sAddrSet(addr("C1a")))
    interfaces(node("C2"),sAddrSet(addr("C2a")))
    interfaces(node("SG1"),sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
    interfaces(node("SG2"),sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")) sAddrSet(addr("SG2c")))
    interfaces(node("SG3"),sAddrSet(addr("SG3a")) sAddrSet(addr("SG3b")))
    interfaces(node("SG4"),sAddrSet(addr("SG4a")) sAddrSet(addr("SG4b")))
    interfaces(node("S"),sAddrSet(addr("Sa")))

    routetab(node("C1"),
       sRouteList(route(addr("C1a"), addr("C1a"), addr("C1a")))
       sRouteList(route(addr("C2a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG1a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG1b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2c"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG3a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG3b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG4a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG4b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("Sa"), addr("C1a"), addr("SG2b"))))

    routetab(node("C2"),
       sRouteList(route(addr("C1a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("C2a"), addr("C2a"), addr("C2a")))
       sRouteList(route(addr("SG1a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG1b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2c"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG3a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG3b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG4a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG4b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("Sa"), addr("C2a"), addr("SG1a"))))

    routetab(node("SG1"),
       sRouteList(route(addr("C1a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("C2a"), addr("SG1a"), addr("C2a")))
       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("SG2c"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG3a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG3b"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG4a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG4b"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("Sa"), addr("SG1b"), addr("SG2a"))))

    routetab(node("SG2"),
       sRouteList(route(addr("C1a"), addr("SG2b"), addr("C1a")))
       sRouteList(route(addr("C2a"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG1a"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG1b"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG2a"), addr("SG2a"), addr("SG2a")))
       sRouteList(route(addr("SG2b"), addr("SG2b"), addr("SG2b")))
       sRouteList(route(addr("SG2c"), addr("SG2c"), addr("SG2c")))
       sRouteList(route(addr("SG3a"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG3b"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG4a"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG4b"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("Sa"), addr("SG2c"), addr("SG3a"))))

    routetab(node("SG3"),
       sRouteList(route(addr("C1a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("C2a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG1a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG1b"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2b"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2c"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG3a"), addr("SG3a"), addr("SG3a")))
       sRouteList(route(addr("SG3b"), addr("SG3b"), addr("SG3b")))
       sRouteList(route(addr("SG4a"), addr("SG3b"), addr("SG4a")))
       sRouteList(route(addr("SG4b"), addr("SG3b"), addr("SG4a")))
       sRouteList(route(addr("Sa"), addr("SG3b"), addr("SG4a"))))

    routetab(node("SG4"),
       sRouteList(route(addr("C1a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("C2a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG1a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG1b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2c"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG3a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG3b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG4a"), addr("SG4a"), addr("SG4a")))
       sRouteList(route(addr("SG4b"), addr("SG4b"), addr("SG4b")))
       sRouteList(route(addr("Sa"), addr("SG4b"), addr("Sa"))))

    routetab(node("S"),
       sRouteList(route(addr("C1a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("C2a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG1a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG1b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2c"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG3a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG3b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG4a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG4b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))))

    rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1")))
    rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2")))
    rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CASG1")) sAddrSet(addr("CAC2")))
    rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CASG2")) sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")))
    rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CASG3")) sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")))
    rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG4")) sAddrSet(addr("CASG3")))
    rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAS")) sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4")))

    sadb(node("C1"),eSASet)
    sadb(node("C2"),eSASet)
    sadb(node("SG1"),eSASet)
    sadb(node("SG2"),eSASet)
    sadb(node("SG3"),eSASet)
    sadb(node("SG4"),eSASet)
    sadb(node("S"),eSASet)

    spdb(node("C1"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("C2"),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("SG3"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG4"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("S"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList))) .


op start : -> State .
op next : -> State .
op terminated : -> State .

rl start =>
   sectrace-start(node("C1"), addr("C1a"), addr("Sa")) .

rl sectrace-terminated(node("C1"), addr("C1a"), addr("Sa")) 
   => next .

rl next =>
   sectrace-start(node("C2"), addr("C2a"), addr("Sa")) .

rl sectrace-terminated(node("C2"), addr("C2a"), addr("Sa")) 
   => terminated .

endm

*** rew (network start) .

search (network start) =>! state:State .