--------------------------  find-examples.m  ---------------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- Finding Routes: Two Examples from the HOOTS Paper

--- The first example floods the networks with independent processes to search
--- for the destination node.  When a process reaches the destination node,
--- it reports the found path to initiator using  a goback function.

--- The second examples uses the resident data services to keep backpointers,
--- `dropping breadcrumbs' in the nodes for the goback phase. As a consequence
--- the processes are not independent any more and usually only one route is 
--- reported back, although it is possible that more than one report is made.

--- First Example from HOOTS Paper

--- requires plan-syntax.m

mod FIND-EXAMPLES is

including PLAN-LITERALS .

ops find-prog-1 find-prog-2 : Addr -> Ex .  

var find-dest : Addr .

eq find-prog-1(find-dest) = 
   (LetRec ["goback" = Lam [ ("remaining","route") : 
            ((TList (TPair TAddr TAddr)),(TList (TPair TAddr TAddr))) ]
     (If (Equal ("remaining"{0}, Nil)) 
        Then (Print "route"{0})
        Else (Let ["nexthop" = (Snd (Hd "remaining"{0}))]
               (OnNeighbor ((Chunk("goback"{0},((Tl "remaining"{0}),"route"{0}))), 
                           "nexthop"{0}, (GetRB empty-exl), (GetDevToHost "nexthop"{0})))))]
   (LetRec ["find" = Lam [ ("dest","route","visited") : 
         (TAddr,(TList (TPair TAddr TAddr)),(TList TAddr)) ]
     (Let ["myaddrs" = 
       (ThisHost empty-exl)]
     (Let ["neighbors" =
       (GetNeighbors empty-exl)]
     (Let ["addifnew" = Lam [ ("neigh","neighl") : 
             ((TPair TAddr TAddr), (TList (TPair TAddr TAddr))) ]
       (If (Not (Member ((Fst "neigh"{0}),"visited"{0})))
        Then (Cons ("neigh"{0},"neighl"{0})) 
        Else "neighl"{0})]
     (Let ["newneighbors" = 
       (Foldr ("addifnew"{0},"neighbors"{0},Nil))]
     (Let ["childrb" =
       (If (Equal ((Length "newneighbors"{0}),(Int 0)))
        Then (GetRB empty-exl)
        Else (Div ((GetRB empty-exl),(Length "newneighbors"{0}))))]
     (Let ["sendchild" = Lam [ ("neigh","dum") : ((TPair TAddr TAddr),TUnit) ]
       (Let ["route" = (Cons ((Pair ((GetSrcDev empty-exl), (Snd "neigh"{0}))),"route"{0}))]
         (OnNeighbor ((Chunk("find"{0},("dest"{0},"route"{0},(Append ("myaddrs"{0},"visited"{0}))))), 
                     (Fst "neigh"{0}), "childrb"{0}, (Snd "neigh"{0}))))]
     (If (ThisHostIs "dest"{0}) 
      Then ("goback"{0} ("route"{0},(Reverse "route"{0})))
      Else (Foldr ("sendchild"{0},"newneighbors"{0},Dummy)))))))))]
   ("find"{0} ((Addr find-dest),Nil,Nil)))) .

--- Second Example from HOOTS Paper (corrected version)

eq find-prog-2(find-dest) = 
   (LetRec ["goback" = Lam [ ("k","route") : (TKey, (TList TAddr)) ]
     (If (ThisHostIs (GetSource empty-exl)) 
        Then (Print "route"{0})
        Else (Let ["nexthop" = (Get ((String ""),"k"{0}))]
             (Let ["d" = (GetDevToHost "nexthop"{0})]
             (Let ["newroute" = (Cons ("d"{0},"route"{0}))]
               (OnNeighbor ((Chunk ("goback"{0}, ("k"{0},"newroute"{0}))), 
                            "nexthop"{0}, (GetRB empty-exl), "d"{0}))))))]
   (LetRec ["find" = Lam [ ("dest","previous","k") :  (TAddr,TAddr,TKey) ]
     (If (Exists ((String ""),"k"{0}))
      Then Dummy
      Else ( 
        (Put ((String ""), "k"{0}, "previous"{0}, (Int 200)));
        (If (ThisHostIs "dest"{0})
         Then ("goback"{0} ("k"{0},Nil)) 
         Else (
           (Let ["neighbors" = (GetNeighbors empty-exl)]
           (Let ["srcdev" =  (GetSrcDev empty-exl)]
           (Let ["childrb" =
             (If (Equal ((Length "neighbors"{0}),(Int 0)))
              Then (GetRB empty-exl)
              Else (Div ((GetRB empty-exl),(Length "neighbors"{0}))))]
           (Let ["sendchild" = Lam [ ("n","u") : ((TPair TAddr TAddr),TUnit) ]
                    (OnNeighbor ((Chunk ("find"{0},
                                         ("dest"{0},(Snd "n"{0}),"k"{0}))), 
                                 (Fst "n"{0}), "childrb"{0}, (Snd "n"{0})))]

              (Foldr ("sendchild"{0},"neighbors"{0},Dummy)) ))))) )))]
     ("find"{0} ((Addr find-dest), 
                 (GetSource empty-exl),
                 (GenerateKey empty-exl))) )) .

endm 

mod FIND-RUNS is

including FIND-EXAMPLES .
including TOPOLOGIES .

endm