atl "not-abuse-freeness-P3-csfw15"
	E F  (	
		T_Abort_Send_P1 & 
		<<P1, P2>> G (~P3_S1)

	     );
-- passed

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