alt: to model alternative sequences, similar to a switch case.

  • Guards are used to select the one path to be executed. They are modelled in square brackets. We may use [else] to signify any other case if other guards fail.
  • Guards must be disjoint to avoid in deterministic behaviour.