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’’’
}