------------------------- topologies.m ----------------------------- --- Date: Sat, 25 Aug 2001 00:44:24 -0700 --- From: Mark-Oliver Stehr --- requires plan-semantics.m mod TOPOLOGIES is including PLAN-SEMANTICS . var ex : Ex . var rb : Int . --- example topology 1 --- ni | --- | na --- loc("l1") ------ loc("l2") -------- loc("l3") --- \ / --- \ nb / --- \ / --- loc("l4") op example-topology-1 : -> Configuration . eq example-topology-1 = FreshKey(10) Node(loc("l1"), (addr("i1"),addr("a1")), ((addr("a1") >> addr("a2"))), ((addr("a2") via (addr("a1") >> addr("a2"))), (addr("b2") via (addr("a1") >> addr("a2"))), (addr("b3") via (addr("a1") >> addr("a2"))), (addr("b4") via (addr("a1") >> addr("a2"))))) Data(loc("l1"), empty-dil) Node(loc("l2"), (addr("a2"),addr("b2")), ((addr("a2") >> addr("a1")), (addr("b2") >> addr("b3")), (addr("b2") >> addr("b4"))), ((addr("a1") via (addr("a2") >> addr("a1"))), (addr("b3") via (addr("b2") >> addr("b3"))), (addr("b4") via (addr("b2") >> addr("b4"))))) Data(loc("l2"), empty-dil) Node(loc("l3"), (addr("b3")), ((addr("b3") >> addr("b2")), (addr("b3") >> addr("b4"))), ((addr("a1") via (addr("b3") >> addr("b2"))), (addr("a2") via (addr("b3") >> addr("b2"))), (addr("b2") via (addr("b3") >> addr("b2"))), (addr("b4") via (addr("b3") >> addr("b4"))))) Data(loc("l3"), empty-dil) Node(loc("l4"), (addr("b4")), ((addr("b4") >> addr("b2")), (addr("b4") >> addr("b3"))), ((addr("a1") via (addr("b4") >> addr("b2"))), (addr("a2") via (addr("b4") >> addr("b2"))), (addr("b2") via (addr("b4") >> addr("b2"))), (addr("b3") via (addr("b4") >> addr("b3"))))) Data(loc("l4"), empty-dil) . --- executing expression ex starting on end node l1 with resource rb op init-conf-1 : Ex Int -> Configuration . eq init-conf-1(ex, rb) = example-topology-1 Process(loc("l1"), addr("i1"), addr("i1"), 1, rb, RedState(?, ex) ) . --- example topology 2 --- with 6 nodes (l0,...,l5) and 5 networks --- l2 --- | / \ --- ni | nb / | --- | na / | nd --- l0 ------ l1 |------ l5 --- \ | --- nc \ | --- \ / --- l4 -------- l3 --- ne op example-topology-2 : -> Configuration . eq example-topology-2 = FreshKey(10) Node(loc("l0"), (addr("i0"),addr("a0")), ((addr("a0") >> addr("a1"))), ((addr("a1") via (addr("a0") >> addr("a1"))), (addr("b1") via (addr("a0") >> addr("a1"))), (addr("c1") via (addr("a0") >> addr("a1"))), (addr("b2") via (addr("a0") >> addr("a1"))), (addr("d2") via (addr("a0") >> addr("a1"))), (addr("c3") via (addr("a0") >> addr("a1"))), (addr("e3") via (addr("a0") >> addr("a1"))), (addr("d3") via (addr("a0") >> addr("a1"))), (addr("e4") via (addr("a0") >> addr("a1"))), (addr("d5") via (addr("a0") >> addr("a1"))))) Data(loc("l0"), empty-dil) Node(loc("l1"), (addr("a1"),addr("b1"),addr("c1")), ((addr("a1") >> addr("a0")), (addr("b1") >> addr("b2")), (addr("c1") >> addr("c3"))), ((addr("a0") via (addr("a1") >> addr("a0"))), (addr("b2") via (addr("b1") >> addr("b2"))), (addr("d2") via (addr("b1") >> addr("b2"))), (addr("c3") via (addr("c1") >> addr("c3"))), (addr("e3") via (addr("c1") >> addr("c3"))), (addr("d3") via (addr("c1") >> addr("c3"))), (addr("e4") via (addr("c1") >> addr("c3"))), (addr("d5") via (addr("b1") >> addr("b2"))))) Data(loc("l1"), empty-dil) Node(loc("l2"), (addr("b2"),addr("d2")), ((addr("b2") >> addr("b1")), (addr("d2") >> addr("d3")), (addr("d2") >> addr("d5"))), ((addr("a0") via (addr("b2") >> addr("b1"))), (addr("a1") via (addr("b2") >> addr("b1"))), (addr("b1") via (addr("b2") >> addr("b1"))), (addr("c1") via (addr("b2") >> addr("b1"))), (addr("c3") via (addr("d2") >> addr("d3"))), (addr("e3") via (addr("d2") >> addr("d3"))), (addr("d3") via (addr("d2") >> addr("d3"))), (addr("e4") via (addr("d2") >> addr("d3"))), (addr("d5") via (addr("d2") >> addr("d5"))))) Data(loc("l2"), empty-dil) Node(loc("l3"), (addr("c3"),addr("e3"),addr("d3")), ((addr("c3") >> addr("c1")), (addr("e3") >> addr("e4")), (addr("d3") >> addr("d2")), (addr("d3") >> addr("d5"))), ((addr("a0") via (addr("c3") >> addr("c1"))), (addr("a1") via (addr("c3") >> addr("c1"))), (addr("b1") via (addr("c3") >> addr("c1"))), (addr("c1") via (addr("c3") >> addr("c1"))), (addr("b2") via (addr("d3") >> addr("d2"))), (addr("d2") via (addr("d3") >> addr("d2"))), (addr("e4") via (addr("e3") >> addr("e4"))), (addr("d5") via (addr("d3") >> addr("d5"))))) Data(loc("l3"), empty-dil) Node(loc("l4"), (addr("e4")), ((addr("e4") >> addr("e3"))), ((addr("a0") via (addr("e4") >> addr("e3"))), (addr("a1") via (addr("e4") >> addr("e3"))), (addr("b1") via (addr("e4") >> addr("e3"))), (addr("c1") via (addr("e4") >> addr("e3"))), (addr("b2") via (addr("e4") >> addr("e3"))), (addr("d2") via (addr("e4") >> addr("e3"))), (addr("c3") via (addr("e4") >> addr("e3"))), (addr("e3") via (addr("e4") >> addr("e3"))), (addr("d3") via (addr("e4") >> addr("e3"))), (addr("d5") via (addr("e4") >> addr("e3"))))) Data(loc("l4"), empty-dil) Node(loc("l5"), (addr("d5")), ((addr("d5") >> addr("d2")), (addr("d5") >> addr("d3"))), ((addr("a0") via (addr("d5") >> addr("d2"))), (addr("a1") via (addr("d5") >> addr("d2"))), (addr("b1") via (addr("d5") >> addr("d2"))), (addr("c1") via (addr("d5") >> addr("d2"))), (addr("b2") via (addr("d5") >> addr("d2"))), (addr("d2") via (addr("d5") >> addr("d2"))), (addr("c3") via (addr("d5") >> addr("d3"))), (addr("e3") via (addr("d5") >> addr("d3"))), (addr("d3") via (addr("d5") >> addr("d3"))), (addr("e4") via (addr("d5") >> addr("d3"))))) Data(loc("l5"), empty-dil) . --- executing expression ex starting on end node l0 with resource rb op init-conf-2 : Ex Int -> Configuration . eq init-conf-2(ex, rb) = example-topology-2 Process(loc("l0"), addr("i0"), addr("i0"), 1, rb, RedState(?, ex) ) . endm