// #TestSpec: rt-inconsistent:; vacuous:; inconsistent:; results:-1
// 2020-01-13: Spec checked by Elli
Input var3 is bool
Input var4 is bool
CONST MAX_TIME is 50.0
Input var1 is bool
CONST time_every is 10.0



req1: Before "var1" It is always the case that "var4" holds at least every "time_every" time units
req2: Before "var1" It is always the case that If "var3" holds, then "!var4" holds after at most "MAX_TIME" time units