atl "not-abuse-freeness-P3-opt"
	E F  (
		T_Abort_Send_P1 & 
		<<P1, P2, Timer>> G (~P3_S1) & 
		<<P1, P2, Timer>> G (P3_stop => P1_S3 )
	     );


--atl "not-abuse-freeness-P3-opt"
--	E F  (
--		T_Abort_Send_P1 & 
--		<<P1, P2, Timer>> G (~P3_S1) &
--		<<P1, P2, Timer>> G (P3_stop => P1_S3 )
--	     );
-- passed