Fixed models

models/combine_EPN.mvc

@@ -259,10 +259,6 @@ A B {
                 }
                 Post_PetriNet/Transition ct2 {
                     label = "1"
-                    value_executing = $
-                        Boolean function value(model : Element, name : String, mapping : Element):
-                            return True!
-                        $
                     value_name = $
                         Integer function value(model : Element, name : String, mapping : Element):
                             return read_attribute(model, mapping["0"], "name")!

models/control_to_EPN.mvc

@@ -304,35 +304,35 @@ All_RAM Control2EPN {
                         name_15 = read_attribute(host_model, mapping["15"], "name")
 
                         // Source part
-                        if (type_0 == "Up"):
+                        if (type_0 == "PW_Control/Up"):
                             if (name_9 != "up"):
                                 return False!
-                        elif (type_0 == "Neutral"):
+                        elif (type_0 == "PW_Control/Neutral"):
                             if (name_9 != "neutral"):
                                 return False!
-                        elif (type_0 == "Down"):
+                        elif (type_0 == "PW_Control/Down"):
                             if (name_9 != "down"):
                                 return False!
 
                         // Target part
-                        if (type_1 == "Up"):
+                        if (type_1 == "PW_Control/Up"):
                             if (name_12 != "up"):
                                 return False!
-                        elif (type_1 == "Neutral"):
+                        elif (type_1 == "PW_Control/Neutral"):
                             if (name_12 != "neutral"):
                                 return False!
-                        elif (type_1 == "Down"):
+                        elif (type_1 == "PW_Control/Down"):
                             if (name_12 != "down"):
                                 return False!
 
                         // Link part
-                        if (type_2 == "UpPressed"):
+                        if (type_2 == "PW_Control/UpPressed"):
                             if (name_15 != "cmdUp"):
                                 return False!
-                        elif (type_2 == "NonePressed"):
+                        elif (type_2 == "PW_Control/NonePressed"):
                             if (name_15 != "cmdNeutral"):
                                 return False!
-                        elif (type_2 == "DownPressed"):
+                        elif (type_2 == "PW_Control/DownPressed"):
                             if (name_15 != "cmdDown"):
                                 return False!
 

models/plant_to_EPN.mvc

@@ -223,7 +223,7 @@ A B {
                 Pre_PW_Plant/State pre_ct_1{
                     label = "1"
                 }
-                Pre_PW_Plant/Transition pre_ct_2{
+                Pre_PW_Plant/Transition pre_ct_2 (pre_ct_0, pre_ct_1) {
                     label = "2"
                 }
                 Pre_Encapsulated_PetriNet/Place pre_ct_3{
@@ -232,10 +232,10 @@ A B {
                 Pre_Encapsulated_PetriNet/Place pre_ct_4{
                     label = "4"
                 }
-                Pre_PLANT2EPN_link (pre_ct_0, pre_ct_3) {
+                Pre_PLANT2EPN_link P2E_l1 (pre_ct_0, pre_ct_3) {
                     label = "5"
                 }
-                Pre_PLANT2EPN_link (pre_ct_1, pre_ct_4) {
+                Pre_PLANT2EPN_link P2E_l2(pre_ct_1, pre_ct_4) {
                     label = "6"
                 }
                 Pre_Encapsulated_PetriNet/Place pre_ct_7 {
@@ -243,10 +243,31 @@ A B {
                 }
                 Pre_Encapsulated_PetriNet/Port pre_ct_8 {
                     label = "8"
+                    constraint_name = $
+                        Boolean function constraint(value : String):
+                            return (bool_or(bool_or(value == "up", value == "neutral"), value == "down"))!
+                        $
                 }
-                Pre_Encapsulated_PetriNet/PortPlace (pre_ct_8, pre_ct_7) {
+                Pre_Encapsulated_PetriNet/PortPlace pp_l (pre_ct_8, pre_ct_7) {
                     label = "9"
                 }
+
+                constraint = $
+                    Boolean function constraint(model : Element, mapping : Element):
+                        String transition_type
+                        String port_name
+                        transition_type = read_type(model, mapping["2"])
+                        port_name = read_attribute(model, mapping["8"], "name")
+                        
+                        if (transition_type == "PW_Plant/OnUp"):
+                            return (port_name == "up")!
+                        elif (transition_type == "PW_Plant/OnNeutral"):
+                            return (port_name == "neutral")!
+                        elif (transition_type == "PW_Plant/OnDown"):
+                            return (port_name == "down")!
+                        else:
+                            return False!
+                        $
             }
             RHS {
                 Post_PW_Plant/State post_ct_0{
@@ -255,7 +276,7 @@ A B {
                 Post_PW_Plant/State post_ct_1{
                     label = "1"
                 }
-                Post_PW_Plant/Transition post_ct_2{
+                Post_PW_Plant/Transition post_ct_2 (post_ct_0, post_ct_1) {
                     label = "2"
                 }
                 Post_Encapsulated_PetriNet/Place post_ct_3{
@@ -282,6 +303,10 @@ A B {
 
                 Post_Encapsulated_PetriNet/Transition post_ct_10 {
                     label = "10"
+                    value_name = $
+                        String function value(model : Element, name : String, mapping : Element):
+                            return read_type(model, mapping["2"])!
+                        $
                 }
                 Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_10) {
                     label = "11"
@@ -306,7 +331,7 @@ A B {
                 Pre_PW_Plant/State pre_co_1{
                     label = "1"
                 }
-                Pre_PW_Plant/Transition pre_co_2{
+                Pre_PW_Plant/Transition pre_co_2 (pre_co_0, pre_co_1) {
                     label = "2"
                     constraint_objPresent = $
                         Boolean function constraint(value : String):
@@ -368,7 +393,7 @@ A B {
                 Post_PW_Plant/State post_co_1{
                     label = "1"
                 }
-                Post_PW_Plant/Transition post_co_2{
+                Post_PW_Plant/Transition post_co_2 (post_co_0, post_co_1) {
                     label = "2"
                 }
                 Post_Encapsulated_PetriNet/Place post_co_3{
@@ -420,7 +445,7 @@ A B {
                 Pre_PW_Plant/ErrorState pre_de_1{
                     label = "1"
                 }
-                Pre_PW_Plant/Transition pre_de_2{
+                Pre_PW_Plant/Transition pre_de_2 (pre_de_0, pre_de_1) {
                     label = "2"
                 }
                 Pre_Encapsulated_PetriNet/Place pre_de_3{
@@ -502,14 +527,14 @@ A B {
                         // Check whether the bound primary places match with the state
                         String source_type
                         String port_name
-                        source_type = read_type(host_model, mapping["0"])
+                        source_type = read_type(host_model, mapping["2"])
                         port_name = read_attribute(host_model, mapping["11"], "name")
 
-                        if (source_type == "Up"):
+                        if (source_type == "PW_Plant/OnUp"):
                             return (port_name == "up")!
-                        elif (source_type == "Neutral"):
+                        elif (source_type == "PW_Plant/OnNeutral"):
                             return (port_name == "neutral")!
-                        elif (source_type == "Down"):
+                        elif (source_type == "PW_Plant/OnDown"):
                             return (port_name == "down")!
                         else:
                             return False!
@@ -522,7 +547,7 @@ A B {
                 Post_PW_Plant/ErrorState post_de_1{
                     label = "1"
                 }
-                Post_PW_Plant/Transition post_de_2{
+                Post_PW_Plant/Transition post_de_2 (post_de_0, post_de_1){
                     label = "2"
                 }
                 Post_Encapsulated_PetriNet/Place post_de_3{
@@ -609,7 +634,7 @@ A B {
                 Pre_PW_Plant/NormalState pre_rd_1{
                     label = "1"
                 }
-                Pre_PW_Plant/Transition pre_rd_2{
+                Pre_PW_Plant/Transition pre_rd_2 (pre_rd_0, pre_rd_1){
                     label = "2"
                 }
                 Pre_Encapsulated_PetriNet/Place pre_rd_3{
@@ -669,7 +694,7 @@ A B {
                 Post_PW_Plant/ErrorState post_rd_1{
                     label = "1"
                 }
-                Post_PW_Plant/Transition post_rd_2{
+                Post_PW_Plant/Transition post_rd_2 (post_rd_0, post_rd_1){
                     label = "2"
                 }
                 Post_Encapsulated_PetriNet/Place post_rd_3{

models/pm_req_analyse.mvc

@@ -178,15 +178,31 @@ ProcessModel analyse_requirements {
     Consumes (refine_query, query) {
         name = "query"
     }
-    Produces (refine_plant, plant_EPN) {
+    Produces (refine_plant, plant_model) {
     }
-    Produces (refine_control, control_EPN) {
+    Produces (refine_control, control_model) {
     }
-    Produces (refine_environment, environment_EPN) {
+    Produces (refine_environment, environment_model) {
     }
     Produces (refine_query, query) {
     }
 
+    Consumes (plant_to_EPN, plant_model) {
+        name = "plant_model"
+    }
+    Produces (plant_to_EPN, plant_EPN) {
+    }
+    Consumes (environment_to_EPN, environment_model) {
+        name = "environment_model"
+    }
+    Produces (environment_to_EPN, environment_EPN) {
+    }
+    Consumes (control_to_EPN, control_model) {
+        name = "control_model"
+    }
+    Produces (control_to_EPN, control_EPN) {
+    }
+
     Consumes (combine_EPN, plant_EPN) {
         name = "epn_1"
     }