/*
	 * Formula As Typed: []  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute))))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute)))))
	 * (formalizing violations of the original)
	 */

never {    /* !([]  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute))))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute) && (returnExecute)) -> goto accept_all
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute)) -> goto T0_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute) && (returnExecute)) -> goto accept_S5
	fi;
accept_S5:
	if
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_all
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S5
	fi;
accept_S21:
	if
	:: (1) -> goto T0_S21
	:: ((returnExecute)) -> goto accept_all
	fi;
accept_S3:
	if
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S21
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_all
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S5
	fi;
T0_S5:
	if
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_all
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S5
	fi;
T0_S21:
	if
	:: (1) -> goto T0_S21
	:: ((returnExecute)) -> goto accept_all
	fi;
T0_S3:
	if
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S21
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_all
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S3
	:: (! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S5
	fi;
accept_all:
	skip
}