Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Trace from the execution

Waiting for the VM to be ready (probing ssh)
...............................
=====================================================================
Generated by BenchKit 2-1668
Executing tool greatspn
Input is SurpriseSharedMemory-PT-000020, examination is ReachabilityFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r07ks-ovh1-140068246001515
=====================================================================

--------------------
content from stdout:

BK_START 1400688331465
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurpriseSharedMemory (PT), instance 000020
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireability.xml INTO /home/mcc/execution/ReachabilityFireability.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 48 -C -f /home/mcc/execution/ReachabilityFireability.rgmedd-ctl
Using FORCE-PINV Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition End_Ext_Acc_16_1 (0/820).
Encoding transition End_Ext_Acc_17_1 (1/820).
Encoding transition End_Ext_Acc_14_1 (2/820).
Encoding transition End_Ext_Acc_15_1 (3/820).
Encoding transition End_Ext_Acc_12_1 (4/820).
Encoding transition End_Ext_Acc_13_1 (5/820).
Encoding transition End_Ext_Acc_10_1 (6/820).
Encoding transition End_Ext_Acc_11_1 (7/820).
Encoding transition End_Ext_Acc_8_1 (8/820).
Encoding transition End_Ext_Acc_9_1 (9/820).
Encoding transition End_Ext_Acc_6_1 (10/820).
Encoding transition End_Ext_Acc_7_1 (11/820).
Encoding transition End_Ext_Acc_4_1 (12/820).
Encoding transition End_Ext_Acc_5_1 (13/820).
Encoding transition End_Ext_Acc_2_1 (14/820).
Encoding transition End_Ext_Acc_3_1 (15/820).
Encoding transition End_Ext_Acc_8_3 (16/820).
Encoding transition End_Ext_Acc_9_3 (17/820).
Encoding transition End_Ext_Acc_10_3 (18/820).
Encoding transition End_Ext_Acc_11_3 (19/820).
Encoding transition End_Ext_Acc_4_3 (20/820).
Encoding transition End_Ext_Acc_5_3 (21/820).
Encoding transition End_Ext_Acc_6_3 (22/820).
Encoding transition End_Ext_Acc_7_3 (23/820).
Encoding transition End_Ext_Acc_19_2 (24/820).
Encoding transition End_Ext_Acc_20_2 (25/820).
Encoding transition End_Ext_Acc_1_3 (26/820).
Encoding transition End_Ext_Acc_2_3 (27/820).
Encoding transition End_Ext_Acc_15_2 (28/820).
Encoding transition End_Ext_Acc_16_2 (29/820).
Encoding transition End_Ext_Acc_17_2 (30/820).
Encoding transition End_Ext_Acc_18_2 (31/820).
Encoding transition End_Ext_Acc_12_2 (32/820).
Encoding transition End_Ext_Acc_11_2 (33/820).
Encoding transition End_Ext_Acc_14_2 (34/820).
Encoding transition End_Ext_Acc_13_2 (35/820).
Encoding transition End_Ext_Acc_8_2 (36/820).
Encoding transition End_Ext_Acc_7_2 (37/820).
Encoding transition End_Ext_Acc_10_2 (38/820).
Encoding transition End_Ext_Acc_9_2 (39/820).
Encoding transition End_Ext_Acc_4_2 (40/820).
Encoding transition End_Ext_Acc_3_2 (41/820).
Encoding transition End_Ext_Acc_6_2 (42/820).
Encoding transition End_Ext_Acc_5_2 (43/820).
Encoding transition End_Ext_Acc_19_1 (44/820).
Encoding transition End_Ext_Acc_18_1 (45/820).
Encoding transition End_Ext_Acc_1_2 (46/820).
Encoding transition End_Ext_Acc_20_1 (47/820).
Encoding transition End_Ext_Acc_12_5 (48/820).
Encoding transition End_Ext_Acc_13_5 (49/820).
Encoding transition End_Ext_Acc_10_5 (50/820).
Encoding transition End_Ext_Acc_11_5 (51/820).
Encoding transition End_Ext_Acc_8_5 (52/820).
Encoding transition End_Ext_Acc_9_5 (53/820).
Encoding transition End_Ext_Acc_6_5 (54/820).
Encoding transition End_Ext_Acc_7_5 (55/820).
Encoding transition End_Ext_Acc_20_5 (56/820).
Encoding transition End_Ext_Acc_1_6 (57/820).
Encoding transition End_Ext_Acc_18_5 (58/820).
Encoding transition End_Ext_Acc_19_5 (59/820).
Encoding transition End_Ext_Acc_16_5 (60/820).
Encoding transition End_Ext_Acc_17_5 (61/820).
Encoding transition End_Ext_Acc_14_5 (62/820).
Encoding transition End_Ext_Acc_15_5 (63/820).
Encoding transition End_Ext_Acc_10_6 (64/820).
Encoding transition End_Ext_Acc_9_6 (65/820).
Encoding transition End_Ext_Acc_8_6 (66/820).
Encoding transition End_Ext_Acc_7_6 (67/820).
Encoding transition End_Ext_Acc_5_6 (68/820).
Encoding transition End_Ext_Acc_4_6 (69/820).
Encoding transition End_Ext_Acc_3_6 (70/820).
Encoding transition End_Ext_Acc_2_6 (71/820).
Encoding transition End_Ext_Acc_18_6 (72/820).
Encoding transition End_Ext_Acc_17_6 (73/820).
Encoding transition End_Ext_Acc_16_6 (74/820).
Encoding transition End_Ext_Acc_15_6 (75/820).
Encoding transition End_Ext_Acc_14_6 (76/820).
Encoding transition End_Ext_Acc_13_6 (77/820).
Encoding transition End_Ext_Acc_12_6 (78/820).
Encoding transition End_Ext_Acc_11_6 (79/820).
Encoding transition End_Ext_Acc_16_3 (80/820).
Encoding transition End_Ext_Acc_17_3 (81/820).
Encoding transition End_Ext_Acc_18_3 (82/820).
Encoding transition End_Ext_Acc_19_3 (83/820).
Encoding transition End_Ext_Acc_12_3 (84/820).
Encoding transition End_Ext_Acc_13_3 (85/820).
Encoding transition End_Ext_Acc_14_3 (86/820).
Encoding transition End_Ext_Acc_15_3 (87/820).
Encoding transition End_Ext_Acc_5_4 (88/820).
Encoding transition End_Ext_Acc_6_4 (89/820).
Encoding transition End_Ext_Acc_7_4 (90/820).
Encoding transition End_Ext_Acc_8_4 (91/820).
Encoding transition End_Ext_Acc_20_3 (92/820).
Encoding transition End_Ext_Acc_1_4 (93/820).
Encoding transition End_Ext_Acc_2_4 (94/820).
Encoding transition End_Ext_Acc_3_4 (95/820).
Encoding transition End_Ext_Acc_14_4 (96/820).
Encoding transition End_Ext_Acc_13_4 (97/820).
Encoding transition End_Ext_Acc_16_4 (98/820).
Encoding transition End_Ext_Acc_15_4 (99/820).
Encoding transition End_Ext_Acc_10_4 (100/820).
Encoding transition End_Ext_Acc_9_4 (101/820).
Encoding transition End_Ext_Acc_12_4 (102/820).
Encoding transition End_Ext_Acc_11_4 (103/820).
Encoding transition End_Ext_Acc_2_5 (104/820).
Encoding transition End_Ext_Acc_1_5 (105/820).
Encoding transition End_Ext_Acc_4_5 (106/820).
Encoding transition End_Ext_Acc_3_5 (107/820).
Encoding transition End_Ext_Acc_18_4 (108/820).
Encoding transition End_Ext_Acc_17_4 (109/820).
Encoding transition End_Ext_Acc_20_4 (110/820).
Encoding transition End_Ext_Acc_19_4 (111/820).
Encoding transition End_Ext_Acc_15_8 (112/820).
Encoding transition End_Ext_Acc_16_8 (113/820).
Encoding transition End_Ext_Acc_13_8 (114/820).
Encoding transition End_Ext_Acc_14_8 (115/820).
Encoding transition End_Ext_Acc_19_8 (116/820).
Encoding transition End_Ext_Acc_20_8 (117/820).
Encoding transition End_Ext_Acc_17_8 (118/820).
Encoding transition End_Ext_Acc_18_8 (119/820).
Encoding transition End_Ext_Acc_3_9 (120/820).
Encoding transition End_Ext_Acc_4_9 (121/820).
Encoding transition End_Ext_Acc_1_9 (122/820).
Encoding transition End_Ext_Acc_2_9 (123/820).
Encoding transition End_Ext_Acc_7_9 (124/820).
Encoding transition End_Ext_Acc_8_9 (125/820).
Encoding transition End_Ext_Acc_5_9 (126/820).
Encoding transition End_Ext_Acc_6_9 (127/820).
Encoding transition End_Ext_Acc_13_9 (128/820).
Encoding transition End_Ext_Acc_12_9 (129/820).
Encoding transition End_Ext_Acc_11_9 (130/820).
Encoding transition End_Ext_Acc_10_9 (131/820).
Encoding transition End_Ext_Acc_17_9 (132/820).
Encoding transition End_Ext_Acc_16_9 (133/820).
Encoding transition End_Ext_Acc_15_9 (134/820).
Encoding transition End_Ext_Acc_14_9 (135/820).
Encoding transition End_Ext_Acc_1_10 (136/820).
Encoding transition End_Ext_Acc_20_9 (137/820).
Encoding transition End_Ext_Acc_19_9 (138/820).
Encoding transition End_Ext_Acc_18_9 (139/820).
Encoding transition End_Ext_Acc_5_10 (140/820).
Encoding transition End_Ext_Acc_4_10 (141/820).
Encoding transition End_Ext_Acc_3_10 (142/820).
Encoding transition End_Ext_Acc_2_10 (143/820).
Encoding transition End_Ext_Acc_19_6 (144/820).
Encoding transition End_Ext_Acc_20_6 (145/820).
Encoding transition End_Ext_Acc_1_7 (146/820).
Encoding transition End_Ext_Acc_2_7 (147/820).
Encoding transition End_Ext_Acc_3_7 (148/820).
Encoding transition End_Ext_Acc_4_7 (149/820).
Encoding transition End_Ext_Acc_5_7 (150/820).
Encoding transition End_Ext_Acc_6_7 (151/820).
Encoding transition End_Ext_Acc_8_7 (152/820).
Encoding transition End_Ext_Acc_9_7 (153/820).
Encoding transition End_Ext_Acc_10_7 (154/820).
Encoding transition End_Ext_Acc_11_7 (155/820).
Encoding transition End_Ext_Acc_12_7 (156/820).
Encoding transition End_Ext_Acc_13_7 (157/820).
Encoding transition End_Ext_Acc_14_7 (158/820).
Encoding transition End_Ext_Acc_15_7 (159/820).
Encoding transition End_Ext_Acc_17_7 (160/820).
Encoding transition End_Ext_Acc_16_7 (161/820).
Encoding transition End_Ext_Acc_19_7 (162/820).
Encoding transition End_Ext_Acc_18_7 (163/820).
Encoding transition End_Ext_Acc_1_8 (164/820).
Encoding transition End_Ext_Acc_20_7 (165/820).
Encoding transition End_Ext_Acc_3_8 (166/820).
Encoding transition End_Ext_Acc_2_8 (167/820).
Encoding transition End_Ext_Acc_5_8 (168/820).
Encoding transition End_Ext_Acc_4_8 (169/820).
Encoding transition End_Ext_Acc_7_8 (170/820).
Encoding transition End_Ext_Acc_6_8 (171/820).
Encoding transition End_Ext_Acc_10_8 (172/820).
Encoding transition End_Ext_Acc_9_8 (173/820).
Encoding transition End_Ext_Acc_12_8 (174/820).
Encoding transition End_Ext_Acc_11_8 (175/820).
Encoding transition End_Ext_Acc_16_12 (176/820).
Encoding transition End_Ext_Acc_15_12 (177/820).
Encoding transition End_Ext_Acc_14_12 (178/820).
Encoding transition End_Ext_Acc_13_12 (179/820).
Encoding transition End_Ext_Acc_11_12 (180/820).
Encoding transition End_Ext_Acc_10_12 (181/820).
Encoding transition End_Ext_Acc_9_12 (182/820).
Encoding transition End_Ext_Acc_8_12 (183/820).
Encoding transition End_Ext_Acc_7_12 (184/820).
Encoding transition End_Ext_Acc_6_12 (185/820).
Encoding transition End_Ext_Acc_5_12 (186/820).
Encoding transition End_Ext_Acc_4_12 (187/820).
Encoding transition End_Ext_Acc_3_12 (188/820).
Encoding transition End_Ext_Acc_2_12 (189/820).
Encoding transition End_Ext_Acc_1_12 (190/820).
Encoding transition End_Ext_Acc_20_11 (191/820).
Encoding transition End_Ext_Acc_11_13 (192/820).
Encoding transition End_Ext_Acc_12_13 (193/820).
Encoding transition End_Ext_Acc_9_13 (194/820).
Encoding transition End_Ext_Acc_10_13 (195/820).
Encoding transition End_Ext_Acc_7_13 (196/820).
Encoding transition End_Ext_Acc_8_13 (197/820).
Encoding transition End_Ext_Acc_5_13 (198/820).
Encoding transition End_Ext_Acc_6_13 (199/820).
Encoding transition End_Ext_Acc_3_13 (200/820).
Encoding transition End_Ext_Acc_4_13 (201/820).
Encoding transition End_Ext_Acc_1_13 (202/820).
Encoding transition End_Ext_Acc_2_13 (203/820).
Encoding transition End_Ext_Acc_19_12 (204/820).
Encoding transition End_Ext_Acc_20_12 (205/820).
Encoding transition End_Ext_Acc_17_12 (206/820).
Encoding transition End_Ext_Acc_18_12 (207/820).
Encoding transition End_Ext_Acc_20_10 (208/820).
Encoding transition End_Ext_Acc_19_10 (209/820).
Encoding transition End_Ext_Acc_2_11 (210/820).
Encoding transition End_Ext_Acc_1_11 (211/820).
Encoding transition End_Ext_Acc_16_10 (212/820).
Encoding transition End_Ext_Acc_15_10 (213/820).
Encoding transition End_Ext_Acc_18_10 (214/820).
Encoding transition End_Ext_Acc_17_10 (215/820).
Encoding transition End_Ext_Acc_12_10 (216/820).
Encoding transition End_Ext_Acc_11_10 (217/820).
Encoding transition End_Ext_Acc_14_10 (218/820).
Encoding transition End_Ext_Acc_13_10 (219/820).
Encoding transition End_Ext_Acc_7_10 (220/820).
Encoding transition End_Ext_Acc_6_10 (221/820).
Encoding transition End_Ext_Acc_9_10 (222/820).
Encoding transition End_Ext_Acc_8_10 (223/820).
Encoding transition End_Ext_Acc_16_11 (224/820).
Encoding transition End_Ext_Acc_17_11 (225/820).
Encoding transition End_Ext_Acc_18_11 (226/820).
Encoding transition End_Ext_Acc_19_11 (227/820).
Encoding transition End_Ext_Acc_12_11 (228/820).
Encoding transition End_Ext_Acc_13_11 (229/820).
Encoding transition End_Ext_Acc_14_11 (230/820).
Encoding transition End_Ext_Acc_15_11 (231/820).
Encoding transition End_Ext_Acc_7_11 (232/820).
Encoding transition End_Ext_Acc_8_11 (233/820).
Encoding transition End_Ext_Acc_9_11 (234/820).
Encoding transition End_Ext_Acc_10_11 (235/820).
Encoding transition End_Ext_Acc_3_11 (236/820).
Encoding transition End_Ext_Acc_4_11 (237/820).
Encoding transition End_Ext_Acc_5_11 (238/820).
Encoding transition End_Ext_Acc_6_11 (239/820).
Encoding transition End_Ext_Acc_19_15 (240/820).
Encoding transition End_Ext_Acc_18_15 (241/820).
Encoding transition End_Ext_Acc_17_15 (242/820).
Encoding transition End_Ext_Acc_16_15 (243/820).
Encoding transition End_Ext_Acc_3_16 (244/820).
Encoding transition End_Ext_Acc_2_16 (245/820).
Encoding transition End_Ext_Acc_1_16 (246/820).
Encoding transition End_Ext_Acc_20_15 (247/820).
Encoding transition End_Ext_Acc_10_15 (248/820).
Encoding transition End_Ext_Acc_9_15 (249/820).
Encoding transition End_Ext_Acc_8_15 (250/820).
Encoding transition End_Ext_Acc_7_15 (251/820).
Encoding transition End_Ext_Acc_14_15 (252/820).
Encoding transition End_Ext_Acc_13_15 (253/820).
Encoding transition End_Ext_Acc_12_15 (254/820).
Encoding transition End_Ext_Acc_11_15 (255/820).
Encoding transition End_Ext_Acc_14_16 (256/820).
Encoding transition End_Ext_Acc_15_16 (257/820).
Encoding transition End_Ext_Acc_12_16 (258/820).
Encoding transition End_Ext_Acc_13_16 (259/820).
Encoding transition End_Ext_Acc_19_16 (260/820).
Encoding transition End_Ext_Acc_20_16 (261/820).
Encoding transition End_Ext_Acc_17_16 (262/820).
Encoding transition End_Ext_Acc_18_16 (263/820).
Encoding transition End_Ext_Acc_6_16 (264/820).
Encoding transition End_Ext_Acc_7_16 (265/820).
Encoding transition End_Ext_Acc_4_16 (266/820).
Encoding transition End_Ext_Acc_5_16 (267/820).
Encoding transition End_Ext_Acc_10_16 (268/820).
Encoding transition End_Ext_Acc_11_16 (269/820).
Encoding transition End_Ext_Acc_8_16 (270/820).
Encoding transition End_Ext_Acc_9_16 (271/820).
Encoding transition End_Ext_Acc_3_14 (272/820).
Encoding transition End_Ext_Acc_2_14 (273/820).
Encoding transition End_Ext_Acc_5_14 (274/820).
Encoding transition End_Ext_Acc_4_14 (275/820).
Encoding transition End_Ext_Acc_7_14 (276/820).
Encoding transition End_Ext_Acc_6_14 (277/820).
Encoding transition End_Ext_Acc_9_14 (278/820).
Encoding transition End_Ext_Acc_8_14 (279/820).
Encoding transition End_Ext_Acc_15_13 (280/820).
Encoding transition End_Ext_Acc_14_13 (281/820).
Encoding transition End_Ext_Acc_17_13 (282/820).
Encoding transition End_Ext_Acc_16_13 (283/820).
Encoding transition End_Ext_Acc_19_13 (284/820).
Encoding transition End_Ext_Acc_18_13 (285/820).
Encoding transition End_Ext_Acc_1_14 (286/820).
Encoding transition End_Ext_Acc_20_13 (287/820).
Encoding transition End_Ext_Acc_19_14 (288/820).
Encoding transition End_Ext_Acc_20_14 (289/820).
Encoding transition End_Ext_Acc_1_15 (290/820).
Encoding transition End_Ext_Acc_2_15 (291/820).
Encoding transition End_Ext_Acc_3_15 (292/820).
Encoding transition End_Ext_Acc_4_15 (293/820).
Encoding transition End_Ext_Acc_5_15 (294/820).
Encoding transition End_Ext_Acc_6_15 (295/820).
Encoding transition End_Ext_Acc_10_14 (296/820).
Encoding transition End_Ext_Acc_11_14 (297/820).
Encoding transition End_Ext_Acc_12_14 (298/820).
Encoding transition End_Ext_Acc_13_14 (299/820).
Encoding transition End_Ext_Acc_15_14 (300/820).
Encoding transition End_Ext_Acc_16_14 (301/820).
Encoding transition End_Ext_Acc_17_14 (302/820).
Encoding transition End_Ext_Acc_18_14 (303/820).
Encoding transition End_Ext_Acc_16_19 (304/820).
Encoding transition End_Ext_Acc_15_19 (305/820).
Encoding transition End_Ext_Acc_18_19 (306/820).
Encoding transition End_Ext_Acc_17_19 (307/820).
Encoding transition End_Ext_Acc_12_19 (308/820).
Encoding transition End_Ext_Acc_11_19 (309/820).
Encoding transition End_Ext_Acc_14_19 (310/820).
Encoding transition End_Ext_Acc_13_19 (311/820).
Encoding transition End_Ext_Acc_5_20 (312/820).
Encoding transition End_Ext_Acc_4_20 (313/820).
Encoding transition End_Ext_Acc_7_20 (314/820).
Encoding transition End_Ext_Acc_6_20 (315/820).
Encoding transition End_Ext_Acc_1_20 (316/820).
Encoding transition End_Ext_Acc_20_19 (317/820).
Encoding transition End_Ext_Acc_3_20 (318/820).
Encoding transition End_Ext_Acc_2_20 (319/820).
Encoding transition End_Ext_Acc_19_18 (320/820).
Encoding transition End_Ext_Acc_20_18 (321/820).
Encoding transition End_Ext_Acc_1_19 (322/820).
Encoding transition End_Ext_Acc_2_19 (323/820).
Encoding transition End_Ext_Acc_14_18 (324/820).
Encoding transition End_Ext_Acc_15_18 (325/820).
Encoding transition End_Ext_Acc_16_18 (326/820).
Encoding transition End_Ext_Acc_17_18 (327/820).
Encoding transition End_Ext_Acc_7_19 (328/820).
Encoding transition End_Ext_Acc_8_19 (329/820).
Encoding transition End_Ext_Acc_9_19 (330/820).
Encoding transition End_Ext_Acc_10_19 (331/820).
Encoding transition End_Ext_Acc_3_19 (332/820).
Encoding transition End_Ext_Acc_4_19 (333/820).
Encoding transition End_Ext_Acc_5_19 (334/820).
Encoding transition End_Ext_Acc_6_19 (335/820).
Encoding transition End_Ext_Acc_5_18 (336/820).
Encoding transition End_Ext_Acc_4_18 (337/820).
Encoding transition End_Ext_Acc_3_18 (338/820).
Encoding transition End_Ext_Acc_2_18 (339/820).
Encoding transition End_Ext_Acc_1_18 (340/820).
Encoding transition End_Ext_Acc_20_17 (341/820).
Encoding transition End_Ext_Acc_19_17 (342/820).
Encoding transition End_Ext_Acc_18_17 (343/820).
Encoding transition End_Ext_Acc_13_18 (344/820).
Encoding transition End_Ext_Acc_12_18 (345/820).
Encoding transition End_Ext_Acc_11_18 (346/820).
Encoding transition End_Ext_Acc_10_18 (347/820).
Encoding transition End_Ext_Acc_9_18 (348/820).
Encoding transition End_Ext_Acc_8_18 (349/820).
Encoding transition End_Ext_Acc_7_18 (350/820).
Encoding transition End_Ext_Acc_6_18 (351/820).
Encoding transition End_Ext_Acc_7_17 (352/820).
Encoding transition End_Ext_Acc_8_17 (353/820).
Encoding transition End_Ext_Acc_5_17 (354/820).
Encoding transition End_Ext_Acc_6_17 (355/820).
Encoding transition End_Ext_Acc_3_17 (356/820).
Encoding transition End_Ext_Acc_4_17 (357/820).
Encoding transition End_Ext_Acc_1_17 (358/820).
Encoding transition End_Ext_Acc_2_17 (359/820).
Encoding transition End_Ext_Acc_15_17 (360/820).
Encoding transition End_Ext_Acc_16_17 (361/820).
Encoding transition End_Ext_Acc_13_17 (362/820).
Encoding transition End_Ext_Acc_14_17 (363/820).
Encoding transition End_Ext_Acc_11_17 (364/820).
Encoding transition End_Ext_Acc_12_17 (365/820).
Encoding transition End_Ext_Acc_9_17 (366/820).
Encoding transition End_Ext_Acc_10_17 (367/820).
Encoding transition Begin_Ext_Acc_20_2 (368/820).
Encoding transition Begin_Ext_Acc_19_2 (369/820).
Encoding transition Begin_Ext_Acc_2_3 (370/820).
Encoding transition Begin_Ext_Acc_1_3 (371/820).
Encoding transition Begin_Ext_Acc_5_3 (372/820).
Encoding transition Begin_Ext_Acc_4_3 (373/820).
Encoding transition Begin_Ext_Acc_7_3 (374/820).
Encoding transition Begin_Ext_Acc_6_3 (375/820).
Encoding transition Begin_Ext_Acc_9_3 (376/820).
Encoding transition Begin_Ext_Acc_8_3 (377/820).
Encoding transition Begin_Ext_Acc_11_3 (378/820).
Encoding transition Begin_Ext_Acc_10_3 (379/820).
Encoding transition Begin_Ext_Acc_13_3 (380/820).
Encoding transition Begin_Ext_Acc_12_3 (381/820).
Encoding transition Begin_Ext_Acc_15_3 (382/820).
Encoding transition Begin_Ext_Acc_14_3 (383/820).
Encoding transition Begin_Ext_Acc_3_2 (384/820).
Encoding transition Begin_Ext_Acc_4_2 (385/820).
Encoding transition Begin_Ext_Acc_5_2 (386/820).
Encoding transition Begin_Ext_Acc_6_2 (387/820).
Encoding transition Begin_Ext_Acc_7_2 (388/820).
Encoding transition Begin_Ext_Acc_8_2 (389/820).
Encoding transition Begin_Ext_Acc_9_2 (390/820).
Encoding transition Begin_Ext_Acc_10_2 (391/820).
Encoding transition Begin_Ext_Acc_11_2 (392/820).
Encoding transition Begin_Ext_Acc_12_2 (393/820).
Encoding transition Begin_Ext_Acc_13_2 (394/820).
Encoding transition Begin_Ext_Acc_14_2 (395/820).
Encoding transition Begin_Ext_Acc_15_2 (396/820).
Encoding transition Begin_Ext_Acc_16_2 (397/820).
Encoding transition Begin_Ext_Acc_17_2 (398/820).
Encoding transition Begin_Ext_Acc_18_2 (399/820).
Encoding transition Begin_Ext_Acc_9_1 (400/820).
Encoding transition Begin_Ext_Acc_8_1 (401/820).
Encoding transition Begin_Ext_Acc_7_1 (402/820).
Encoding transition Begin_Ext_Acc_6_1 (403/820).
Encoding transition Begin_Ext_Acc_13_1 (404/820).
Encoding transition Begin_Ext_Acc_12_1 (405/820).
Encoding transition Begin_Ext_Acc_11_1 (406/820).
Encoding transition Begin_Ext_Acc_10_1 (407/820).
Encoding transition Begin_Ext_Acc_17_1 (408/820).
Encoding transition Begin_Ext_Acc_16_1 (409/820).
Encoding transition Begin_Ext_Acc_15_1 (410/820).
Encoding transition Begin_Ext_Acc_14_1 (411/820).
Encoding transition Begin_Ext_Acc_1_2 (412/820).
Encoding transition Begin_Ext_Acc_20_1 (413/820).
Encoding transition Begin_Ext_Acc_19_1 (414/820).
Encoding transition Begin_Ext_Acc_18_1 (415/820).
Encoding transition End_Ext_Acc_10_20 (416/820).
Encoding transition End_Ext_Acc_11_20 (417/820).
Encoding transition End_Ext_Acc_8_20 (418/820).
Encoding transition End_Ext_Acc_9_20 (419/820).
Encoding transition End_Ext_Acc_14_20 (420/820).
Encoding transition End_Ext_Acc_15_20 (421/820).
Encoding transition End_Ext_Acc_12_20 (422/820).
Encoding transition End_Ext_Acc_13_20 (423/820).
Encoding transition End_Ext_Acc_18_20 (424/820).
Encoding transition End_Ext_Acc_19_20 (425/820).
Encoding transition End_Ext_Acc_16_20 (426/820).
Encoding transition End_Ext_Acc_17_20 (427/820).
Encoding transition Begin_Ext_Acc_4_1 (428/820).
Encoding transition Begin_Ext_Acc_5_1 (429/820).
Encoding transition Begin_Ext_Acc_2_1 (430/820).
Encoding transition Begin_Ext_Acc_3_1 (431/820).
Encoding transition Begin_Ext_Acc_19_6 (432/820).
Encoding transition Begin_Ext_Acc_20_6 (433/820).
Encoding transition Begin_Ext_Acc_1_7 (434/820).
Encoding transition Begin_Ext_Acc_2_7 (435/820).
Encoding transition Begin_Ext_Acc_15_6 (436/820).
Encoding transition Begin_Ext_Acc_16_6 (437/820).
Encoding transition Begin_Ext_Acc_17_6 (438/820).
Encoding transition Begin_Ext_Acc_18_6 (439/820).
Encoding transition Begin_Ext_Acc_11_6 (440/820).
Encoding transition Begin_Ext_Acc_12_6 (441/820).
Encoding transition Begin_Ext_Acc_13_6 (442/820).
Encoding transition Begin_Ext_Acc_14_6 (443/820).
Encoding transition Begin_Ext_Acc_7_6 (444/820).
Encoding transition Begin_Ext_Acc_8_6 (445/820).
Encoding transition Begin_Ext_Acc_9_6 (446/820).
Encoding transition Begin_Ext_Acc_10_6 (447/820).
Encoding transition Begin_Ext_Acc_3_6 (448/820).
Encoding transition Begin_Ext_Acc_2_6 (449/820).
Encoding transition Begin_Ext_Acc_5_6 (450/820).
Encoding transition Begin_Ext_Acc_4_6 (451/820).
Encoding transition Begin_Ext_Acc_19_5 (452/820).
Encoding transition Begin_Ext_Acc_18_5 (453/820).
Encoding transition Begin_Ext_Acc_1_6 (454/820).
Encoding transition Begin_Ext_Acc_20_5 (455/820).
Encoding transition Begin_Ext_Acc_15_5 (456/820).
Encoding transition Begin_Ext_Acc_14_5 (457/820).
Encoding transition Begin_Ext_Acc_17_5 (458/820).
Encoding transition Begin_Ext_Acc_16_5 (459/820).
Encoding transition Begin_Ext_Acc_11_5 (460/820).
Encoding transition Begin_Ext_Acc_10_5 (461/820).
Encoding transition Begin_Ext_Acc_13_5 (462/820).
Encoding transition Begin_Ext_Acc_12_5 (463/820).
Encoding transition Begin_Ext_Acc_8_5 (464/820).
Encoding transition Begin_Ext_Acc_9_5 (465/820).
Encoding transition Begin_Ext_Acc_6_5 (466/820).
Encoding transition Begin_Ext_Acc_7_5 (467/820).
Encoding transition Begin_Ext_Acc_3_5 (468/820).
Encoding transition Begin_Ext_Acc_4_5 (469/820).
Encoding transition Begin_Ext_Acc_1_5 (470/820).
Encoding transition Begin_Ext_Acc_2_5 (471/820).
Encoding transition Begin_Ext_Acc_19_4 (472/820).
Encoding transition Begin_Ext_Acc_20_4 (473/820).
Encoding transition Begin_Ext_Acc_17_4 (474/820).
Encoding transition Begin_Ext_Acc_18_4 (475/820).
Encoding transition Begin_Ext_Acc_15_4 (476/820).
Encoding transition Begin_Ext_Acc_16_4 (477/820).
Encoding transition Begin_Ext_Acc_13_4 (478/820).
Encoding transition Begin_Ext_Acc_14_4 (479/820).
Encoding transition Begin_Ext_Acc_12_4 (480/820).
Encoding transition Begin_Ext_Acc_11_4 (481/820).
Encoding transition Begin_Ext_Acc_10_4 (482/820).
Encoding transition Begin_Ext_Acc_9_4 (483/820).
Encoding transition Begin_Ext_Acc_8_4 (484/820).
Encoding transition Begin_Ext_Acc_7_4 (485/820).
Encoding transition Begin_Ext_Acc_6_4 (486/820).
Encoding transition Begin_Ext_Acc_5_4 (487/820).
Encoding transition Begin_Ext_Acc_3_4 (488/820).
Encoding transition Begin_Ext_Acc_2_4 (489/820).
Encoding transition Begin_Ext_Acc_1_4 (490/820).
Encoding transition Begin_Ext_Acc_20_3 (491/820).
Encoding transition Begin_Ext_Acc_19_3 (492/820).
Encoding transition Begin_Ext_Acc_18_3 (493/820).
Encoding transition Begin_Ext_Acc_17_3 (494/820).
Encoding transition Begin_Ext_Acc_16_3 (495/820).
Encoding transition Begin_Ext_Acc_2_10 (496/820).
Encoding transition Begin_Ext_Acc_3_10 (497/820).
Encoding transition Begin_Ext_Acc_4_10 (498/820).
Encoding transition Begin_Ext_Acc_5_10 (499/820).
Encoding transition Begin_Ext_Acc_6_10 (500/820).
Encoding transition Begin_Ext_Acc_7_10 (501/820).
Encoding transition Begin_Ext_Acc_8_10 (502/820).
Encoding transition Begin_Ext_Acc_9_10 (503/820).
Encoding transition Begin_Ext_Acc_14_9 (504/820).
Encoding transition Begin_Ext_Acc_15_9 (505/820).
Encoding transition Begin_Ext_Acc_16_9 (506/820).
Encoding transition Begin_Ext_Acc_17_9 (507/820).
Encoding transition Begin_Ext_Acc_18_9 (508/820).
Encoding transition Begin_Ext_Acc_19_9 (509/820).
Encoding transition Begin_Ext_Acc_20_9 (510/820).
Encoding transition Begin_Ext_Acc_1_10 (511/820).
Encoding transition Begin_Ext_Acc_6_9 (512/820).
Encoding transition Begin_Ext_Acc_5_9 (513/820).
Encoding transition Begin_Ext_Acc_8_9 (514/820).
Encoding transition Begin_Ext_Acc_7_9 (515/820).
Encoding transition Begin_Ext_Acc_11_9 (516/820).
Encoding transition Begin_Ext_Acc_10_9 (517/820).
Encoding transition Begin_Ext_Acc_13_9 (518/820).
Encoding transition Begin_Ext_Acc_12_9 (519/820).
Encoding transition Begin_Ext_Acc_18_8 (520/820).
Encoding transition Begin_Ext_Acc_17_8 (521/820).
Encoding transition Begin_Ext_Acc_20_8 (522/820).
Encoding transition Begin_Ext_Acc_19_8 (523/820).
Encoding transition Begin_Ext_Acc_2_9 (524/820).
Encoding transition Begin_Ext_Acc_1_9 (525/820).
Encoding transition Begin_Ext_Acc_4_9 (526/820).
Encoding transition Begin_Ext_Acc_3_9 (527/820).
Encoding transition Begin_Ext_Acc_11_8 (528/820).
Encoding transition Begin_Ext_Acc_12_8 (529/820).
Encoding transition Begin_Ext_Acc_9_8 (530/820).
Encoding transition Begin_Ext_Acc_10_8 (531/820).
Encoding transition Begin_Ext_Acc_15_8 (532/820).
Encoding transition Begin_Ext_Acc_16_8 (533/820).
Encoding transition Begin_Ext_Acc_13_8 (534/820).
Encoding transition Begin_Ext_Acc_14_8 (535/820).
Encoding transition Begin_Ext_Acc_2_8 (536/820).
Encoding transition Begin_Ext_Acc_3_8 (537/820).
Encoding transition Begin_Ext_Acc_20_7 (538/820).
Encoding transition Begin_Ext_Acc_1_8 (539/820).
Encoding transition Begin_Ext_Acc_6_8 (540/820).
Encoding transition Begin_Ext_Acc_7_8 (541/820).
Encoding transition Begin_Ext_Acc_4_8 (542/820).
Encoding transition Begin_Ext_Acc_5_8 (543/820).
Encoding transition Begin_Ext_Acc_15_7 (544/820).
Encoding transition Begin_Ext_Acc_14_7 (545/820).
Encoding transition Begin_Ext_Acc_13_7 (546/820).
Encoding transition Begin_Ext_Acc_12_7 (547/820).
Encoding transition Begin_Ext_Acc_19_7 (548/820).
Encoding transition Begin_Ext_Acc_18_7 (549/820).
Encoding transition Begin_Ext_Acc_17_7 (550/820).
Encoding transition Begin_Ext_Acc_16_7 (551/820).
Encoding transition Begin_Ext_Acc_6_7 (552/820).
Encoding transition Begin_Ext_Acc_5_7 (553/820).
Encoding transition Begin_Ext_Acc_4_7 (554/820).
Encoding transition Begin_Ext_Acc_3_7 (555/820).
Encoding transition Begin_Ext_Acc_11_7 (556/820).
Encoding transition Begin_Ext_Acc_10_7 (557/820).
Encoding transition Begin_Ext_Acc_9_7 (558/820).
Encoding transition Begin_Ext_Acc_8_7 (559/820).
Encoding transition Begin_Ext_Acc_10_14 (560/820).
Encoding transition Begin_Ext_Acc_11_14 (561/820).
Encoding transition Begin_Ext_Acc_12_14 (562/820).
Encoding transition Begin_Ext_Acc_13_14 (563/820).
Encoding transition Begin_Ext_Acc_6_14 (564/820).
Encoding transition Begin_Ext_Acc_7_14 (565/820).
Encoding transition Begin_Ext_Acc_8_14 (566/820).
Encoding transition Begin_Ext_Acc_9_14 (567/820).
Encoding transition Begin_Ext_Acc_2_14 (568/820).
Encoding transition Begin_Ext_Acc_3_14 (569/820).
Encoding transition Begin_Ext_Acc_4_14 (570/820).
Encoding transition Begin_Ext_Acc_5_14 (571/820).
Encoding transition Begin_Ext_Acc_18_13 (572/820).
Encoding transition Begin_Ext_Acc_19_13 (573/820).
Encoding transition Begin_Ext_Acc_20_13 (574/820).
Encoding transition Begin_Ext_Acc_1_14 (575/820).
Encoding transition Begin_Ext_Acc_8_15 (576/820).
Encoding transition Begin_Ext_Acc_7_15 (577/820).
Encoding transition Begin_Ext_Acc_10_15 (578/820).
Encoding transition Begin_Ext_Acc_9_15 (579/820).
Encoding transition Begin_Ext_Acc_4_15 (580/820).
Encoding transition Begin_Ext_Acc_3_15 (581/820).
Encoding transition Begin_Ext_Acc_6_15 (582/820).
Encoding transition Begin_Ext_Acc_5_15 (583/820).
Encoding transition Begin_Ext_Acc_20_14 (584/820).
Encoding transition Begin_Ext_Acc_19_14 (585/820).
Encoding transition Begin_Ext_Acc_2_15 (586/820).
Encoding transition Begin_Ext_Acc_1_15 (587/820).
Encoding transition Begin_Ext_Acc_16_14 (588/820).
Encoding transition Begin_Ext_Acc_15_14 (589/820).
Encoding transition Begin_Ext_Acc_18_14 (590/820).
Encoding transition Begin_Ext_Acc_17_14 (591/820).
Encoding transition Begin_Ext_Acc_6_16 (592/820).
Encoding transition Begin_Ext_Acc_7_16 (593/820).
Encoding transition Begin_Ext_Acc_4_16 (594/820).
Encoding transition Begin_Ext_Acc_5_16 (595/820).
Encoding transition Begin_Ext_Acc_2_16 (596/820).
Encoding transition Begin_Ext_Acc_3_16 (597/820).
Encoding transition Begin_Ext_Acc_20_15 (598/820).
Encoding transition Begin_Ext_Acc_1_16 (599/820).
Encoding transition Begin_Ext_Acc_18_15 (600/820).
Encoding transition Begin_Ext_Acc_19_15 (601/820).
Encoding transition Begin_Ext_Acc_16_15 (602/820).
Encoding transition Begin_Ext_Acc_17_15 (603/820).
Encoding transition Begin_Ext_Acc_13_15 (604/820).
Encoding transition Begin_Ext_Acc_14_15 (605/820).
Encoding transition Begin_Ext_Acc_11_15 (606/820).
Encoding transition Begin_Ext_Acc_12_15 (607/820).
Encoding transition Begin_Ext_Acc_4_17 (608/820).
Encoding transition Begin_Ext_Acc_3_17 (609/820).
Encoding transition Begin_Ext_Acc_2_17 (610/820).
Encoding transition Begin_Ext_Acc_1_17 (611/820).
Encoding transition Begin_Ext_Acc_20_16 (612/820).
Encoding transition Begin_Ext_Acc_19_16 (613/820).
Encoding transition Begin_Ext_Acc_18_16 (614/820).
Encoding transition Begin_Ext_Acc_17_16 (615/820).
Encoding transition Begin_Ext_Acc_15_16 (616/820).
Encoding transition Begin_Ext_Acc_14_16 (617/820).
Encoding transition Begin_Ext_Acc_13_16 (618/820).
Encoding transition Begin_Ext_Acc_12_16 (619/820).
Encoding transition Begin_Ext_Acc_11_16 (620/820).
Encoding transition Begin_Ext_Acc_10_16 (621/820).
Encoding transition Begin_Ext_Acc_9_16 (622/820).
Encoding transition Begin_Ext_Acc_8_16 (623/820).
Encoding transition Begin_Ext_Acc_19_10 (624/820).
Encoding transition Begin_Ext_Acc_20_10 (625/820).
Encoding transition Begin_Ext_Acc_1_11 (626/820).
Encoding transition Begin_Ext_Acc_2_11 (627/820).
Encoding transition Begin_Ext_Acc_3_11 (628/820).
Encoding transition Begin_Ext_Acc_4_11 (629/820).
Encoding transition Begin_Ext_Acc_5_11 (630/820).
Encoding transition Begin_Ext_Acc_6_11 (631/820).
Encoding transition Begin_Ext_Acc_11_10 (632/820).
Encoding transition Begin_Ext_Acc_12_10 (633/820).
Encoding transition Begin_Ext_Acc_13_10 (634/820).
Encoding transition Begin_Ext_Acc_14_10 (635/820).
Encoding transition Begin_Ext_Acc_15_10 (636/820).
Encoding transition Begin_Ext_Acc_16_10 (637/820).
Encoding transition Begin_Ext_Acc_17_10 (638/820).
Encoding transition Begin_Ext_Acc_18_10 (639/820).
Encoding transition Begin_Ext_Acc_17_11 (640/820).
Encoding transition Begin_Ext_Acc_16_11 (641/820).
Encoding transition Begin_Ext_Acc_19_11 (642/820).
Encoding transition Begin_Ext_Acc_18_11 (643/820).
Encoding transition Begin_Ext_Acc_1_12 (644/820).
Encoding transition Begin_Ext_Acc_20_11 (645/820).
Encoding transition Begin_Ext_Acc_3_12 (646/820).
Encoding transition Begin_Ext_Acc_2_12 (647/820).
Encoding transition Begin_Ext_Acc_8_11 (648/820).
Encoding transition Begin_Ext_Acc_7_11 (649/820).
Encoding transition Begin_Ext_Acc_10_11 (650/820).
Encoding transition Begin_Ext_Acc_9_11 (651/820).
Encoding transition Begin_Ext_Acc_13_11 (652/820).
Encoding transition Begin_Ext_Acc_12_11 (653/820).
Encoding transition Begin_Ext_Acc_15_11 (654/820).
Encoding transition Begin_Ext_Acc_14_11 (655/820).
Encoding transition Begin_Ext_Acc_15_12 (656/820).
Encoding transition Begin_Ext_Acc_16_12 (657/820).
Encoding transition Begin_Ext_Acc_13_12 (658/820).
Encoding transition Begin_Ext_Acc_14_12 (659/820).
Encoding transition Begin_Ext_Acc_19_12 (660/820).
Encoding transition Begin_Ext_Acc_20_12 (661/820).
Encoding transition Begin_Ext_Acc_17_12 (662/820).
Encoding transition Begin_Ext_Acc_18_12 (663/820).
Encoding transition Begin_Ext_Acc_6_12 (664/820).
Encoding transition Begin_Ext_Acc_7_12 (665/820).
Encoding transition Begin_Ext_Acc_4_12 (666/820).
Encoding transition Begin_Ext_Acc_5_12 (667/820).
Encoding transition Begin_Ext_Acc_10_12 (668/820).
Encoding transition Begin_Ext_Acc_11_12 (669/820).
Encoding transition Begin_Ext_Acc_8_12 (670/820).
Encoding transition Begin_Ext_Acc_9_12 (671/820).
Encoding transition Begin_Ext_Acc_12_13 (672/820).
Encoding transition Begin_Ext_Acc_11_13 (673/820).
Encoding transition Begin_Ext_Acc_10_13 (674/820).
Encoding transition Begin_Ext_Acc_9_13 (675/820).
Encoding transition Begin_Ext_Acc_17_13 (676/820).
Encoding transition Begin_Ext_Acc_16_13 (677/820).
Encoding transition Begin_Ext_Acc_15_13 (678/820).
Encoding transition Begin_Ext_Acc_14_13 (679/820).
Encoding transition Begin_Ext_Acc_4_13 (680/820).
Encoding transition Begin_Ext_Acc_3_13 (681/820).
Encoding transition Begin_Ext_Acc_2_13 (682/820).
Encoding transition Begin_Ext_Acc_1_13 (683/820).
Encoding transition Begin_Ext_Acc_8_13 (684/820).
Encoding transition Begin_Ext_Acc_7_13 (685/820).
Encoding transition Begin_Ext_Acc_6_13 (686/820).
Encoding transition Begin_Ext_Acc_5_13 (687/820).
Encoding transition Begin_Ext_Acc_17_20 (688/820).
Encoding transition Begin_Ext_Acc_16_20 (689/820).
Encoding transition Begin_Ext_Acc_19_20 (690/820).
Encoding transition Begin_Ext_Acc_18_20 (691/820).
Encoding transition Begin_Ext_Acc_13_20 (692/820).
Encoding transition Begin_Ext_Acc_12_20 (693/820).
Encoding transition Begin_Ext_Acc_15_20 (694/820).
Encoding transition Begin_Ext_Acc_14_20 (695/820).
Encoding transition Req_Ext_Acc_6 (696/820).
Encoding transition Req_Ext_Acc_5 (697/820).
Encoding transition Req_Ext_Acc_8 (698/820).
Encoding transition Req_Ext_Acc_7 (699/820).
Encoding transition Req_Ext_Acc_2 (700/820).
Encoding transition Req_Ext_Acc_1 (701/820).
Encoding transition Req_Ext_Acc_4 (702/820).
Encoding transition Req_Ext_Acc_3 (703/820).
Encoding transition Req_Ext_Acc_13 (704/820).
Encoding transition Req_Ext_Acc_14 (705/820).
Encoding transition Req_Ext_Acc_15 (706/820).
Encoding transition Req_Ext_Acc_16 (707/820).
Encoding transition Req_Ext_Acc_9 (708/820).
Encoding transition Req_Ext_Acc_10 (709/820).
Encoding transition Req_Ext_Acc_11 (710/820).
Encoding transition Req_Ext_Acc_12 (711/820).
Encoding transition End_Own_Acc_1_1 (712/820).
Encoding transition End_Own_Acc_2_2 (713/820).
Encoding transition End_Own_Acc_3_3 (714/820).
Encoding transition End_Own_Acc_4_4 (715/820).
Encoding transition Req_Ext_Acc_17 (716/820).
Encoding transition Req_Ext_Acc_18 (717/820).
Encoding transition Req_Ext_Acc_19 (718/820).
Encoding transition Req_Ext_Acc_20 (719/820).
Encoding transition End_Own_Acc_12_12 (720/820).
Encoding transition End_Own_Acc_11_11 (721/820).
Encoding transition End_Own_Acc_10_10 (722/820).
Encoding transition End_Own_Acc_9_9 (723/820).
Encoding transition End_Own_Acc_8_8 (724/820).
Encoding transition End_Own_Acc_7_7 (725/820).
Encoding transition End_Own_Acc_6_6 (726/820).
Encoding transition End_Own_Acc_5_5 (727/820).
Encoding transition End_Own_Acc_20_20 (728/820).
Encoding transition End_Own_Acc_19_19 (729/820).
Encoding transition End_Own_Acc_18_18 (730/820).
Encoding transition End_Own_Acc_17_17 (731/820).
Encoding transition End_Own_Acc_16_16 (732/820).
Encoding transition End_Own_Acc_15_15 (733/820).
Encoding transition End_Own_Acc_14_14 (734/820).
Encoding transition End_Own_Acc_13_13 (735/820).
Encoding transition Begin_Own_Acc_7 (736/820).
Encoding transition Begin_Own_Acc_8 (737/820).
Encoding transition Begin_Own_Acc_5 (738/820).
Encoding transition Begin_Own_Acc_6 (739/820).
Encoding transition Begin_Own_Acc_3 (740/820).
Encoding transition Begin_Own_Acc_4 (741/820).
Encoding transition Begin_Own_Acc_1 (742/820).
Encoding transition Begin_Own_Acc_2 (743/820).
Encoding transition Begin_Own_Acc_15 (744/820).
Encoding transition Begin_Own_Acc_16 (745/820).
Encoding transition Begin_Own_Acc_13 (746/820).
Encoding transition Begin_Own_Acc_14 (747/820).
Encoding transition Begin_Own_Acc_11 (748/820).
Encoding transition Begin_Own_Acc_12 (749/820).
Encoding transition Begin_Own_Acc_9 (750/820).
Encoding transition Begin_Own_Acc_10 (751/820).
Encoding transition Begin_Ext_Acc_6_17 (752/820).
Encoding transition Begin_Ext_Acc_5_17 (753/820).
Encoding transition Begin_Ext_Acc_8_17 (754/820).
Encoding transition Begin_Ext_Acc_7_17 (755/820).
Encoding transition Begin_Ext_Acc_10_17 (756/820).
Encoding transition Begin_Ext_Acc_9_17 (757/820).
Encoding transition Begin_Ext_Acc_12_17 (758/820).
Encoding transition Begin_Ext_Acc_11_17 (759/820).
Encoding transition Begin_Ext_Acc_14_17 (760/820).
Encoding transition Begin_Ext_Acc_13_17 (761/820).
Encoding transition Begin_Ext_Acc_16_17 (762/820).
Encoding transition Begin_Ext_Acc_15_17 (763/820).
Encoding transition Begin_Ext_Acc_19_17 (764/820).
Encoding transition Begin_Ext_Acc_18_17 (765/820).
Encoding transition Begin_Ext_Acc_1_18 (766/820).
Encoding transition Begin_Ext_Acc_20_17 (767/820).
Encoding transition Begin_Ext_Acc_2_18 (768/820).
Encoding transition Begin_Ext_Acc_3_18 (769/820).
Encoding transition Begin_Ext_Acc_4_18 (770/820).
Encoding transition Begin_Ext_Acc_5_18 (771/820).
Encoding transition Begin_Ext_Acc_6_18 (772/820).
Encoding transition Begin_Ext_Acc_7_18 (773/820).
Encoding transition Begin_Ext_Acc_8_18 (774/820).
Encoding transition Begin_Ext_Acc_9_18 (775/820).
Encoding transition Begin_Ext_Acc_10_18 (776/820).
Encoding transition Begin_Ext_Acc_11_18 (777/820).
Encoding transition Begin_Ext_Acc_12_18 (778/820).
Encoding transition Begin_Ext_Acc_13_18 (779/820).
Encoding transition Begin_Ext_Acc_14_18 (780/820).
Encoding transition Begin_Ext_Acc_15_18 (781/820).
Encoding transition Begin_Ext_Acc_16_18 (782/820).
Encoding transition Begin_Ext_Acc_17_18 (783/820).
Encoding transition Begin_Ext_Acc_2_19 (784/820).
Encoding transition Begin_Ext_Acc_1_19 (785/820).
Encoding transition Begin_Ext_Acc_20_18 (786/820).
Encoding transition Begin_Ext_Acc_19_18 (787/820).
Encoding transition Begin_Ext_Acc_6_19 (788/820).
Encoding transition Begin_Ext_Acc_5_19 (789/820).
Encoding transition Begin_Ext_Acc_4_19 (790/820).
Encoding transition Begin_Ext_Acc_3_19 (791/820).
Encoding transition Begin_Ext_Acc_10_19 (792/820).
Encoding transition Begin_Ext_Acc_9_19 (793/820).
Encoding transition Begin_Ext_Acc_8_19 (794/820).
Encoding transition Begin_Ext_Acc_7_19 (795/820).
Encoding transition Begin_Ext_Acc_14_19 (796/820).
Encoding transition Begin_Ext_Acc_13_19 (797/820).
Encoding transition Begin_Ext_Acc_12_19 (798/820).
Encoding transition Begin_Ext_Acc_11_19 (799/820).
Encoding transition Begin_Ext_Acc_17_19 (800/820).
Encoding transition Begin_Ext_Acc_18_19 (801/820).
Encoding transition Begin_Ext_Acc_15_19 (802/820).
Encoding transition Begin_Ext_Acc_16_19 (803/820).
Encoding transition Begin_Ext_Acc_2_20 (804/820).
Encoding transition Begin_Ext_Acc_3_20 (805/820).
Encoding transition Begin_Ext_Acc_20_19 (806/820).
Encoding transition Begin_Ext_Acc_1_20 (807/820).
Encoding transition Begin_Ext_Acc_6_20 (808/820).
Encoding transition Begin_Ext_Acc_7_20 (809/820).
Encoding transition Begin_Ext_Acc_4_20 (810/820).
Encoding transition Begin_Ext_Acc_5_20 (811/820).
Encoding transition Begin_Ext_Acc_10_20 (812/820).
Encoding transition Begin_Ext_Acc_11_20 (813/820).
Encoding transition Begin_Ext_Acc_8_20 (814/820).
Encoding transition Begin_Ext_Acc_9_20 (815/820).
Encoding transition Begin_Own_Acc_19 (816/820).
Encoding transition Begin_Own_Acc_20 (817/820).
Encoding transition Begin_Own_Acc_17 (818/820).
Encoding transition Begin_Own_Acc_18 (819/820).
----------------------------------------
End firing rule encoding

----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------

Total Used Memory: 66588KB
CANNOT_COMPUTE

BK_STOP 1400688739962

--------------------
content from stderr:

MEDDLY Error: Insufficient memory

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

set -x
# this is for BenchKit: configuration of major elements for the test
export BK_INPUT="SurpriseSharedMemory-PT-000020"
export BK_EXAMINATION="ReachabilityFireability"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/srv/fko/BK_RESULTS/OUTPUTS"
export BK_TIME_CONFINEMENT="3600"

# this is specific to your benchmark or test

export BIN_DIR="$HOME/BenchKit/bin"

# remove the execution directoty if it exists (to avoid increse of .vmdk images)
if [ -d execution ] ; then
rm -rf execution
fi

tar xzf /home/mcc/BenchKit/INPUTS/SurpriseSharedMemory-PT-000020.tgz
mv SurpriseSharedMemory-PT-000020 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is SurpriseSharedMemory-PT-000020, examination is ReachabilityFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r07ks-ovh1-140068246001515"
echo "====================================================================="
echo
echo "--------------------"
echo "content from stdout:"
echo
echo -n "BK_START "
date -u +%s%3N
timeout -s 9 $BK_TIME_CONFINEMENT bash -c "/home/mcc/BenchKit/BenchKit_head.sh 2> STDERR ; echo ; echo -n \"BK_STOP \" ; date -u +%s%3N"
if [ $? -eq 137 ] ; then
echo
echo "BK_TIME_CONFINEMENT_REACHED"
fi
echo
echo "--------------------"
echo "content from stderr:"
echo
cat STDERR ;