never { /* !(!(GFcs)) */
T0_init :    /* init */
	if
	:: (cs) -> goto accept_S1
	:: (1) -> goto T0_init
	fi;
accept_S1 :    /* 1 */
	if
	:: (cs) -> goto accept_S1
	:: (1) -> goto T0_init
	fi;
}