never { /* !(G((!cs) -> F(cs))) */
T0_init :    /* init */
	if
	:: (1) -> goto T0_init
	:: (!cs) -> goto accept_S2
	fi;
accept_S2 :    /* 1 */
	if
	:: (!cs) -> goto accept_S2
	fi;
}