/*
	 * Formula As Typed: ( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->     ([]  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->     ([]  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork)))
	 * (formalizing violations of the original)
	 */

never {    /* !(( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->     ([]  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork))) */
T0_init:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_init
	:: (! ((calldoWork)) && ! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && (acceptActivePoolGet) && (workCountGRzero)) -> goto accept_S10
	fi;
accept_S10:
	if
	:: (! ((calldoWork)) && ! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_S10
	fi;
T0_S10:
	if
	:: (! ((calldoWork)) && ! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto accept_S10
	fi;
accept_all:
	skip
}