never {    /* ![]((c_start && <>c_exit) -> ((c_gimme -> (!c_exit U c_gimme_ok)) && (c_free -> (!c_exit U c_free_ok))) U c_exit) */
T0_init:
	if
	:: (! ((c_exit)) && (c_start)) -> goto T0_S45
	:: (! ((c_exit)) && ! ((c_gimme_ok)) && (c_gimme) && (c_start)) -> goto T0_S90
	:: (! ((c_exit)) && ! ((c_free_ok)) && (c_free) && (c_start)) -> goto T0_S97
	:: (1) -> goto T0_init
	fi;
accept_S57:
	if
	:: (! ((c_gimme_ok))) -> goto accept_S57
	:: (! ((c_gimme_ok)) && (c_exit)) -> goto accept_all
	fi;
accept_S74:
	if
	:: (! ((c_free_ok))) -> goto accept_S74
	:: (! ((c_free_ok)) && (c_exit)) -> goto accept_all
	fi;
accept_S89:
	if
	:: ((c_exit)) -> goto accept_all
	:: (1) -> goto T0_S89
	fi;
T0_S45:
	if
	:: (! ((c_exit))) -> goto T0_S45
	:: (! ((c_exit)) && ! ((c_gimme_ok)) && (c_gimme)) -> goto T0_S90
	:: (! ((c_exit)) && ! ((c_free_ok)) && (c_free)) -> goto T0_S97
	fi;
T0_S90:
	if
	:: (! ((c_gimme_ok)) && (c_exit)) -> goto accept_S57
	:: (! ((c_gimme_ok)) && (c_exit)) -> goto accept_all
	:: (! ((c_gimme_ok))) -> goto T0_S90
	:: (! ((c_gimme_ok)) && (c_exit)) -> goto accept_S89
	fi;
T0_S97:
	if
	:: (! ((c_free_ok)) && (c_exit)) -> goto accept_S74
	:: (! ((c_free_ok)) && (c_exit)) -> goto accept_all
	:: (! ((c_free_ok))) -> goto T0_S97
	:: (! ((c_free_ok)) && (c_exit)) -> goto accept_S89
	fi;
T0_S89:
	if
	:: ((c_exit)) -> goto accept_all
	:: (1) -> goto T0_S89
	fi;
accept_all:
	skip
}