/* 
Set Inputs:
 	I1 := 3  I2 := false  
 Wait 5  
 
Set Inputs:
 	I1 := 3  I2 := true  
 Wait at most 5  for: 
	O1 == true  
 
Set Inputs:
 	I1 := 3  I2 := false  
 Wait at most 5  for: 
	O1 == true
*/


Input I1 is int 
Output O1 is bool 
Internal S1 is bool 
Input I2 is bool 

req1: Globally, it is always the case that if "I1 == 3" holds for at least "5" time units, then "S1" holds afterwards
req2: Globally, it is always the case that if "I1 != 3" holds for at least "5" time units, then "!S1" holds afterwards
req3: Globally, it is always the case that if "S1 && I2" holds, then "O1" holds for at least "5" time units