never {    /* ![](c_start -> (!c_exit U c_alloc)) */
T0_init:
	if
	:: (! ((c_alloc)) && (c_start)) -> goto accept_S4
	:: (! ((c_alloc)) && (c_exit) && (c_start)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_S4:
	if
	:: (! ((c_alloc))) -> goto accept_S4
	:: (! ((c_alloc)) && (c_exit)) -> goto accept_all
	fi;
accept_all:
	skip
}