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

GLOBAL {
  PARAMETERS {
    n = 3;       
  }

  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) =
      &&[

... [truncated 1.0 kB]

 && g[i])
    );    
  }

  INVARIANTS {
    // ensure mutual exclusion on the output bus
    mutual_exclusion(g);      
      
    /* Making the benchmark unrealizable: ask for two grants at the same time, 
     * eventually.
     */
    &&[0 <= i <n] ( &&[i < j < n] (r[i] && X r[j] -> 
      F (g[i] && g[j])) );
  }

  GUARANTEES {
    // every request is eventually granted
    &&[0 <= i < n]
      G (r[i] -> F g[i]);
  }
  
}
//#!SYNTCOMP
//STATUS : unrealizable
//REF_SIZE : 5
//#.