|
|
@@ -8,7 +8,7 @@ All_RAM Control2EPN {
|
|
|
{Contains} Atomic init_ports {
|
|
|
LHS {}
|
|
|
RHS {
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_0 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_00 {
|
|
|
label = "00"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -19,18 +19,18 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_0 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_10 {
|
|
|
label = "10"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "cmdDown"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_0, init_place_0) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_10, post_ports_00) {
|
|
|
label = "20"
|
|
|
}
|
|
|
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_1 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_01 {
|
|
|
label = "01"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -38,20 +38,20 @@ All_RAM Control2EPN {
|
|
|
$
|
|
|
value_tokens = #
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
- return 0!
|
|
|
+ return 1!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_1 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_11 {
|
|
|
label = "11"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "cmdNeutral"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_1, init_place_1) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_11, post_ports_01) {
|
|
|
label = "21"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_02 {
|
|
|
label = "02"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -62,17 +62,17 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_2 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_12 {
|
|
|
label = "12"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "cmdUp"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_2, init_place_2) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_12, post_ports_02) {
|
|
|
label = "22"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_3 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_03 {
|
|
|
label = "03"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -83,17 +83,17 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_3 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_13 {
|
|
|
label = "13"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "objDetected"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_3, init_place_3) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_13, post_ports_03) {
|
|
|
label = "23"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_4 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_04 {
|
|
|
label = "04"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -101,20 +101,20 @@ All_RAM Control2EPN {
|
|
|
$
|
|
|
value_tokens = #
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
- return 0!
|
|
|
+ return 1!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_4 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_14 {
|
|
|
label = "14"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "no_objDetected"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_4, init_place_4) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_14, post_ports_04) {
|
|
|
label = "24"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_5 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_05 {
|
|
|
label = "05"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -125,17 +125,17 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_5 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_15 {
|
|
|
label = "15"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "up"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_5, init_place_5) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_15, post_ports_05) {
|
|
|
label = "25"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_6 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_06 {
|
|
|
label = "06"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -143,20 +143,20 @@ All_RAM Control2EPN {
|
|
|
$
|
|
|
value_tokens = #
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
- return 0!
|
|
|
+ return 1!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_6 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_16 {
|
|
|
label = "16"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "neutral"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_6, init_place_6) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_16, post_ports_06) {
|
|
|
label = "26"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_7 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_07 {
|
|
|
label = "07"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -167,18 +167,18 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_7 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_17 {
|
|
|
label = "17"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "down"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_7, init_place_7) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_17, post_ports_07) {
|
|
|
label = "27"
|
|
|
}
|
|
|
|
|
|
- Post_Encapsulated_PetriNet/Place init_place_8 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ports_08 {
|
|
|
label = "08"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -189,14 +189,14 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port init_port_8 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ports_18 {
|
|
|
label = "18"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
return "interrupt"!
|
|
|
$
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (init_port_8, init_place_8) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ports_18, post_ports_08) {
|
|
|
label = "28"
|
|
|
}
|
|
|
}
|
|
|
@@ -208,10 +208,10 @@ All_RAM Control2EPN {
|
|
|
}
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_Control_PW/State cs_s {
|
|
|
+ Post_Control_PW/State post_cs_0 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place cs_p {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_cs1 {
|
|
|
label = "1"
|
|
|
value_name = $
|
|
|
String function value(model : Element, name : String, mapping : Element):
|
|
|
@@ -225,7 +225,7 @@ All_RAM Control2EPN {
|
|
|
return 0!
|
|
|
$
|
|
|
}
|
|
|
- Post_CTRL2EPN_link (cs_s, cs_p) {
|
|
|
+ Post_CTRL2EPN_link (post_cs_0, post_cs_1) {
|
|
|
label = "2"
|
|
|
}
|
|
|
}
|
|
|
@@ -233,210 +233,241 @@ All_RAM Control2EPN {
|
|
|
|
|
|
{Contains} ForAll create_transitions {
|
|
|
LHS {
|
|
|
- Pre_Control_PW/State pre_ct_s1 {
|
|
|
+ Pre_Control_PW/State pre_ct_0 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Pre_Control_PW/State pre_ct_s2 {
|
|
|
+ Pre_Control_PW/State pre_ct_1 {
|
|
|
label = "1"
|
|
|
}
|
|
|
- Pre_Control_PW/Transition (pre_ct_s1, pre_ct_s2) {
|
|
|
+ Pre_Control_PW/Transition (pre_ct_0, pre_ct_1) {
|
|
|
label = "2"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_ct_p1 {
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_3 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_ct_p2 {
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_4 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Pre_CTRL2EPN_link (pre_ct_s1, pre_ct_p1) {
|
|
|
+ Pre_CTRL2EPN_link (pre_ct_s1, pre_ct_3) {
|
|
|
label = "5"
|
|
|
}
|
|
|
- Pre_CTRL2EPN_link (pre_ct_s2, pre_ct_p2) {
|
|
|
+ Pre_CTRL2EPN_link (pre_ct_s2, pre_ct_4) {
|
|
|
label = "6"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_ps1 {
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_7 {
|
|
|
label = "7"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_ps2 {
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_ct_8 {
|
|
|
label = "8"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Port pre_pp1 {
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_ct_8, pre_ct_7) {
|
|
|
label = "9"
|
|
|
- constraint_name = $
|
|
|
- Boolean constraint(host_model : Element, name : String):
|
|
|
- String t
|
|
|
- t = read_attribute(host_model, name, "name")
|
|
|
- if (bool_or(bool_or(t == "up", t == "neutral"), t == "down")):
|
|
|
- return True:
|
|
|
- $
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Port pre_pp2 {
|
|
|
+
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_10 {
|
|
|
label = "10"
|
|
|
- constraint_name = $
|
|
|
- Boolean constraint(host_model : Element, name : String):
|
|
|
- String t
|
|
|
- t = read_attribute(host_model, name, "name")
|
|
|
- if (bool_or(bool_or(t == "up", t == "neutral"), t == "down")):
|
|
|
- return True:
|
|
|
- $
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/PortPlace (pre_pp1, pre_ps1) {
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_ct_11 {
|
|
|
label = "11"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/PortPlace (pre_pp2, pre_ps2) {
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_ct_11, pre_ct_10) {
|
|
|
label = "12"
|
|
|
}
|
|
|
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_ct_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_ct_14 {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_ct_14, pre_ct_13) {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+
|
|
|
constraint = $
|
|
|
Boolean constraint (host_model : Element, mapping : Element):
|
|
|
// Check whether the bound primary places match with the state
|
|
|
- String s1_type
|
|
|
- String s2_type
|
|
|
- String ps1_type
|
|
|
- String ps2_type
|
|
|
- s1_type = read_type(host_model, mapping["0"])
|
|
|
- s2_type = read_type(host_model, mapping["1"])
|
|
|
- ps1_type = read_attribute(host_model, mapping["9"], "name")
|
|
|
- ps2_type = read_attribute(host_model, mapping["10"], "name")
|
|
|
+ String type_0
|
|
|
+ String type_1
|
|
|
+ String type_2
|
|
|
+ String name_9
|
|
|
+ String name_12
|
|
|
+ String name_15
|
|
|
+
|
|
|
+ type_0 = read_type(host_model, mapping["0"])
|
|
|
+ type_1 = read_type(host_model, mapping["1"])
|
|
|
+ type_2 = read_type(host_model, mapping["2"])
|
|
|
+ name_9 = read_attribute(host_model, mapping["9"], "name")
|
|
|
+ name_12 = read_attribute(host_model, mapping["12"], "name")
|
|
|
+ name_15 = read_attribute(host_model, mapping["15"], "name")
|
|
|
|
|
|
- if (s1_type == "Up"):
|
|
|
- if (ps1_type != "up"):
|
|
|
+ // Source part
|
|
|
+ if (type_0 == "Up"):
|
|
|
+ if (name_9 != "up"):
|
|
|
return False!
|
|
|
- elif (s1_type == "Down"):
|
|
|
- if (ps1_type != "down"):
|
|
|
+ elif (type_0 == "Neutral"):
|
|
|
+ if (name_9 != "neutral"):
|
|
|
return False!
|
|
|
- elif (s1_type == "Neutral"):
|
|
|
- if (ps1_type != "neutral"):
|
|
|
+ elif (type_0 == "Down"):
|
|
|
+ if (name_9 != "down"):
|
|
|
return False!
|
|
|
|
|
|
- if (s2_type == "Up"):
|
|
|
- if (ps2_type != "up"):
|
|
|
+ // Target part
|
|
|
+ if (type_1 == "Up"):
|
|
|
+ if (name_12 != "up"):
|
|
|
return False!
|
|
|
- elif (s2_type == "Down"):
|
|
|
- if (ps2_type != "down"):
|
|
|
+ elif (type_1 == "Neutral"):
|
|
|
+ if (name_12 != "neutral"):
|
|
|
return False!
|
|
|
- elif (s2_type == "Neutral"):
|
|
|
- if (ps2_type != "neutral"):
|
|
|
+ elif (type_1 == "Down"):
|
|
|
+ if (name_12 != "down"):
|
|
|
return False!
|
|
|
|
|
|
+ // Link part
|
|
|
+ if (type_2 == "OnUp"):
|
|
|
+ if (name_15 != "cmdUp"):
|
|
|
+ return False!
|
|
|
+ elif (type_2 == "OnNeutral"):
|
|
|
+ if (name_15 != "cmdNeutral"):
|
|
|
+ return False!
|
|
|
+ elif (type_2 == "OnDown"):
|
|
|
+ if (name_15 != "cmdDown"):
|
|
|
+ return False!
|
|
|
+
|
|
|
+ // All passed, so OK!
|
|
|
return True!
|
|
|
$
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_Control_PW/State post_ct_s1 {
|
|
|
+ Post_Control_PW/State post_ct_0 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_Control_PW/State post_ct_s2 {
|
|
|
+ Post_Control_PW/State post_ct_1 {
|
|
|
label = "1"
|
|
|
}
|
|
|
- Post_Control_PW/Transition (post_ct_s1, post_ct_s2) {
|
|
|
+ Post_Control_PW/Transition (post_ct_0, post_ct_1) {
|
|
|
label = "2"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ct_p1 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_3 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ct_p2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_4 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Post_CTRL2EPN_link (post_ct_s1, post_ct_p1) {
|
|
|
+ Post_CTRL2EPN_link (post_ct_0, post_ct_3) {
|
|
|
label = "5"
|
|
|
}
|
|
|
- Post_CTRL2EPN_link (post_ct_s2, post_ct_p2) {
|
|
|
+ Post_CTRL2EPN_link (post_ct_1, post_ct_4) {
|
|
|
label = "6"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ps1 {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_7 {
|
|
|
label = "7"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ps2 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ct_9 {
|
|
|
label = "8"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port post_pp1 {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ct_9, post_ct_8) {
|
|
|
label = "9"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port post_pp2 {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_10 {
|
|
|
label = "10"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (post_pp1, post_ps1) {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ct_11 {
|
|
|
label = "11"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (post_pp2, post_ps2) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ct_11, post_ct_10) {
|
|
|
label = "12"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Transition post_ct_t {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Place post_ct_13 {
|
|
|
label = "13"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/P2T (post_ps1, post_ct_t) {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_ct_14 {
|
|
|
label = "14"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ps2) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_ct_14, post_ct_13) {
|
|
|
label = "15"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/P2T (post_ct_p1, post_ct_t) {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_ct_16 {
|
|
|
label = "16"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ct_p2) {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_16) {
|
|
|
label = "17"
|
|
|
}
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_4) {
|
|
|
+ label = "18"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_ct_7, post_ct_16) {
|
|
|
+ label = "19"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_10) {
|
|
|
+ label = "20"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_ct_13, post_ct_16) {
|
|
|
+ label = "21"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_13) {
|
|
|
+ label = "22"
|
|
|
+ }
|
|
|
}
|
|
|
}
|
|
|
|
|
|
{Contains} ForAll check_object {
|
|
|
LHS {
|
|
|
- Pre_Control_PW/State pre_cop_s1 {
|
|
|
+ Pre_Control_PW/State pre_co_0 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Pre_Control_PW/State pre_cop_s2 {
|
|
|
+ Pre_Control_PW/State pre_co_1 {
|
|
|
label = "1"
|
|
|
}
|
|
|
- Pre_Control_PW/Transition (pre_cop_s1, pre_cop_s2) {
|
|
|
+ Pre_Control_PW/Transition (pre_co_0, pre_co_1) {
|
|
|
label = "2"
|
|
|
constraint_objDetected = $
|
|
|
Boolean constraint(host_model : Element, name : String):
|
|
|
String t
|
|
|
t = read_attribute(host_model, name, "objDetected")
|
|
|
- if (bool_or(t == "Y", t == "N")):
|
|
|
- return True!
|
|
|
- else:
|
|
|
- return False!
|
|
|
+ return (bool_or(t == "Y", t == "N"))!
|
|
|
$
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_cop_p1 {
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_3 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_cop_p2 {
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_4 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Pre_CTRL2EPN_link (pre_cop_s1, pre_cop_p1) {
|
|
|
+ Pre_CTRL2EPN_link (pre_co_0, pre_co_3) {
|
|
|
label = "5"
|
|
|
}
|
|
|
- Pre_CTRL2EPN_link (pre_cop_s2, pre_cop_p2) {
|
|
|
+ Pre_CTRL2EPN_link (pre_co_1, pre_co_4) {
|
|
|
label = "6"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Place pre_cop_ps1 {
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_co_8 {
|
|
|
label = "8"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Port pre_pp1 {
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_co_11 {
|
|
|
label = "11"
|
|
|
constraint_name = $
|
|
|
Boolean constraint(host_model : Element, name : String):
|
|
|
String t
|
|
|
t = read_attribute(host_model, name, "name")
|
|
|
- if (bool_or(t == "objDetected", t == "no_objDetected")):
|
|
|
- return True!
|
|
|
- else:
|
|
|
- return False!
|
|
|
+ return (bool_or(t == "objDetected", t == "no_objDetected"))!
|
|
|
$
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/PortPlace (pre_pp1, pre_ps1) {
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_co_11, pre_co_8) {
|
|
|
label = "12"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/Transition pre_cop_t {
|
|
|
+ Pre_Encapsulated_PetriNet/Transition pre_co_15 {
|
|
|
label = "15"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/P2T (pre_ps1, pre_cop_t) {
|
|
|
+ Pre_Encapsulated_PetriNet/P2T (pre_co_3, pre_co_15) {
|
|
|
label = "16"
|
|
|
}
|
|
|
- Pre_Encapsulated_PetriNet/T2P (pre_cop_t, pre_ps2) {
|
|
|
+ Pre_Encapsulated_PetriNet/T2P (pre_co_15, pre_co_4) {
|
|
|
label = "17"
|
|
|
}
|
|
|
|
|
|
@@ -449,63 +480,181 @@ All_RAM Control2EPN {
|
|
|
ps1_type = read_attribute(host_model, mapping["11"], "name")
|
|
|
|
|
|
if (s1_value == "Y"):
|
|
|
- if (ps1_type == "objDetected"):
|
|
|
- return True!
|
|
|
+ return (ps1_type == "objDetected")!
|
|
|
elif (s1_value == "N"):
|
|
|
- if (ps1_type != "no_objDetected"):
|
|
|
- return True!
|
|
|
-
|
|
|
- return False!
|
|
|
+ return (ps1_type == "no_objDetected")!
|
|
|
+ else:
|
|
|
+ return False!
|
|
|
$
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_Control_PW/State post_ct_s1 {
|
|
|
+ Post_Control_PW/State post_co_0 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_Control_PW/State post_ct_s2 {
|
|
|
+ Post_Control_PW/State post_co_1 {
|
|
|
label = "1"
|
|
|
}
|
|
|
- Post_Control_PW/Transition (post_ct_s1, post_ct_s2) {
|
|
|
+ Post_Control_PW/Transition (post_co_0, post_co_1) {
|
|
|
label = "2"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ct_p1 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_3 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ct_p2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_4 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Post_CTRL2EPN_link (post_ct_s1, post_ct_p1) {
|
|
|
+ Post_CTRL2EPN_link (post_co_0, post_co_3) {
|
|
|
label = "5"
|
|
|
}
|
|
|
- Post_CTRL2EPN_link (post_ct_s2, post_ct_p2) {
|
|
|
+ Post_CTRL2EPN_link (post_co_1, post_co_4) {
|
|
|
label = "6"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Place post_ps1 {
|
|
|
+ Post_Encapsulated_PetriNet/Place post_co_8 {
|
|
|
label = "8"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Port post_pp1 {
|
|
|
+ Post_Encapsulated_PetriNet/Port post_co_11 {
|
|
|
label = "11"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/PortPlace (post_pp1, post_ps1) {
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_co_11, post_co_8) {
|
|
|
label = "12"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/Transition post_ct_t {
|
|
|
+
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_co_15 {
|
|
|
label = "15"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/P2T (post_ps1, post_ct_t) {
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_co_3, post_co_15) {
|
|
|
label = "16"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ps2) {
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
|
|
|
label = "17"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/P2T (post_cop_obj, post_cop_t) {
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_co_8, post_co_15) {
|
|
|
label = "9"
|
|
|
}
|
|
|
- Post_Encapsulated_PetriNet/T2P (post_cop_t, post_cop_obj) {
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
|
|
|
label = "10"
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
+
|
|
|
+ {Contains} ForAll fix_interrupt {
|
|
|
+ LHS {
|
|
|
+ Pre_Control_PW/State pre_fi_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_Control_PW/ErrorState pre_fi_1 {
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_fi_2 {
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_fi_3 {
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_CTRL2EPN_link (pre_fi_0, pre_fi_2) {
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_CTRL2EPN_link (pre_fi_1, pre_fi_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_fi_6 {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Place pre_fi_12 {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_fi_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_fi_13, pre_fi_12) {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/Port pre_fi_15 {
|
|
|
+ label = "15"
|
|
|
+ constraint_name = $
|
|
|
+ Boolean constraint(host_model : Element, name : String):
|
|
|
+ String t
|
|
|
+ t = read_attribute(host_model, name, "name")
|
|
|
+ return (t == "interrupt")!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Pre_Encapsulated_PetriNet/PortPlace (pre_fi_15, pre_fi_6) {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+
|
|
|
+ constraint = $
|
|
|
+ Boolean constraint (host_model : Element, mapping : Element):
|
|
|
+ // Check whether the bound primary places match with the state
|
|
|
+ String s_err_type
|
|
|
+ String p_name
|
|
|
+ s_err_type = read_type(host_model, mapping["1"])
|
|
|
+ p_name = read_attribute(host_model, mapping["13"], "name")
|
|
|
+
|
|
|
+ if (s_err_type == "Up"):
|
|
|
+ return (p_name == "up")!
|
|
|
+ elif (s_err_type == "Neutral"):
|
|
|
+ return (p_name == "neutral")!
|
|
|
+ elif (s_err_type == "Down"):
|
|
|
+ return (p_name == "down")!
|
|
|
+ else:
|
|
|
+ return False!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_Control_PW/State post_fi_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_Control_PW/ErrorState post_fi_1 {
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_fi_2 {
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_fi_3 {
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_CTRL2EPN_link (post_fi_0, post_fi_2) {
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_CTRL2EPN_link (post_fi_1, post_fi_3) {
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_fi_6 {
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Place post_fi_12 {
|
|
|
+ label = "12"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_fi_13 {
|
|
|
+ label = "13"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_fi_13, post_fi_12) {
|
|
|
+ label = "14"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Port post_fi_15 {
|
|
|
+ label = "15"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/PortPlace (post_fi_15, post_fi_6) {
|
|
|
+ label = "16"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/Transition post_fi_7 {
|
|
|
+ label = "7"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_fi_2, post_fi_7) {
|
|
|
+ label = "8"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_fi_7, post_fi_3) {
|
|
|
+ label = "9"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/P2T (post_fi_6, post_fi_7) {
|
|
|
+ label = "10"
|
|
|
+ }
|
|
|
+ Post_Encapsulated_PetriNet/T2P (post_fi_7, post_fi_12) {
|
|
|
+ label = "11"
|
|
|
+ }
|
|
|
+
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|
|
|
Initial (schedule, init_ports) {}
|
|
|
|
|
|
@@ -513,15 +662,13 @@ All_RAM Control2EPN {
|
|
|
OnSuccess (create_states, create_transitions) {}
|
|
|
OnSuccess (create_transitions, check_object) {}
|
|
|
OnSuccess (check_object, fix_interrupt) {}
|
|
|
- OnSuccess (fix_interrupt, check_input) {}
|
|
|
- OnSuccess (check_input, success) {}
|
|
|
+ OnSuccess (fix_interrupt, fix_interrupt_self) {}
|
|
|
+ OnSuccess (fix_interrupt_self, success) {}
|
|
|
|
|
|
OnFailure (init_ports, create_states) {}
|
|
|
OnFailure (create_states, create_transitions) {}
|
|
|
OnFailure (create_transitions, check_object) {}
|
|
|
OnFailure (check_object, fix_interrupt) {}
|
|
|
- OnFailure (fix_interrupt, check_input) {}
|
|
|
- OnFailure (check_input, success) {}
|
|
|
+ OnFailure (fix_interrupt, fix_interrupt_self) {}
|
|
|
+ OnFailure (fix_interrupt_self, success) {}
|
|
|
}
|
|
|
-
|
|
|
-export annotate to models/pn_annotate
|
