pn_simulate.mvc 7.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181
  1. import models/RAM_PetriNets_Runtime_Runtime as RAM_PN_R
  2. RAM_PN_R s {
  3. Composite schedule {
  4. {Contains} Failure failure {}
  5. {Contains} Success success {}
  6. {Contains} Atomic mark {
  7. LHS {
  8. Pre_PetriNets_Runtime/Transition {
  9. label = "1"
  10. }
  11. }
  12. NAC {
  13. Pre_PetriNets_Runtime/Transition mark_nac_t {
  14. label = "1"
  15. }
  16. Pre_PetriNets_Runtime/Place mark_nac_p{
  17. label = "10"
  18. }
  19. Pre_PetriNets_Runtime/P2T (mark_nac_p, mark_nac_t){
  20. label = "11"
  21. }
  22. constraint = $
  23. include "primitives.alh"
  24. include "modelling.alh"
  25. Boolean function constraint(host_model : Element, mapping : Element):
  26. Integer tokens
  27. Integer weight
  28. tokens = read_attribute(host_model, mapping["10"], "tokens")
  29. weight = read_attribute(host_model, mapping["11"], "weight")
  30. return (tokens < weight)!
  31. $
  32. }
  33. RHS {
  34. Post_PetriNets_Runtime/Transition {
  35. label = "1"
  36. action = $
  37. include "primitives.alh"
  38. include "modelling.alh"
  39. Void function action(host_model : Element, name : String, mapping : Element):
  40. log("MARK " + name)
  41. unset_attribute(host_model, name, "executing")
  42. instantiate_attribute(host_model, name, "executing", True)
  43. return!
  44. $
  45. }
  46. }
  47. }
  48. {Contains} ForAll consume {
  49. LHS {
  50. Pre_PetriNets_Runtime/Transition lhs_consume_t{
  51. label = "0"
  52. constraint = $
  53. include "primitives.alh"
  54. include "modelling.alh"
  55. Boolean function constraint(host_model : Element, name : String):
  56. // Check if this node is executing currently
  57. return value_eq(read_attribute(host_model, name, "executing"), True)!
  58. $
  59. }
  60. Pre_PetriNets_Runtime/Place lhs_consume_p{
  61. label = "1"
  62. }
  63. Pre_PetriNets_Runtime/P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
  64. label = "2"
  65. }
  66. }
  67. RHS {
  68. Post_PetriNets_Runtime/Transition rhs_consume_t {
  69. label = "0"
  70. }
  71. Post_PetriNets_Runtime/Place rhs_consume_p {
  72. label = "1"
  73. action = $
  74. include "primitives.alh"
  75. include "modelling.alh"
  76. Void function action(host_model : Element, name : String, mapping : Element):
  77. Integer tokens
  78. Integer weight
  79. tokens = read_attribute(host_model, name, "tokens")
  80. weight = read_attribute(host_model, mapping["2"], "weight")
  81. unset_attribute(host_model, name, "tokens")
  82. instantiate_attribute(host_model, name, "tokens", tokens - weight)
  83. log("Consume for " + cast_v2s(read_attribute(host_model, name, "name")))
  84. log("Previous: " + cast_v2s(tokens))
  85. log("Now: " + cast_v2s(tokens - weight))
  86. return!
  87. $
  88. }
  89. Post_PetriNets_Runtime/P2T (rhs_consume_p, rhs_consume_t){
  90. label = "2"
  91. }
  92. }
  93. }
  94. {Contains} ForAll produce {
  95. LHS {
  96. Pre_PetriNets_Runtime/Transition lhs_produce_t{
  97. label = "0"
  98. constraint = $
  99. include "primitives.alh"
  100. include "modelling.alh"
  101. Boolean function constraint(host_model : Element, name : String):
  102. // Check if this node is executing currently
  103. return value_eq(read_attribute(host_model, name, "executing"), True)!
  104. $
  105. }
  106. Pre_PetriNets_Runtime/Place lhs_produce_p{
  107. label = "1"
  108. }
  109. Pre_PetriNets_Runtime/T2P (lhs_produce_t, lhs_produce_p){
  110. label = "2"
  111. }
  112. }
  113. RHS {
  114. Post_PetriNets_Runtime/Transition rhs_produce_t{
  115. label = "0"
  116. }
  117. Post_PetriNets_Runtime/Place rhs_produce_p{
  118. label = "1"
  119. action = $
  120. include "primitives.alh"
  121. include "modelling.alh"
  122. Void function action(host_model : Element, name : String, mapping : Element):
  123. Integer tokens
  124. Integer weight
  125. tokens = read_attribute(host_model, name, "tokens")
  126. weight = read_attribute(host_model, mapping["2"], "weight")
  127. unset_attribute(host_model, name, "tokens")
  128. instantiate_attribute(host_model, name, "tokens", tokens + weight)
  129. log("Produce for " + cast_v2s(read_attribute(host_model, name, "name")))
  130. log("Previous: " + cast_v2s(tokens))
  131. log("Now: " + cast_v2s(tokens + weight))
  132. return!
  133. $
  134. }
  135. Post_PetriNets_Runtime/T2P (rhs_produce_t, rhs_produce_p){
  136. label = "2"
  137. }
  138. }
  139. }
  140. {Contains} Atomic unmark_transition {
  141. LHS {
  142. Pre_PetriNets_Runtime/Transition {
  143. label = "0"
  144. constraint = $
  145. include "primitives.alh"
  146. include "modelling.alh"
  147. Boolean function constraint(host_model : Element, name : String):
  148. // Check if this node is executing currently
  149. return value_eq(read_attribute(host_model, name, "executing"), True)!
  150. $
  151. }
  152. }
  153. RHS {
  154. Post_PetriNets_Runtime/Transition {
  155. label = "0"
  156. action = $
  157. include "primitives.alh"
  158. include "modelling.alh"
  159. Void function action(host_model : Element, name : String, mapping : Element):
  160. unset_attribute(host_model, name, "executing")
  161. instantiate_attribute(host_model, name, "executing", False)
  162. return!
  163. $
  164. }
  165. }
  166. }
  167. }
  168. OnSuccess (mark, consume) {}
  169. OnFailure (mark, failure) {}
  170. OnSuccess (consume, produce) {}
  171. OnFailure (consume, produce) {}
  172. OnSuccess (produce, unmark_transition) {}
  173. OnFailure (produce, unmark_transition) {}
  174. OnSuccess (unmark_transition, success) {}
  175. OnFailure (unmark_transition, failure) {}
  176. Initial (schedule, mark) {}
  177. }
  178. export s to models/pn_simulate