/*
 - ReqTestResultTest: Found Test for testgen_req6_Globally_BndInvariance_tt4    
Set Inputs:
 	I1 := true  
 Wait 1  
 
Set Inputs:
 	I1 := false  
 Wait 5  
 
Set Inputs:
 	I1 := false  
 Wait at most 5  for: 
	O1 == true  
 
Set Inputs:
 	I1 := false  
 Wait at most 5  for: 
	O1 == true  
 
Set Inputs:
 	I1 := false  
 Wait at most 5  for: 
	O1 == true  
 
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 
Internal S2 is bool 
Internal S3 is bool 
Internal S4 is bool 
Internal S5 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
req2: Globally, it is always the case that if "S1" holds, then "S2" holds for at least "5" time units
req3: Globally, it is always the case that if "S2" holds, then "S3" holds for at least "5" time units
req4: Globally, it is always the case that if "S3" holds, then "S4" holds for at least "5" time units
req5: Globally, it is always the case that if "S4" holds, then "S5" holds for at least "5" time units
req6: Globally, it is always the case that if "S5" holds, then "O1" holds for at least "5" time units