combine_EPN.mvc 13 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432
  1. include "primitives.alh"
  2. include "modelling.alh"
  3. include "object_operations.alh"
  4. Composite schedule {
  5. {Contains} Success success {}
  6. {Contains} Failure failure {}
  7. {Contains} ForAll link {
  8. LHS {
  9. Pre_Architecture/Group pre_l_0{
  10. label = "0"
  11. }
  12. Pre_Architecture/Port pre_l_1{
  13. label = "1"
  14. }
  15. Pre_Architecture/Contains pre_l_10 (pre_l_0, pre_l_1){
  16. label = "10"
  17. }
  18. Pre_Encapsulated_PetriNet/Port pre_l_2{
  19. label = "2"
  20. }
  21. Pre_Architecture/Group pre_l_3{
  22. label = "3"
  23. }
  24. Pre_Architecture/Port pre_l_4{
  25. label = "4"
  26. }
  27. Pre_Architecture/Contains pre_l_11 (pre_l_3, pre_l_4){
  28. label = "11"
  29. }
  30. Pre_Encapsulated_PetriNet/Port pre_l_5{
  31. label = "5"
  32. }
  33. Pre_Architecture/Connects (pre_l_1, pre_l_4){
  34. label = "6"
  35. }
  36. constraint = $
  37. Boolean function constraint(model : Element, mapping : Element):
  38. String name_0
  39. String name_1
  40. String name_2
  41. String name_3
  42. String name_4
  43. String name_5
  44. name_0 = read_attribute(model, mapping["0"], "name")
  45. name_1 = read_attribute(model, mapping["1"], "name")
  46. name_2 = read_attribute(model, mapping["2"], "name")
  47. name_3 = read_attribute(model, mapping["3"], "name")
  48. name_4 = read_attribute(model, mapping["4"], "name")
  49. name_5 = read_attribute(model, mapping["5"], "name")
  50. if bool_not(name_0 + "/" + name_1 == name_2):
  51. return False!
  52. if bool_not(name_3 + "/" + name_4 == name_5):
  53. return False!
  54. return True!
  55. $
  56. }
  57. RHS {
  58. Post_Architecture/Group post_l_0{
  59. label = "0"
  60. }
  61. Post_Architecture/Port post_l_1{
  62. label = "1"
  63. }
  64. Post_Architecture/Contains post_l_10 (post_l_0, post_l_1){
  65. label = "10"
  66. }
  67. Post_Encapsulated_PetriNet/Port post_l_2{
  68. label = "2"
  69. }
  70. Post_Architecture/Group post_l_3{
  71. label = "3"
  72. }
  73. Post_Architecture/Port post_l_4{
  74. label = "4"
  75. }
  76. Post_Architecture/Contains post_l_11 (post_l_3, post_l_4){
  77. label = "11"
  78. }
  79. Post_Encapsulated_PetriNet/Port post_l_5{
  80. label = "5"
  81. }
  82. Post_Architecture/Connects (post_l_1, post_l_4){
  83. label = "6"
  84. }
  85. Post_Encapsulated_PetriNet/Related (post_l_2, post_l_5){
  86. label = "7"
  87. }
  88. }
  89. }
  90. {Contains} ForAll remove_old {
  91. LHS {
  92. Pre_Encapsulated_PetriNet/Port pre_ro_0 {
  93. label = "0"
  94. }
  95. Pre_Encapsulated_PetriNet/Port pre_ro_1 {
  96. label = "1"
  97. }
  98. Pre_Encapsulated_PetriNet/Place pre_ro_2 {
  99. label = "2"
  100. }
  101. Pre_Encapsulated_PetriNet/Related (pre_ro_0, pre_ro_1) {
  102. label = "3"
  103. }
  104. Pre_Encapsulated_PetriNet/PortPlace (pre_ro_1, pre_ro_2) {
  105. label = "4"
  106. }
  107. }
  108. RHS {
  109. Post_Encapsulated_PetriNet/Port {
  110. label = "0"
  111. }
  112. }
  113. }
  114. {Contains} ForAll merge_P2T {
  115. LHS {
  116. Pre_Encapsulated_PetriNet/Place pre_p2t_1 {
  117. label = "1"
  118. }
  119. Pre_Encapsulated_PetriNet/Port pre_p2t_2 {
  120. label = "2"
  121. }
  122. Pre_Encapsulated_PetriNet/PortPlace (pre_p2t_2, pre_p2t_1){
  123. label = "3"
  124. }
  125. Pre_Encapsulated_PetriNet/Place pre_p2t_4 {
  126. label = "4"
  127. }
  128. Pre_Encapsulated_PetriNet/Port pre_p2t_5 {
  129. label = "5"
  130. }
  131. Pre_Encapsulated_PetriNet/PortPlace (pre_p2t_5, pre_p2t_4){
  132. label = "6"
  133. }
  134. Pre_Encapsulated_PetriNet/Transition pre_p2t_7 {
  135. label = "7"
  136. }
  137. Pre_Encapsulated_PetriNet/P2T (pre_p2t_4, pre_p2t_7) {
  138. label = "8"
  139. }
  140. Pre_Encapsulated_PetriNet/Related (pre_p2t_2, pre_p2t_5) {
  141. label = "10"
  142. }
  143. }
  144. RHS {
  145. Post_Encapsulated_PetriNet/Place post_p2t_1 {
  146. label = "1"
  147. }
  148. Post_Encapsulated_PetriNet/Port post_p2t_2 {
  149. label = "2"
  150. }
  151. Post_Encapsulated_PetriNet/PortPlace (post_p2t_2, post_p2t_1){
  152. label = "3"
  153. }
  154. Post_Encapsulated_PetriNet/Place post_p2t_4 {
  155. label = "4"
  156. }
  157. Post_Encapsulated_PetriNet/Port post_p2t_5 {
  158. label = "5"
  159. }
  160. Post_Encapsulated_PetriNet/PortPlace (post_p2t_5, post_p2t_4){
  161. label = "6"
  162. }
  163. Post_Encapsulated_PetriNet/Transition post_p2t_7 {
  164. label = "7"
  165. }
  166. Post_Encapsulated_PetriNet/P2T (post_p2t_4, post_p2t_7) {
  167. label = "8"
  168. }
  169. Post_Encapsulated_PetriNet/P2T (post_p2t_1, post_p2t_7) {
  170. label = "9"
  171. }
  172. Post_Encapsulated_PetriNet/Related (post_p2t_2, post_p2t_5) {
  173. label = "10"
  174. }
  175. }
  176. }
  177. {Contains} ForAll merge_T2P {
  178. LHS {
  179. Pre_Encapsulated_PetriNet/Place pre_t2p_1 {
  180. label = "1"
  181. }
  182. Pre_Encapsulated_PetriNet/Port pre_t2p_2 {
  183. label = "2"
  184. }
  185. Pre_Encapsulated_PetriNet/PortPlace (pre_t2p_2, pre_t2p_1){
  186. label = "3"
  187. }
  188. Pre_Encapsulated_PetriNet/Place pre_t2p_4 {
  189. label = "4"
  190. }
  191. Pre_Encapsulated_PetriNet/Port pre_t2p_5 {
  192. label = "5"
  193. }
  194. Pre_Encapsulated_PetriNet/PortPlace (pre_t2p_5, pre_t2p_4){
  195. label = "6"
  196. }
  197. Pre_Encapsulated_PetriNet/Transition pre_t2p_7 {
  198. label = "7"
  199. }
  200. Pre_Encapsulated_PetriNet/T2P (pre_t2p_7, pre_t2p_4) {
  201. label = "8"
  202. }
  203. Pre_Encapsulated_PetriNet/Related (pre_t2p_2, pre_t2p_5) {
  204. label = "10"
  205. }
  206. }
  207. RHS {
  208. Post_Encapsulated_PetriNet/Place post_t2p_1 {
  209. label = "1"
  210. }
  211. Post_Encapsulated_PetriNet/Port post_t2p_2 {
  212. label = "2"
  213. }
  214. Post_Encapsulated_PetriNet/PortPlace (post_t2p_2, post_t2p_1){
  215. label = "3"
  216. }
  217. Post_Encapsulated_PetriNet/Place post_t2p_4 {
  218. label = "4"
  219. }
  220. Post_Encapsulated_PetriNet/Port post_t2p_5 {
  221. label = "5"
  222. }
  223. Post_Encapsulated_PetriNet/PortPlace (post_t2p_5, post_t2p_4){
  224. label = "6"
  225. }
  226. Post_Encapsulated_PetriNet/Transition post_t2p_7 {
  227. label = "7"
  228. }
  229. Post_Encapsulated_PetriNet/T2P (post_t2p_7, post_t2p_4) {
  230. label = "8"
  231. }
  232. Post_Encapsulated_PetriNet/T2P (post_t2p_7, post_t2p_1) {
  233. label = "9"
  234. }
  235. Post_Encapsulated_PetriNet/Related (post_t2p_2, post_t2p_5) {
  236. label = "10"
  237. }
  238. }
  239. }
  240. {Contains} ForAll copy_transitions {
  241. LHS {
  242. Pre_Encapsulated_PetriNet/Transition {
  243. label = "0"
  244. }
  245. }
  246. RHS {
  247. Post_Encapsulated_PetriNet/Transition ct1 {
  248. label = "0"
  249. }
  250. Post_PetriNet/Transition ct2 {
  251. label = "1"
  252. value_name = $
  253. Integer function value(model : Element, name : String, mapping : Element):
  254. return read_attribute(model, mapping["0"], "name")!
  255. $
  256. }
  257. Post_EPN2PN_transition_link (ct1, ct2){
  258. label = "2"
  259. }
  260. }
  261. }
  262. {Contains} ForAll copy_places {
  263. LHS {
  264. Pre_Encapsulated_PetriNet/Place {
  265. label = "0"
  266. }
  267. }
  268. RHS {
  269. Post_Encapsulated_PetriNet/Place cp1 {
  270. label = "0"
  271. }
  272. Post_PetriNet/Place cp2 {
  273. label = "1"
  274. value_tokens = $
  275. Integer function value(model : Element, name : String, mapping : Element):
  276. return read_attribute(model, mapping["0"], "tokens")!
  277. $
  278. value_name = $
  279. Integer function value(model : Element, name : String, mapping : Element):
  280. return read_attribute(model, mapping["0"], "name")!
  281. $
  282. }
  283. Post_EPN2PN_place_link (cp1, cp2){
  284. label = "2"
  285. }
  286. }
  287. }
  288. {Contains} ForAll copy_P2T {
  289. LHS {
  290. Pre_Encapsulated_PetriNet/Place cp2t_p{
  291. label = "0"
  292. }
  293. Pre_Encapsulated_PetriNet/Transition cp2t_t{
  294. label = "1"
  295. }
  296. Pre_Encapsulated_PetriNet/P2T (cp2t_p, cp2t_t){
  297. label = "2"
  298. }
  299. Pre_PetriNet/Place cp2t_p2{
  300. label = "3"
  301. }
  302. Pre_PetriNet/Transition cp2t_t2{
  303. label = "4"
  304. }
  305. Pre_EPN2PN_place_link (cp2t_p, cp2t_p2){
  306. label = "5"
  307. }
  308. Pre_EPN2PN_transition_link (cp2t_t, cp2t_t2){
  309. label = "6"
  310. }
  311. }
  312. RHS {
  313. Post_Encapsulated_PetriNet/Place rhs_cp2t_p{
  314. label = "0"
  315. }
  316. Post_Encapsulated_PetriNet/Transition rhs_cp2t_t{
  317. label = "1"
  318. }
  319. Post_Encapsulated_PetriNet/P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){
  320. label = "2"
  321. }
  322. Post_PetriNet/Place rhs_cp2t_p2 {
  323. label = "3"
  324. }
  325. Post_PetriNet/Transition rhs_cp2t_t2 {
  326. label = "4"
  327. }
  328. Post_EPN2PN_place_link (rhs_cp2t_p, rhs_cp2t_p2){
  329. label = "5"
  330. }
  331. Post_EPN2PN_transition_link (rhs_cp2t_t, rhs_cp2t_t2){
  332. label = "6"
  333. }
  334. Post_PetriNet/P2T rhs_cp2t_p2t2(rhs_cp2t_p2, rhs_cp2t_t2) {
  335. label = "7"
  336. value_weight = $
  337. Integer function value(host_model : Element, name : String, mapping : Element):
  338. return 1!
  339. $
  340. }
  341. }
  342. }
  343. {Contains} ForAll copy_T2P {
  344. LHS {
  345. Pre_Encapsulated_PetriNet/Place ct2p_p{
  346. label = "0"
  347. }
  348. Pre_Encapsulated_PetriNet/Transition ct2p_t{
  349. label = "1"
  350. }
  351. Pre_Encapsulated_PetriNet/T2P (ct2p_t, ct2p_p){
  352. label = "2"
  353. }
  354. Pre_PetriNet/Place ct2p_p2{
  355. label = "3"
  356. }
  357. Pre_PetriNet/Transition ct2p_t2{
  358. label = "4"
  359. }
  360. Pre_EPN2PN_place_link (ct2p_p, ct2p_p2){
  361. label = "5"
  362. }
  363. Pre_EPN2PN_transition_link (ct2p_t, ct2p_t2){
  364. label = "6"
  365. }
  366. }
  367. RHS {
  368. Post_Encapsulated_PetriNet/Place rhs_ct2p_p{
  369. label = "0"
  370. }
  371. Post_Encapsulated_PetriNet/Transition rhs_ct2p_t{
  372. label = "1"
  373. }
  374. Post_Encapsulated_PetriNet/T2P (rhs_ct2p_t, rhs_ct2p_p){
  375. label = "2"
  376. }
  377. Post_PetriNet/Place rhs_ct2p_p2 {
  378. label = "3"
  379. }
  380. Post_PetriNet/Transition rhs_ct2p_t2 {
  381. label = "4"
  382. }
  383. Post_EPN2PN_place_link (rhs_ct2p_p, rhs_ct2p_p2){
  384. label = "5"
  385. }
  386. Post_EPN2PN_transition_link (rhs_ct2p_t, rhs_ct2p_t2){
  387. label = "6"
  388. }
  389. Post_PetriNet/T2P (rhs_ct2p_t2, rhs_ct2p_p2) {
  390. label = "7"
  391. value_weight = $
  392. Integer function value(host_model : Element, name : String, mapping : Element):
  393. return 1!
  394. $
  395. }
  396. }
  397. }
  398. }
  399. Initial (schedule, link) {}
  400. OnSuccess (link, merge_P2T) {}
  401. OnFailure (link, merge_P2T) {}
  402. OnSuccess (merge_P2T, merge_T2P) {}
  403. OnFailure (merge_P2T, merge_T2P) {}
  404. OnSuccess (merge_T2P, remove_old) {}
  405. OnFailure (merge_T2P, remove_old) {}
  406. OnSuccess (remove_old, copy_places) {}
  407. OnFailure (remove_old, copy_places) {}
  408. OnSuccess (copy_places, copy_transitions) {}
  409. OnSuccess (copy_transitions, copy_P2T) {}
  410. OnSuccess (copy_P2T, copy_T2P) {}
  411. OnSuccess (copy_T2P, success) {}
  412. OnFailure (copy_places, copy_transitions) {}
  413. OnFailure (copy_transitions, copy_P2T) {}
  414. OnFailure (copy_P2T, copy_T2P) {}
  415. OnFailure (copy_T2P, success) {}