a choice point branch transition is an outgoing transition from a choice point and is traversed if its conditions is evaluated to true
Transition tr3: cp cp0 -> state1 { cond ’‘‘0<=counter && counter<3’’’}