import models/PetriNets_Design as PetriNets

PetriNets pn {
    Place critical_section_1 {
        tokens = 0
        name = "critical_section_1"
    }
    Place critical_section_2 {
        tokens = 0
        name = "critical_section_2"
    }
    Place lock_available {
        tokens = 1
        name = "lock_available"
    }

    Transition release_section_1 {}
    Transition release_section_2 {}
    Transition acquire_section_1 {}
    Transition acquire_section_2 {}

    P2T (critical_section_1, release_section_1) {
        weight = 1
    }

    P2T (critical_section_2, release_section_2) {
        weight = 1
    }

    P2T (lock_available, acquire_section_1) {
        weight = 1
    }

    P2T (lock_available, acquire_section_2) {
        weight = 1
    }

    T2P (release_section_1, lock_available) {
        weight = 1
    }

    T2P (release_section_2, lock_available) {
        weight = 1
    }

    T2P (acquire_section_1, critical_section_1) {
        weight = 1
    }

    T2P (acquire_section_2, critical_section_2) {
        weight = 1
    }
}

export pn to models/pn