PLACE
    MUTEX_0,
    MUTEX_1,
    PROGRAM_END,
    PROGRAM_PANIC,
    PROGRAM_START,
    first_deadlock_0_BB1,
    first_deadlock_0_BB2,
    first_deadlock_0_BB3,
    first_deadlock_0_BB4,
    first_deadlock_0_BB5,
    first_deadlock_0_BB6,
    first_deadlock_0_BB7,
    main_BB1,
    main_BB2,
    second_deadlock_0_BB1,
    second_deadlock_0_BB2,
    second_deadlock_0_BB3,
    second_deadlock_0_BB4,
    second_deadlock_0_BB5,
    second_deadlock_0_BB6,
    second_deadlock_0_BB7;

MARKING
    MUTEX_0 : 1,
    MUTEX_1 : 1,
    PROGRAM_END : 0,
    PROGRAM_PANIC : 0,
    PROGRAM_START : 1,
    first_deadlock_0_BB1 : 0,
    first_deadlock_0_BB2 : 0,
    first_deadlock_0_BB3 : 0,
    first_deadlock_0_BB4 : 0,
    first_deadlock_0_BB5 : 0,
    first_deadlock_0_BB6 : 0,
    first_deadlock_0_BB7 : 0,
    main_BB1 : 0,
    main_BB2 : 0,
    second_deadlock_0_BB1 : 0,
    second_deadlock_0_BB2 : 0,
    second_deadlock_0_BB3 : 0,
    second_deadlock_0_BB4 : 0,
    second_deadlock_0_BB5 : 0,
    second_deadlock_0_BB6 : 0,
    second_deadlock_0_BB7 : 0;

TRANSITION first_deadlock_0_DROP_3
  CONSUME
    first_deadlock_0_BB3 : 1;
  PRODUCE
    MUTEX_0 : 1,
    first_deadlock_0_BB4 : 1;
TRANSITION first_deadlock_0_DROP_4
  CONSUME
    first_deadlock_0_BB4 : 1;
  PRODUCE
    MUTEX_0 : 1,
    first_deadlock_0_BB5 : 1;
TRANSITION first_deadlock_0_DROP_6
  CONSUME
    first_deadlock_0_BB6 : 1;
  PRODUCE
    MUTEX_0 : 1,
    first_deadlock_0_BB7 : 1;
TRANSITION first_deadlock_0_DROP_UNWIND_3
  CONSUME
    first_deadlock_0_BB3 : 1;
  PRODUCE
    MUTEX_0 : 1,
    first_deadlock_0_BB6 : 1;
TRANSITION first_deadlock_0_RETURN
  CONSUME
    first_deadlock_0_BB5 : 1;
  PRODUCE
    main_BB1 : 1;
TRANSITION first_deadlock_0_UNWIND_7
  CONSUME
    first_deadlock_0_BB7 : 1;
  PRODUCE
    PROGRAM_PANIC : 1;
TRANSITION main_RETURN
  CONSUME
    main_BB2 : 1;
  PRODUCE
    PROGRAM_END : 1;
TRANSITION second_deadlock_0_DROP_3
  CONSUME
    second_deadlock_0_BB3 : 1;
  PRODUCE
    MUTEX_1 : 1,
    second_deadlock_0_BB4 : 1;
TRANSITION second_deadlock_0_DROP_4
  CONSUME
    second_deadlock_0_BB4 : 1;
  PRODUCE
    MUTEX_1 : 1,
    second_deadlock_0_BB5 : 1;
TRANSITION second_deadlock_0_DROP_6
  CONSUME
    second_deadlock_0_BB6 : 1;
  PRODUCE
    MUTEX_1 : 1,
    second_deadlock_0_BB7 : 1;
TRANSITION second_deadlock_0_DROP_UNWIND_3
  CONSUME
    second_deadlock_0_BB3 : 1;
  PRODUCE
    MUTEX_1 : 1,
    second_deadlock_0_BB6 : 1;
TRANSITION second_deadlock_0_RETURN
  CONSUME
    second_deadlock_0_BB5 : 1;
  PRODUCE
    main_BB2 : 1;
TRANSITION second_deadlock_0_UNWIND_7
  CONSUME
    second_deadlock_0_BB7 : 1;
  PRODUCE
    PROGRAM_PANIC : 1;
TRANSITION std_sync_Mutex_T_lock_0_CALL
  CONSUME
    MUTEX_0 : 1,
    first_deadlock_0_BB1 : 1;
  PRODUCE
    first_deadlock_0_BB2 : 1;
TRANSITION std_sync_Mutex_T_lock_1_CALL
  CONSUME
    MUTEX_0 : 1,
    first_deadlock_0_BB2 : 1;
  PRODUCE
    first_deadlock_0_BB3 : 1;
TRANSITION std_sync_Mutex_T_lock_2_CALL
  CONSUME
    MUTEX_1 : 1,
    second_deadlock_0_BB1 : 1;
  PRODUCE
    second_deadlock_0_BB2 : 1;
TRANSITION std_sync_Mutex_T_lock_3_CALL
  CONSUME
    MUTEX_1 : 1,
    second_deadlock_0_BB2 : 1;
  PRODUCE
    second_deadlock_0_BB3 : 1;
TRANSITION std_sync_Mutex_T_new_0_CALL
  CONSUME
    PROGRAM_START : 1;
  PRODUCE
    first_deadlock_0_BB1 : 1;
TRANSITION std_sync_Mutex_T_new_1_CALL
  CONSUME
    main_BB1 : 1;
  PRODUCE
    second_deadlock_0_BB1 : 1;