INFO {
  TITLE:       "Parameterized Load Balancer, unrealizable variant 1"
  DESCRIPTION: "Parameterized Load Balancer (generalized version of the Acacia+ benchmark)"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

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

}

  INVARIANTS {
    X mutual_exclusion(grant);    
    &&[0 <= i < n] (X grant[i] -> request[i]);
    &&[0 < i < n] (request[0] -> grant[i]);
    !idle -> X &&[0 <= i < n] !grant[i];    
      
    /* Making the benchmark unrealizable: ask for two grants at the same time, 
     * after u steps.
     */
    &&[0 <= i <n] ( &&[i < j < n] (request[i] && X request[j] -> 
      X[u] (grant[i] && grant[j])) ); 
  }

  GUARANTEES {
    &&[0 <= i < n] ! F G (request[i] && X !grant[i]);
  }

}