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