Transition rules are constructed as in 3.2, except that instead of the import constructor, we use the Choose (or Choice) Constructor:
