INFO {
  TITLE:       "Parameterized Input Monitor"
  DESCRIPTION: "Checks whether all input signals are eventually true"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 6;
  }
}

MAIN {

  INPUTS {
    r[n]; // request signals
  } 

  OUTPUTS {
    g; // grant signal
  }

  GUARANTEES {
    &&[0 <= i < n] G F r[i] <-> G F g;
  }
  
}

//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 374
//#.