-------------------------   find-runs.m  -----------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- modified by clt 01Aug30

--- in p.m
--- in topologies.m
--- in find-examples.m


----------------------------------------------------
--- Finding Routes: Two Examples from the HOOTS Paper

--- find-1 in topology-1
rew init-conf-1(find-prog-1(addr("b3")), 100) .

***(
rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, find-prog-1(addr("b3")))) .

rewrites: 245513 in 3280ms cpu (3290ms real) (74851 rewrites/second)
result Configuration: 
    FreshKey(10) 
    Data(loc("l1"), empty-dil) 
    Data(loc("l2"), empty-dil) 
    Data(loc("l3"), empty-dil) 
    Data(loc("l4"), empty-dil) 
    ...
    Process(loc("l1"), addr("i1"), addr("a1"), 1, 44, 
      RedState(?, Print (Cons (Pair (Addr addr("i1"),Addr addr("a1")),
                         Cons (Pair (Addr addr("a2"),Addr addr("b2")),
                         Cons (Pair (Addr addr("b4"),Addr addr("b4")),Nil))))))
    Process(loc("l1"), addr("i1"), addr("a1"), 1, 46, 
      RedState(?, Print (Cons (Pair (Addr addr("i1"),Addr addr("a1")),
                         Cons (Pair (Addr addr("a2"),Addr addr("b2")),Nil))))) 
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i1"), addr("a2"), 1, 1, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i1"), addr("b2"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l2"), addr("i1"), addr("b2"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i1"), addr("b3"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i1"), addr("b3"), 1, 0,
      RedState(?, Dummy)) 
    Process(loc("l4"), addr("i1"), addr("b4"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l4"), addr("i1"), addr("b4"), 1, 0, 
      RedState(?, Dummy))
)

--- find-2 in topology-1
rew init-conf-1(find-prog-2(addr("b3")), 100) .


***(
rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, find-prog-2(addr("b3")))) .

rewrites: 169699 in 2350ms cpu (2360ms real) (72212 rewrites/second)
result Configuration: 
    FreshKey(11) 
    Data(loc("l1"), DataItem("", 10, Addr addr("i1"), 200)) 
    Data(loc("l2"), DataItem("", 10, Addr addr("a1"), 200)) 
    Data(loc("l3"), DataItem("", 10, Addr addr("b2"), 200)) 
    Data(loc("l4"), DataItem("", 10, Addr addr("b2"), 200)) 
    ...
    Process(loc("l1"), addr("i1"), addr("a1"), 1, 30, 
      RedState(?, Print (Cons (Addr addr("a2"),
                         Cons (Addr addr("b3"),Nil))))) 
    Process(loc("l1"), addr("i1"), addr("a1"), 1, 32,
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l2"), addr("i1"), addr("a2"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i1"), addr("b2"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l2"), addr("i1"), addr("b2"), 1, 15,
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i1"), addr("b3"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l3"), addr("i1"), addr("b3"), 1, 15, 
      RedState(?, Dummy)) 
    Process(loc("l4"), addr("i1"), addr("b4"), 1, 0, 
     RedState(?, Dummy))
)



--- find-1 in topology-2
rew init-conf-2(find-prog-1(addr("e4")), 100) .


***(

rew example-topology-2
    Process(loc("l0"), addr("i0"), addr("i0"), 1, 100, 
      RedState(?, find-prog-1(addr("e4")))) .

rewrites: 774851 in 11640ms cpu (11690ms real) (66567 rewrites/second)
result Configuration: 
    FreshKey(10) 
    Data(loc("l0"), empty-dil) Data(loc("l1"), empty-dil) 
    Data(loc("l2"), empty-dil) Data(loc("l3"), empty-dil)
    Data(loc("l4"), empty-dil) Data(loc("l5"), empty-dil) 
    ...
    Process(loc("l0"), addr("i0"), addr("a0"), 1, 6,
      RedState(?, Print (Cons (Pair (Addr addr("i0"),Addr addr("a0")),
                         Cons (Pair (Addr addr("a1"),Addr addr("b1")),
                         Cons (Pair (Addr addr("b2"),Addr addr("d2")),
                         Cons (Pair (Addr addr("d3"),Addr addr("e3")),Nil))))))) 
    Process(loc("l0"), addr("i0"), addr("a0"), 1, 12, 
      RedState(?, Print (Cons (Pair (Addr addr("i0"),Addr addr("a0")),
                         Cons (Pair (Addr addr("a1"),Addr addr("c1")),
                         Cons (Pair (Addr addr("c3"),Addr addr("e3")),Nil)))))) 
    Process(loc("l0"), addr("i0"), addr("a0"), 1, 16, 
      RedState(?, Print (Cons (Pair (Addr addr("i0"),Addr addr("a0")),
                         Cons (Pair (Addr addr("a1"),Addr addr("b1")),
                         Cons (Pair (Addr addr("b2"),Addr addr("d2")),
                         Cons (Pair (Addr addr("d5"),Addr addr("d5")),
                         Cons (Pair (Addr addr("d3"),Addr addr("e3")),Nil)))))))) 
    Process(loc("l0"), addr("i0"), addr("i0"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i0"), addr("a1"), 1, 1, 
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i0"), addr("b1"), 1, 0, 
      RedState(?,Dummy)) 
    Process(loc("l1"), addr("i0"), addr("b1"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i0"), addr("c1"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("b2"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 14, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("c3"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l3"), addr("i0"), addr("d3"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("d3"), 1, 1, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("e3"), 1, 0,
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("e3"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l3"), addr("i0"), addr("e3"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l4"), addr("i0"), addr("e4"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l4"), addr("i0"), addr("e4"), 1, 0,
      RedState(?, Dummy)) 
    Process(loc("l4"), addr("i0"), addr("e4"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 0,
      RedState(?, Dummy)) 
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 10, 
      RedState(?, Dummy))
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 14, 
      RedState(?, Dummy))
)

--- find-2 in topology-2
rew init-conf-2(find-prog-2(addr("e4")), 100) .

***(
rew example-topology-2
    Process(loc("l0"), addr("i0"), addr("i0"), 1, 100, 
      RedState(?, find-prog-2(addr("e4")))) .

rewrites: 328040 in 4740ms cpu (4790ms real) (69206 rewrites/second)
result Configuration: 
    FreshKey(11) 
    Data(loc("l0"), DataItem("", 10, Addr addr("i0"), 200)) 
    Data(loc("l1"), DataItem("", 10, Addr addr("a0"), 200)) 
    Data(loc("l2"), DataItem("", 10, Addr addr("b1"), 200)) 
    Data(loc("l3"), DataItem("", 10, Addr addr("c1"), 200)) 
    Data(loc("l4"), DataItem("", 10, Addr addr("e3"), 200)) 
    Data(loc("l5"), DataItem("", 10, Addr addr("d3"), 200)) 
    ...
    Process(loc("l0"), addr("i0"), addr("a0"), 1, 4, 
      RedState(?,Print (Cons (Addr addr("a1"),
                        Cons (Addr addr("c3"),
                        Cons (Addr addr("e4"),Nil)))))) 
    Process(loc("l0"), addr("i0"), addr("a0"), 1, 32, 
      RedState(?, Dummy)) 
    Process(loc("l0"), addr("i0"), addr("i0"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i0"), addr("a1"), 1, 0, 
      RedState(?,Dummy)) 
    Process(loc("l1"), addr("i0"), addr("b1"), 1, 9, 
      RedState(?, Dummy))
    Process(loc("l1"), addr("i0"), addr("c1"), 1, 0, 
      RedState(?, Dummy)) 
    Process(loc("l1"), addr("i0"), addr("c1"), 1, 7, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("b2"), 1, 2, 
      RedState(?, Dummy))
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 2, 
      RedState(?, Dummy)) 
    Process(loc("l2"), addr("i0"), addr("d2"), 1, 7, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("c3"), 1, 0,
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("d3"), 1, 2, 
      RedState(?, Dummy))
    Process(loc("l3"), addr("i0"), addr("d3"), 1, 9, 
      RedState(?, Dummy)) 
    Process(loc("l3"), addr("i0"), addr("e3"), 1, 0, 
      RedState(?, Dummy))
    Process(loc("l4"), addr("i0"), addr("e4"), 1, 0,
      RedState(?, Dummy))  
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 1, 
      RedState(?, Dummy))
    Process(loc("l5"), addr("i0"), addr("d5"), 1, 9, 
      RedState(?, Dummy))
)



