/* THE ARROW DISTRIBUTED DIRECTORY PROTOCOL (Demmer, Herlihy 98) */

defproc 
    TerminalOwner(find,move,obj) =
        find?(mymove,myfind).Owner(find,move,myfind,mymove,obj)
and
    Owner(find,move,link,queue,obj) = 
        select {
            find?(mymove,myfind).(Owner(find,move,myfind,queue,obj) |
                                  link!(mymove,find));
            tau.(Idle(find,move,link) | queue!(obj))
        }
and
    Idle(find,move,link) =
        select {
            find?(mymove,myfind).(Idle(find,move,myfind) |
                                  link!(mymove,find));
            tau.(TerminalWaiter(find,move) | link!(move,find))
        }
and
    TerminalWaiter(find,move) =
        select {
            find?(mymove,myfind).Waiter(find,move,myfind,mymove);
            move?(obj).TerminalOwner(find,move,obj)
        }
and
    Waiter(find,move,link,queue) =
        select {
            find?(mymove,myfind).(Waiter(find,move,myfind,queue) |
                                  link!(mymove,find));
            move?(obj).Owner(find,move,link,queue,obj)
        };

/* --- */

defproc
    Dir =  
        new find1,move1,find2,move2,find3,move3,obj in 
            ( obj!() |
                TerminalOwner(find1,move1,obj) |
                Idle(find2,move2,find1) |
                Idle(find3,move3,find2));

/* PROPERTIES */

defprop deadlockfree = always(<>true);

check Dir |= deadlockfree;

/* ---------- */

defprop object(s) = < s! > 0;

defprop node(f) = 1 and (fresh a. fresh b. < f?(a,b) > true);

defprop owns(i,obj) = (node(i) and @obj);

defprop exclusive(i,obj) = (owns(i,obj) | not @obj);

defprop live = hidden obj.
    inside (object(obj) |
            forall i. ((node(i) | true) => eventually exclusive(i,obj)));

check Dir |= always(live);