Browse Source

Putting things together in the PM

Yentl Van Tendeloo 8 years ago
parent
commit
1ab9dd9529

+ 0 - 2
bootstrap/ramify.alc

@@ -24,8 +24,6 @@ Element function ramify(model : Element):
 	old_m = model["model"]
 	old_m = model["model"]
 	mm = new_model["metamodel"]["model"]
 	mm = new_model["metamodel"]["model"]
 
 
-	log("Metamodel has elements: " + set_to_string(dict_keys(model["metamodel"]["model"])))
-
 	// Add in some primitives
 	// Add in some primitives
 	instantiate_node(new_model, "SimpleAttribute", "Natural")
 	instantiate_node(new_model, "SimpleAttribute", "Natural")
 	instantiate_attribute(new_model, "Natural", "constraint", constraint_Natural)
 	instantiate_attribute(new_model, "Natural", "constraint", constraint_Natural)

+ 3 - 6
core/core_algorithm.alc

@@ -643,6 +643,7 @@ Boolean function enact_action(pm : Element, element : String, prefix : String, u
 
 
 			// 3) Transform
 			// 3) Transform
 
 
+			output("Please perform manual transformation " + cast_v2s(read_attribute(pm, element, "name")))
 			modify(merged_model, True)
 			modify(merged_model, True)
 
 
 			// 4) Split in different files depending on type
 			// 4) Split in different files depending on type
@@ -685,7 +686,7 @@ Void function enact_PM(pm : Element, prefix : String, user_id : String):
 
 
 	// Initialize Join counters
 	// Initialize Join counters
 	counters = create_node()
 	counters = create_node()
-	join_nodes = allInstances(pm, "Join")
+	join_nodes = allInstances(pm, "ForkJoin")
 	while (read_nr_out(join_nodes) > 0):
 	while (read_nr_out(join_nodes) > 0):
 		dict_add(counters, set_pop(join_nodes), 0)
 		dict_add(counters, set_pop(join_nodes), 0)
 
 
@@ -712,7 +713,7 @@ Void function enact_PM(pm : Element, prefix : String, user_id : String):
 		elif (type == "Finish"):
 		elif (type == "Finish"):
 			// Should be impossible, as we would have ended...
 			// Should be impossible, as we would have ended...
 			result = result
 			result = result
-		elif (type == "JoinFork"):
+		elif (type == "ForkJoin"):
 			// Only do this if all dependencies are fullfilled
 			// Only do this if all dependencies are fullfilled
 			// So add to the counter of this Join
 			// So add to the counter of this Join
 			dict_overwrite(counters, element, integer_addition(counters[element], 1))
 			dict_overwrite(counters, element, integer_addition(counters[element], 1))
@@ -1247,26 +1248,22 @@ Void function user_function_skip_init(user_id : String):
 					String tracability_link
 					String tracability_link
 
 
 					// New location is available, so write
 					// New location is available, so write
-					log("FUSE")
 					merged_formalism = model_fuse(set_copy(all_formalisms))
 					merged_formalism = model_fuse(set_copy(all_formalisms))
 					model_create(merged_formalism, "__merged_" + name, user_id, type_id, "Model")
 					model_create(merged_formalism, "__merged_" + name, user_id, type_id, "Model")
 					merged_formalism_id = get_model_id("__merged_" + name)
 					merged_formalism_id = get_model_id("__merged_" + name)
 
 
 					// Add tracability links at this level
 					// Add tracability links at this level
-					log("TRACE")
 					while (read_nr_out(all_formalisms) > 0):
 					while (read_nr_out(all_formalisms) > 0):
 						source_formalism_id = get_model_id(list_read(set_pop(all_formalisms), 0))
 						source_formalism_id = get_model_id(list_read(set_pop(all_formalisms), 0))
 						tracability_link = instantiate_link(core, "tracability", "", merged_formalism_id, source_formalism_id)
 						tracability_link = instantiate_link(core, "tracability", "", merged_formalism_id, source_formalism_id)
 						instantiate_attribute(core, tracability_link, "type", "merged")
 						instantiate_attribute(core, tracability_link, "type", "merged")
 
 
 					// Merge complete, now RAMify!
 					// Merge complete, now RAMify!
-					log("RAM")
 					ramified_formalism = ramify(merged_formalism)
 					ramified_formalism = ramify(merged_formalism)
 					model_create(ramified_formalism, name, user_id, type_id, "Model")
 					model_create(ramified_formalism, name, user_id, type_id, "Model")
 					ramified_formalism_id = get_model_id(name)
 					ramified_formalism_id = get_model_id(name)
 
 
 					// Add tracability link at this level
 					// Add tracability link at this level
-					log("NEWTRACE")
 					tracability_link = instantiate_link(core, "tracability", "", ramified_formalism_id, merged_formalism_id)
 					tracability_link = instantiate_link(core, "tracability", "", ramified_formalism_id, merged_formalism_id)
 					instantiate_attribute(core, tracability_link, "type", "RAMified")
 					instantiate_attribute(core, tracability_link, "type", "RAMified")
 
 

+ 7 - 0
core/mini_modify.alc

@@ -37,6 +37,7 @@ Element function modify(model : Element, write : Boolean):
 				output("  rename        -- Rename an existing element")
 				output("  rename        -- Rename an existing element")
 				output("  modify        -- Modify the attributes of an element")
 				output("  modify        -- Modify the attributes of an element")
 				output("  retype        -- Change the type of an element")
 				output("  retype        -- Change the type of an element")
+				output("  upload        -- Upload a completely new model")
 			else:
 			else:
 				output(" == READ-ONLY ==")
 				output(" == READ-ONLY ==")
 			output("  list          -- Prints the list of elements in the model")
 			output("  list          -- Prints the list of elements in the model")
@@ -47,6 +48,12 @@ Element function modify(model : Element, write : Boolean):
 			output("  exit          -- Leave the modification interface")
 			output("  exit          -- Leave the modification interface")
 		elif (cmd == "exit"):
 		elif (cmd == "exit"):
 			return model!
 			return model!
+		elif (cmd == "upload"):
+			Element new_model
+			output("Waiting for model constructors...")
+			new_model = construct_model_raw(model["metamodel"])
+			dict_overwrite(model, "model", new_model["model"])
+			dict_overwrite(model, "type_mapping", new_model["type_mapping"])
 		elif (cmd == "instantiate"):
 		elif (cmd == "instantiate"):
 			if (write):
 			if (write):
 				String mm_type_name
 				String mm_type_name

+ 102 - 22
integration/test_powerwindow.py

@@ -90,17 +90,17 @@ class TestPowerWindow(unittest.TestCase):
                     "__merged_All_RAM",
                     "__merged_All_RAM",
                         "instantiate",
                         "instantiate",
                             "Association",
                             "Association",
-                            "CTRL2EPN/link",
+                            "CTRL2EPN_link",
                             "PW_Control/State",
                             "PW_Control/State",
                             "Encapsulated_PetriNet/Place",
                             "Encapsulated_PetriNet/Place",
                         "instantiate",
                         "instantiate",
                             "Association",
                             "Association",
-                            "PLANT2EPN/link",
+                            "PLANT2EPN_link",
                             "PW_Plant/State",
                             "PW_Plant/State",
                             "Encapsulated_PetriNet/Place",
                             "Encapsulated_PetriNet/Place",
                         "instantiate",
                         "instantiate",
                             "Association",
                             "Association",
-                            "ENV2EPN/link",
+                            "ENV2EPN_link",
                             "PW_Environment/Event",
                             "PW_Environment/Event",
                             "Encapsulated_PetriNet/Place",
                             "Encapsulated_PetriNet/Place",
                         "exit",
                         "exit",
@@ -178,6 +178,29 @@ class TestPowerWindow(unittest.TestCase):
                     "reachability",
                     "reachability",
                     ] + get_constructor(open("integration/code/reachability.alc", "r").read()) + [
                     ] + get_constructor(open("integration/code/reachability.alc", "r").read()) + [
                 "model_list",
                 "model_list",
+                "process_execute",
+                "pm_powerwindow",
+                "pm_",
+                # define_req
+                "upload",
+                ] + get_model_constructor(open("models/requirements_model.mvc", "r").read()) + [
+                "exit",
+                # refine_plant
+                "upload",
+                ] + get_model_constructor(open("models/plant_model.mvc", "r").read()) + [
+                "exit",
+                # refine_environment
+                "upload",
+                ] + get_model_constructor(open("models/environment_model.mvc", "r").read()) + [
+                "exit",
+                # refine_control
+                "upload",
+                ] + get_model_constructor(open("models/control_model.mvc", "r").read()) + [
+                "exit",
+                # refine_query
+                "upload",
+                ] + get_model_constructor(open("models/query_model.mvc", "r").read()) + [
+                "exit",
             ],
             ],
             [   # bootup phase
             [   # bootup phase
                 "Desired username for admin user?",
                 "Desired username for admin user?",
@@ -265,6 +288,25 @@ class TestPowerWindow(unittest.TestCase):
                 "Model added as target",
                 "Model added as target",
                 "Model added as target",
                 "Model added as target",
                 "Model added as target",
                 "Model added as target",
+                "Name of new transformation?",
+                "Waiting for model constructors...",
+                "Ready for command...",
+                # transformation_add_MT
+                "RAMified metamodel to use?",
+                "Supported metamodels:",
+                set(["  PetriNet",
+                     "  Encapsulated_PetriNet",
+                     "  Query",
+                     "  PW_Plant",
+                     "  PW_Environment",
+                     "  Requirements",
+                     "  PW_Control",
+                     "  ReachabilityGraph",
+                    ]),
+                "",
+                "Which ones do you want to use as source (empty string to finish)?",
+                "Model added as source",
+                "Which ones do you want to use as target (empty string to finish)?",
                 "Model added as target",
                 "Model added as target",
                 "Name of new transformation?",
                 "Name of new transformation?",
                 "Waiting for model constructors...",
                 "Waiting for model constructors...",
@@ -290,25 +332,25 @@ class TestPowerWindow(unittest.TestCase):
                 "Waiting for model constructors...",
                 "Waiting for model constructors...",
                 "Ready for command...",
                 "Ready for command...",
                 # transformation_add_MT
                 # transformation_add_MT
-                ] + [   "RAMified metamodel to use?",
-                        "Supported metamodels:",
-                        set(["  PetriNet",
-                             "  Encapsulated_PetriNet",
-                             "  Query",
-                             "  PW_Plant",
-                             "  PW_Environment",
-                             "  Requirements",
-                             "  PW_Control",
-                             "  ReachabilityGraph",
-                            ]),
-                        "",
-                        "Which ones do you want to use as source (empty string to finish)?",
-                        "Model added as source",
-                        "Which ones do you want to use as target (empty string to finish)?",
-                        "Model added as target",
-                        "Name of new transformation?",
-                        "Waiting for model constructors...",
-                        "Ready for command...", ] * 3 + [
+                "RAMified metamodel to use?",
+                "Supported metamodels:",
+                set(["  PetriNet",
+                     "  Encapsulated_PetriNet",
+                     "  Query",
+                     "  PW_Plant",
+                     "  PW_Environment",
+                     "  Requirements",
+                     "  PW_Control",
+                     "  ReachabilityGraph",
+                    ]),
+                "",
+                "Which ones do you want to use as source (empty string to finish)?",
+                "Model added as source",
+                "Which ones do you want to use as target (empty string to finish)?",
+                "Model added as target",
+                "Name of new transformation?",
+                "Waiting for model constructors...",
+                "Ready for command...",
                 # transformation_add_AL
                 # transformation_add_AL
                 ] + [   "Which metamodels do you want to use as source for the action code (empty string to finish)?",
                 ] + [   "Which metamodels do you want to use as source for the action code (empty string to finish)?",
                         "Model added as source",
                         "Model added as source",
@@ -348,4 +390,42 @@ class TestPowerWindow(unittest.TestCase):
                      "  ReachabilityGraph : SimpleClassDiagrams",
                      "  ReachabilityGraph : SimpleClassDiagrams",
                      ]),
                      ]),
                 "Ready for command...",
                 "Ready for command...",
+                # process_execute
+                "Which process model do you want to execute?",
+                "Model prefix to use?",
+                # Manual transformation define_req
+                "Please perform manual transformation \"define_req\"",
+                "Model loaded, ready for commands!",
+                "Use 'help' command for a list of possible commands",
+                "Please give your command.",
+                "Waiting for model constructors...",
+                "Please give your command.",
+                # Manual transformation refine_plant
+                "Please perform manual transformation \"refine_plant\"",
+                "Model loaded, ready for commands!",
+                "Use 'help' command for a list of possible commands",
+                "Please give your command.",
+                "Waiting for model constructors...",
+                "Please give your command.",
+                # Manual transformation refine_environment
+                "Please perform manual transformation \"refine_environment\"",
+                "Model loaded, ready for commands!",
+                "Use 'help' command for a list of possible commands",
+                "Please give your command.",
+                "Waiting for model constructors...",
+                "Please give your command.",
+                # Manual transformation refine_control
+                "Please perform manual transformation \"refine_control\"",
+                "Model loaded, ready for commands!",
+                "Use 'help' command for a list of possible commands",
+                "Please give your command.",
+                "Waiting for model constructors...",
+                "Please give your command.",
+                # Manual transformation refine_query
+                "Please perform manual transformation \"refine_query\"",
+                "Model loaded, ready for commands!",
+                "Use 'help' command for a list of possible commands",
+                "Please give your command.",
+                "Waiting for model constructors...",
+                "Please give your command.",
             ]))
             ]))

+ 3 - 3
models/control_PW.mvc

@@ -26,7 +26,7 @@ SimpleClassDiagram Control_PW{
     Association Transition (State, State) {
     Association Transition (State, State) {
         objectDetected : TriState
         objectDetected : TriState
     }
     }
-    Association UpPressed : Transition {}
-    Association NonePressed : Transition {}
-    Association DownPressed : Transition {}
+    Association UpPressed : Transition (State, State) {}
+    Association NonePressed : Transition (State, State) {}
+    Association DownPressed : Transition (State, State) {}
 }
 }

+ 23 - 23
models/control_to_EPN.mvc

@@ -204,12 +204,12 @@ All_RAM Control2EPN {
         }
         }
         {Contains} ForAll create_states {
         {Contains} ForAll create_states {
             LHS {
             LHS {
-                Pre_Control_PW/State {
+                Pre_PW_Control/State {
                     label = "0"
                     label = "0"
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Control_PW/State post_cs_0 {
+                Post_PW_Control/State post_cs_0 {
                     label = "0"
                     label = "0"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_cs1 {
                 Post_Encapsulated_PetriNet/Place post_cs1 {
@@ -234,13 +234,13 @@ All_RAM Control2EPN {
 
 
         {Contains} ForAll create_transitions {
         {Contains} ForAll create_transitions {
             LHS {
             LHS {
-                Pre_Control_PW/State pre_ct_0 {
+                Pre_PW_Control/State pre_ct_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Control_PW/State pre_ct_1 {
+                Pre_PW_Control/State pre_ct_1 {
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Control_PW/Transition (pre_ct_0, pre_ct_1) {
+                Pre_PW_Control/Transition (pre_ct_0, pre_ct_1) {
                     label = "2"
                     label = "2"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_ct_3 {
                 Pre_Encapsulated_PetriNet/Place pre_ct_3 {
@@ -326,13 +326,13 @@ All_RAM Control2EPN {
                                 return False!
                                 return False!
 
 
                         // Link part
                         // Link part
-                        if (type_2 == "OnUp"):
+                        if (type_2 == "UpPressed"):
                             if (name_15 != "cmdUp"):
                             if (name_15 != "cmdUp"):
                                 return False!
                                 return False!
-                        elif (type_2 == "OnNeutral"):
+                        elif (type_2 == "NonePressed"):
                             if (name_15 != "cmdNeutral"):
                             if (name_15 != "cmdNeutral"):
                                 return False!
                                 return False!
-                        elif (type_2 == "OnDown"):
+                        elif (type_2 == "DownPressed"):
                             if (name_15 != "cmdDown"):
                             if (name_15 != "cmdDown"):
                                 return False!
                                 return False!
 
 
@@ -341,13 +341,13 @@ All_RAM Control2EPN {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Control_PW/State post_ct_0 {
+                Post_PW_Control/State post_ct_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Control_PW/State post_ct_1 {
+                Post_PW_Control/State post_ct_1 {
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Control_PW/Transition (post_ct_0, post_ct_1) {
+                Post_PW_Control/Transition (post_ct_0, post_ct_1) {
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_ct_3 {
                 Post_Encapsulated_PetriNet/Place post_ct_3 {
@@ -420,13 +420,13 @@ All_RAM Control2EPN {
 
 
         {Contains} ForAll check_object {
         {Contains} ForAll check_object {
             LHS {
             LHS {
-                Pre_Control_PW/State pre_co_0 {
+                Pre_PW_Control/State pre_co_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Control_PW/State pre_co_1 {
+                Pre_PW_Control/State pre_co_1 {
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Control_PW/Transition (pre_co_0, pre_co_1) {
+                Pre_PW_Control/Transition (pre_co_0, pre_co_1) {
                     label = "2"
                     label = "2"
                     constraint_objDetected = $
                     constraint_objDetected = $
                         Boolean function constraint(value : String):
                         Boolean function constraint(value : String):
@@ -485,13 +485,13 @@ All_RAM Control2EPN {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Control_PW/State post_co_0 {
+                Post_PW_Control/State post_co_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Control_PW/State post_co_1 {
+                Post_PW_Control/State post_co_1 {
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Control_PW/Transition (post_co_0, post_co_1) {
+                Post_PW_Control/Transition (post_co_0, post_co_1) {
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_co_3 {
                 Post_Encapsulated_PetriNet/Place post_co_3 {
@@ -536,10 +536,10 @@ All_RAM Control2EPN {
 
 
         {Contains} ForAll fix_interrupt {
         {Contains} ForAll fix_interrupt {
             LHS {
             LHS {
-                Pre_Control_PW/State pre_fi_0 {
+                Pre_PW_Control/State pre_fi_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Control_PW/State pre_fi_1 {
+                Pre_PW_Control/State pre_fi_1 {
                     label = "1"
                     label = "1"
                     constraint_isError = $
                     constraint_isError = $
                         Boolean function constraint(value : Boolean):
                         Boolean function constraint(value : Boolean):
@@ -600,10 +600,10 @@ All_RAM Control2EPN {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Control_PW/State post_fi_0 {
+                Post_PW_Control/State post_fi_0 {
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Control_PW/State post_fi_1 {
+                Post_PW_Control/State post_fi_1 {
                     label = "1"
                     label = "1"
                     constraint_isError = $
                     constraint_isError = $
                         Boolean function constraint(value : Boolean):
                         Boolean function constraint(value : Boolean):
@@ -660,7 +660,7 @@ All_RAM Control2EPN {
 
 
         {Contains} ForAll fix_interrupt_self {
         {Contains} ForAll fix_interrupt_self {
             LHS {
             LHS {
-                Pre_Control_PW/State pre_fis_0 {
+                Pre_PW_Control/State pre_fis_0 {
                     label = "0"
                     label = "0"
                     constraint_isError = $
                     constraint_isError = $
                         Boolean function constraint(value : Boolean):
                         Boolean function constraint(value : Boolean):
@@ -717,7 +717,7 @@ All_RAM Control2EPN {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Control_PW/State post_fis_0 {
+                Post_PW_Control/State post_fis_0 {
                     label = "0"
                     label = "0"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_fis_1 {
                 Post_Encapsulated_PetriNet/Place post_fis_1 {

+ 12 - 12
models/environment_to_EPN.mvc

@@ -8,12 +8,12 @@ A B {
         {Contains} Failure failure {}
         {Contains} Failure failure {}
         {Contains} ForAll create_ports {
         {Contains} ForAll create_ports {
             LHS {
             LHS {
-                Pre_Environment_PW/Event {
+                Pre_PW_Environment/Event {
                     label = "1"
                     label = "1"
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Environment_PW/Event {
+                Post_PW_Environment/Event {
                     label = "1"
                     label = "1"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place cp_place {
                 Post_Encapsulated_PetriNet/Place cp_place {
@@ -44,19 +44,19 @@ A B {
         }
         }
         {Contains} ForAll create_switches {
         {Contains} ForAll create_switches {
             LHS {
             LHS {
-                Pre_Environment_PW/Group pre_grp {
+                Pre_PW_Environment/Group pre_grp {
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Environment_PW/Event pre_evt_a {
+                Pre_PW_Environment/Event pre_evt_a {
                     label = "2"
                     label = "2"
                 }
                 }
-                Pre_Environment_PW/Event pre_evt_b {
+                Pre_PW_Environment/Event pre_evt_b {
                     label = "3"
                     label = "3"
                 }
                 }
-                Pre_Environment_PW/Contains (pre_grp, pre_evt_a) {
+                Pre_PW_Environment/Contains (pre_grp, pre_evt_a) {
                     label = "4"
                     label = "4"
                 }
                 }
-                Pre_Environment_PW/Contains (pre_grp, pre_evt_b) {
+                Pre_PW_Environment/Contains (pre_grp, pre_evt_b) {
                     label = "5"
                     label = "5"
                 }
                 }
                 Pre_ENV2EPN_link (pre_evt_a, pre_place_a) {
                 Pre_ENV2EPN_link (pre_evt_a, pre_place_a) {
@@ -73,19 +73,19 @@ A B {
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Environment_PW/Group post_grp {
+                Post_PW_Environment/Group post_grp {
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Environment_PW/Event post_evt_a {
+                Post_PW_Environment/Event post_evt_a {
                     label = "2"
                     label = "2"
                 }
                 }
-                Post_Environment_PW/Event post_evt_b {
+                Post_PW_Environment/Event post_evt_b {
                     label = "3"
                     label = "3"
                 }
                 }
-                Post_Environment_PW/Contains (post_grp, post_evt_a) {
+                Post_PW_Environment/Contains (post_grp, post_evt_a) {
                     label = "4"
                     label = "4"
                 }
                 }
-                Post_Environment_PW/Contains (post_grp, post_evt_b) {
+                Post_PW_Environment/Contains (post_grp, post_evt_b) {
                     label = "5"
                     label = "5"
                 }
                 }
                 Post_ENV2EPN_link (post_evt_a, post_place_a) {
                 Post_ENV2EPN_link (post_evt_a, post_place_a) {

+ 1 - 1
models/petrinet_ports.mvc

@@ -25,7 +25,7 @@ SimpleClassDiagrams PetriNetsPorts {
         name : String
         name : String
     }
     }
     Class Place : Named {
     Class Place : Named {
-        nbTokens : Natural
+        tokens : Natural
     }
     }
     Class Transition : Named {}
     Class Transition : Named {}
     Class Port : Named {}
     Class Port : Named {}

+ 19 - 0
models/plant_PW.mvc

@@ -0,0 +1,19 @@
+A B{
+    SimpleAttribute TriState {}
+    SimpleAttribute String {}
+    SimpleAttribute Boolean {}
+
+    Class State {
+        name : String
+        isInitial : Boolean
+    }
+    Class ErrorState : State {}
+    Class NormalState : State {}
+
+    Association Transition (State, State) {
+        objectPresent : TriState
+    }
+    Association OnUp : Transition (State, State) {}
+    Association OnDown : Transition (State, State) {}
+    Association OnNeutral : Transition (State, State) {}
+}

+ 113 - 0
models/plant_model.mvc

@@ -0,0 +1,113 @@
+B C{
+    NormalState lt {
+        name = "low_top"
+        isInitial = False
+    }
+    NormalState mt {
+        name = "medium_top"
+        isInitial = False
+    }
+    NormalState ht {
+        name = "high_top"
+        isInitial = False
+    }
+    NormalState lm {
+        name = "low_medium"
+        isInitial = False
+    }
+    ErrorState mm {
+        name = "medium_medium"
+        isInitial = False
+    }
+    ErrorState hm {
+        name = "high_medium"
+        isInitial = False
+    }
+    NormalState lb {
+        name = "low_bottom"
+        isInitial = False
+    }
+    NormalState mb {
+        name = "medium_bottom"
+        isInitial = False
+    }
+    NormalState hb {
+        name = "high_bottom"
+        isInitial = True
+    }
+
+    OnUp (hb, mb) {
+        objectPresent = "*"
+    }
+    OnUp (mb, lb) {
+        objectPresent = "*"
+    }
+    OnUp (lb, lm) {
+        objectPresent = "*"
+    }
+    OnUp (lm, lt) {
+        objectPresent = "N"
+    }
+    OnUp (lm, mm) {
+        objectPresent = "Y"
+    }
+    OnUp (mm, hm) {
+        objectPresent = "Y"
+    }
+    OnUp (lt, mt) {
+        objectPresent = "*"
+    }
+    OnUp (mt, ht) {
+        objectPresent = "*"
+    }
+
+    OnDown (ht, mt) {
+        objectPresent = "*"
+    }
+    OnDown (mt, lt) {
+        objectPresent = "*"
+    }
+    OnDown (lt, lm) {
+        objectPresent = "*"
+    }
+    OnDown (hm, mm) {
+        objectPresent = "*"
+    }
+    OnDown (mm, lm) {
+        objectPresent = "*"
+    }
+    OnDown (lm, lb) {
+        objectPresent = "*"
+    }
+    OnDown (lb, mb) {
+        objectPresent = "*"
+    }
+    OnDown (mb, hb) {
+        objectPresent = "*"
+    }
+
+    OnNeutral (hb, mb) {
+        objectPresent = "*"
+    }
+    OnNeutral (mb, lb) {
+        objectPresent = "*"
+    }
+    OnNeutral (hm, mm) {
+        objectPresent = "*"
+    }
+    OnNeutral (mm, lm) {
+        objectPresent = "*"
+    }
+    OnNeutral (hm, mm) {
+        objectPresent = "*"
+    }
+    OnNeutral (mm, lm) {
+        objectPresent = "*"
+    }
+    OnNeutral (ht, mt) {
+        objectPresent = "*"
+    }
+    OnNeutral (mt, lt) {
+        objectPresent = "*"
+    }
+}

+ 42 - 42
models/plant_to_EPN.mvc

@@ -188,12 +188,12 @@ A B {
         }
         }
         {Contains} ForAll create_states {
         {Contains} ForAll create_states {
             LHS {
             LHS {
-                Pre_Plant_PW/State {
+                Pre_PW_Plant/State {
                     label = "0"
                     label = "0"
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Plant_PW/State post_cs_0 {
+                Post_PW_Plant/State post_cs_0 {
                     label = "0"
                     label = "0"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_cs1 {
                 Post_Encapsulated_PetriNet/Place post_cs1 {
@@ -217,13 +217,13 @@ A B {
         }
         }
         {Contains} ForAll command_transition {
         {Contains} ForAll command_transition {
             LHS {
             LHS {
-                Pre_Plant_PW/State pre_ct_0{
+                Pre_PW_Plant/State pre_ct_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Plant_PW/State pre_ct_1{
+                Pre_PW_Plant/State pre_ct_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Plant_PW/Transition pre_ct_2{
+                Pre_PW_Plant/Transition pre_ct_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_ct_3{
                 Pre_Encapsulated_PetriNet/Place pre_ct_3{
@@ -232,10 +232,10 @@ A B {
                 Pre_Encapsulated_PetriNet/Place pre_ct_4{
                 Pre_Encapsulated_PetriNet/Place pre_ct_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_ct_0, pre_ct_3) {
+                Pre_PLANT2EPN_link (pre_ct_0, pre_ct_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_ct_1, pre_ct_4) {
+                Pre_PLANT2EPN_link (pre_ct_1, pre_ct_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_ct_7 {
                 Pre_Encapsulated_PetriNet/Place pre_ct_7 {
@@ -249,13 +249,13 @@ A B {
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Plant_PW/State post_ct_0{
+                Post_PW_Plant/State post_ct_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Plant_PW/State post_ct_1{
+                Post_PW_Plant/State post_ct_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Plant_PW/Transition post_ct_2{
+                Post_PW_Plant/Transition post_ct_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_ct_3{
                 Post_Encapsulated_PetriNet/Place post_ct_3{
@@ -264,10 +264,10 @@ A B {
                 Post_Encapsulated_PetriNet/Place post_ct_4{
                 Post_Encapsulated_PetriNet/Place post_ct_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Post_PLANT2EPN/link (post_ct_0, post_ct_3) {
+                Post_PLANT2EPN_link (post_ct_0, post_ct_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Post_PLANT2EPN/link (post_ct_1, post_ct_4) {
+                Post_PLANT2EPN_link (post_ct_1, post_ct_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_ct_7 {
                 Post_Encapsulated_PetriNet/Place post_ct_7 {
@@ -300,13 +300,13 @@ A B {
 
 
         {Contains} ForAll check_object {
         {Contains} ForAll check_object {
             LHS {
             LHS {
-                Pre_Plant_PW/State pre_co_0{
+                Pre_PW_Plant/State pre_co_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Plant_PW/State pre_co_1{
+                Pre_PW_Plant/State pre_co_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Plant_PW/Transition pre_co_2{
+                Pre_PW_Plant/Transition pre_co_2{
                     label = "2"
                     label = "2"
                     constraint_objPresent = $
                     constraint_objPresent = $
                         Boolean function constraint(value : String):
                         Boolean function constraint(value : String):
@@ -319,10 +319,10 @@ A B {
                 Pre_Encapsulated_PetriNet/Place pre_co_4{
                 Pre_Encapsulated_PetriNet/Place pre_co_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_co_0, pre_co_3) {
+                Pre_PLANT2EPN_link (pre_co_0, pre_co_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_co_1, pre_co_4) {
+                Pre_PLANT2EPN_link (pre_co_1, pre_co_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_co_8 {
                 Pre_Encapsulated_PetriNet/Place pre_co_8 {
@@ -362,13 +362,13 @@ A B {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Plant_PW/State post_co_0{
+                Post_PW_Plant/State post_co_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Plant_PW/State post_co_1{
+                Post_PW_Plant/State post_co_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Plant_PW/Transition post_co_2{
+                Post_PW_Plant/Transition post_co_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_co_3{
                 Post_Encapsulated_PetriNet/Place post_co_3{
@@ -377,10 +377,10 @@ A B {
                 Post_Encapsulated_PetriNet/Place post_co_4{
                 Post_Encapsulated_PetriNet/Place post_co_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Post_PLANT2EPN/link (post_co_0, post_co_3) {
+                Post_PLANT2EPN_link (post_co_0, post_co_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Post_PLANT2EPN/link (post_co_1, post_co_4) {
+                Post_PLANT2EPN_link (post_co_1, post_co_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_co_8 {
                 Post_Encapsulated_PetriNet/Place post_co_8 {
@@ -414,13 +414,13 @@ A B {
 
 
         {Contains} ForAll detect {
         {Contains} ForAll detect {
             LHS {
             LHS {
-                Pre_Plant_PW/NormalState pre_de_0{
+                Pre_PW_Plant/NormalState pre_de_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Plant_PW/ErrorState pre_de_1{
+                Pre_PW_Plant/ErrorState pre_de_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Plant_PW/Transition pre_de_2{
+                Pre_PW_Plant/Transition pre_de_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_de_3{
                 Pre_Encapsulated_PetriNet/Place pre_de_3{
@@ -429,10 +429,10 @@ A B {
                 Pre_Encapsulated_PetriNet/Place pre_de_4{
                 Pre_Encapsulated_PetriNet/Place pre_de_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_de_0, pre_de_3) {
+                Pre_PLANT2EPN_link (pre_de_0, pre_de_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_de_1, pre_de_4) {
+                Pre_PLANT2EPN_link (pre_de_1, pre_de_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Transition pre_de_7 {
                 Pre_Encapsulated_PetriNet/Transition pre_de_7 {
@@ -516,13 +516,13 @@ A B {
                     $
                     $
             }
             }
             RHS {
             RHS {
-                Post_Plant_PW/NormalState post_de_0{
+                Post_PW_Plant/NormalState post_de_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Plant_PW/ErrorState post_de_1{
+                Post_PW_Plant/ErrorState post_de_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Plant_PW/Transition post_de_2{
+                Post_PW_Plant/Transition post_de_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_de_3{
                 Post_Encapsulated_PetriNet/Place post_de_3{
@@ -531,10 +531,10 @@ A B {
                 Post_Encapsulated_PetriNet/Place post_de_4{
                 Post_Encapsulated_PetriNet/Place post_de_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Post_PLANT2EPN/link (post_de_0, post_de_3) {
+                Post_PLANT2EPN_link (post_de_0, post_de_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Post_PLANT2EPN/link (post_de_1, post_de_4) {
+                Post_PLANT2EPN_link (post_de_1, post_de_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Post_Encapsulated_PetriNet/Transition post_de_7 {
                 Post_Encapsulated_PetriNet/Transition post_de_7 {
@@ -603,13 +603,13 @@ A B {
         }
         }
         {Contains} ForAll remove_detect {
         {Contains} ForAll remove_detect {
             LHS {
             LHS {
-                Pre_Plant_PW/ErrorState pre_rd_0{
+                Pre_PW_Plant/ErrorState pre_rd_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Pre_Plant_PW/NormalState pre_rd_1{
+                Pre_PW_Plant/NormalState pre_rd_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Pre_Plant_PW/Transition pre_rd_2{
+                Pre_PW_Plant/Transition pre_rd_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Place pre_rd_3{
                 Pre_Encapsulated_PetriNet/Place pre_rd_3{
@@ -618,10 +618,10 @@ A B {
                 Pre_Encapsulated_PetriNet/Place pre_rd_4{
                 Pre_Encapsulated_PetriNet/Place pre_rd_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_rd_0, pre_rd_3) {
+                Pre_PLANT2EPN_link (pre_rd_0, pre_rd_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Pre_PLANT2EPN/link (pre_rd_1, pre_rd_4) {
+                Pre_PLANT2EPN_link (pre_rd_1, pre_rd_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
                 Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
@@ -663,13 +663,13 @@ A B {
                 }
                 }
             }
             }
             RHS {
             RHS {
-                Post_Plant_PW/NormalState post_rd_0{
+                Post_PW_Plant/NormalState post_rd_0{
                     label = "0"
                     label = "0"
                 }
                 }
-                Post_Plant_PW/ErrorState post_rd_1{
+                Post_PW_Plant/ErrorState post_rd_1{
                     label = "1"
                     label = "1"
                 }
                 }
-                Post_Plant_PW/Transition post_rd_2{
+                Post_PW_Plant/Transition post_rd_2{
                     label = "2"
                     label = "2"
                 }
                 }
                 Post_Encapsulated_PetriNet/Place post_rd_3{
                 Post_Encapsulated_PetriNet/Place post_rd_3{
@@ -678,10 +678,10 @@ A B {
                 Post_Encapsulated_PetriNet/Place post_rd_4{
                 Post_Encapsulated_PetriNet/Place post_rd_4{
                     label = "4"
                     label = "4"
                 }
                 }
-                Post_PLANT2EPN/link (post_rd_0, post_rd_3) {
+                Post_PLANT2EPN_link (post_rd_0, post_rd_3) {
                     label = "5"
                     label = "5"
                 }
                 }
-                Post_PLANT2EPN/link (post_rd_1, post_rd_4) {
+                Post_PLANT2EPN_link (post_rd_1, post_rd_4) {
                     label = "6"
                     label = "6"
                 }
                 }
                 Post_Encapsulated_PetriNet/Transition post_rd_7 {
                 Post_Encapsulated_PetriNet/Transition post_rd_7 {

+ 5 - 1
models/requirements_model.mvc

@@ -1,3 +1,7 @@
 Requirements req {
 Requirements req {
-    name = "Raise passenger window"
+    UseCase {
+        name = "Raise passenger window"
+        scope = "System-wide"
+        postconditions = "Window has stopped."
+    }
 }
 }