plant_to_EPN.mvc 31 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804
  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} Atomic init_ports {
  9. LHS {}
  10. RHS {
  11. Post_Encapsulated_PetriNet/Place post_ports_00 {
  12. label = "00"
  13. value_name = $
  14. String function value(model : Element, name : String, mapping : Element):
  15. return "up"!
  16. $
  17. value_tokens = $
  18. Integer function value(model : Element, name : String, mapping : Element):
  19. return 0!
  20. $
  21. }
  22. Post_Encapsulated_PetriNet/Port post_ports_10 {
  23. label = "10"
  24. value_name = $
  25. String function value(model : Element, name : String, mapping : Element):
  26. return "up"!
  27. $
  28. }
  29. Post_Encapsulated_PetriNet/PortPlace (post_ports_10, post_ports_00) {
  30. label = "20"
  31. }
  32. Post_Encapsulated_PetriNet/Place post_ports_01 {
  33. label = "01"
  34. value_name = $
  35. String function value(model : Element, name : String, mapping : Element):
  36. return "neutral"!
  37. $
  38. value_tokens = $
  39. Integer function value(model : Element, name : String, mapping : Element):
  40. return 0!
  41. $
  42. }
  43. Post_Encapsulated_PetriNet/Port post_ports_11 {
  44. label = "11"
  45. value_name = $
  46. String function value(model : Element, name : String, mapping : Element):
  47. return "neutral"!
  48. $
  49. }
  50. Post_Encapsulated_PetriNet/PortPlace (post_ports_11, post_ports_01) {
  51. label = "21"
  52. }
  53. Post_Encapsulated_PetriNet/Place post_ports_02 {
  54. label = "02"
  55. value_name = $
  56. String function value(model : Element, name : String, mapping : Element):
  57. return "down"!
  58. $
  59. value_tokens = $
  60. Integer function value(model : Element, name : String, mapping : Element):
  61. return 0!
  62. $
  63. }
  64. Post_Encapsulated_PetriNet/Port post_ports_12 {
  65. label = "12"
  66. value_name = $
  67. String function value(model : Element, name : String, mapping : Element):
  68. return "down"!
  69. $
  70. }
  71. Post_Encapsulated_PetriNet/PortPlace (post_ports_12, post_ports_02) {
  72. label = "22"
  73. }
  74. Post_Encapsulated_PetriNet/Place post_ports_03 {
  75. label = "03"
  76. value_name = $
  77. String function value(model : Element, name : String, mapping : Element):
  78. return "interrupt"!
  79. $
  80. value_tokens = $
  81. Integer function value(model : Element, name : String, mapping : Element):
  82. return 0!
  83. $
  84. }
  85. Post_Encapsulated_PetriNet/Port post_ports_13 {
  86. label = "13"
  87. value_name = $
  88. String function value(model : Element, name : String, mapping : Element):
  89. return "interrupt"!
  90. $
  91. }
  92. Post_Encapsulated_PetriNet/PortPlace (post_ports_13, post_ports_03) {
  93. label = "23"
  94. }
  95. Post_Encapsulated_PetriNet/Place post_ports_04 {
  96. label = "04"
  97. value_name = $
  98. String function value(model : Element, name : String, mapping : Element):
  99. return "objDetected"!
  100. $
  101. value_tokens = $
  102. Integer function value(model : Element, name : String, mapping : Element):
  103. return 0!
  104. $
  105. }
  106. Post_Encapsulated_PetriNet/Port post_ports_14 {
  107. label = "14"
  108. value_name = $
  109. String function value(model : Element, name : String, mapping : Element):
  110. return "objDetected"!
  111. $
  112. }
  113. Post_Encapsulated_PetriNet/PortPlace (post_ports_14, post_ports_04) {
  114. label = "24"
  115. }
  116. Post_Encapsulated_PetriNet/Place post_ports_05 {
  117. label = "05"
  118. value_name = $
  119. String function value(model : Element, name : String, mapping : Element):
  120. return "no_objDetected"!
  121. $
  122. value_tokens = $
  123. Integer function value(model : Element, name : String, mapping : Element):
  124. return 1!
  125. $
  126. }
  127. Post_Encapsulated_PetriNet/Port post_ports_15 {
  128. label = "15"
  129. value_name = $
  130. String function value(model : Element, name : String, mapping : Element):
  131. return "no_objDetected"!
  132. $
  133. }
  134. Post_Encapsulated_PetriNet/PortPlace (post_ports_15, post_ports_05) {
  135. label = "25"
  136. }
  137. Post_Encapsulated_PetriNet/Place post_ports_06 {
  138. label = "06"
  139. value_name = $
  140. String function value(model : Element, name : String, mapping : Element):
  141. return "objPresent"!
  142. $
  143. value_tokens = $
  144. Integer function value(model : Element, name : String, mapping : Element):
  145. return 0!
  146. $
  147. }
  148. Post_Encapsulated_PetriNet/Port post_ports_16 {
  149. label = "16"
  150. value_name = $
  151. String function value(model : Element, name : String, mapping : Element):
  152. return "objPresent"!
  153. $
  154. }
  155. Post_Encapsulated_PetriNet/PortPlace (post_ports_16, post_ports_06) {
  156. label = "26"
  157. }
  158. Post_Encapsulated_PetriNet/Place post_ports_07 {
  159. label = "07"
  160. value_name = $
  161. String function value(model : Element, name : String, mapping : Element):
  162. return "no_objPresent"!
  163. $
  164. value_tokens = $
  165. Integer function value(model : Element, name : String, mapping : Element):
  166. return 1!
  167. $
  168. }
  169. Post_Encapsulated_PetriNet/Port post_ports_17 {
  170. label = "17"
  171. value_name = $
  172. String function value(model : Element, name : String, mapping : Element):
  173. return "no_objPresent"!
  174. $
  175. }
  176. Post_Encapsulated_PetriNet/PortPlace (post_ports_17, post_ports_07) {
  177. label = "27"
  178. }
  179. }
  180. }
  181. {Contains} ForAll create_states {
  182. LHS {
  183. Pre_PW_Plant/State {
  184. label = "0"
  185. }
  186. }
  187. RHS {
  188. Post_PW_Plant/State post_cs_0 {
  189. label = "0"
  190. }
  191. Post_Encapsulated_PetriNet/Place post_cs_1 {
  192. label = "1"
  193. value_name = $
  194. String function value(model : Element, name : String, mapping : Element):
  195. return read_attribute(model, mapping["0"], "name")!
  196. $
  197. value_tokens = $
  198. Integer function value(model : Element, name : String, mapping : Element):
  199. if (value_eq(read_attribute(model, mapping["0"], "isInitial"), True)):
  200. return 1!
  201. else:
  202. return 0!
  203. $
  204. }
  205. Post_PLANT2EPN_link (post_cs_0, post_cs_1) {
  206. label = "2"
  207. }
  208. }
  209. }
  210. {Contains} ForAll command_transition {
  211. LHS {
  212. Pre_PW_Plant/State pre_ct_0{
  213. label = "0"
  214. }
  215. Pre_PW_Plant/State pre_ct_1{
  216. label = "1"
  217. }
  218. Pre_PW_Plant/Transition pre_ct_2 (pre_ct_0, pre_ct_1) {
  219. label = "2"
  220. }
  221. Pre_Encapsulated_PetriNet/Place pre_ct_3{
  222. label = "3"
  223. }
  224. Pre_Encapsulated_PetriNet/Place pre_ct_4{
  225. label = "4"
  226. }
  227. Pre_PLANT2EPN_link P2E_l1 (pre_ct_0, pre_ct_3) {
  228. label = "5"
  229. }
  230. Pre_PLANT2EPN_link P2E_l2(pre_ct_1, pre_ct_4) {
  231. label = "6"
  232. }
  233. Pre_Encapsulated_PetriNet/Place pre_ct_7 {
  234. label = "7"
  235. constraint_name = $
  236. Boolean function constraint(value : String):
  237. return (bool_or(bool_or(value == "up", value == "neutral"), value == "down"))!
  238. $
  239. }
  240. Pre_Encapsulated_PetriNet/Port pre_ct_8 {
  241. label = "8"
  242. constraint_name = $
  243. Boolean function constraint(value : String):
  244. return (bool_or(bool_or(value == "up", value == "neutral"), value == "down"))!
  245. $
  246. }
  247. Pre_Encapsulated_PetriNet/PortPlace pp_l (pre_ct_8, pre_ct_7) {
  248. label = "9"
  249. }
  250. constraint = $
  251. Boolean function constraint(model : Element, mapping : Element):
  252. String transition_type
  253. String port_name
  254. transition_type = read_type(model, mapping["2"])
  255. port_name = read_attribute(model, mapping["8"], "name")
  256. log("TT " + transition_type)
  257. log("PN " + port_name)
  258. if (transition_type == "PW_Plant/OnUp"):
  259. log(cast_v2s(port_name == "up"))
  260. return (port_name == "up")!
  261. elif (transition_type == "PW_Plant/OnNeutral"):
  262. log(cast_v2s(port_name == "neutral"))
  263. return (port_name == "neutral")!
  264. elif (transition_type == "PW_Plant/OnDown"):
  265. log(cast_v2s(port_name == "down"))
  266. return (port_name == "down")!
  267. else:
  268. log("FALSE")
  269. return False!
  270. $
  271. }
  272. RHS {
  273. Post_PW_Plant/State post_ct_0{
  274. label = "0"
  275. }
  276. Post_PW_Plant/State post_ct_1{
  277. label = "1"
  278. }
  279. Post_PW_Plant/Transition post_ct_2 (post_ct_0, post_ct_1) {
  280. label = "2"
  281. }
  282. Post_Encapsulated_PetriNet/Place post_ct_3{
  283. label = "3"
  284. }
  285. Post_Encapsulated_PetriNet/Place post_ct_4{
  286. label = "4"
  287. }
  288. Post_PLANT2EPN_link (post_ct_0, post_ct_3) {
  289. label = "5"
  290. }
  291. Post_PLANT2EPN_link (post_ct_1, post_ct_4) {
  292. label = "6"
  293. }
  294. Post_Encapsulated_PetriNet/Place post_ct_7 {
  295. label = "7"
  296. }
  297. Post_Encapsulated_PetriNet/Port post_ct_8 {
  298. label = "8"
  299. }
  300. Post_Encapsulated_PetriNet/PortPlace (post_ct_8, post_ct_7) {
  301. label = "9"
  302. }
  303. Post_Encapsulated_PetriNet/Transition post_ct_10 {
  304. label = "10"
  305. value_name = $
  306. String function value(model : Element, name : String, mapping : Element):
  307. return read_type(model, mapping["2"])!
  308. $
  309. }
  310. Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_10) {
  311. label = "11"
  312. }
  313. Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_4) {
  314. label = "12"
  315. }
  316. Post_Encapsulated_PetriNet/P2T (post_ct_7, post_ct_10) {
  317. label = "13"
  318. }
  319. Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_7) {
  320. label = "14"
  321. }
  322. Post_PLANT2EPN_tlink (post_ct_2, post_ct_10) {
  323. label = "100"
  324. }
  325. }
  326. }
  327. {Contains} ForAll check_object {
  328. LHS {
  329. Pre_PW_Plant/State pre_co_0{
  330. label = "0"
  331. }
  332. Pre_PW_Plant/State pre_co_1{
  333. label = "1"
  334. }
  335. Pre_PW_Plant/Transition pre_co_2 (pre_co_0, pre_co_1) {
  336. label = "2"
  337. constraint_objPresent = $
  338. Boolean function constraint(value : String):
  339. return (bool_or(value == "Y", value == "N"))!
  340. $
  341. }
  342. Pre_Encapsulated_PetriNet/Place pre_co_3{
  343. label = "3"
  344. }
  345. Pre_Encapsulated_PetriNet/Place pre_co_4{
  346. label = "4"
  347. }
  348. Pre_PLANT2EPN_link (pre_co_0, pre_co_3) {
  349. label = "5"
  350. }
  351. Pre_PLANT2EPN_link (pre_co_1, pre_co_4) {
  352. label = "6"
  353. }
  354. Pre_Encapsulated_PetriNet/Place pre_co_8 {
  355. label = "8"
  356. }
  357. Pre_Encapsulated_PetriNet/Port pre_co_11 {
  358. label = "11"
  359. constraint_name = $
  360. Boolean function constraint(value : String):
  361. return (bool_or(value == "objPresent", value == "no_objPresent"))!
  362. $
  363. }
  364. Pre_Encapsulated_PetriNet/PortPlace (pre_co_11, pre_co_8) {
  365. label = "12"
  366. }
  367. Pre_Encapsulated_PetriNet/Transition pre_co_15 {
  368. label = "15"
  369. }
  370. Pre_Encapsulated_PetriNet/P2T (pre_co_3, pre_co_15) {
  371. label = "16"
  372. }
  373. Pre_Encapsulated_PetriNet/T2P (pre_co_15, pre_co_4) {
  374. label = "17"
  375. }
  376. Pre_PLANT2EPN_tlink (pre_co_2, pre_co_15) {
  377. label = "100"
  378. }
  379. constraint = $
  380. Boolean function constraint (host_model : Element, mapping : Element):
  381. // Check whether the bound primary places match with the state
  382. String objPresent
  383. String port_name
  384. objPresent = read_attribute(host_model, mapping["2"], "objPresent")
  385. port_name = read_attribute(host_model, mapping["11"], "name")
  386. if (objPresent == "Y"):
  387. return (port_name == "objPresent")!
  388. elif (objPresent == "N"):
  389. return (port_name == "no_objPresent")!
  390. else:
  391. return False!
  392. $
  393. }
  394. RHS {
  395. Post_PW_Plant/State post_co_0{
  396. label = "0"
  397. }
  398. Post_PW_Plant/State post_co_1{
  399. label = "1"
  400. }
  401. Post_PW_Plant/Transition post_co_2 (post_co_0, post_co_1) {
  402. label = "2"
  403. }
  404. Post_Encapsulated_PetriNet/Place post_co_3{
  405. label = "3"
  406. }
  407. Post_Encapsulated_PetriNet/Place post_co_4{
  408. label = "4"
  409. }
  410. Post_PLANT2EPN_link (post_co_0, post_co_3) {
  411. label = "5"
  412. }
  413. Post_PLANT2EPN_link (post_co_1, post_co_4) {
  414. label = "6"
  415. }
  416. Post_Encapsulated_PetriNet/Place post_co_8 {
  417. label = "8"
  418. }
  419. Post_Encapsulated_PetriNet/Port post_co_11 {
  420. label = "11"
  421. }
  422. Post_Encapsulated_PetriNet/PortPlace (post_co_11, post_co_8) {
  423. label = "12"
  424. }
  425. Post_Encapsulated_PetriNet/Transition post_co_15 {
  426. label = "15"
  427. }
  428. Post_Encapsulated_PetriNet/P2T (post_co_3, post_co_15) {
  429. label = "16"
  430. }
  431. Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
  432. label = "17"
  433. }
  434. Post_Encapsulated_PetriNet/P2T (post_co_8, post_co_15) {
  435. label = "9"
  436. }
  437. Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_8) {
  438. label = "10"
  439. }
  440. Post_PLANT2EPN_tlink (post_co_2, post_co_15) {
  441. label = "100"
  442. }
  443. }
  444. }
  445. {Contains} ForAll detect {
  446. LHS {
  447. Pre_PW_Plant/NormalState pre_de_0{
  448. label = "0"
  449. }
  450. Pre_PW_Plant/ErrorState pre_de_1{
  451. label = "1"
  452. }
  453. Pre_PW_Plant/Transition pre_de_2 (pre_de_0, pre_de_1) {
  454. label = "2"
  455. }
  456. Pre_Encapsulated_PetriNet/Place pre_de_3{
  457. label = "3"
  458. }
  459. Pre_Encapsulated_PetriNet/Place pre_de_4{
  460. label = "4"
  461. }
  462. Pre_PLANT2EPN_link (pre_de_0, pre_de_3) {
  463. label = "5"
  464. }
  465. Pre_PLANT2EPN_link (pre_de_1, pre_de_4) {
  466. label = "6"
  467. }
  468. Pre_Encapsulated_PetriNet/Transition pre_de_7 {
  469. label = "7"
  470. }
  471. Pre_Encapsulated_PetriNet/P2T (pre_de_3, pre_de_7) {
  472. label = "8"
  473. }
  474. Pre_Encapsulated_PetriNet/T2P (pre_de_7, pre_de_4) {
  475. label = "9"
  476. }
  477. Pre_Encapsulated_PetriNet/Place pre_de_10 {
  478. label = "10"
  479. }
  480. Pre_Encapsulated_PetriNet/Port pre_de_11 {
  481. label = "11"
  482. }
  483. Pre_Encapsulated_PetriNet/PortPlace (pre_de_11, pre_de_10) {
  484. label = "12"
  485. }
  486. Pre_Encapsulated_PetriNet/Place pre_de_13 {
  487. label = "13"
  488. }
  489. Pre_Encapsulated_PetriNet/Port pre_de_14 {
  490. label = "14"
  491. constraint_name = $
  492. Boolean function constraint(value : String):
  493. return (value == "interrupt")!
  494. $
  495. }
  496. Pre_Encapsulated_PetriNet/PortPlace (pre_de_14, pre_de_13) {
  497. label = "15"
  498. }
  499. Pre_Encapsulated_PetriNet/Place pre_de_16 {
  500. label = "16"
  501. }
  502. Pre_Encapsulated_PetriNet/Port pre_de_17 {
  503. label = "17"
  504. constraint_name = $
  505. Boolean function constraint(value : String):
  506. return (value == "no_objDetected")!
  507. $
  508. }
  509. Pre_Encapsulated_PetriNet/PortPlace (pre_de_17, pre_de_16) {
  510. label = "18"
  511. }
  512. Pre_Encapsulated_PetriNet/Place pre_de_19 {
  513. label = "19"
  514. }
  515. Pre_Encapsulated_PetriNet/Port pre_de_20 {
  516. label = "20"
  517. constraint_name = $
  518. Boolean function constraint(value : String):
  519. return (value == "objDetected")!
  520. $
  521. }
  522. Pre_Encapsulated_PetriNet/PortPlace (pre_de_20, pre_de_19) {
  523. label = "21"
  524. }
  525. Pre_PLANT2EPN_tlink (pre_de_2, pre_de_7) {
  526. label = "100"
  527. }
  528. constraint = $
  529. Boolean function constraint (host_model : Element, mapping : Element):
  530. // Check whether the bound primary places match with the state
  531. String source_type
  532. String port_name
  533. source_type = read_type(host_model, mapping["2"])
  534. port_name = read_attribute(host_model, mapping["11"], "name")
  535. if (source_type == "PW_Plant/OnUp"):
  536. return (port_name == "up")!
  537. elif (source_type == "PW_Plant/OnNeutral"):
  538. return (port_name == "neutral")!
  539. elif (source_type == "PW_Plant/OnDown"):
  540. return (port_name == "down")!
  541. else:
  542. return False!
  543. $
  544. }
  545. RHS {
  546. Post_PW_Plant/NormalState post_de_0{
  547. label = "0"
  548. }
  549. Post_PW_Plant/ErrorState post_de_1{
  550. label = "1"
  551. }
  552. Post_PW_Plant/Transition post_de_2 (post_de_0, post_de_1){
  553. label = "2"
  554. }
  555. Post_Encapsulated_PetriNet/Place post_de_3{
  556. label = "3"
  557. }
  558. Post_Encapsulated_PetriNet/Place post_de_4{
  559. label = "4"
  560. }
  561. Post_PLANT2EPN_link (post_de_0, post_de_3) {
  562. label = "5"
  563. }
  564. Post_PLANT2EPN_link (post_de_1, post_de_4) {
  565. label = "6"
  566. }
  567. Post_Encapsulated_PetriNet/Transition post_de_7 {
  568. label = "7"
  569. }
  570. Post_Encapsulated_PetriNet/P2T (post_de_3, post_de_7) {
  571. label = "8"
  572. }
  573. Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_4) {
  574. label = "9"
  575. }
  576. Post_Encapsulated_PetriNet/Place post_de_10 {
  577. label = "10"
  578. }
  579. Post_Encapsulated_PetriNet/Port post_de_11 {
  580. label = "11"
  581. }
  582. Post_Encapsulated_PetriNet/PortPlace (post_de_11, post_de_10) {
  583. label = "12"
  584. }
  585. Post_Encapsulated_PetriNet/Place post_de_13 {
  586. label = "13"
  587. }
  588. Post_Encapsulated_PetriNet/Port post_de_14 {
  589. label = "14"
  590. }
  591. Post_Encapsulated_PetriNet/PortPlace (post_de_14, post_de_13) {
  592. label = "15"
  593. }
  594. Post_Encapsulated_PetriNet/Place post_de_16 {
  595. label = "16"
  596. }
  597. Post_Encapsulated_PetriNet/Port post_de_17 {
  598. label = "17"
  599. }
  600. Post_Encapsulated_PetriNet/PortPlace (post_de_17, post_de_16) {
  601. label = "18"
  602. }
  603. Post_Encapsulated_PetriNet/Place post_de_19 {
  604. label = "19"
  605. }
  606. Post_Encapsulated_PetriNet/Port post_de_20 {
  607. label = "20"
  608. }
  609. Post_Encapsulated_PetriNet/PortPlace (post_de_20, post_de_19) {
  610. label = "21"
  611. }
  612. Post_Encapsulated_PetriNet/P2T (post_de_10, post_de_7) {
  613. label = "22"
  614. }
  615. Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_13) {
  616. label = "23"
  617. }
  618. Post_Encapsulated_PetriNet/P2T (post_de_16, post_de_7) {
  619. label = "24"
  620. }
  621. Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_19) {
  622. label = "25"
  623. }
  624. Post_PLANT2EPN_tlink (post_de_2, post_de_7) {
  625. label = "100"
  626. }
  627. }
  628. }
  629. {Contains} ForAll remove_detect {
  630. LHS {
  631. Pre_PW_Plant/ErrorState pre_rd_0{
  632. label = "0"
  633. }
  634. Pre_PW_Plant/NormalState pre_rd_1{
  635. label = "1"
  636. }
  637. Pre_PW_Plant/Transition pre_rd_2 (pre_rd_0, pre_rd_1){
  638. label = "2"
  639. }
  640. Pre_Encapsulated_PetriNet/Place pre_rd_3{
  641. label = "3"
  642. }
  643. Pre_Encapsulated_PetriNet/Place pre_rd_4{
  644. label = "4"
  645. }
  646. Pre_PLANT2EPN_link (pre_rd_0, pre_rd_3) {
  647. label = "5"
  648. }
  649. Pre_PLANT2EPN_link (pre_rd_1, pre_rd_4) {
  650. label = "6"
  651. }
  652. Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
  653. label = "7"
  654. }
  655. Pre_Encapsulated_PetriNet/P2T (pre_rd_3, pre_rd_7) {
  656. label = "8"
  657. }
  658. Pre_Encapsulated_PetriNet/T2P (pre_rd_7, pre_rd_4) {
  659. label = "9"
  660. }
  661. Pre_Encapsulated_PetriNet/Place pre_rd_10 {
  662. label = "10"
  663. }
  664. Pre_Encapsulated_PetriNet/Port pre_rd_11 {
  665. label = "11"
  666. constraint_name = $
  667. Boolean function constraint(value : String):
  668. return (value == "objDetected")!
  669. $
  670. }
  671. Pre_Encapsulated_PetriNet/PortPlace (pre_rd_11, pre_rd_10) {
  672. label = "12"
  673. }
  674. Pre_Encapsulated_PetriNet/Place pre_rd_13 {
  675. label = "13"
  676. }
  677. Pre_Encapsulated_PetriNet/Port pre_rd_14 {
  678. label = "14"
  679. constraint_name = $
  680. Boolean function constraint(value : String):
  681. return (value == "no_objDetected")!
  682. $
  683. }
  684. Pre_Encapsulated_PetriNet/PortPlace (pre_rd_14, pre_rd_13) {
  685. label = "15"
  686. }
  687. Pre_PLANT2EPN_tlink (pre_rd_2, pre_rd_7) {
  688. label = "100"
  689. }
  690. }
  691. RHS {
  692. Post_PW_Plant/ErrorState post_rd_0{
  693. label = "0"
  694. }
  695. Post_PW_Plant/NormalState post_rd_1{
  696. label = "1"
  697. }
  698. Post_PW_Plant/Transition post_rd_2 (post_rd_0, post_rd_1){
  699. label = "2"
  700. }
  701. Post_Encapsulated_PetriNet/Place post_rd_3{
  702. label = "3"
  703. }
  704. Post_Encapsulated_PetriNet/Place post_rd_4{
  705. label = "4"
  706. }
  707. Post_PLANT2EPN_link (post_rd_0, post_rd_3) {
  708. label = "5"
  709. }
  710. Post_PLANT2EPN_link (post_rd_1, post_rd_4) {
  711. label = "6"
  712. }
  713. Post_Encapsulated_PetriNet/Transition post_rd_7 {
  714. label = "7"
  715. }
  716. Post_Encapsulated_PetriNet/P2T (post_rd_3, post_rd_7) {
  717. label = "8"
  718. }
  719. Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_4) {
  720. label = "9"
  721. }
  722. Post_Encapsulated_PetriNet/Place post_rd_10 {
  723. label = "10"
  724. }
  725. Post_Encapsulated_PetriNet/Port post_rd_11 {
  726. label = "11"
  727. }
  728. Post_Encapsulated_PetriNet/PortPlace (post_rd_11, post_rd_10) {
  729. label = "12"
  730. }
  731. Post_Encapsulated_PetriNet/Place post_rd_13 {
  732. label = "13"
  733. }
  734. Post_Encapsulated_PetriNet/Port post_rd_14 {
  735. label = "14"
  736. }
  737. Post_Encapsulated_PetriNet/PortPlace (post_rd_14, post_rd_13) {
  738. label = "15"
  739. }
  740. Post_Encapsulated_PetriNet/P2T (post_rd_10, post_rd_7) {
  741. label = "16"
  742. }
  743. Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_13) {
  744. label = "17"
  745. }
  746. Post_PLANT2EPN_tlink (post_rd_2, post_rd_7) {
  747. label = "100"
  748. }
  749. }
  750. }
  751. }
  752. Initial (schedule, init_ports) {}
  753. OnSuccess (init_ports, create_states) {}
  754. OnSuccess (create_states, command_transition) {}
  755. OnSuccess (command_transition, check_object) {}
  756. OnSuccess (check_object, detect) {}
  757. OnSuccess (detect, remove_detect) {}
  758. OnSuccess (remove_detect, success) {}
  759. OnFailure (init_ports, create_states) {}
  760. OnFailure (create_states, command_transition) {}
  761. OnFailure (command_transition, check_object) {}
  762. OnFailure (check_object, detect) {}
  763. OnFailure (detect, remove_detect) {}
  764. OnFailure (remove_detect, success) {}
  765. }