/* Found Test for TEST_req6_Globally_BndInvariance_tt4
Set Inputs:
 	I1 := true  
 Wait 1  
 
Set Inputs:
 	I1 := false  
 Wait at most 5  for: 
	O1 == true  
 
Set Inputs:
 	I1 := false  
 Wait at most 5  for: 
	O1 == true   
*/

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


req1: Globally, it is always the case that if "I1" holds, then "S1" holds for at least "5" time units
req6: Globally, it is always the case that if "S1" holds, then "O1" holds for at least "5" time units