modelverse/models/PetriNets/models/critical_section.mvc

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 {
    name = "release_section_1"
}
Transition release_section_2 {
    name = "release_section_2"
}
Transition acquire_section_1 {
    name = "acquire_section_1"
}
Transition acquire_section_2 {
    name = "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
}