PLACE
    CONDVAR_0_NOTIFY,
    CONDVAR_0_WAIT_ENABLED,
    MUTEX_0,
    PROGRAM_END,
    PROGRAM_PANIC,
    PROGRAM_START,
    main_BB1,
    main_BB10,
    main_BB2,
    main_BB3,
    main_BB4,
    main_BB5,
    main_BB6,
    main_BB7,
    main_BB8,
    main_BB9;

MARKING
    CONDVAR_0_NOTIFY : 0,
    CONDVAR_0_WAIT_ENABLED : 1,
    MUTEX_0 : 1,
    PROGRAM_END : 0,
    PROGRAM_PANIC : 0,
    PROGRAM_START : 1,
    main_BB1 : 0,
    main_BB10 : 0,
    main_BB2 : 0,
    main_BB3 : 0,
    main_BB4 : 0,
    main_BB5 : 0,
    main_BB6 : 0,
    main_BB7 : 0,
    main_BB8 : 0,
    main_BB9 : 0;

TRANSITION CONDVAR_0_LOST_SIGNAL
  CONSUME
    CONDVAR_0_NOTIFY : 1,
    CONDVAR_0_WAIT_ENABLED : 1;
  PRODUCE
    CONDVAR_0_WAIT_ENABLED : 1;
TRANSITION CONDVAR_0_NOTIFY_RECEIVED
  CONSUME
    CONDVAR_0_NOTIFY : 1,
    MUTEX_0 : 1;
  PRODUCE
    CONDVAR_0_WAIT_ENABLED : 1,
    main_BB6 : 1;
TRANSITION CONDVAR_0_WAIT_START
  CONSUME
    CONDVAR_0_WAIT_ENABLED : 1,
    main_BB5 : 1;
  PRODUCE
    MUTEX_0 : 1;
TRANSITION main_DROP_6
  CONSUME
    main_BB6 : 1;
  PRODUCE
    MUTEX_0 : 1,
    main_BB7 : 1;
TRANSITION main_DROP_9
  CONSUME
    main_BB9 : 1;
  PRODUCE
    MUTEX_0 : 1,
    main_BB8 : 1;
TRANSITION main_DROP_UNWIND_6
  CONSUME
    main_BB6 : 1;
  PRODUCE
    MUTEX_0 : 1,
    main_BB10 : 1;
TRANSITION main_RETURN
  CONSUME
    main_BB7 : 1;
  PRODUCE
    PROGRAM_END : 1;
TRANSITION main_SWITCH_INT_FROM_BB10_TO_BB8
  CONSUME
    main_BB10 : 1;
  PRODUCE
    main_BB8 : 1;
TRANSITION main_SWITCH_INT_FROM_BB10_TO_BB9
  CONSUME
    main_BB10 : 1;
  PRODUCE
    main_BB9 : 1;
TRANSITION main_UNWIND_8
  CONSUME
    main_BB8 : 1;
  PRODUCE
    PROGRAM_PANIC : 1;
TRANSITION std_result_Result_unwrap_0_CALL
  CONSUME
    main_BB3 : 1;
  PRODUCE
    main_BB4 : 1;
TRANSITION std_sync_Condvar_new_0_CALL
  CONSUME
    main_BB1 : 1;
  PRODUCE
    main_BB2 : 1;
TRANSITION std_sync_Condvar_notify_one_0_CALL
  CONSUME
    main_BB4 : 1;
  PRODUCE
    CONDVAR_0_NOTIFY : 1,
    main_BB5 : 1;
TRANSITION std_sync_Mutex_T_lock_0_CALL
  CONSUME
    MUTEX_0 : 1,
    main_BB2 : 1;
  PRODUCE
    main_BB3 : 1;
TRANSITION std_sync_Mutex_T_new_0_CALL
  CONSUME
    PROGRAM_START : 1;
  PRODUCE
    main_BB1 : 1;