PLACE
    PROGRAM_END,
    PROGRAM_PANIC,
    PROGRAM_START,
    main_BB1,
    main_BB2,
    main_BB3,
    main_BB4,
    main_BB5,
    main_BB6;

MARKING
    PROGRAM_END : 0,
    PROGRAM_PANIC : 0,
    PROGRAM_START : 1,
    main_BB1 : 0,
    main_BB2 : 0,
    main_BB3 : 0,
    main_BB4 : 0,
    main_BB5 : 0,
    main_BB6 : 0;

TRANSITION call_0_RETURN
  CONSUME
    main_BB5 : 1;
  PRODUCE
    main_BB2 : 1;
TRANSITION main_GOTO_1
  CONSUME
    main_BB1 : 1;
  PRODUCE
    main_BB2 : 1;
TRANSITION main_RETURN
  CONSUME
    main_BB6 : 1;
  PRODUCE
    PROGRAM_END : 1;
TRANSITION main_SWITCH_INT_FROM_BB3_TO_BB4
  CONSUME
    main_BB3 : 1;
  PRODUCE
    main_BB4 : 1;
TRANSITION main_SWITCH_INT_FROM_BB3_TO_BB5
  CONSUME
    main_BB3 : 1;
  PRODUCE
    main_BB5 : 1;
TRANSITION main_SWITCH_INT_FROM_BB3_TO_BB6
  CONSUME
    main_BB3 : 1;
  PRODUCE
    main_BB6 : 1;
TRANSITION main_UNREACHABLE_4
  CONSUME
    main_BB4 : 1;
  PRODUCE
    PROGRAM_END : 1;
TRANSITION std_iter_IntoIterator_into_iter_0_CALL
  CONSUME
    PROGRAM_START : 1;
  PRODUCE
    main_BB1 : 1;
TRANSITION std_iter_Iterator_next_0_CALL
  CONSUME
    main_BB2 : 1;
  PRODUCE
    main_BB3 : 1;