nametype Index = {1,2}

channel non_crit, enter_crit, exit_crit: Index 

RUN(X) = []x:X @ x -> RUN(X)

EN = {| enter_crit |}

SPEC1 =  enter_crit.1 -> RUN(EN) [EN || Events] RUN(Events)