 --> [ local path prefix ]/state_machine/redef/nested_choice.fpp:6:12
  |
6 |     choice C { if g enter S else enter S }
  |            ^ redefinition of symbol C
  |
 ::: [ local path prefix ]/state_machine/redef/nested_choice.fpp:5:5
  |
5 |     choice C { if g enter S else enter S }
  |     -------------------------------------- previous definition is here

 --> [ local path prefix ]/state_machine/redef/nested_choice.fpp:1:15
  |
1 | state machine M {
  |               ^ state machine must have initial transition

 --> [ local path prefix ]/state_machine/redef/nested_choice.fpp:3:9
  |
3 |   state S {
  |         ^ state with substates must have initial transition

