digraph petrinet {
    MUTEX_0 [shape="circle" xlabel="MUTEX_0" label="•"];
    MUTEX_1 [shape="circle" xlabel="MUTEX_1" label="•"];
    PROGRAM_END [shape="circle" xlabel="PROGRAM_END" label=""];
    PROGRAM_PANIC [shape="circle" xlabel="PROGRAM_PANIC" label=""];
    PROGRAM_START [shape="circle" xlabel="PROGRAM_START" label="•"];
    first_deadlock_0_BB1 [shape="circle" xlabel="first_deadlock_0_BB1" label=""];
    first_deadlock_0_BB2 [shape="circle" xlabel="first_deadlock_0_BB2" label=""];
    first_deadlock_0_BB3 [shape="circle" xlabel="first_deadlock_0_BB3" label=""];
    first_deadlock_0_BB4 [shape="circle" xlabel="first_deadlock_0_BB4" label=""];
    first_deadlock_0_BB5 [shape="circle" xlabel="first_deadlock_0_BB5" label=""];
    first_deadlock_0_BB6 [shape="circle" xlabel="first_deadlock_0_BB6" label=""];
    first_deadlock_0_BB7 [shape="circle" xlabel="first_deadlock_0_BB7" label=""];
    main_BB1 [shape="circle" xlabel="main_BB1" label=""];
    main_BB2 [shape="circle" xlabel="main_BB2" label=""];
    second_deadlock_0_BB1 [shape="circle" xlabel="second_deadlock_0_BB1" label=""];
    second_deadlock_0_BB2 [shape="circle" xlabel="second_deadlock_0_BB2" label=""];
    second_deadlock_0_BB3 [shape="circle" xlabel="second_deadlock_0_BB3" label=""];
    second_deadlock_0_BB4 [shape="circle" xlabel="second_deadlock_0_BB4" label=""];
    second_deadlock_0_BB5 [shape="circle" xlabel="second_deadlock_0_BB5" label=""];
    second_deadlock_0_BB6 [shape="circle" xlabel="second_deadlock_0_BB6" label=""];
    second_deadlock_0_BB7 [shape="circle" xlabel="second_deadlock_0_BB7" label=""];
    first_deadlock_0_DROP_3 [shape="box" xlabel="" label="first_deadlock_0_DROP_3"];
    first_deadlock_0_DROP_4 [shape="box" xlabel="" label="first_deadlock_0_DROP_4"];
    first_deadlock_0_DROP_6 [shape="box" xlabel="" label="first_deadlock_0_DROP_6"];
    first_deadlock_0_DROP_UNWIND_3 [shape="box" xlabel="" label="first_deadlock_0_DROP_UNWIND_3"];
    first_deadlock_0_RETURN [shape="box" xlabel="" label="first_deadlock_0_RETURN"];
    first_deadlock_0_UNWIND_7 [shape="box" xlabel="" label="first_deadlock_0_UNWIND_7"];
    main_RETURN [shape="box" xlabel="" label="main_RETURN"];
    second_deadlock_0_DROP_3 [shape="box" xlabel="" label="second_deadlock_0_DROP_3"];
    second_deadlock_0_DROP_4 [shape="box" xlabel="" label="second_deadlock_0_DROP_4"];
    second_deadlock_0_DROP_6 [shape="box" xlabel="" label="second_deadlock_0_DROP_6"];
    second_deadlock_0_DROP_UNWIND_3 [shape="box" xlabel="" label="second_deadlock_0_DROP_UNWIND_3"];
    second_deadlock_0_RETURN [shape="box" xlabel="" label="second_deadlock_0_RETURN"];
    second_deadlock_0_UNWIND_7 [shape="box" xlabel="" label="second_deadlock_0_UNWIND_7"];
    std_sync_Mutex_T_lock_0_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_lock_0_CALL"];
    std_sync_Mutex_T_lock_1_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_lock_1_CALL"];
    std_sync_Mutex_T_lock_2_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_lock_2_CALL"];
    std_sync_Mutex_T_lock_3_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_lock_3_CALL"];
    std_sync_Mutex_T_new_0_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_new_0_CALL"];
    std_sync_Mutex_T_new_1_CALL [shape="box" xlabel="" label="std_sync_Mutex_T_new_1_CALL"];
    MUTEX_0 -> std_sync_Mutex_T_lock_0_CALL;
    MUTEX_0 -> std_sync_Mutex_T_lock_1_CALL;
    MUTEX_1 -> std_sync_Mutex_T_lock_2_CALL;
    MUTEX_1 -> std_sync_Mutex_T_lock_3_CALL;
    PROGRAM_START -> std_sync_Mutex_T_new_0_CALL;
    first_deadlock_0_BB1 -> std_sync_Mutex_T_lock_0_CALL;
    first_deadlock_0_BB2 -> std_sync_Mutex_T_lock_1_CALL;
    first_deadlock_0_BB3 -> first_deadlock_0_DROP_3;
    first_deadlock_0_BB3 -> first_deadlock_0_DROP_UNWIND_3;
    first_deadlock_0_BB4 -> first_deadlock_0_DROP_4;
    first_deadlock_0_BB5 -> first_deadlock_0_RETURN;
    first_deadlock_0_BB6 -> first_deadlock_0_DROP_6;
    first_deadlock_0_BB7 -> first_deadlock_0_UNWIND_7;
    main_BB1 -> std_sync_Mutex_T_new_1_CALL;
    main_BB2 -> main_RETURN;
    second_deadlock_0_BB1 -> std_sync_Mutex_T_lock_2_CALL;
    second_deadlock_0_BB2 -> std_sync_Mutex_T_lock_3_CALL;
    second_deadlock_0_BB3 -> second_deadlock_0_DROP_3;
    second_deadlock_0_BB3 -> second_deadlock_0_DROP_UNWIND_3;
    second_deadlock_0_BB4 -> second_deadlock_0_DROP_4;
    second_deadlock_0_BB5 -> second_deadlock_0_RETURN;
    second_deadlock_0_BB6 -> second_deadlock_0_DROP_6;
    second_deadlock_0_BB7 -> second_deadlock_0_UNWIND_7;
    first_deadlock_0_DROP_3 -> MUTEX_0;
    first_deadlock_0_DROP_3 -> first_deadlock_0_BB4;
    first_deadlock_0_DROP_4 -> MUTEX_0;
    first_deadlock_0_DROP_4 -> first_deadlock_0_BB5;
    first_deadlock_0_DROP_6 -> MUTEX_0;
    first_deadlock_0_DROP_6 -> first_deadlock_0_BB7;
    first_deadlock_0_DROP_UNWIND_3 -> MUTEX_0;
    first_deadlock_0_DROP_UNWIND_3 -> first_deadlock_0_BB6;
    first_deadlock_0_RETURN -> main_BB1;
    first_deadlock_0_UNWIND_7 -> PROGRAM_PANIC;
    main_RETURN -> PROGRAM_END;
    second_deadlock_0_DROP_3 -> MUTEX_1;
    second_deadlock_0_DROP_3 -> second_deadlock_0_BB4;
    second_deadlock_0_DROP_4 -> MUTEX_1;
    second_deadlock_0_DROP_4 -> second_deadlock_0_BB5;
    second_deadlock_0_DROP_6 -> MUTEX_1;
    second_deadlock_0_DROP_6 -> second_deadlock_0_BB7;
    second_deadlock_0_DROP_UNWIND_3 -> MUTEX_1;
    second_deadlock_0_DROP_UNWIND_3 -> second_deadlock_0_BB6;
    second_deadlock_0_RETURN -> main_BB2;
    second_deadlock_0_UNWIND_7 -> PROGRAM_PANIC;
    std_sync_Mutex_T_lock_0_CALL -> first_deadlock_0_BB2;
    std_sync_Mutex_T_lock_1_CALL -> first_deadlock_0_BB3;
    std_sync_Mutex_T_lock_2_CALL -> second_deadlock_0_BB2;
    std_sync_Mutex_T_lock_3_CALL -> second_deadlock_0_BB3;
    std_sync_Mutex_T_new_0_CALL -> first_deadlock_0_BB1;
    std_sync_Mutex_T_new_1_CALL -> second_deadlock_0_BB1;
}