|
|
@@ -31,6 +31,7 @@ all_files = [ "pn_interface.alc",
|
|
|
"conformance_scd.alc",
|
|
|
"library.alc",
|
|
|
"transform.alc",
|
|
|
+ "model_management.alc",
|
|
|
"ramify.alc",
|
|
|
"metamodels.alc",
|
|
|
"random.alc",
|
|
|
@@ -971,7 +972,7 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
- {Contains} Atomic consume {
|
|
|
+ {Contains} ForAll consume {
|
|
|
LHS {
|
|
|
Pre_Transition lhs_consume_t{
|
|
|
label = "0"
|
|
|
@@ -985,13 +986,6 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
}
|
|
|
Pre_Place lhs_consume_p{
|
|
|
label = "1"
|
|
|
- constraint = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Boolean function constraint(host_model : Element, name : String):
|
|
|
- // Check if this node is executing currently
|
|
|
- return value_eq(read_attribute(host_model, name, "executed"), False)!
|
|
|
- $
|
|
|
}
|
|
|
Pre_P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
|
|
|
label = "2"
|
|
|
@@ -1013,8 +1007,6 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
unset_attribute(host_model, name, "tokens")
|
|
|
instantiate_attribute(host_model, name, "tokens", tokens - weight)
|
|
|
- unset_attribute(host_model, name, "executed")
|
|
|
- instantiate_attribute(host_model, name, "executed", True)
|
|
|
return!
|
|
|
$
|
|
|
}
|
|
|
@@ -1023,7 +1015,7 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
- {Contains} Atomic produce {
|
|
|
+ {Contains} ForAll produce {
|
|
|
LHS {
|
|
|
Pre_Transition lhs_produce_t{
|
|
|
label = "0"
|
|
|
@@ -1037,13 +1029,6 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
}
|
|
|
Pre_Place lhs_produce_p{
|
|
|
label = "1"
|
|
|
- constraint = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Boolean function constraint(host_model : Element, name : String):
|
|
|
- // Check if this node is executing currently
|
|
|
- return value_eq(read_attribute(host_model, name, "executed"), False)!
|
|
|
- $
|
|
|
}
|
|
|
Pre_T2P (lhs_produce_t, lhs_produce_p){
|
|
|
label = "2"
|
|
|
@@ -1065,8 +1050,6 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
unset_attribute(host_model, name, "tokens")
|
|
|
instantiate_attribute(host_model, name, "tokens", tokens + weight)
|
|
|
- unset_attribute(host_model, name, "executed")
|
|
|
- instantiate_attribute(host_model, name, "executed", True)
|
|
|
return!
|
|
|
$
|
|
|
}
|
|
|
@@ -1102,57 +1085,309 @@ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
- {Contains} Atomic unmark_place {
|
|
|
+ }
|
|
|
+ OnSuccess (mark, consume) {}
|
|
|
+ OnFailure (mark, failure) {}
|
|
|
+ OnSuccess (consume, produce) {}
|
|
|
+ OnFailure (consume, produce) {}
|
|
|
+ OnSuccess (produce, unmark_transition) {}
|
|
|
+ OnFailure (produce, unmark_transition) {}
|
|
|
+ OnSuccess (unmark_transition, success) {}
|
|
|
+ OnFailure (unmark_transition, failure) {}
|
|
|
+ Initial (schedule, mark) {}
|
|
|
+ }
|
|
|
+
|
|
|
+ export s to models/pn_simulate
|
|
|
+ """
|
|
|
+
|
|
|
+ self.assertTrue(run_file(all_files,
|
|
|
+ get_model_constructor(PN_runtime) + \
|
|
|
+ get_model_constructor(PN_model) + [
|
|
|
+ "ramify", "PetriNets_Runtime_SCHEDULE", "PetriNets_Runtime",
|
|
|
+ ] + get_model_constructor(schedule_model) + [
|
|
|
+ "transform", "pn", "pn_simulate",
|
|
|
+ "load", "pn",
|
|
|
+ "list",
|
|
|
+ "verify",
|
|
|
+ "read", "t1",
|
|
|
+ "read", "p1",
|
|
|
+ "read", "p2",
|
|
|
+ "read", "p3",
|
|
|
+ "exit",
|
|
|
+ ],
|
|
|
+ None, "PO"))
|
|
|
+
|
|
|
+ def test_po_pn_interface_transform_pn_to_runtime(self):
|
|
|
+ PN_runtime = \
|
|
|
+ """
|
|
|
+ import models/SimpleClassDiagrams as SimpleClassDiagrams
|
|
|
+
|
|
|
+ SimpleClassDiagrams (Inheritance) PetriNets_Design{
|
|
|
+ Class Natural {}
|
|
|
+ Class Place {
|
|
|
+ tokens : Natural
|
|
|
+ }
|
|
|
+ Class Transition {}
|
|
|
+ Association P2T (Place, Transition) {
|
|
|
+ weight : Natural
|
|
|
+ }
|
|
|
+ Association T2P (Transition, Place) {
|
|
|
+ weight : Natural
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ SimpleClassDiagrams (Inheritance) PetriNets_Runtime{
|
|
|
+ Class Natural {}
|
|
|
+ Class Boolean {}
|
|
|
+ Class Place {
|
|
|
+ tokens : Natural
|
|
|
+ }
|
|
|
+ Class Transition {
|
|
|
+ executing : Boolean
|
|
|
+ }
|
|
|
+ Association P2T (Place, Transition) {
|
|
|
+ weight : Natural
|
|
|
+ }
|
|
|
+ Association T2P (Transition, Place) {
|
|
|
+ weight : Natural
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ export PetriNets_Design to models/PetriNets_Design
|
|
|
+ export PetriNets_Runtime to models/PetriNets_Runtime
|
|
|
+ """
|
|
|
+
|
|
|
+ PN_model = \
|
|
|
+ """
|
|
|
+ import models/PetriNets_Design as PetriNets
|
|
|
+
|
|
|
+ PetriNets pn {
|
|
|
+ Place p1 {
|
|
|
+ tokens = 1
|
|
|
+ }
|
|
|
+ Place p2 {
|
|
|
+ tokens = 2
|
|
|
+ }
|
|
|
+ Place p3 {
|
|
|
+ tokens = 3
|
|
|
+ }
|
|
|
+ Transition t1 {}
|
|
|
+ P2T (p1, t1) {
|
|
|
+ weight = 1
|
|
|
+ }
|
|
|
+ P2T (p2, t1) {
|
|
|
+ weight = 1
|
|
|
+ }
|
|
|
+ T2P (t1, p3) {
|
|
|
+ weight = 2
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ export pn to models/pn
|
|
|
+ """
|
|
|
+
|
|
|
+ schedule_model = \
|
|
|
+ """
|
|
|
+ import models/PetriNets_SCHEDULE as PN_Transform
|
|
|
+
|
|
|
+ PN_Transform annotate {
|
|
|
+ Composite schedule {
|
|
|
+ {Contains} Failure failure {}
|
|
|
+ {Contains} Success success {}
|
|
|
+ {Contains} ForAll copy_transitions {
|
|
|
+ LHS {
|
|
|
+ Pre_SOURCE_Transition {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_SOURCE_Transition ct1 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_TARGET_Transition ct2 {
|
|
|
+ label = "1"
|
|
|
+ action = $
|
|
|
+ include "primitives.alh"
|
|
|
+ include "modelling.alh"
|
|
|
+ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
+ instantiate_attribute(host_model, name, "executing", False)
|
|
|
+ return!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_TransitionLink (ct1, ct2){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ {Contains} ForAll copy_places {
|
|
|
LHS {
|
|
|
- Pre_Place {
|
|
|
+ Pre_SOURCE_Place {
|
|
|
label = "0"
|
|
|
- constraint = $
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_SOURCE_Place cp1 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_TARGET_Place cp2 {
|
|
|
+ label = "1"
|
|
|
+ action = $
|
|
|
include "primitives.alh"
|
|
|
include "modelling.alh"
|
|
|
- Boolean function constraint(host_model : Element, name : String):
|
|
|
- // Check if this node is executing currently
|
|
|
- return value_eq(read_attribute(host_model, name, "executed"), True)!
|
|
|
+ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
+ instantiate_attribute(host_model, name, "tokens", read_attribute(host_model, mapping["0"], "tokens"))
|
|
|
+ return!
|
|
|
$
|
|
|
}
|
|
|
+ Post_PlaceLink (cp1, cp2){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ {Contains} ForAll copy_P2T {
|
|
|
+ LHS {
|
|
|
+ Pre_SOURCE_Place cp2t_p{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_SOURCE_Transition cp2t_t{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_SOURCE_P2T (cp2t_p, cp2t_t){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_TARGET_Place cp2t_p2{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_TARGET_Transition cp2t_t2{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PlaceLink (cp2t_p, cp2t_p2){
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_TransitionLink (cp2t_t, cp2t_t2){
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_Place {
|
|
|
+ Post_SOURCE_Place cp2t_p{
|
|
|
label = "0"
|
|
|
+ }
|
|
|
+ Post_SOURCE_Transition cp2t_t{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_SOURCE_P2T cp2t_p2t (cp2t_p, cp2t_t){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_TARGET_Place cp2t_p2 {
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_TARGET_Transition cp2t_t2 {
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PlaceLink (cp2t_p, cp2t_p2){
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_TransitionLink (cp2t_t, cp2t_t2){
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_TARGET_P2T cp2t_p2t2(cp2t_p2, cp2t_t2) {
|
|
|
+ label = "7"
|
|
|
action = $
|
|
|
include "primitives.alh"
|
|
|
include "modelling.alh"
|
|
|
Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- unset_attribute(host_model, name, "executed")
|
|
|
- instantiate_attribute(host_model, name, "executed", False)
|
|
|
+ instantiate_attribute(host_model, name, "weight", read_attribute(host_model, mapping["2"], "weight"))
|
|
|
+ return!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ {Contains} ForAll copy_T2P {
|
|
|
+ LHS {
|
|
|
+ Pre_SOURCE_Place ct2p_p{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_SOURCE_Transition ct2p_t{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_SOURCE_T2P (ct2p_p, ct2p_t){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Pre_TARGET_Place ct2p_p2{
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Pre_TARGET_Transition ct2p_t2{
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Pre_PlaceLink (ct2p_p, ct2p_p2){
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Pre_TransitionLink (ct2p_t, ct2p_t2){
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_SOURCE_Place ct2p_p{
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_SOURCE_Transition ct2p_t{
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_SOURCE_T2P (ct2p_p, ct2p_t){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ Post_TARGET_Place ct2p_p2 {
|
|
|
+ label = "3"
|
|
|
+ }
|
|
|
+ Post_TARGET_Transition ct2p_t2 {
|
|
|
+ label = "4"
|
|
|
+ }
|
|
|
+ Post_PlaceLink (ct2p_p, ct2p_p2){
|
|
|
+ label = "5"
|
|
|
+ }
|
|
|
+ Post_TransitionLink (ct2p_t, ct2p_t2){
|
|
|
+ label = "6"
|
|
|
+ }
|
|
|
+ Post_TARGET_T2P (ct2p_p2, ct2p_t2) {
|
|
|
+ label = "7"
|
|
|
+ action = $
|
|
|
+ include "primitives.alh"
|
|
|
+ include "modelling.alh"
|
|
|
+ Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
+ instantiate_attribute(host_model, name, "weight", read_attribute(host_model, mapping["2"], "weight"))
|
|
|
return!
|
|
|
$
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
-
|
|
|
}
|
|
|
- OnSuccess (mark, consume) {}
|
|
|
- OnFailure (mark, failure) {}
|
|
|
- OnSuccess (consume, consume) {}
|
|
|
- OnFailure (consume, produce) {}
|
|
|
- OnSuccess (produce, produce) {}
|
|
|
- OnFailure (produce, unmark_transition) {}
|
|
|
- OnSuccess (unmark_transition, unmark_place) {}
|
|
|
- OnFailure (unmark_transition, failure) {}
|
|
|
- OnSuccess (unmark_place, unmark_place) {}
|
|
|
- OnFailure (unmark_place, success) {}
|
|
|
- Initial (schedule, mark) {}
|
|
|
+ OnSuccess (copy_places, copy_transitions) {}
|
|
|
+ OnSuccess (copy_transitions, copy_P2T) {}
|
|
|
+ OnSuccess (copy_P2T, copy_T2P) {}
|
|
|
+ OnSuccess (copy_T2P, success) {}
|
|
|
+ OnFailure (copy_places, copy_transitions) {}
|
|
|
+ OnFailure (copy_transitions, copy_P2T) {}
|
|
|
+ OnFailure (copy_P2T, copy_T2P) {}
|
|
|
+ OnFailure (copy_T2P, success) {}
|
|
|
+ Initial (schedule, copy_places) {}
|
|
|
}
|
|
|
|
|
|
- export s to models/pn_simulate
|
|
|
+ export annotate to models/pn_annotate
|
|
|
"""
|
|
|
|
|
|
self.assertTrue(run_file(all_files,
|
|
|
get_model_constructor(PN_runtime) + \
|
|
|
get_model_constructor(PN_model) + [
|
|
|
- "ramify", "PetriNets_Runtime_SCHEDULE", "in", "PetriNets_Runtime",
|
|
|
+ "unify", "PetriNets_Design_to_Runtime", "PetriNets_Design", "SOURCE_", "PetriNets_Runtime", "TARGET_",
|
|
|
+ "join", "pn", "PetriNets_Design_to_Runtime", "SOURCE_",
|
|
|
+ "load", "PetriNets_Design_to_Runtime",
|
|
|
+ "instantiate", "Association", "PlaceLink", "SOURCE_Place", "TARGET_Place",
|
|
|
+ "instantiate", "Association", "TransitionLink", "SOURCE_Transition", "TARGET_Transition",
|
|
|
+ "exit",
|
|
|
+ "ramify", "PetriNets_SCHEDULE", "PetriNets_Design_to_Runtime",
|
|
|
] + get_model_constructor(schedule_model) + [
|
|
|
- "transform", "pn", "pn_simulate",
|
|
|
+ "transform", "pn", "pn_annotate",
|
|
|
+ "split", "pn", "PetriNets_Runtime", "TARGET/",
|
|
|
"load", "pn",
|
|
|
"list",
|
|
|
"verify",
|
