import models/RAM_PetriNets_Runtime_Runtime as RAM_PN_R RAM_PN_R s { Composite schedule { {Contains} Failure failure {} {Contains} Success success {} {Contains} Atomic mark { LHS { Pre_PetriNets_Runtime/Transition { label = "1" } } NAC { Pre_PetriNets_Runtime/Transition mark_nac_t { label = "1" } Pre_PetriNets_Runtime/Place mark_nac_p{ label = "10" } Pre_PetriNets_Runtime/P2T (mark_nac_p, mark_nac_t){ label = "11" } constraint = $ include "primitives.alh" include "modelling.alh" Boolean function constraint(host_model : Element, mapping : Element): Integer tokens Integer weight tokens = read_attribute(host_model, mapping["10"], "tokens") weight = read_attribute(host_model, mapping["11"], "weight") return (tokens < weight)! $ } RHS { Post_PetriNets_Runtime/Transition { label = "1" action = $ include "primitives.alh" include "modelling.alh" Void function action(host_model : Element, name : String, mapping : Element): unset_attribute(host_model, name, "executing") instantiate_attribute(host_model, name, "executing", True) return! $ } } } {Contains} ForAll consume { LHS { Pre_PetriNets_Runtime/Transition lhs_consume_t{ label = "0" constraint = $ include "primitives.alh" include "modelling.alh" Boolean function constraint(host_model : Element, name : String): // Check if this node is executing currently return value_eq(read_attribute(host_model, name, "executing"), True)! $ } Pre_PetriNets_Runtime/Place lhs_consume_p{ label = "1" } Pre_PetriNets_Runtime/P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){ label = "2" } } RHS { Post_PetriNets_Runtime/Transition rhs_consume_t { label = "0" } Post_PetriNets_Runtime/Place rhs_consume_p { label = "1" action = $ include "primitives.alh" include "modelling.alh" Void function action(host_model : Element, name : String, mapping : Element): Integer tokens Integer weight tokens = read_attribute(host_model, name, "tokens") weight = read_attribute(host_model, mapping["2"], "weight") unset_attribute(host_model, name, "tokens") instantiate_attribute(host_model, name, "tokens", tokens - weight) log("Consume for " + cast_v2s(read_attribute(host_model, name, "name"))) log("Previous: " + cast_v2s(tokens)) log("Now: " + cast_v2s(tokens - weight)) return! $ } Post_PetriNets_Runtime/P2T (rhs_consume_p, rhs_consume_t){ label = "2" } } } {Contains} ForAll produce { LHS { Pre_PetriNets_Runtime/Transition lhs_produce_t{ label = "0" constraint = $ include "primitives.alh" include "modelling.alh" Boolean function constraint(host_model : Element, name : String): // Check if this node is executing currently return value_eq(read_attribute(host_model, name, "executing"), True)! $ } Pre_PetriNets_Runtime/Place lhs_produce_p{ label = "1" } Pre_PetriNets_Runtime/T2P (lhs_produce_t, lhs_produce_p){ label = "2" } } RHS { Post_PetriNets_Runtime/Transition rhs_produce_t{ label = "0" } Post_PetriNets_Runtime/Place rhs_produce_p{ label = "1" action = $ include "primitives.alh" include "modelling.alh" Void function action(host_model : Element, name : String, mapping : Element): Integer tokens Integer weight tokens = read_attribute(host_model, name, "tokens") weight = read_attribute(host_model, mapping["2"], "weight") unset_attribute(host_model, name, "tokens") instantiate_attribute(host_model, name, "tokens", tokens + weight) log("Produce for " + cast_v2s(read_attribute(host_model, name, "name"))) log("Previous: " + cast_v2s(tokens)) log("Now: " + cast_v2s(tokens + weight)) return! $ } Post_PetriNets_Runtime/T2P (rhs_produce_t, rhs_produce_p){ label = "2" } } } {Contains} Atomic unmark_transition { LHS { Pre_PetriNets_Runtime/Transition { label = "0" constraint = $ include "primitives.alh" include "modelling.alh" Boolean function constraint(host_model : Element, name : String): // Check if this node is executing currently return value_eq(read_attribute(host_model, name, "executing"), True)! $ } } RHS { Post_PetriNets_Runtime/Transition { label = "0" action = $ include "primitives.alh" include "modelling.alh" Void function action(host_model : Element, name : String, mapping : Element): unset_attribute(host_model, name, "executing") instantiate_attribute(host_model, name, "executing", False) return! $ } } } } OnSuccess (mark, consume) {} OnFailure (mark, failure) {} OnSuccess (consume, produce) {} OnFailure (consume, produce) {} OnSuccess (produce, unmark_transition) {} OnFailure (produce, unmark_transition) {} OnSuccess (unmark_transition, success) {} OnFailure (unmark_transition, failure) {} Initial (schedule, mark) {} } export s to models/pn_simulate