// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //

macro NumProc = 10;


module Arbiter([NumProc]bool ?req, event bool ?rdy, [NumProc]bool ack, tok, prs, bool arb, bool static) {
    loop{
        for (i=0 .. (NumProc-1)) do || {
            next(tok[i]) = true;
            await (arb);
            next(tok[i]) = false;
        }
    }
    ||
    for (i=0 .. (NumProc-1)) do ||
        loop {
            await (req[i] & tok[i]);
            next(prs[i]) = true;
            await (not req[i]);
            next(prs[i]) = false;
        }
    ||
    loop {
        arb = true;
        await(exists(i=0 .. (NumProc-1)) req[i]);
        arb = false;
        static = not exists(i=0 .. (NumProc-1)) (prs[i] & tok[i]);
        
        if (not(static))
            for (i = (NumProc-1) .. 0) do || {
                if (req[i] & tok[i] & prs[i] & forall (j=i..(NumProc-1)) ack[j]==false)
                ack[i] = true;
            }
        else {
            for (i=NumProc .. 0) do || {
                if (req[i] & forall(j=i..(NumProc)) (req[j]==false))
                ack[i] = true;
            }
        }
        wfa : await (rdy);
    }
}