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