INFO {
  TITLE:       "Prioritized Arbiter"
  DESCRIPTION: "Parameterized Arbiter with a unique master process which has priority angainst others"
  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 a

... [truncated 781 Bytes]

ss
  }

  ASSUMPTIONS {
    // The master cannot starve the others
    G F !r_m;
  }

  INVARIANTS {
    // ensure mutual exclusion between the standard grants
    mutual_exclusion(g);

    // ensure mutual exclusion against the master
    &&[0 <= i < n]
      !(g_m && g[i]);
  }

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

    // a master request is granted before any other request
    G (r_m -> X (&&[0 <= i < n] !g[i] U g_m));
  }
  
}