|
@@ -55,6 +55,7 @@ all_files = [ "pn_interface.alc",
|
|
|
"object_operations.alc",
|
|
|
"conformance_scd.alc",
|
|
|
"library.alc",
|
|
|
+ "ftg.alc",
|
|
|
"transform.alc",
|
|
|
"model_management.alc",
|
|
|
"ramify.alc",
|
|
@@ -566,245 +567,9 @@ Element function constraint(model : Element, name : String):
|
|
|
mode))
|
|
|
|
|
|
def test_po_pn_interface_model_transform_pn(self):
|
|
|
- PN_runtime = \
|
|
|
- """
|
|
|
- import models/SimpleClassDiagrams as SimpleClassDiagrams
|
|
|
-
|
|
|
- SimpleClassDiagrams 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_Runtime to models/PetriNets_Runtime
|
|
|
- """
|
|
|
-
|
|
|
- PN_model = \
|
|
|
- """
|
|
|
- import models/PetriNets_Runtime as PetriNets_Runtime
|
|
|
-
|
|
|
- PetriNets_Runtime pn {
|
|
|
- Place p1 {
|
|
|
- tokens = 1
|
|
|
- }
|
|
|
- Place p2 {
|
|
|
- tokens = 2
|
|
|
- }
|
|
|
- Place p3 {
|
|
|
- tokens = 3
|
|
|
- }
|
|
|
- Transition t1 {
|
|
|
- executing = False
|
|
|
- }
|
|
|
- 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_Runtime_SCHEDULE as PN_Transform
|
|
|
-
|
|
|
- PN_Transform s {
|
|
|
- Composite schedule {
|
|
|
- {Contains} Failure failure {}
|
|
|
- {Contains} Success success {}
|
|
|
- {Contains} Atomic mark {
|
|
|
- NAC {
|
|
|
- Pre_Transition mark_nac_t {
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_Place mark_nac_p{
|
|
|
- label = "10"
|
|
|
- }
|
|
|
- Pre_P2T (mark_nac_p, mark_nac_t){
|
|
|
- label = "11"
|
|
|
- }
|
|
|
-
|
|
|
- constraint = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Boolean function constraint(host_model : Element, mapping : Element):
|
|
|
- Integer tokens
|
|
|
- Integer weight
|
|
|
- tokens = read_attribute(host_model, mapping["10"], "tokens")
|
|
|
- weight = read_attribute(host_model, mapping["11"], "weight")
|
|
|
- log("NAC == tokens " + cast_v2s(tokens))
|
|
|
- log("NAC == weight " + cast_v2s(weight))
|
|
|
- if (tokens < weight):
|
|
|
- log("TRUE")
|
|
|
- return True!
|
|
|
- else:
|
|
|
- log("FALSE")
|
|
|
- return False!
|
|
|
- $
|
|
|
- }
|
|
|
- LHS {
|
|
|
- Pre_Transition {
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition {
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- unset_attribute(host_model, name, "executing")
|
|
|
- instantiate_attribute(host_model, name, "executing", True)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} ForAll consume {
|
|
|
- LHS {
|
|
|
- Pre_Transition lhs_consume_t{
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- Pre_Place lhs_consume_p{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition rhs_consume_t {
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_Place rhs_consume_p {
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- Integer tokens
|
|
|
- Integer weight
|
|
|
- tokens = read_attribute(host_model, name, "tokens")
|
|
|
- weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
- unset_attribute(host_model, name, "tokens")
|
|
|
- instantiate_attribute(host_model, name, "tokens", tokens - weight)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- Post_P2T (rhs_consume_p, rhs_consume_t){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} ForAll produce {
|
|
|
- LHS {
|
|
|
- Pre_Transition lhs_produce_t{
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- Pre_Place lhs_produce_p{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_T2P (lhs_produce_t, lhs_produce_p){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition rhs_produce_t{
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_Place rhs_produce_p{
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- Integer tokens
|
|
|
- Integer weight
|
|
|
- tokens = read_attribute(host_model, name, "tokens")
|
|
|
- weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
- unset_attribute(host_model, name, "tokens")
|
|
|
- instantiate_attribute(host_model, name, "tokens", tokens + weight)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- Post_T2P (rhs_produce_t, rhs_produce_p){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} Atomic unmark_transition {
|
|
|
- LHS {
|
|
|
- Pre_Transition {
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition {
|
|
|
- label = "0"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- unset_attribute(host_model, name, "executing")
|
|
|
- instantiate_attribute(host_model, name, "executing", False)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- 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
|
|
|
- """
|
|
|
+ PN_runtime = open("integration/code/pn_runtime.mvc", "r").read()
|
|
|
+ PN_model = open("integration/code/pn_runtime_model.mvc", "r").read()
|
|
|
+ schedule_model = open("integration/code/pn_simulate.mvc", "r").read()
|
|
|
|
|
|
self.assertTrue(run_file(all_files,
|
|
|
get_model_constructor(PN_runtime) + [
|
|
@@ -815,7 +580,7 @@ Element function constraint(model : Element, name : String):
|
|
|
"read", "p2",
|
|
|
"read", "p3",
|
|
|
"exit",
|
|
|
- "ramify", "PetriNets_Runtime_SCHEDULE", "PetriNets_Runtime",
|
|
|
+ "ramify", "RAM_PetriNets_Runtime", "PetriNets_Runtime",
|
|
|
] + get_model_constructor(schedule_model) + [
|
|
|
"transform", "pn", "pn_simulate",
|
|
|
"transform", "pn", "pn_simulate",
|
|
@@ -847,480 +612,17 @@ Element function constraint(model : Element, name : String):
|
|
|
"PO"))
|
|
|
|
|
|
def test_po_pn_interface_transform_pn_to_runtime(self):
|
|
|
- PN_runtime = \
|
|
|
- """
|
|
|
- import models/SimpleClassDiagrams as SimpleClassDiagrams
|
|
|
-
|
|
|
- SimpleClassDiagrams PetriNets_Design{
|
|
|
- Class Natural {}
|
|
|
- Class Place {
|
|
|
- tokens : Natural
|
|
|
- }
|
|
|
- Class Transition {}
|
|
|
- Association P2T (Place, Transition) {
|
|
|
- weight : Natural
|
|
|
- }
|
|
|
- Association T2P (Transition, Place) {
|
|
|
- weight : Natural
|
|
|
- }
|
|
|
- }
|
|
|
-
|
|
|
- SimpleClassDiagrams PetriNets_Runtime{
|
|
|
- Class Natural {}
|
|
|
- Class Boolean {}
|
|
|
- Class String {}
|
|
|
- Class Place {
|
|
|
- tokens : Natural
|
|
|
- name : String
|
|
|
- }
|
|
|
- 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_annotate = \
|
|
|
- """
|
|
|
- import models/RAM_PetriNets_Design_Runtime as RAM_PN_DR
|
|
|
-
|
|
|
- RAM_PN_DR 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_SOURCE_Place {
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_SOURCE_Place cp1 {
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_TARGET_Place cp2 {
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- instantiate_attribute(host_model, name, "tokens", read_attribute(host_model, mapping["0"], "tokens"))
|
|
|
- instantiate_attribute(host_model, name, "name", mapping["0"])
|
|
|
- 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_SOURCE_Place rhs_cp2t_p{
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_SOURCE_Transition rhs_cp2t_t{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Post_SOURCE_P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- Post_TARGET_Place rhs_cp2t_p2 {
|
|
|
- label = "3"
|
|
|
- }
|
|
|
- Post_TARGET_Transition rhs_cp2t_t2 {
|
|
|
- label = "4"
|
|
|
- }
|
|
|
- Post_PlaceLink (rhs_cp2t_p, rhs_cp2t_p2){
|
|
|
- label = "5"
|
|
|
- }
|
|
|
- Post_TransitionLink (rhs_cp2t_t, rhs_cp2t_t2){
|
|
|
- label = "6"
|
|
|
- }
|
|
|
- Post_TARGET_P2T rhs_cp2t_p2t2(rhs_cp2t_p2, rhs_cp2t_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!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} ForAll copy_T2P {
|
|
|
- LHS {
|
|
|
- Pre_SOURCE_Place ct2p_p{
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Pre_SOURCE_Transition ct2p_t{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_SOURCE_T2P (ct2p_t, ct2p_p){
|
|
|
- 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 rhs_ct2p_p{
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_SOURCE_Transition rhs_ct2p_t{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Post_SOURCE_T2P (rhs_ct2p_t, rhs_ct2p_p){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- Post_TARGET_Place rhs_ct2p_p2 {
|
|
|
- label = "3"
|
|
|
- }
|
|
|
- Post_TARGET_Transition rhs_ct2p_t2 {
|
|
|
- label = "4"
|
|
|
- }
|
|
|
- Post_PlaceLink (rhs_ct2p_p, rhs_ct2p_p2){
|
|
|
- label = "5"
|
|
|
- }
|
|
|
- Post_TransitionLink (rhs_ct2p_t, rhs_ct2p_t2){
|
|
|
- label = "6"
|
|
|
- }
|
|
|
- Post_TARGET_T2P (rhs_ct2p_t2, rhs_ct2p_p2) {
|
|
|
- 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 (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 annotate to models/pn_annotate
|
|
|
- """
|
|
|
+ PN_runtime = open("integration/code/pn_runtime.mvc", "r").read()
|
|
|
+ PN_design = open("integration/code/pn_design.mvc", "r").read()
|
|
|
+ PN_model = open("integration/code/pn_design_model.mvc", "r").read()
|
|
|
+ schedule_model_annotate = open("integration/code/pn_design_to_runtime.mvc", "r").read()
|
|
|
+ schedule_model_print = open("integration/code/pn_print.mvc", "r").read()
|
|
|
+ schedule_model_simulate = open("integration/code/pn_simulate.mvc", "r").read()
|
|
|
|
|
|
- schedule_model_print = \
|
|
|
- """
|
|
|
- import models/RAM_PetriNets_Runtime as RAM_PN_R
|
|
|
-
|
|
|
- RAM_PN_R print {
|
|
|
- Composite schedule {
|
|
|
- {Contains} Success success {}
|
|
|
- {Contains} ForAll print_tokens {
|
|
|
- LHS {
|
|
|
- Pre_Place {
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Place {
|
|
|
- label = "0"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- output((cast_v2s(read_attribute(host_model, name, "name")) + " --> ") + cast_v2s(read_attribute(host_model, name, "tokens")))
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- OnSuccess (print_tokens, success) {}
|
|
|
- OnFailure (print_tokens, success) {}
|
|
|
- Initial (schedule, print_tokens) {}
|
|
|
- }
|
|
|
-
|
|
|
- export print to models/pn_print
|
|
|
- """
|
|
|
-
|
|
|
- schedule_model_simulate = \
|
|
|
- """
|
|
|
- import models/RAM_PetriNets_Runtime as RAM_PN_R
|
|
|
-
|
|
|
- RAM_PN_R s {
|
|
|
- Composite schedule {
|
|
|
- {Contains} Failure failure {}
|
|
|
- {Contains} Success success {}
|
|
|
- {Contains} Atomic mark {
|
|
|
- LHS {
|
|
|
- Pre_Transition {
|
|
|
- label = "1"
|
|
|
- constraint = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- include "object_operations.alh"
|
|
|
- Boolean function constraint(host_model : Element, name : String):
|
|
|
- Element links
|
|
|
- String link
|
|
|
- String place
|
|
|
- links = allIncomingAssociationInstances(host_model, name, "P2T")
|
|
|
- while (read_nr_out(links) > 0):
|
|
|
- link = set_pop(links)
|
|
|
- place = readAssociationSource(host_model, link)
|
|
|
- if (integer_lt(read_attribute(host_model, place, "tokens"), read_attribute(host_model, link, "weight"))):
|
|
|
- return False!
|
|
|
- return True!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition {
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- unset_attribute(host_model, name, "executing")
|
|
|
- instantiate_attribute(host_model, name, "executing", True)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} ForAll consume {
|
|
|
- LHS {
|
|
|
- Pre_Transition lhs_consume_t{
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- Pre_Place lhs_consume_p{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition rhs_consume_t {
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_Place rhs_consume_p {
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- Integer tokens
|
|
|
- Integer weight
|
|
|
- tokens = read_attribute(host_model, name, "tokens")
|
|
|
- weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
- unset_attribute(host_model, name, "tokens")
|
|
|
- instantiate_attribute(host_model, name, "tokens", tokens - weight)
|
|
|
- log("Consume for " + cast_v2s(read_attribute(host_model, name, "name")))
|
|
|
- log("Previous: " + cast_v2s(tokens))
|
|
|
- log("Now: " + cast_v2s(tokens - weight))
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- Post_P2T (rhs_consume_p, rhs_consume_t){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} ForAll produce {
|
|
|
- LHS {
|
|
|
- Pre_Transition lhs_produce_t{
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- Pre_Place lhs_produce_p{
|
|
|
- label = "1"
|
|
|
- }
|
|
|
- Pre_T2P (lhs_produce_t, lhs_produce_p){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition rhs_produce_t{
|
|
|
- label = "0"
|
|
|
- }
|
|
|
- Post_Place rhs_produce_p{
|
|
|
- label = "1"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- Integer tokens
|
|
|
- Integer weight
|
|
|
- tokens = read_attribute(host_model, name, "tokens")
|
|
|
- weight = read_attribute(host_model, mapping["2"], "weight")
|
|
|
- unset_attribute(host_model, name, "tokens")
|
|
|
- instantiate_attribute(host_model, name, "tokens", tokens + weight)
|
|
|
- log("Produce for " + cast_v2s(read_attribute(host_model, name, "name")))
|
|
|
- log("Previous: " + cast_v2s(tokens))
|
|
|
- log("Now: " + cast_v2s(tokens + weight))
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- Post_T2P (rhs_produce_t, rhs_produce_p){
|
|
|
- label = "2"
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- {Contains} Atomic unmark_transition {
|
|
|
- LHS {
|
|
|
- Pre_Transition {
|
|
|
- label = "0"
|
|
|
- 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, "executing"), True)!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- RHS {
|
|
|
- Post_Transition {
|
|
|
- label = "0"
|
|
|
- action = $
|
|
|
- include "primitives.alh"
|
|
|
- include "modelling.alh"
|
|
|
- Void function action(host_model : Element, name : String, mapping : Element):
|
|
|
- unset_attribute(host_model, name, "executing")
|
|
|
- instantiate_attribute(host_model, name, "executing", False)
|
|
|
- return!
|
|
|
- $
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- }
|
|
|
- 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_design) + \
|
|
|
get_model_constructor(PN_model) + [
|
|
|
"unify", "PetriNets_Design_to_Runtime", "PetriNets_Design", "SOURCE_", "PetriNets_Runtime", "TARGET_",
|
|
|
"join", "pn", "PetriNets_Design_to_Runtime", "SOURCE_",
|
|
@@ -1339,7 +641,7 @@ Element function constraint(model : Element, name : String):
|
|
|
"transform", "pn", "pn_simulate",
|
|
|
"transform", "pn", "pn_print",
|
|
|
],
|
|
|
- greeting + prompt * 3 +
|
|
|
+ greeting + prompt * 4 +
|
|
|
unify + prompt +
|
|
|
join + prompt +
|
|
|
load + loaded +
|
|
@@ -1358,3 +660,16 @@ Element function constraint(model : Element, name : String):
|
|
|
transform + [set(['"p1" --> 0', '"p2" --> 1', '"p3" --> 5'])] + transform_result_true + prompt
|
|
|
,
|
|
|
"PO"))
|
|
|
+
|
|
|
+ def test_po_pn_interface_ftg(self):
|
|
|
+ self.pn_interface_ftg("PO")
|
|
|
+
|
|
|
+ def pn_interface_ftg(self, mode):
|
|
|
+ self.assertTrue(run_file(all_files,
|
|
|
+ ["generate_ftg", "generated_ftg",
|
|
|
+ "load", "generated_ftg",
|
|
|
+ "list",
|
|
|
+ "verify",
|
|
|
+ ],
|
|
|
+ None,
|
|
|
+ mode))
|