About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
5497.74 | 1290236 | 159.6 | CC | normal |
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-1667
Executing tool greatspn
Input is Peterson-PT-6, examination is CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r03kn-qhx2-140036872301126
=====================================================================
--------------------
content from stdout:
BK_START 1400398093430
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Peterson (PT), instance 6
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/CTLCardinality.xml INTO /home/mcc/execution/CTLCardinality.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -P -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLCardinality.rgmedd-ctl
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition Loop_0_0_0 (0/2030).
Encoding transition EndLoop_6_5 (1/2030).
Encoding transition EndLoop_5_5 (2/2030).
Encoding transition EndLoop_4_5 (3/2030).
Encoding transition EndLoop_3_5 (4/2030).
Encoding transition EndLoop_2_5 (5/2030).
Encoding transition EndLoop_1_5 (6/2030).
Encoding transition EndLoop_0_5 (7/2030).
Encoding transition EndLoop_6_4 (8/2030).
Encoding transition EndLoop_5_4 (9/2030).
Encoding transition EndLoop_4_4 (10/2030).
Encoding transition EndLoop_3_4 (11/2030).
Encoding transition EndLoop_2_4 (12/2030).
Encoding transition EndLoop_1_4 (13/2030).
Encoding transition EndLoop_0_4 (14/2030).
Encoding transition EndLoop_6_3 (15/2030).
Encoding transition EndLoop_4_3 (16/2030).
Encoding transition EndLoop_5_3 (17/2030).
Encoding transition EndLoop_2_3 (18/2030).
Encoding transition EndLoop_3_3 (19/2030).
Encoding transition EndLoop_0_3 (20/2030).
Encoding transition EndLoop_1_3 (21/2030).
Encoding transition EndLoop_5_2 (22/2030).
Encoding transition EndLoop_6_2 (23/2030).
Encoding transition EndLoop_3_2 (24/2030).
Encoding transition EndLoop_4_2 (25/2030).
Encoding transition EndLoop_1_2 (26/2030).
Encoding transition EndLoop_2_2 (27/2030).
Encoding transition EndLoop_6_1 (28/2030).
Encoding transition EndLoop_0_2 (29/2030).
Encoding transition EndLoop_4_1 (30/2030).
Encoding transition EndLoop_5_1 (31/2030).
Encoding transition Loop_2_4_0 (32/2030).
Encoding transition Loop_1_4_0 (33/2030).
Encoding transition Loop_4_4_0 (34/2030).
Encoding transition Loop_3_4_0 (35/2030).
Encoding transition Loop_5_3_0 (36/2030).
Encoding transition Loop_4_3_0 (37/2030).
Encoding transition Loop_0_4_0 (38/2030).
Encoding transition Loop_6_3_0 (39/2030).
Encoding transition Loop_1_3_0 (40/2030).
Encoding transition Loop_0_3_0 (41/2030).
Encoding transition Loop_3_3_0 (42/2030).
Encoding transition Loop_2_3_0 (43/2030).
Encoding transition Loop_4_2_0 (44/2030).
Encoding transition Loop_3_2_0 (45/2030).
Encoding transition Loop_6_2_0 (46/2030).
Encoding transition Loop_5_2_0 (47/2030).
Encoding transition Loop_6_1_0 (48/2030).
Encoding transition Loop_0_2_0 (49/2030).
Encoding transition Loop_1_2_0 (50/2030).
Encoding transition Loop_2_2_0 (51/2030).
Encoding transition Loop_2_1_0 (52/2030).
Encoding transition Loop_3_1_0 (53/2030).
Encoding transition Loop_4_1_0 (54/2030).
Encoding transition Loop_5_1_0 (55/2030).
Encoding transition Loop_5_0_0 (56/2030).
Encoding transition Loop_6_0_0 (57/2030).
Encoding transition Loop_0_1_0 (58/2030).
Encoding transition Loop_1_1_0 (59/2030).
Encoding transition Loop_1_0_0 (60/2030).
Encoding transition Loop_2_0_0 (61/2030).
Encoding transition Loop_3_0_0 (62/2030).
Encoding transition Loop_4_0_0 (63/2030).
Encoding transition EndLoop_4_0 (64/2030).
Encoding transition EndLoop_3_0 (65/2030).
Encoding transition EndLoop_6_0 (66/2030).
Encoding transition EndLoop_5_0 (67/2030).
Encoding transition EndLoop_1_1 (68/2030).
Encoding transition EndLoop_0_1 (69/2030).
Encoding transition EndLoop_3_1 (70/2030).
Encoding transition EndLoop_2_1 (71/2030).
Encoding transition EndLoop_0_0 (72/2030).
Encoding transition EndLoop_2_0 (73/2030).
Encoding transition EndLoop_1_0 (74/2030).
Encoding transition Loop_0_5_2 (75/2030).
Encoding transition Loop_1_5_2 (76/2030).
Encoding transition Loop_5_4_2 (77/2030).
Encoding transition Loop_6_4_2 (78/2030).
Encoding transition Loop_3_4_2 (79/2030).
Encoding transition Loop_4_4_2 (80/2030).
Encoding transition Loop_1_4_2 (81/2030).
Encoding transition Loop_2_4_2 (82/2030).
Encoding transition Loop_1_0_3 (83/2030).
Encoding transition Loop_2_0_3 (84/2030).
Encoding transition Loop_6_5_2 (85/2030).
Encoding transition Loop_0_0_3 (86/2030).
Encoding transition Loop_4_5_2 (87/2030).
Encoding transition Loop_5_5_2 (88/2030).
Encoding transition Loop_2_5_2 (89/2030).
Encoding transition Loop_3_5_2 (90/2030).
Encoding transition Loop_6_2_2 (91/2030).
Encoding transition Loop_5_2_2 (92/2030).
Encoding transition Loop_4_2_2 (93/2030).
Encoding transition Loop_3_2_2 (94/2030).
Encoding transition Loop_2_2_2 (95/2030).
Encoding transition Loop_1_2_2 (96/2030).
Encoding transition Loop_0_2_2 (97/2030).
Encoding transition Loop_6_1_2 (98/2030).
Encoding transition Loop_0_4_2 (99/2030).
Encoding transition Loop_6_3_2 (100/2030).
Encoding transition Loop_5_3_2 (101/2030).
Encoding transition Loop_4_3_2 (102/2030).
Encoding transition Loop_3_3_2 (103/2030).
Encoding transition Loop_2_3_2 (104/2030).
Encoding transition Loop_1_3_2 (105/2030).
Encoding transition Loop_0_3_2 (106/2030).
Encoding transition Loop_2_3_3 (107/2030).
Encoding transition Loop_3_3_3 (108/2030).
Encoding transition Loop_4_3_3 (109/2030).
Encoding transition Loop_5_3_3 (110/2030).
Encoding transition Loop_5_2_3 (111/2030).
Encoding transition Loop_6_2_3 (112/2030).
Encoding transition Loop_0_3_3 (113/2030).
Encoding transition Loop_1_3_3 (114/2030).
Encoding transition Loop_3_4_3 (115/2030).
Encoding transition Loop_4_4_3 (116/2030).
Encoding transition Loop_5_4_3 (117/2030).
Encoding transition Loop_6_4_3 (118/2030).
Encoding transition Loop_6_3_3 (119/2030).
Encoding transition Loop_0_4_3 (120/2030).
Encoding transition Loop_1_4_3 (121/2030).
Encoding transition Loop_2_4_3 (122/2030).
Encoding transition Loop_1_1_3 (123/2030).
Encoding transition Loop_0_1_3 (124/2030).
Encoding transition Loop_3_1_3 (125/2030).
Encoding transition Loop_2_1_3 (126/2030).
Encoding transition Loop_4_0_3 (127/2030).
Encoding transition Loop_3_0_3 (128/2030).
Encoding transition Loop_6_0_3 (129/2030).
Encoding transition Loop_5_0_3 (130/2030).
Encoding transition Loop_2_2_3 (131/2030).
Encoding transition Loop_1_2_3 (132/2030).
Encoding transition Loop_4_2_3 (133/2030).
Encoding transition Loop_3_2_3 (134/2030).
Encoding transition Loop_5_1_3 (135/2030).
Encoding transition Loop_4_1_3 (136/2030).
Encoding transition Loop_0_2_3 (137/2030).
Encoding transition Loop_6_1_3 (138/2030).
Encoding transition Loop_2_1_1 (139/2030).
Encoding transition Loop_3_1_1 (140/2030).
Encoding transition Loop_0_1_1 (141/2030).
Encoding transition Loop_1_1_1 (142/2030).
Encoding transition Loop_6_1_1 (143/2030).
Encoding transition Loop_0_2_1 (144/2030).
Encoding transition Loop_4_1_1 (145/2030).
Encoding transition Loop_5_1_1 (146/2030).
Encoding transition Loop_3_2_1 (147/2030).
Encoding transition Loop_4_2_1 (148/2030).
Encoding transition Loop_1_2_1 (149/2030).
Encoding transition Loop_2_2_1 (150/2030).
Encoding transition Loop_0_3_1 (151/2030).
Encoding transition Loop_1_3_1 (152/2030).
Encoding transition Loop_5_2_1 (153/2030).
Encoding transition Loop_6_2_1 (154/2030).
Encoding transition Loop_1_5_0 (155/2030).
Encoding transition Loop_0_5_0 (156/2030).
Encoding transition Loop_6_4_0 (157/2030).
Encoding transition Loop_5_4_0 (158/2030).
Encoding transition Loop_5_5_0 (159/2030).
Encoding transition Loop_4_5_0 (160/2030).
Encoding transition Loop_3_5_0 (161/2030).
Encoding transition Loop_2_5_0 (162/2030).
Encoding transition Loop_2_0_1 (163/2030).
Encoding transition Loop_1_0_1 (164/2030).
Encoding transition Loop_0_0_1 (165/2030).
Encoding transition Loop_6_5_0 (166/2030).
Encoding transition Loop_6_0_1 (167/2030).
Encoding transition Loop_5_0_1 (168/2030).
Encoding transition Loop_4_0_1 (169/2030).
Encoding transition Loop_3_0_1 (170/2030).
Encoding transition Loop_4_5_1 (171/2030).
Encoding transition Loop_5_5_1 (172/2030).
Encoding transition Loop_6_5_1 (173/2030).
Encoding transition Loop_0_0_2 (174/2030).
Encoding transition Loop_1_0_2 (175/2030).
Encoding transition Loop_2_0_2 (176/2030).
Encoding transition Loop_3_0_2 (177/2030).
Encoding transition Loop_4_0_2 (178/2030).
Encoding transition Loop_5_0_2 (179/2030).
Encoding transition Loop_6_0_2 (180/2030).
Encoding transition Loop_0_1_2 (181/2030).
Encoding transition Loop_1_1_2 (182/2030).
Encoding transition Loop_2_1_2 (183/2030).
Encoding transition Loop_3_1_2 (184/2030).
Encoding transition Loop_4_1_2 (185/2030).
Encoding transition Loop_5_1_2 (186/2030).
Encoding transition Loop_3_3_1 (187/2030).
Encoding transition Loop_2_3_1 (188/2030).
Encoding transition Loop_5_3_1 (189/2030).
Encoding transition Loop_4_3_1 (190/2030).
Encoding transition Loop_0_4_1 (191/2030).
Encoding transition Loop_6_3_1 (192/2030).
Encoding transition Loop_2_4_1 (193/2030).
Encoding transition Loop_1_4_1 (194/2030).
Encoding transition Loop_4_4_1 (195/2030).
Encoding transition Loop_3_4_1 (196/2030).
Encoding transition Loop_6_4_1 (197/2030).
Encoding transition Loop_5_4_1 (198/2030).
Encoding transition Loop_1_5_1 (199/2030).
Encoding transition Loop_0_5_1 (200/2030).
Encoding transition Loop_3_5_1 (201/2030).
Encoding transition Loop_2_5_1 (202/2030).
Encoding transition Alone1_4_2_0 (203/2030).
Encoding transition Alone1_5_2_0 (204/2030).
Encoding transition Alone1_1_2_0 (205/2030).
Encoding transition Alone1_3_2_0 (206/2030).
Encoding transition Alone1_1_3_0 (207/2030).
Encoding transition Alone1_2_3_0 (208/2030).
Encoding transition Alone1_6_2_0 (209/2030).
Encoding transition Alone1_0_3_0 (210/2030).
Encoding transition Alone1_2_1_0 (211/2030).
Encoding transition Alone1_3_1_0 (212/2030).
Encoding transition Alone1_6_0_0 (213/2030).
Encoding transition Alone1_0_1_0 (214/2030).
Encoding transition Alone1_6_1_0 (215/2030).
Encoding transition Alone1_0_2_0 (216/2030).
Encoding transition Alone1_4_1_0 (217/2030).
Encoding transition Alone1_5_1_0 (218/2030).
Encoding transition Alone1_2_5_0 (219/2030).
Encoding transition Alone1_1_5_0 (220/2030).
Encoding transition Alone1_0_5_0 (221/2030).
Encoding transition Alone1_6_4_0 (222/2030).
Encoding transition Alone1_0_6_0 (223/2030).
Encoding transition Alone1_6_5_0 (224/2030).
Encoding transition Alone1_4_5_0 (225/2030).
Encoding transition Alone1_3_5_0 (226/2030).
Encoding transition Alone1_0_4_0 (227/2030).
Encoding transition Alone1_6_3_0 (228/2030).
Encoding transition Alone1_5_3_0 (229/2030).
Encoding transition Alone1_4_3_0 (230/2030).
Encoding transition Alone1_5_4_0 (231/2030).
Encoding transition Alone1_3_4_0 (232/2030).
Encoding transition Alone1_2_4_0 (233/2030).
Encoding transition Alone1_1_4_0 (234/2030).
Encoding transition Loop_2_3_5 (235/2030).
Encoding transition Loop_3_3_5 (236/2030).
Encoding transition Loop_4_3_5 (237/2030).
Encoding transition Loop_5_3_5 (238/2030).
Encoding transition Loop_6_3_5 (239/2030).
Encoding transition Loop_0_4_5 (240/2030).
Encoding transition Loop_1_4_5 (241/2030).
Encoding transition Loop_2_4_5 (242/2030).
Encoding transition Loop_1_2_5 (243/2030).
Encoding transition Loop_2_2_5 (244/2030).
Encoding transition Loop_3_2_5 (245/2030).
Encoding transition Loop_4_2_5 (246/2030).
Encoding transition Loop_5_2_5 (247/2030).
Encoding transition Loop_6_2_5 (248/2030).
Encoding transition Loop_0_3_5 (249/2030).
Encoding transition Loop_1_3_5 (250/2030).
Encoding transition Loop_5_5_5 (251/2030).
Encoding transition Loop_4_5_5 (252/2030).
Encoding transition Alone1_1_0_0 (253/2030).
Encoding transition Loop_6_5_5 (254/2030).
Encoding transition Alone1_3_0_0 (255/2030).
Encoding transition Alone1_2_0_0 (256/2030).
Encoding transition Alone1_5_0_0 (257/2030).
Encoding transition Alone1_4_0_0 (258/2030).
Encoding transition Loop_4_4_5 (259/2030).
Encoding transition Loop_3_4_5 (260/2030).
Encoding transition Loop_6_4_5 (261/2030).
Encoding transition Loop_5_4_5 (262/2030).
Encoding transition Loop_1_5_5 (263/2030).
Encoding transition Loop_0_5_5 (264/2030).
Encoding transition Loop_3_5_5 (265/2030).
Encoding transition Loop_2_5_5 (266/2030).
Encoding transition Loop_4_5_4 (267/2030).
Encoding transition Loop_5_5_4 (268/2030).
Encoding transition Loop_2_5_4 (269/2030).
Encoding transition Loop_3_5_4 (270/2030).
Encoding transition Loop_0_5_4 (271/2030).
Encoding transition Loop_1_5_4 (272/2030).
Encoding transition Loop_5_4_4 (273/2030).
Encoding transition Loop_6_4_4 (274/2030).
Encoding transition Loop_3_4_4 (275/2030).
Encoding transition Loop_4_4_4 (276/2030).
Encoding transition Loop_1_4_4 (277/2030).
Encoding transition Loop_2_4_4 (278/2030).
Encoding transition Loop_6_3_4 (279/2030).
Encoding transition Loop_0_4_4 (280/2030).
Encoding transition Loop_4_3_4 (281/2030).
Encoding transition Loop_5_3_4 (282/2030).
Encoding transition Loop_0_2_5 (283/2030).
Encoding transition Loop_6_1_5 (284/2030).
Encoding transition Loop_5_1_5 (285/2030).
Encoding transition Loop_4_1_5 (286/2030).
Encoding transition Loop_3_1_5 (287/2030).
Encoding transition Loop_2_1_5 (288/2030).
Encoding transition Loop_1_1_5 (289/2030).
Encoding transition Loop_0_1_5 (290/2030).
Encoding transition Loop_6_0_5 (291/2030).
Encoding transition Loop_5_0_5 (292/2030).
Encoding transition Loop_4_0_5 (293/2030).
Encoding transition Loop_3_0_5 (294/2030).
Encoding transition Loop_2_0_5 (295/2030).
Encoding transition Loop_1_0_5 (296/2030).
Encoding transition Loop_0_0_5 (297/2030).
Encoding transition Loop_6_5_4 (298/2030).
Encoding transition Loop_5_0_4 (299/2030).
Encoding transition Loop_6_0_4 (300/2030).
Encoding transition Loop_0_1_4 (301/2030).
Encoding transition Loop_1_1_4 (302/2030).
Encoding transition Loop_1_0_4 (303/2030).
Encoding transition Loop_2_0_4 (304/2030).
Encoding transition Loop_3_0_4 (305/2030).
Encoding transition Loop_4_0_4 (306/2030).
Encoding transition Loop_4_5_3 (307/2030).
Encoding transition Loop_5_5_3 (308/2030).
Encoding transition Loop_6_5_3 (309/2030).
Encoding transition Loop_0_0_4 (310/2030).
Encoding transition Loop_0_5_3 (311/2030).
Encoding transition Loop_1_5_3 (312/2030).
Encoding transition Loop_2_5_3 (313/2030).
Encoding transition Loop_3_5_3 (314/2030).
Encoding transition Loop_1_3_4 (315/2030).
Encoding transition Loop_0_3_4 (316/2030).
Encoding transition Loop_3_3_4 (317/2030).
Encoding transition Loop_2_3_4 (318/2030).
Encoding transition Loop_4_2_4 (319/2030).
Encoding transition Loop_3_2_4 (320/2030).
Encoding transition Loop_6_2_4 (321/2030).
Encoding transition Loop_5_2_4 (322/2030).
Encoding transition Loop_0_2_4 (323/2030).
Encoding transition Loop_6_1_4 (324/2030).
Encoding transition Loop_2_2_4 (325/2030).
Encoding transition Loop_1_2_4 (326/2030).
Encoding transition Loop_3_1_4 (327/2030).
Encoding transition Loop_2_1_4 (328/2030).
Encoding transition Loop_5_1_4 (329/2030).
Encoding transition Loop_4_1_4 (330/2030).
Encoding transition Alone1_5_1_3 (331/2030).
Encoding transition Alone1_4_1_3 (332/2030).
Encoding transition Alone1_3_1_3 (333/2030).
Encoding transition Alone1_2_1_3 (334/2030).
Encoding transition Alone1_3_2_3 (335/2030).
Encoding transition Alone1_1_2_3 (336/2030).
Encoding transition Alone1_0_2_3 (337/2030).
Encoding transition Alone1_6_1_3 (338/2030).
Encoding transition Alone1_0_3_3 (339/2030).
Encoding transition Alone1_6_2_3 (340/2030).
Encoding transition Alone1_5_2_3 (341/2030).
Encoding transition Alone1_4_2_3 (342/2030).
Encoding transition Alone1_5_3_3 (343/2030).
Encoding transition Alone1_4_3_3 (344/2030).
Encoding transition Alone1_2_3_3 (345/2030).
Encoding transition Alone1_1_3_3 (346/2030).
Encoding transition Alone1_1_4_3 (347/2030).
Encoding transition Alone1_2_4_3 (348/2030).
Encoding transition Alone1_6_3_3 (349/2030).
Encoding transition Alone1_0_4_3 (350/2030).
Encoding transition Alone1_6_4_3 (351/2030).
Encoding transition Alone1_0_5_3 (352/2030).
Encoding transition Alone1_3_4_3 (353/2030).
Encoding transition Alone1_5_4_3 (354/2030).
Encoding transition Alone1_3_5_3 (355/2030).
Encoding transition Alone1_4_5_3 (356/2030).
Encoding transition Alone1_1_5_3 (357/2030).
Encoding transition Alone1_2_5_3 (358/2030).
Encoding transition Alone1_1_6_3 (359/2030).
Encoding transition Alone1_2_6_3 (360/2030).
Encoding transition Alone1_6_5_3 (361/2030).
Encoding transition Alone1_0_6_3 (362/2030).
Encoding transition Alone1_0_3_2 (363/2030).
Encoding transition Alone1_6_2_2 (364/2030).
Encoding transition Alone1_2_3_2 (365/2030).
Encoding transition Alone1_1_3_2 (366/2030).
Encoding transition Alone1_5_3_2 (367/2030).
Encoding transition Alone1_4_3_2 (368/2030).
Encoding transition Alone1_0_4_2 (369/2030).
Encoding transition Alone1_6_3_2 (370/2030).
Encoding transition Alone1_2_4_2 (371/2030).
Encoding transition Alone1_1_4_2 (372/2030).
Encoding transition Alone1_5_4_2 (373/2030).
Encoding transition Alone1_3_4_2 (374/2030).
Encoding transition Alone1_0_5_2 (375/2030).
Encoding transition Alone1_6_4_2 (376/2030).
Encoding transition Alone1_2_5_2 (377/2030).
Encoding transition Alone1_1_5_2 (378/2030).
Encoding transition Alone1_3_5_2 (379/2030).
Encoding transition Alone1_4_5_2 (380/2030).
Encoding transition Alone1_6_5_2 (381/2030).
Encoding transition Alone1_0_6_2 (382/2030).
Encoding transition Alone1_1_6_2 (383/2030).
Encoding transition Alone1_2_6_2 (384/2030).
Encoding transition Alone1_3_6_2 (385/2030).
Encoding transition Alone1_4_6_2 (386/2030).
Encoding transition Alone1_5_6_2 (387/2030).
Encoding transition Alone1_1_0_3 (388/2030).
Encoding transition Alone1_2_0_3 (389/2030).
Encoding transition Alone1_3_0_3 (390/2030).
Encoding transition Alone1_4_0_3 (391/2030).
Encoding transition Alone1_5_0_3 (392/2030).
Encoding transition Alone1_6_0_3 (393/2030).
Encoding transition Alone1_0_1_3 (394/2030).
Encoding transition Alone1_4_5_1 (395/2030).
Encoding transition Alone1_3_5_1 (396/2030).
Encoding transition Alone1_2_5_1 (397/2030).
Encoding transition Alone1_1_5_1 (398/2030).
Encoding transition Alone1_0_5_1 (399/2030).
Encoding transition Alone1_6_4_1 (400/2030).
Encoding transition Alone1_5_4_1 (401/2030).
Encoding transition Alone1_3_4_1 (402/2030).
Encoding transition Alone1_1_0_2 (403/2030).
Encoding transition Alone1_5_6_1 (404/2030).
Encoding transition Alone1_4_6_1 (405/2030).
Encoding transition Alone1_3_6_1 (406/2030).
Encoding transition Alone1_2_6_1 (407/2030).
Encoding transition Alone1_1_6_1 (408/2030).
Encoding transition Alone1_0_6_1 (409/2030).
Encoding transition Alone1_6_5_1 (410/2030).
Encoding transition Alone1_2_1_2 (411/2030).
Encoding transition Alone1_3_1_2 (412/2030).
Encoding transition Alone1_6_0_2 (413/2030).
Encoding transition Alone1_0_1_2 (414/2030).
Encoding transition Alone1_4_0_2 (415/2030).
Encoding transition Alone1_5_0_2 (416/2030).
Encoding transition Alone1_2_0_2 (417/2030).
Encoding transition Alone1_3_0_2 (418/2030).
Encoding transition Alone1_4_2_2 (419/2030).
Encoding transition Alone1_5_2_2 (420/2030).
Encoding transition Alone1_1_2_2 (421/2030).
Encoding transition Alone1_3_2_2 (422/2030).
Encoding transition Alone1_6_1_2 (423/2030).
Encoding transition Alone1_0_2_2 (424/2030).
Encoding transition Alone1_4_1_2 (425/2030).
Encoding transition Alone1_5_1_2 (426/2030).
Encoding transition Alone1_1_0_1 (427/2030).
Encoding transition Alone1_5_6_0 (428/2030).
Encoding transition Alone1_3_0_1 (429/2030).
Encoding transition Alone1_2_0_1 (430/2030).
Encoding transition Alone1_2_6_0 (431/2030).
Encoding transition Alone1_1_6_0 (432/2030).
Encoding transition Alone1_4_6_0 (433/2030).
Encoding transition Alone1_3_6_0 (434/2030).
Encoding transition Alone1_3_1_1 (435/2030).
Encoding transition Alone1_2_1_1 (436/2030).
Encoding transition Alone1_5_1_1 (437/2030).
Encoding transition Alone1_4_1_1 (438/2030).
Encoding transition Alone1_5_0_1 (439/2030).
Encoding transition Alone1_4_0_1 (440/2030).
Encoding transition Alone1_0_1_1 (441/2030).
Encoding transition Alone1_6_0_1 (442/2030).
Encoding transition Alone1_4_2_1 (443/2030).
Encoding transition Alone1_5_2_1 (444/2030).
Encoding transition Alone1_6_2_1 (445/2030).
Encoding transition Alone1_0_3_1 (446/2030).
Encoding transition Alone1_6_1_1 (447/2030).
Encoding transition Alone1_0_2_1 (448/2030).
Encoding transition Alone1_1_2_1 (449/2030).
Encoding transition Alone1_3_2_1 (450/2030).
Encoding transition Alone1_6_3_1 (451/2030).
Encoding transition Alone1_0_4_1 (452/2030).
Encoding transition Alone1_1_4_1 (453/2030).
Encoding transition Alone1_2_4_1 (454/2030).
Encoding transition Alone1_1_3_1 (455/2030).
Encoding transition Alone1_2_3_1 (456/2030).
Encoding transition Alone1_4_3_1 (457/2030).
Encoding transition Alone1_5_3_1 (458/2030).
Encoding transition NotAlone_4_5_0 (459/2030).
Encoding transition NotAlone_3_5_0 (460/2030).
Encoding transition NotAlone_0_6_0 (461/2030).
Encoding transition NotAlone_6_5_0 (462/2030).
Encoding transition NotAlone_2_6_0 (463/2030).
Encoding transition NotAlone_1_6_0 (464/2030).
Encoding transition NotAlone_4_6_0 (465/2030).
Encoding transition NotAlone_3_6_0 (466/2030).
Encoding transition NotAlone_2_4_0 (467/2030).
Encoding transition NotAlone_1_4_0 (468/2030).
Encoding transition NotAlone_5_4_0 (469/2030).
Encoding transition NotAlone_3_4_0 (470/2030).
Encoding transition NotAlone_0_5_0 (471/2030).
Encoding transition NotAlone_6_4_0 (472/2030).
Encoding transition NotAlone_2_5_0 (473/2030).
Encoding transition NotAlone_1_5_0 (474/2030).
Encoding transition NotAlone_6_2_0 (475/2030).
Encoding transition NotAlone_0_3_0 (476/2030).
Encoding transition NotAlone_1_3_0 (477/2030).
Encoding transition NotAlone_2_3_0 (478/2030).
Encoding transition NotAlone_4_3_0 (479/2030).
Encoding transition NotAlone_5_3_0 (480/2030).
Encoding transition NotAlone_6_3_0 (481/2030).
Encoding transition NotAlone_0_4_0 (482/2030).
Encoding transition NotAlone_4_1_0 (483/2030).
Encoding transition NotAlone_5_1_0 (484/2030).
Encoding transition NotAlone_6_1_0 (485/2030).
Encoding transition NotAlone_0_2_0 (486/2030).
Encoding transition NotAlone_1_2_0 (487/2030).
Encoding transition NotAlone_3_2_0 (488/2030).
Encoding transition NotAlone_4_2_0 (489/2030).
Encoding transition NotAlone_5_2_0 (490/2030).
Encoding transition NotAlone_5_0_0 (491/2030).
Encoding transition NotAlone_4_0_0 (492/2030).
Encoding transition NotAlone_3_0_0 (493/2030).
Encoding transition NotAlone_2_0_0 (494/2030).
Encoding transition NotAlone_3_1_0 (495/2030).
Encoding transition NotAlone_2_1_0 (496/2030).
Encoding transition NotAlone_0_1_0 (497/2030).
Encoding transition NotAlone_6_0_0 (498/2030).
Encoding transition Alone1_2_6_5 (499/2030).
Encoding transition Alone1_1_6_5 (500/2030).
Encoding transition Alone1_0_6_5 (501/2030).
Encoding transition Alone1_6_5_5 (502/2030).
Encoding transition NotAlone_1_0_0 (503/2030).
Encoding transition Alone1_5_6_5 (504/2030).
Encoding transition Alone1_4_6_5 (505/2030).
Encoding transition Alone1_3_6_5 (506/2030).
Encoding transition Alone1_6_4_5 (507/2030).
Encoding transition Alone1_0_5_5 (508/2030).
Encoding transition Alone1_3_4_5 (509/2030).
Encoding transition Alone1_5_4_5 (510/2030).
Encoding transition Alone1_3_5_5 (511/2030).
Encoding transition Alone1_4_5_5 (512/2030).
Encoding transition Alone1_1_5_5 (513/2030).
Encoding transition Alone1_2_5_5 (514/2030).
Encoding transition Alone1_4_3_5 (515/2030).
Encoding transition Alone1_5_3_5 (516/2030).
Encoding transition Alone1_1_3_5 (517/2030).
Encoding transition Alone1_2_3_5 (518/2030).
Encoding transition Alone1_1_4_5 (519/2030).
Encoding transition Alone1_2_4_5 (520/2030).
Encoding transition Alone1_6_3_5 (521/2030).
Encoding transition Alone1_0_4_5 (522/2030).
Encoding transition Alone1_5_2_5 (523/2030).
Encoding transition Alone1_4_2_5 (524/2030).
Encoding transition Alone1_0_3_5 (525/2030).
Encoding transition Alone1_6_2_5 (526/2030).
Encoding transition Alone1_0_2_5 (527/2030).
Encoding transition Alone1_6_1_5 (528/2030).
Encoding transition Alone1_3_2_5 (529/2030).
Encoding transition Alone1_1_2_5 (530/2030).
Encoding transition Alone1_3_1_5 (531/2030).
Encoding transition Alone1_2_1_5 (532/2030).
Encoding transition Alone1_5_1_5 (533/2030).
Encoding transition Alone1_4_1_5 (534/2030).
Encoding transition Alone1_5_0_5 (535/2030).
Encoding transition Alone1_4_0_5 (536/2030).
Encoding transition Alone1_0_1_5 (537/2030).
Encoding transition Alone1_6_0_5 (538/2030).
Encoding transition Alone1_5_6_4 (539/2030).
Encoding transition Alone1_1_0_5 (540/2030).
Encoding transition Alone1_2_0_5 (541/2030).
Encoding transition Alone1_3_0_5 (542/2030).
Encoding transition Alone1_1_6_4 (543/2030).
Encoding transition Alone1_2_6_4 (544/2030).
Encoding transition Alone1_3_6_4 (545/2030).
Encoding transition Alone1_4_6_4 (546/2030).
Encoding transition Alone1_3_5_4 (547/2030).
Encoding transition Alone1_4_5_4 (548/2030).
Encoding transition Alone1_6_5_4 (549/2030).
Encoding transition Alone1_0_6_4 (550/2030).
Encoding transition Alone1_6_4_4 (551/2030).
Encoding transition Alone1_0_5_4 (552/2030).
Encoding transition Alone1_1_5_4 (553/2030).
Encoding transition Alone1_2_5_4 (554/2030).
Encoding transition Alone1_5_4_4 (555/2030).
Encoding transition Alone1_3_4_4 (556/2030).
Encoding transition Alone1_2_4_4 (557/2030).
Encoding transition Alone1_1_4_4 (558/2030).
Encoding transition Alone1_0_4_4 (559/2030).
Encoding transition Alone1_6_3_4 (560/2030).
Encoding transition Alone1_5_3_4 (561/2030).
Encoding transition Alone1_4_3_4 (562/2030).
Encoding transition Alone1_2_3_4 (563/2030).
Encoding transition Alone1_1_3_4 (564/2030).
Encoding transition Alone1_0_3_4 (565/2030).
Encoding transition Alone1_6_2_4 (566/2030).
Encoding transition Alone1_5_2_4 (567/2030).
Encoding transition Alone1_4_2_4 (568/2030).
Encoding transition Alone1_3_2_4 (569/2030).
Encoding transition Alone1_1_2_4 (570/2030).
Encoding transition Alone1_6_1_4 (571/2030).
Encoding transition Alone1_0_2_4 (572/2030).
Encoding transition Alone1_4_1_4 (573/2030).
Encoding transition Alone1_5_1_4 (574/2030).
Encoding transition Alone1_2_1_4 (575/2030).
Encoding transition Alone1_3_1_4 (576/2030).
Encoding transition Alone1_6_0_4 (577/2030).
Encoding transition Alone1_0_1_4 (578/2030).
Encoding transition Alone1_4_0_4 (579/2030).
Encoding transition Alone1_5_0_4 (580/2030).
Encoding transition Alone1_2_0_4 (581/2030).
Encoding transition Alone1_3_0_4 (582/2030).
Encoding transition Alone1_5_6_3 (583/2030).
Encoding transition Alone1_1_0_4 (584/2030).
Encoding transition Alone1_3_6_3 (585/2030).
Encoding transition Alone1_4_6_3 (586/2030).
Encoding transition NotAlone_3_4_3 (587/2030).
Encoding transition NotAlone_5_4_3 (588/2030).
Encoding transition NotAlone_6_4_3 (589/2030).
Encoding transition NotAlone_0_5_3 (590/2030).
Encoding transition NotAlone_1_5_3 (591/2030).
Encoding transition NotAlone_2_5_3 (592/2030).
Encoding transition NotAlone_3_5_3 (593/2030).
Encoding transition NotAlone_4_5_3 (594/2030).
Encoding transition NotAlone_6_5_3 (595/2030).
Encoding transition NotAlone_0_6_3 (596/2030).
Encoding transition NotAlone_1_6_3 (597/2030).
Encoding transition NotAlone_2_6_3 (598/2030).
Encoding transition NotAlone_3_6_3 (599/2030).
Encoding transition NotAlone_4_6_3 (600/2030).
Encoding transition NotAlone_5_6_3 (601/2030).
Encoding transition NotAlone_1_0_4 (602/2030).
Encoding transition NotAlone_0_2_3 (603/2030).
Encoding transition NotAlone_6_1_3 (604/2030).
Encoding transition NotAlone_3_2_3 (605/2030).
Encoding transition NotAlone_1_2_3 (606/2030).
Encoding transition NotAlone_5_2_3 (607/2030).
Encoding transition NotAlone_4_2_3 (608/2030).
Encoding transition NotAlone_0_3_3 (609/2030).
Encoding transition NotAlone_6_2_3 (610/2030).
Encoding transition NotAlone_2_3_3 (611/2030).
Encoding transition NotAlone_1_3_3 (612/2030).
Encoding transition NotAlone_5_3_3 (613/2030).
Encoding transition NotAlone_4_3_3 (614/2030).
Encoding transition NotAlone_0_4_3 (615/2030).
Encoding transition NotAlone_6_3_3 (616/2030).
Encoding transition NotAlone_2_4_3 (617/2030).
Encoding transition NotAlone_1_4_3 (618/2030).
Encoding transition NotAlone_3_6_2 (619/2030).
Encoding transition NotAlone_4_6_2 (620/2030).
Encoding transition NotAlone_1_6_2 (621/2030).
Encoding transition NotAlone_2_6_2 (622/2030).
Encoding transition NotAlone_2_0_3 (623/2030).
Encoding transition NotAlone_3_0_3 (624/2030).
Encoding transition NotAlone_5_6_2 (625/2030).
Encoding transition NotAlone_1_0_3 (626/2030).
Encoding transition NotAlone_6_0_3 (627/2030).
Encoding transition NotAlone_0_1_3 (628/2030).
Encoding transition NotAlone_4_0_3 (629/2030).
Encoding transition NotAlone_5_0_3 (630/2030).
Encoding transition NotAlone_4_1_3 (631/2030).
Encoding transition NotAlone_5_1_3 (632/2030).
Encoding transition NotAlone_2_1_3 (633/2030).
Encoding transition NotAlone_3_1_3 (634/2030).
Encoding transition NotAlone_0_4_2 (635/2030).
Encoding transition NotAlone_6_3_2 (636/2030).
Encoding transition NotAlone_5_3_2 (637/2030).
Encoding transition NotAlone_4_3_2 (638/2030).
Encoding transition NotAlone_5_4_2 (639/2030).
Encoding transition NotAlone_3_4_2 (640/2030).
Encoding transition NotAlone_2_4_2 (641/2030).
Encoding transition NotAlone_1_4_2 (642/2030).
Encoding transition NotAlone_2_5_2 (643/2030).
Encoding transition NotAlone_1_5_2 (644/2030).
Encoding transition NotAlone_0_5_2 (645/2030).
Encoding transition NotAlone_6_4_2 (646/2030).
Encoding transition NotAlone_0_6_2 (647/2030).
Encoding transition NotAlone_6_5_2 (648/2030).
Encoding transition NotAlone_4_5_2 (649/2030).
Encoding transition NotAlone_3_5_2 (650/2030).
Encoding transition NotAlone_4_1_2 (651/2030).
Encoding transition NotAlone_5_1_2 (652/2030).
Encoding transition NotAlone_6_1_2 (653/2030).
Encoding transition NotAlone_0_2_2 (654/2030).
Encoding transition NotAlone_6_0_2 (655/2030).
Encoding transition NotAlone_0_1_2 (656/2030).
Encoding transition NotAlone_2_1_2 (657/2030).
Encoding transition NotAlone_3_1_2 (658/2030).
Encoding transition NotAlone_6_2_2 (659/2030).
Encoding transition NotAlone_0_3_2 (660/2030).
Encoding transition NotAlone_1_3_2 (661/2030).
Encoding transition NotAlone_2_3_2 (662/2030).
Encoding transition NotAlone_1_2_2 (663/2030).
Encoding transition NotAlone_3_2_2 (664/2030).
Encoding transition NotAlone_4_2_2 (665/2030).
Encoding transition NotAlone_5_2_2 (666/2030).
Encoding transition NotAlone_0_6_1 (667/2030).
Encoding transition NotAlone_6_5_1 (668/2030).
Encoding transition NotAlone_2_6_1 (669/2030).
Encoding transition NotAlone_1_6_1 (670/2030).
Encoding transition NotAlone_2_5_1 (671/2030).
Encoding transition NotAlone_1_5_1 (672/2030).
Encoding transition NotAlone_4_5_1 (673/2030).
Encoding transition NotAlone_3_5_1 (674/2030).
Encoding transition NotAlone_3_0_2 (675/2030).
Encoding transition NotAlone_2_0_2 (676/2030).
Encoding transition NotAlone_5_0_2 (677/2030).
Encoding transition NotAlone_4_0_2 (678/2030).
Encoding transition NotAlone_4_6_1 (679/2030).
Encoding transition NotAlone_3_6_1 (680/2030).
Encoding transition NotAlone_1_0_2 (681/2030).
Encoding transition NotAlone_5_6_1 (682/2030).
Encoding transition NotAlone_4_3_1 (683/2030).
Encoding transition NotAlone_5_3_1 (684/2030).
Encoding transition NotAlone_1_3_1 (685/2030).
Encoding transition NotAlone_2_3_1 (686/2030).
Encoding transition NotAlone_6_2_1 (687/2030).
Encoding transition NotAlone_0_3_1 (688/2030).
Encoding transition NotAlone_4_2_1 (689/2030).
Encoding transition NotAlone_5_2_1 (690/2030).
Encoding transition NotAlone_6_4_1 (691/2030).
Encoding transition NotAlone_0_5_1 (692/2030).
Encoding transition NotAlone_3_4_1 (693/2030).
Encoding transition NotAlone_5_4_1 (694/2030).
Encoding transition NotAlone_1_4_1 (695/2030).
Encoding transition NotAlone_2_4_1 (696/2030).
Encoding transition NotAlone_6_3_1 (697/2030).
Encoding transition NotAlone_0_4_1 (698/2030).
Encoding transition NotAlone_0_1_1 (699/2030).
Encoding transition NotAlone_6_0_1 (700/2030).
Encoding transition NotAlone_5_0_1 (701/2030).
Encoding transition NotAlone_4_0_1 (702/2030).
Encoding transition NotAlone_3_0_1 (703/2030).
Encoding transition NotAlone_2_0_1 (704/2030).
Encoding transition NotAlone_1_0_1 (705/2030).
Encoding transition NotAlone_5_6_0 (706/2030).
Encoding transition NotAlone_3_2_1 (707/2030).
Encoding transition NotAlone_1_2_1 (708/2030).
Encoding transition NotAlone_0_2_1 (709/2030).
Encoding transition NotAlone_6_1_1 (710/2030).
Encoding transition NotAlone_5_1_1 (711/2030).
Encoding transition NotAlone_4_1_1 (712/2030).
Encoding transition NotAlone_3_1_1 (713/2030).
Encoding transition NotAlone_2_1_1 (714/2030).
Encoding transition ContinueLoop_6_2_1 (715/2030).
Encoding transition ContinueLoop_0_3_1 (716/2030).
Encoding transition ContinueLoop_1_3_1 (717/2030).
Encoding transition ContinueLoop_2_3_1 (718/2030).
Encoding transition ContinueLoop_3_3_1 (719/2030).
Encoding transition ContinueLoop_4_3_1 (720/2030).
Encoding transition ContinueLoop_5_3_1 (721/2030).
Encoding transition ContinueLoop_6_3_1 (722/2030).
Encoding transition ContinueLoop_5_1_1 (723/2030).
Encoding transition ContinueLoop_6_1_1 (724/2030).
Encoding transition ContinueLoop_0_2_1 (725/2030).
Encoding transition ContinueLoop_1_2_1 (726/2030).
Encoding transition ContinueLoop_2_2_1 (727/2030).
Encoding transition ContinueLoop_3_2_1 (728/2030).
Encoding transition ContinueLoop_4_2_1 (729/2030).
Encoding transition ContinueLoop_5_2_1 (730/2030).
Encoding transition ContinueLoop_5_0_1 (731/2030).
Encoding transition ContinueLoop_4_0_1 (732/2030).
Encoding transition ContinueLoop_0_1_1 (733/2030).
Encoding transition ContinueLoop_6_0_1 (734/2030).
Encoding transition ContinueLoop_2_1_1 (735/2030).
Encoding transition ContinueLoop_1_1_1 (736/2030).
Encoding transition ContinueLoop_4_1_1 (737/2030).
Encoding transition ContinueLoop_3_1_1 (738/2030).
Encoding transition ContinueLoop_4_6_0 (739/2030).
Encoding transition ContinueLoop_3_6_0 (740/2030).
Encoding transition ContinueLoop_6_6_0 (741/2030).
Encoding transition ContinueLoop_5_6_0 (742/2030).
Encoding transition ContinueLoop_1_0_1 (743/2030).
Encoding transition ContinueLoop_0_0_1 (744/2030).
Encoding transition ContinueLoop_3_0_1 (745/2030).
Encoding transition ContinueLoop_2_0_1 (746/2030).
Encoding transition ContinueLoop_5_0_2 (747/2030).
Encoding transition ContinueLoop_6_0_2 (748/2030).
Encoding transition ContinueLoop_3_0_2 (749/2030).
Encoding transition ContinueLoop_4_0_2 (750/2030).
Encoding transition ContinueLoop_2_1_2 (751/2030).
Encoding transition ContinueLoop_3_1_2 (752/2030).
Encoding transition ContinueLoop_0_1_2 (753/2030).
Encoding transition ContinueLoop_1_1_2 (754/2030).
Encoding transition ContinueLoop_4_6_1 (755/2030).
Encoding transition ContinueLoop_5_6_1 (756/2030).
Encoding transition ContinueLoop_2_6_1 (757/2030).
Encoding transition ContinueLoop_3_6_1 (758/2030).
Encoding transition ContinueLoop_1_0_2 (759/2030).
Encoding transition ContinueLoop_2_0_2 (760/2030).
Encoding transition ContinueLoop_6_6_1 (761/2030).
Encoding transition ContinueLoop_0_0_2 (762/2030).
Encoding transition ContinueLoop_4_5_1 (763/2030).
Encoding transition ContinueLoop_3_5_1 (764/2030).
Encoding transition ContinueLoop_2_5_1 (765/2030).
Encoding transition ContinueLoop_1_5_1 (766/2030).
Encoding transition ContinueLoop_1_6_1 (767/2030).
Encoding transition ContinueLoop_0_6_1 (768/2030).
Encoding transition ContinueLoop_6_5_1 (769/2030).
Encoding transition ContinueLoop_5_5_1 (770/2030).
Encoding transition ContinueLoop_3_4_1 (771/2030).
Encoding transition ContinueLoop_2_4_1 (772/2030).
Encoding transition ContinueLoop_1_4_1 (773/2030).
Encoding transition ContinueLoop_0_4_1 (774/2030).
Encoding transition ContinueLoop_0_5_1 (775/2030).
Encoding transition ContinueLoop_6_4_1 (776/2030).
Encoding transition ContinueLoop_5_4_1 (777/2030).
Encoding transition ContinueLoop_4_4_1 (778/2030).
Encoding transition ContinueLoop_4_5_2 (779/2030).
Encoding transition ContinueLoop_5_5_2 (780/2030).
Encoding transition ContinueLoop_6_5_2 (781/2030).
Encoding transition ContinueLoop_0_6_2 (782/2030).
Encoding transition ContinueLoop_0_5_2 (783/2030).
Encoding transition ContinueLoop_1_5_2 (784/2030).
Encoding transition ContinueLoop_2_5_2 (785/2030).
Encoding transition ContinueLoop_3_5_2 (786/2030).
Encoding transition ContinueLoop_3_4_2 (787/2030).
Encoding transition ContinueLoop_4_4_2 (788/2030).
Encoding transition ContinueLoop_5_4_2 (789/2030).
Encoding transition ContinueLoop_6_4_2 (790/2030).
Encoding transition ContinueLoop_6_3_2 (791/2030).
Encoding transition ContinueLoop_0_4_2 (792/2030).
Encoding transition ContinueLoop_1_4_2 (793/2030).
Encoding transition ContinueLoop_2_4_2 (794/2030).
Encoding transition ContinueLoop_3_3_2 (795/2030).
Encoding transition ContinueLoop_2_3_2 (796/2030).
Encoding transition ContinueLoop_5_3_2 (797/2030).
Encoding transition ContinueLoop_4_3_2 (798/2030).
Encoding transition ContinueLoop_6_2_2 (799/2030).
Encoding transition ContinueLoop_5_2_2 (800/2030).
Encoding transition ContinueLoop_1_3_2 (801/2030).
Encoding transition ContinueLoop_0_3_2 (802/2030).
Encoding transition ContinueLoop_2_2_2 (803/2030).
Encoding transition ContinueLoop_1_2_2 (804/2030).
Encoding transition ContinueLoop_4_2_2 (805/2030).
Encoding transition ContinueLoop_3_2_2 (806/2030).
Encoding transition ContinueLoop_5_1_2 (807/2030).
Encoding transition ContinueLoop_4_1_2 (808/2030).
Encoding transition ContinueLoop_0_2_2 (809/2030).
Encoding transition ContinueLoop_6_1_2 (810/2030).
Encoding transition ContinueLoop_3_3_3 (811/2030).
Encoding transition ContinueLoop_4_3_3 (812/2030).
Encoding transition ContinueLoop_1_3_3 (813/2030).
Encoding transition ContinueLoop_2_3_3 (814/2030).
Encoding transition ContinueLoop_6_2_3 (815/2030).
Encoding transition ContinueLoop_0_3_3 (816/2030).
Encoding transition ContinueLoop_4_2_3 (817/2030).
Encoding transition ContinueLoop_5_2_3 (818/2030).
Encoding transition ContinueLoop_2_2_3 (819/2030).
Encoding transition ContinueLoop_3_2_3 (820/2030).
Encoding transition ContinueLoop_0_2_3 (821/2030).
Encoding transition ContinueLoop_1_2_3 (822/2030).
Encoding transition ContinueLoop_5_1_3 (823/2030).
Encoding transition ContinueLoop_6_1_3 (824/2030).
Encoding transition ContinueLoop_3_1_3 (825/2030).
Encoding transition ContinueLoop_4_1_3 (826/2030).
Encoding transition ContinueLoop_2_1_3 (827/2030).
Encoding transition ContinueLoop_1_1_3 (828/2030).
Encoding transition ContinueLoop_0_1_3 (829/2030).
Encoding transition ContinueLoop_6_0_3 (830/2030).
Encoding transition ContinueLoop_5_0_3 (831/2030).
Encoding transition ContinueLoop_4_0_3 (832/2030).
Encoding transition ContinueLoop_3_0_3 (833/2030).
Encoding transition ContinueLoop_2_0_3 (834/2030).
Encoding transition ContinueLoop_1_0_3 (835/2030).
Encoding transition ContinueLoop_0_0_3 (836/2030).
Encoding transition ContinueLoop_6_6_2 (837/2030).
Encoding transition ContinueLoop_5_6_2 (838/2030).
Encoding transition ContinueLoop_4_6_2 (839/2030).
Encoding transition ContinueLoop_3_6_2 (840/2030).
Encoding transition ContinueLoop_2_6_2 (841/2030).
Encoding transition ContinueLoop_1_6_2 (842/2030).
Encoding transition NotAlone_0_3_4 (843/2030).
Encoding transition NotAlone_6_2_4 (844/2030).
Encoding transition NotAlone_2_3_4 (845/2030).
Encoding transition NotAlone_1_3_4 (846/2030).
Encoding transition NotAlone_5_3_4 (847/2030).
Encoding transition NotAlone_4_3_4 (848/2030).
Encoding transition NotAlone_0_4_4 (849/2030).
Encoding transition NotAlone_6_3_4 (850/2030).
Encoding transition NotAlone_2_4_4 (851/2030).
Encoding transition NotAlone_1_4_4 (852/2030).
Encoding transition NotAlone_5_4_4 (853/2030).
Encoding transition NotAlone_3_4_4 (854/2030).
Encoding transition NotAlone_0_5_4 (855/2030).
Encoding transition NotAlone_6_4_4 (856/2030).
Encoding transition NotAlone_2_5_4 (857/2030).
Encoding transition NotAlone_1_5_4 (858/2030).
Encoding transition NotAlone_2_0_4 (859/2030).
Encoding transition NotAlone_3_0_4 (860/2030).
Encoding transition NotAlone_4_0_4 (861/2030).
Encoding transition NotAlone_5_0_4 (862/2030).
Encoding transition NotAlone_6_0_4 (863/2030).
Encoding transition NotAlone_0_1_4 (864/2030).
Encoding transition NotAlone_2_1_4 (865/2030).
Encoding transition NotAlone_3_1_4 (866/2030).
Encoding transition NotAlone_4_1_4 (867/2030).
Encoding transition NotAlone_5_1_4 (868/2030).
Encoding transition NotAlone_6_1_4 (869/2030).
Encoding transition NotAlone_0_2_4 (870/2030).
Encoding transition NotAlone_1_2_4 (871/2030).
Encoding transition NotAlone_3_2_4 (872/2030).
Encoding transition NotAlone_4_2_4 (873/2030).
Encoding transition NotAlone_5_2_4 (874/2030).
Encoding transition NotAlone_5_1_5 (875/2030).
Encoding transition NotAlone_4_1_5 (876/2030).
Encoding transition NotAlone_3_1_5 (877/2030).
Encoding transition NotAlone_2_1_5 (878/2030).
Encoding transition NotAlone_3_2_5 (879/2030).
Encoding transition NotAlone_1_2_5 (880/2030).
Encoding transition NotAlone_0_2_5 (881/2030).
Encoding transition NotAlone_6_1_5 (882/2030).
Encoding transition NotAlone_0_3_5 (883/2030).
Encoding transition NotAlone_6_2_5 (884/2030).
Encoding transition NotAlone_5_2_5 (885/2030).
Encoding transition NotAlone_4_2_5 (886/2030).
Encoding transition NotAlone_5_3_5 (887/2030).
Encoding transition NotAlone_4_3_5 (888/2030).
Encoding transition NotAlone_2_3_5 (889/2030).
Encoding transition NotAlone_1_3_5 (890/2030).
Encoding transition NotAlone_6_5_4 (891/2030).
Encoding transition NotAlone_0_6_4 (892/2030).
Encoding transition NotAlone_3_5_4 (893/2030).
Encoding transition NotAlone_4_5_4 (894/2030).
Encoding transition NotAlone_3_6_4 (895/2030).
Encoding transition NotAlone_4_6_4 (896/2030).
Encoding transition NotAlone_1_6_4 (897/2030).
Encoding transition NotAlone_2_6_4 (898/2030).
Encoding transition NotAlone_2_0_5 (899/2030).
Encoding transition NotAlone_3_0_5 (900/2030).
Encoding transition NotAlone_5_6_4 (901/2030).
Encoding transition NotAlone_1_0_5 (902/2030).
Encoding transition NotAlone_6_0_5 (903/2030).
Encoding transition NotAlone_0_1_5 (904/2030).
Encoding transition NotAlone_4_0_5 (905/2030).
Encoding transition NotAlone_5_0_5 (906/2030).
Encoding transition ContinueLoop_2_0_0 (907/2030).
Encoding transition ContinueLoop_1_0_0 (908/2030).
Encoding transition ContinueLoop_4_0_0 (909/2030).
Encoding transition ContinueLoop_3_0_0 (910/2030).
Encoding transition NotAlone_4_6_5 (911/2030).
Encoding transition NotAlone_3_6_5 (912/2030).
Encoding transition ContinueLoop_0_0_0 (913/2030).
Encoding transition NotAlone_5_6_5 (914/2030).
Encoding transition ContinueLoop_3_1_0 (915/2030).
Encoding transition ContinueLoop_2_1_0 (916/2030).
Encoding transition ContinueLoop_5_1_0 (917/2030).
Encoding transition ContinueLoop_4_1_0 (918/2030).
Encoding transition ContinueLoop_6_0_0 (919/2030).
Encoding transition ContinueLoop_5_0_0 (920/2030).
Encoding transition ContinueLoop_1_1_0 (921/2030).
Encoding transition ContinueLoop_0_1_0 (922/2030).
Encoding transition NotAlone_3_4_5 (923/2030).
Encoding transition NotAlone_5_4_5 (924/2030).
Encoding transition NotAlone_6_4_5 (925/2030).
Encoding transition NotAlone_0_5_5 (926/2030).
Encoding transition NotAlone_6_3_5 (927/2030).
Encoding transition NotAlone_0_4_5 (928/2030).
Encoding transition NotAlone_1_4_5 (929/2030).
Encoding transition NotAlone_2_4_5 (930/2030).
Encoding transition NotAlone_6_5_5 (931/2030).
Encoding transition NotAlone_0_6_5 (932/2030).
Encoding transition NotAlone_1_6_5 (933/2030).
Encoding transition NotAlone_2_6_5 (934/2030).
Encoding transition NotAlone_1_5_5 (935/2030).
Encoding transition NotAlone_2_5_5 (936/2030).
Encoding transition NotAlone_3_5_5 (937/2030).
Encoding transition NotAlone_4_5_5 (938/2030).
Encoding transition ContinueLoop_1_5_0 (939/2030).
Encoding transition ContinueLoop_0_5_0 (940/2030).
Encoding transition ContinueLoop_6_4_0 (941/2030).
Encoding transition ContinueLoop_5_4_0 (942/2030).
Encoding transition ContinueLoop_4_4_0 (943/2030).
Encoding transition ContinueLoop_3_4_0 (944/2030).
Encoding transition ContinueLoop_2_4_0 (945/2030).
Encoding transition ContinueLoop_1_4_0 (946/2030).
Encoding transition ContinueLoop_2_6_0 (947/2030).
Encoding transition ContinueLoop_1_6_0 (948/2030).
Encoding transition ContinueLoop_0_6_0 (949/2030).
Encoding transition ContinueLoop_6_5_0 (950/2030).
Encoding transition ContinueLoop_5_5_0 (951/2030).
Encoding transition ContinueLoop_4_5_0 (952/2030).
Encoding transition ContinueLoop_3_5_0 (953/2030).
Encoding transition ContinueLoop_2_5_0 (954/2030).
Encoding transition ContinueLoop_5_2_0 (955/2030).
Encoding transition ContinueLoop_6_2_0 (956/2030).
Encoding transition ContinueLoop_3_2_0 (957/2030).
Encoding transition ContinueLoop_4_2_0 (958/2030).
Encoding transition ContinueLoop_1_2_0 (959/2030).
Encoding transition ContinueLoop_2_2_0 (960/2030).
Encoding transition ContinueLoop_6_1_0 (961/2030).
Encoding transition ContinueLoop_0_2_0 (962/2030).
Encoding transition ContinueLoop_6_3_0 (963/2030).
Encoding transition ContinueLoop_0_4_0 (964/2030).
Encoding transition ContinueLoop_4_3_0 (965/2030).
Encoding transition ContinueLoop_5_3_0 (966/2030).
Encoding transition ContinueLoop_2_3_0 (967/2030).
Encoding transition ContinueLoop_3_3_0 (968/2030).
Encoding transition ContinueLoop_0_3_0 (969/2030).
Encoding transition ContinueLoop_1_3_0 (970/2030).
Encoding transition TurnDiff_0_3_0 (971/2030).
Encoding transition TurnDiff_6_2_0 (972/2030).
Encoding transition TurnDiff_5_2_0 (973/2030).
Encoding transition TurnDiff_4_2_0 (974/2030).
Encoding transition TurnDiff_5_3_0 (975/2030).
Encoding transition TurnDiff_4_3_0 (976/2030).
Encoding transition TurnDiff_2_3_0 (977/2030).
Encoding transition TurnDiff_1_3_0 (978/2030).
Encoding transition TurnDiff_5_1_0 (979/2030).
Encoding transition TurnDiff_4_1_0 (980/2030).
Encoding transition TurnDiff_3_1_0 (981/2030).
Encoding transition TurnDiff_2_1_0 (982/2030).
Encoding transition TurnDiff_3_2_0 (983/2030).
Encoding transition TurnDiff_1_2_0 (984/2030).
Encoding transition TurnDiff_0_2_0 (985/2030).
Encoding transition TurnDiff_6_1_0 (986/2030).
Encoding transition TurnDiff_3_5_0 (987/2030).
Encoding transition TurnDiff_4_5_0 (988/2030).
Encoding transition TurnDiff_1_5_0 (989/2030).
Encoding transition TurnDiff_2_5_0 (990/2030).
Encoding transition TurnDiff_1_6_0 (991/2030).
Encoding transition TurnDiff_2_6_0 (992/2030).
Encoding transition TurnDiff_6_5_0 (993/2030).
Encoding transition TurnDiff_0_6_0 (994/2030).
Encoding transition TurnDiff_1_4_0 (995/2030).
Encoding transition TurnDiff_2_4_0 (996/2030).
Encoding transition TurnDiff_6_3_0 (997/2030).
Encoding transition TurnDiff_0_4_0 (998/2030).
Encoding transition TurnDiff_6_4_0 (999/2030).
Encoding transition TurnDiff_0_5_0 (1000/2030).
Encoding transition TurnDiff_3_4_0 (1001/2030).
Encoding transition TurnDiff_5_4_0 (1002/2030).
Encoding transition TurnDiff_0_1_1 (1003/2030).
Encoding transition TurnDiff_6_0_1 (1004/2030).
Encoding transition TurnDiff_3_1_1 (1005/2030).
Encoding transition TurnDiff_2_1_1 (1006/2030).
Encoding transition TurnDiff_5_1_1 (1007/2030).
Encoding transition TurnDiff_4_1_1 (1008/2030).
Encoding transition TurnDiff_0_2_1 (1009/2030).
Encoding transition TurnDiff_6_1_1 (1010/2030).
Encoding transition TurnDiff_4_6_0 (1011/2030).
Encoding transition TurnDiff_3_6_0 (1012/2030).
Encoding transition TurnDiff_1_0_1 (1013/2030).
Encoding transition TurnDiff_5_6_0 (1014/2030).
Encoding transition TurnDiff_3_0_1 (1015/2030).
Encoding transition TurnDiff_2_0_1 (1016/2030).
Encoding transition TurnDiff_5_0_1 (1017/2030).
Encoding transition TurnDiff_4_0_1 (1018/2030).
Encoding transition TurnDiff_4_3_1 (1019/2030).
Encoding transition TurnDiff_5_3_1 (1020/2030).
Encoding transition TurnDiff_6_3_1 (1021/2030).
Encoding transition TurnDiff_0_4_1 (1022/2030).
Encoding transition TurnDiff_1_4_1 (1023/2030).
Encoding transition TurnDiff_2_4_1 (1024/2030).
Encoding transition TurnDiff_3_4_1 (1025/2030).
Encoding transition TurnDiff_5_4_1 (1026/2030).
Encoding transition TurnDiff_1_2_1 (1027/2030).
Encoding transition TurnDiff_3_2_1 (1028/2030).
Encoding transition TurnDiff_4_2_1 (1029/2030).
Encoding transition TurnDiff_5_2_1 (1030/2030).
Encoding transition TurnDiff_6_2_1 (1031/2030).
Encoding transition TurnDiff_0_3_1 (1032/2030).
Encoding transition TurnDiff_1_3_1 (1033/2030).
Encoding transition TurnDiff_2_3_1 (1034/2030).
Encoding transition TurnDiff_3_0_2 (1035/2030).
Encoding transition TurnDiff_2_0_2 (1036/2030).
Encoding transition TurnDiff_1_0_2 (1037/2030).
Encoding transition TurnDiff_5_6_1 (1038/2030).
Encoding transition TurnDiff_4_6_1 (1039/2030).
Encoding transition TurnDiff_3_6_1 (1040/2030).
Encoding transition TurnDiff_2_6_1 (1041/2030).
Encoding transition TurnDiff_1_6_1 (1042/2030).
Encoding transition TurnDiff_0_6_1 (1043/2030).
Encoding transition TurnDiff_6_5_1 (1044/2030).
Encoding transition TurnDiff_4_5_1 (1045/2030).
Encoding transition TurnDiff_3_5_1 (1046/2030).
Encoding transition TurnDiff_2_5_1 (1047/2030).
Encoding transition TurnDiff_1_5_1 (1048/2030).
Encoding transition TurnDiff_0_5_1 (1049/2030).
Encoding transition TurnDiff_6_4_1 (1050/2030).
Encoding transition TurnDiff_6_2_2 (1051/2030).
Encoding transition TurnDiff_0_3_2 (1052/2030).
Encoding transition TurnDiff_4_2_2 (1053/2030).
Encoding transition TurnDiff_5_2_2 (1054/2030).
Encoding transition TurnDiff_1_2_2 (1055/2030).
Encoding transition TurnDiff_3_2_2 (1056/2030).
Encoding transition TurnDiff_6_1_2 (1057/2030).
Encoding transition TurnDiff_0_2_2 (1058/2030).
Encoding transition TurnDiff_4_1_2 (1059/2030).
Encoding transition TurnDiff_5_1_2 (1060/2030).
Encoding transition TurnDiff_2_1_2 (1061/2030).
Encoding transition TurnDiff_3_1_2 (1062/2030).
Encoding transition TurnDiff_6_0_2 (1063/2030).
Encoding transition TurnDiff_0_1_2 (1064/2030).
Encoding transition TurnDiff_4_0_2 (1065/2030).
Encoding transition TurnDiff_5_0_2 (1066/2030).
Encoding transition TurnDiff_2_5_2 (1067/2030).
Encoding transition TurnDiff_1_5_2 (1068/2030).
Encoding transition TurnDiff_4_5_2 (1069/2030).
Encoding transition TurnDiff_3_5_2 (1070/2030).
Encoding transition TurnDiff_5_4_2 (1071/2030).
Encoding transition TurnDiff_3_4_2 (1072/2030).
Encoding transition TurnDiff_0_5_2 (1073/2030).
Encoding transition TurnDiff_6_4_2 (1074/2030).
Encoding transition TurnDiff_0_4_2 (1075/2030).
Encoding transition TurnDiff_6_3_2 (1076/2030).
Encoding transition TurnDiff_2_4_2 (1077/2030).
Encoding transition TurnDiff_1_4_2 (1078/2030).
Encoding transition TurnDiff_2_3_2 (1079/2030).
Encoding transition TurnDiff_1_3_2 (1080/2030).
Encoding transition TurnDiff_5_3_2 (1081/2030).
Encoding transition TurnDiff_4_3_2 (1082/2030).
Encoding transition TurnDiff_6_0_3 (1083/2030).
Encoding transition TurnDiff_0_1_3 (1084/2030).
Encoding transition TurnDiff_2_1_3 (1085/2030).
Encoding transition TurnDiff_3_1_3 (1086/2030).
Encoding transition TurnDiff_2_0_3 (1087/2030).
Encoding transition TurnDiff_3_0_3 (1088/2030).
Encoding transition TurnDiff_4_0_3 (1089/2030).
Encoding transition TurnDiff_5_0_3 (1090/2030).
Encoding transition TurnDiff_3_6_2 (1091/2030).
Encoding transition TurnDiff_4_6_2 (1092/2030).
Encoding transition TurnDiff_5_6_2 (1093/2030).
Encoding transition TurnDiff_1_0_3 (1094/2030).
BK_STOP 1400399384207
--------------------
content from stderr:
terminate called after throwing an instance of 'MEDDLY::error'
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 167: 1699 Aborted ~/BenchKit/bin/bin/RGMEDD model ${PLACE_ORDER} ${MEDDLY_CACHE} ${BOUND} -C -f ${NEW_FRM}
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="Peterson-PT-6"
export BK_EXAMINATION="CTLCardinality"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/home/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/Peterson-PT-6.tgz
mv Peterson-PT-6 execution
# this is for BenchKit: explicit launching of the test
cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1667"
echo " Executing tool greatspn"
echo " Input is Peterson-PT-6, examination is CTLCardinality"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r03kn-qhx2-140036872301126"
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 ;