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

GLOBAL {
  PARAMETERS {
    n = 2;
    u = 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]

... [truncated 907 Bytes]

t bus
    mutual_exclusion(g);   
      
    /* Making the benchmark unrealizable: ask for two grants at the same time, 
     * after u steps.
     */
    &&[0 <= i <n] ( &&[i < j < n] (r[i] && X r[j] -> 
      X[u] (g[i] && g[j])) ); 
  }

  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])
    );
  }
  
}

//#!SYNTCOMP
//STATUS : unrealizable
//REF_SIZE : 0
//#.