INFO {
  TITLE:       "Simple Arbiter"
  DESCRIPTION: "Parameterized Arbiter, where each request has to be eventually granted"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 8;
  }

  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 at most one of the si

... [truncated 372 Bytes]

half is HIGH
      (mone(bus, i, m(i,j)) && none(bus, m(i,j) + 1, j));

    // returns the position between i and j
    m(i,j) = (i + j) / 2;
  } 
}

MAIN {

  INPUTS {
    r[n]; // request signals
  } 

  OUTPUTS {
    g[n]; // grant signals
  }


  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 : 19
//#.