environment_to_EPN.mvc 4.2 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121
  1. include "primitives.alh"
  2. include "modelling.alh"
  3. include "object_operations.alh"
  4. A B {
  5. Composite schedule {
  6. {Contains} Success success {}
  7. {Contains} Failure failure {}
  8. {Contains} ForAll create_ports {
  9. LHS {
  10. Pre_Environment_PW/Event {
  11. label = "1"
  12. }
  13. }
  14. RHS {
  15. Post_Environment_PW/Event {
  16. label = "1"
  17. }
  18. Post_Encapsulated_PetriNet/Place cp_place {
  19. label = "2"
  20. value_name = $
  21. String function value(model : Element, name : String, mapping : Element):
  22. return read_attribute(model, mapping["0"], "name")!
  23. $
  24. }
  25. Post_Encapsulated_PetriNet/Port cp_port {
  26. label = "3"
  27. value_name = $
  28. String function value(model : Element, name : String, mapping : Element):
  29. return read_attribute(model, mapping["0"], "name")!
  30. $
  31. }
  32. Post_ENV2EPN_link (cp_evt, cp_place) {
  33. label = "4"
  34. }
  35. Post_Encapsulated_PetriNet/PortPlace (cp_port, cp_place) {
  36. label = "5"
  37. value_tokens = $
  38. Integer function value(model : Element, name : String, mapping : Element):
  39. return 0!
  40. $
  41. }
  42. }
  43. }
  44. {Contains} ForAll create_switches {
  45. LHS {
  46. Pre_Environment_PW/Group pre_grp {
  47. label = "1"
  48. }
  49. Pre_Environment_PW/Event pre_evt_a {
  50. label = "2"
  51. }
  52. Pre_Environment_PW/Event pre_evt_b {
  53. label = "3"
  54. }
  55. Pre_Environment_PW/Contains (pre_grp, pre_evt_a) {
  56. label = "4"
  57. }
  58. Pre_Environment_PW/Contains (pre_grp, pre_evt_b) {
  59. label = "5"
  60. }
  61. Pre_ENV2EPN_link (pre_evt_a, pre_place_a) {
  62. label = "6"
  63. }
  64. Pre_ENV2EPN_link (pre_evt_b, pre_place_b) {
  65. label = "7"
  66. }
  67. Pre_Encapsulated_PetriNet/Place pre_place_a {
  68. label = "8"
  69. }
  70. Pre_Encapsulated_PetriNet/Place pre_place_b {
  71. label = "9"
  72. }
  73. }
  74. RHS {
  75. Post_Environment_PW/Group post_grp {
  76. label = "1"
  77. }
  78. Post_Environment_PW/Event post_evt_a {
  79. label = "2"
  80. }
  81. Post_Environment_PW/Event post_evt_b {
  82. label = "3"
  83. }
  84. Post_Environment_PW/Contains (post_grp, post_evt_a) {
  85. label = "4"
  86. }
  87. Post_Environment_PW/Contains (post_grp, post_evt_b) {
  88. label = "5"
  89. }
  90. Post_ENV2EPN_link (post_evt_a, post_place_a) {
  91. label = "6"
  92. }
  93. Post_ENV2EPN_link (post_evt_b, post_place_b) {
  94. label = "7"
  95. }
  96. Post_Encapsulated_PetriNet/Place post_place_a {
  97. label = "8"
  98. }
  99. Post_Encapsulated_PetriNet/Place post_place_b {
  100. label = "9"
  101. }
  102. Post_Encapsulated_PetriNet/P2T (post_place_a, post_transition) {
  103. label = "10"
  104. }
  105. Post_Encapsulated_PetriNet/T2P (post_transition, post_place_b) {
  106. label = "11"
  107. }
  108. Post_Encapsulated_PetriNet/Transition post_transition {
  109. label = "12"
  110. }
  111. }
  112. }
  113. }
  114. Initial (schedule, create_ports) {}
  115. OnSuccess (create_ports, create_switches) {}
  116. OnSuccess (create_switches, success) {}
  117. OnFailure (create_ports, failure) {}
  118. OnFailure (create_switches, failure) {}
  119. }