Plan To Validate

Time         Happening



2.6: 		 
 (prepareobs1) - start 



4.6: 		 
 Invariant for  (prepareobs1) 

4.6: 		 
 (prepareobs1) - end 



4.7: 		 
 (observe1) - start 



6.7: 		 
 Invariant for  (observe1) 

6.7: 		 
 (observe1) - end 



6.8: 		 
 (prepareobs2) - start 



7.8: 		 
 Invariant for  (prepareobs2) 

7.8: 		 
 (prepareobs2) - end 



7.9: 		 
 (observe2) - start 



9.9: 		 
 Invariant for  (observe2) 

9.9: 		 
 (observe2) - end 



10: 		 
 (Timed Initial Literal Action 1)