models/step2: replaced Choice automata with select-statements
models/step2: Channel iteration loop rewritten with reset_b() and forall-expression