|
|
@@ -5,22 +5,720 @@ A B {
|
|
|
{Contains} Success success {}
|
|
|
{Contains} Failure failure {}
|
|
|
{Contains} Atomic init_ports {
|
|
|
+ LHS {}
|
|
|
+ RHS {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_00 {
|
|
|
+ label = "00"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "down"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_10 {
|
|
|
+ label = "10"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "down"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_10, post_ports_00) {
|
|
|
+ label = "20"
|
|
|
+ }
|
|
|
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_01 {
|
|
|
+ label = "01"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "neutral"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_11 {
|
|
|
+ label = "11"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "neutral"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_11, post_ports_01) {
|
|
|
+ label = "21"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_02 {
|
|
|
+ label = "02"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "down"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_12 {
|
|
|
+ label = "12"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "down"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_12, post_ports_02) {
|
|
|
+ label = "22"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_03 {
|
|
|
+ label = "03"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "interrupt"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_13 {
|
|
|
+ label = "13"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "interrupt"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_13, post_ports_03) {
|
|
|
+ label = "23"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_04 {
|
|
|
+ label = "04"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "objDetected"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_14 {
|
|
|
+ label = "14"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "objDetected"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_14, post_ports_04) {
|
|
|
+ label = "24"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_05 {
|
|
|
+ label = "05"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "no_objDetected"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 1!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_15 {
|
|
|
+ label = "15"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "no_objDetected"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_15, post_ports_05) {
|
|
|
+ label = "25"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_06 {
|
|
|
+ label = "06"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "objPresent"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_16 {
|
|
|
+ label = "16"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "objPresent"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_16, post_ports_06) {
|
|
|
+ label = "26"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_07 {
|
|
|
+ label = "07"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "no_objPresent"!
|
|
|
+ $
|
|
|
+ value_tokens = #
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ return 1!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_17 {
|
|
|
+ label = "17"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "no_objPresent"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_17, post_ports_07) {
|
|
|
+ label = "27"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
{Contains} ForAll create_states {
|
|
|
-
|
|
|
+ LHS {
|
|
|
+ Pre_Plant_PW/State {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Plant_PW/State post_cs_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_cs1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_tokens = $
|
|
|
+ Integer function value(model : Element, name : String, mapping : Element):
|
|
|
+ if (value_eq(read_attribute(model, mapping["0"], "isInitial"), True)):
|
|
|
+ return 1!
|
|
|
+ else:
|
|
|
+ return 0!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN_link (post_cs_0, post_cs_1) {
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
{Contains} ForAll command_transition {
|
|
|
+ LHS {
|
|
|
+ Pre_Plant_PW/State pre_ct_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/State pre_ct_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/Transition pre_ct_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_ct_0, pre_ct_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_ct_1, pre_ct_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_ct_8 {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_ct_8, pre_ct_7) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Plant_PW/State post_ct_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/State post_ct_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/Transition post_ct_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_ct_0, post_ct_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_ct_1, post_ct_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ct_8 {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ct_8, post_ct_7) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_ct_10 {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_10) {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_4) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_ct_7, post_ct_10) {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_7) {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
+
|
|
|
{Contains} ForAll check_object {
|
|
|
+ LHS {
|
|
|
+ Pre_Plant_PW/State pre_co_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/State pre_co_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/Transition pre_co_2{
|
|
|
+ label = "2"
|
|
|
+ constraint_objPresent = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (bool_or(value == "Y", value == "N"))!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_co_0, pre_co_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_co_1, pre_co_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_8 {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_co_11 {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_co_11, pre_co_8) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Transition pre_co_15 {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/P2T (pre_co_3, pre_co_15) {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/T2P (pre_co_15, pre_co_4) {
|
|
|
+ label = "17"
|
|
|
+ }
|
|
|
+
|
|
|
+ constraint = $
|
|
|
+ Boolean constraint (host_model : Element, mapping : Element):
|
|
|
+ // Check whether the bound primary places match with the state
|
|
|
+ String objPresent
|
|
|
+ String port_name
|
|
|
+ objPresent = read_attribute(host_model, mapping["2"], "objPresent")
|
|
|
+ port_name = read_attribute(host_model, mapping["11"], "name")
|
|
|
+
|
|
|
+ if (objPresent == "Y"):
|
|
|
+ return (port_name == "objPresent")!
|
|
|
+ elif (objPresent == "N"):
|
|
|
+ return (port_name == "no_objPresent")!
|
|
|
+ else:
|
|
|
+ return False!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Plant_PW/State post_co_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/State post_co_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/Transition post_co_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_co_0, post_co_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_co_1, post_co_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_8 {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_co_11 {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_co_11, post_co_8) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_co_15 {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_co_3, post_co_15) {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
|
|
|
+ label = "17"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_co_8, post_co_15) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_8) {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
+
|
|
|
{Contains} ForAll detect {
|
|
|
+ LHS {
|
|
|
+ Pre_Plant_PW/NormalState pre_de_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/ErrorState pre_de_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/Transition pre_de_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_de_0, pre_de_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_de_1, pre_de_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Transition pre_de_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/P2T (pre_de_3, pre_de_7) {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/T2P (pre_de_7, pre_de_4) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_10 {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_de_11 {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_de_11, pre_de_10) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_de_14 {
|
|
|
+ label = "14"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (value == "interrupt")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_de_14, pre_de_13) {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_16 {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_de_17 {
|
|
|
+ label = "17"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (value == "no_objDetected")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_de_17, pre_de_16) {
|
|
|
+ label = "18"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_de_19 {
|
|
|
+ label = "19"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_de_20 {
|
|
|
+ label = "20"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (value == "objDetected")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_de_20, pre_de_19) {
|
|
|
+ label = "21"
|
|
|
+ }
|
|
|
+
|
|
|
+ constraint = $
|
|
|
+ Boolean constraint (host_model : Element, mapping : Element):
|
|
|
+ // Check whether the bound primary places match with the state
|
|
|
+ String source_type
|
|
|
+ String port_name
|
|
|
+ source_type = read_type(host_model, mapping["0"])
|
|
|
+ port_name = read_attribute(host_model, mapping["11"], "name")
|
|
|
+
|
|
|
+ if (source_type == "Up"):
|
|
|
+ return (port_name == "up")!
|
|
|
+ elif (source_type == "Neutral"):
|
|
|
+ return (port_name == "neutral")!
|
|
|
+ elif (source_type == "Down"):
|
|
|
+ return (port_name == "down")!
|
|
|
+ else:
|
|
|
+ return False!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Plant_PW/NormalState post_de_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/ErrorState post_de_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/Transition post_de_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_de_0, post_de_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_de_1, post_de_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_de_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_de_3, post_de_7) {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_4) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_10 {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_de_11 {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_de_11, post_de_10) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_de_14 {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_de_14, post_de_13) {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_16 {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_de_17 {
|
|
|
+ label = "17"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_de_17, post_de_16) {
|
|
|
+ label = "18"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_de_19 {
|
|
|
+ label = "19"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_de_20 {
|
|
|
+ label = "20"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_de_20, post_de_19) {
|
|
|
+ label = "21"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_de_10, post_de_7) {
|
|
|
+ label = "22"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_13) {
|
|
|
+ label = "23"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_de_16, post_de_7) {
|
|
|
+ label = "22"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_19) {
|
|
|
+ label = "23"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
{Contains} ForAll remove_detect {
|
|
|
+ LHS {
|
|
|
+ Pre_Plant_PW/ErrorState pre_rd_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/NormalState pre_rd_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_Plant_PW/Transition pre_rd_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_rd_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_rd_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_rd_0, pre_rd_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_PLANT2EPN/link (pre_rd_1, pre_rd_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/P2T (pre_rd_3, pre_rd_7) {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/T2P (pre_rd_7, pre_rd_4) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_rd_10 {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_rd_11 {
|
|
|
+ label = "11"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (value == "objDetected")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_rd_11, pre_rd_10) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_rd_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_rd_14 {
|
|
|
+ label = "14"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(value : String):
|
|
|
+ return (value == "no_objDetected")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_rd_14, pre_rd_13) {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Plant_PW/NormalState post_rd_0{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/ErrorState post_rd_1{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_Plant_PW/Transition post_rd_2{
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_rd_3{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_rd_4{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_rd_0, post_rd_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_PLANT2EPN/link (post_rd_1, post_rd_4) {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_rd_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_rd_3, post_rd_7) {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_4) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_rd_10 {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_rd_11 {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_rd_11, post_rd_10) {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_rd_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_rd_14 {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_rd_14, post_rd_13) {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_rd_10, post_rd_7) {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_13) {
|
|
|
+ label = "17"
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
}
|
|
|
Initial (schedule, init_ports) {}
|
