INFO {
  TITLE:       "Full Arbiter"
  DESCRIPTION: "Parameterized Arbiter, where no spurious grants are allowed"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 6;
  }

  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 signals
    // 

... [truncated 531 Bytes]

 r[n]; // request signals
  } 

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

  INVARIANTS {
    // no spurious grants
    &&[0 <= i < n] (
      (g[i] && G !r[i] -> F !g[i]) &&
      (g[i] && X (!r[i] && !g[i]) -> X (r[i] R !g[i]))
    );

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

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