INFO {
  TITLE:       "Round Robin Arbiter"
  DESCRIPTION: "Parameterized Arbiter, where requst signals have to remain HIGH until they are granted"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 4;
  }

  DEFINITIONS {
    // ensures mutual exclusion on an n-ary bus
    mutual_exclusion(bus) =
     mone(bus,0,(SIZEOF bus) - 1);

    // ensures that none of the signals
    // bus[i] - bus[j] is HIGH
    none(bus,i,j) =
      &&[i <= t <= j]
        !bus[t];

    // ensures that 

... [truncated 731 Bytes]

 is granted
      ( r[i] && !g[i] -> X  r[i]) &&
      // every request signal swaps to LOW when granted     
      (!r[i] &&  g[i] -> X !r[i]) &&
      // fairness: the arbiter cannot be starved by a process
      F !(r[i] && g[i])
    );    
  }

  INVARIANTS {
    // ensure mutual exclusion on the output bus
    mutual_exclusion(g);
  }

  GUARANTEES {
    // every request is eventually granted
    &&[0 <= i < n]
      G (r[i] -> F g[i]);
  }
  
}

//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 28
//#.