// #TestSpec: rt-inconsistent:req1+req2; vacuous:; inconsistent:; results:-1
// 2020-01-13: Spec checked by Elli
Input var3 is bool
Input var4 is bool
CONST time_at_least is 30.0



req1: Globally It is always the case that once "var4" becomes satisfied, it holds for at least "time_at_least" time units
req2: Globally It is always the case that If "var3" holds for at least "time_at_least" time units, then "!var4" holds afterwards