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 SurpriseLamportFastMutEx-PT-8, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r08ks-qhx2-140068993901219
=====================================================================

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

BK_START 1400734955233
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurpriseLamportFastMutEx (PT), instance 8
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/CTLFireability.xml INTO /home/mcc/execution/CTLFireability.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 24 -C -f /home/mcc/execution/CTLFireability.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 T-setbi_2_1 (0/666).
Encoding transition T-setbi_2_2 (1/666).
Encoding transition T-setbi_2_3 (2/666).
Encoding transition T-setbi_2_4 (3/666).
Encoding transition T-setbi_2_5 (4/666).
Encoding transition T-setbi_2_6 (5/666).
Encoding transition T-setbi_2_7 (6/666).
Encoding transition T-setbi_2_8 (7/666).
Encoding transition T-setbi_2_9 (8/666).
Encoding transition T-setbi_2_10 (9/666).
Encoding transition T-setbi_2_11 (10/666).
Encoding transition T-setbi_2_12 (11/666).
Encoding transition T-setbi_2_13 (12/666).
Encoding transition T-setbi_2_14 (13/666).
Encoding transition T-setbi_2_15 (14/666).
Encoding transition T-setbi_2_16 (15/666).
Encoding transition T-setbi_2_17 (16/666).
Encoding transition T-setbi_2_18 (17/666).
Encoding transition T-setx_3_1 (18/666).
Encoding transition T-setx_3_2 (19/666).
Encoding transition T-setx_3_3 (20/666).
Encoding transition T-setx_3_4 (21/666).
Encoding transition T-setx_3_5 (22/666).
Encoding transition T-setx_3_6 (23/666).
Encoding transition T-setx_3_7 (24/666).
Encoding transition T-setx_3_8 (25/666).
Encoding transition T-setx_3_9 (26/666).
Encoding transition T-setx_3_10 (27/666).
Encoding transition T-setx_3_11 (28/666).
Encoding transition T-setx_3_12 (29/666).
Encoding transition T-setx_3_13 (30/666).
Encoding transition T-setx_3_14 (31/666).
Encoding transition T-setx_3_15 (32/666).
Encoding transition T-setx_3_16 (33/666).
Encoding transition T-setx_3_17 (34/666).
Encoding transition T-setx_3_18 (35/666).
Encoding transition T-setx_3_19 (36/666).
Encoding transition T-setx_3_20 (37/666).
Encoding transition T-setx_3_21 (38/666).
Encoding transition T-setx_3_22 (39/666).
Encoding transition T-setx_3_23 (40/666).
Encoding transition T-setx_3_24 (41/666).
Encoding transition T-setx_3_25 (42/666).
Encoding transition T-setx_3_26 (43/666).
Encoding transition T-setx_3_27 (44/666).
Encoding transition T-setx_3_28 (45/666).
Encoding transition T-setx_3_29 (46/666).
Encoding transition T-setx_3_30 (47/666).
Encoding transition T-setx_3_31 (48/666).
Encoding transition T-setx_3_32 (49/666).
Encoding transition T-setx_3_33 (50/666).
Encoding transition T-setx_3_34 (51/666).
Encoding transition T-setx_3_35 (52/666).
Encoding transition T-setx_3_36 (53/666).
Encoding transition T-setx_3_37 (54/666).
Encoding transition T-setx_3_38 (55/666).
Encoding transition T-setx_3_39 (56/666).
Encoding transition T-setx_3_40 (57/666).
Encoding transition T-setx_3_41 (58/666).
Encoding transition T-setx_3_42 (59/666).
Encoding transition T-setx_3_43 (60/666).
Encoding transition T-setx_3_44 (61/666).
Encoding transition T-setx_3_45 (62/666).
Encoding transition T-setx_3_46 (63/666).
Encoding transition T-setx_3_47 (64/666).
Encoding transition T-setx_3_48 (65/666).
Encoding transition T-setx_3_49 (66/666).
Encoding transition T-setx_3_50 (67/666).
Encoding transition T-setx_3_51 (68/666).
Encoding transition T-setx_3_52 (69/666).
Encoding transition T-setx_3_53 (70/666).
Encoding transition T-setx_3_54 (71/666).
Encoding transition T-setx_3_55 (72/666).
Encoding transition T-setx_3_56 (73/666).
Encoding transition T-setx_3_57 (74/666).
Encoding transition T-setx_3_58 (75/666).
Encoding transition T-setx_3_59 (76/666).
Encoding transition T-setx_3_60 (77/666).
Encoding transition T-setx_3_61 (78/666).
Encoding transition T-setx_3_62 (79/666).
Encoding transition T-setx_3_63 (80/666).
Encoding transition T-setx_3_64 (81/666).
Encoding transition T-setx_3_65 (82/666).
Encoding transition T-setx_3_66 (83/666).
Encoding transition T-setx_3_67 (84/666).
Encoding transition T-setx_3_68 (85/666).
Encoding transition T-setx_3_69 (86/666).
Encoding transition T-setx_3_70 (87/666).
Encoding transition T-setx_3_71 (88/666).
Encoding transition T-setx_3_72 (89/666).
Encoding transition T-setx_3_73 (90/666).
Encoding transition T-setx_3_74 (91/666).
Encoding transition T-setx_3_75 (92/666).
Encoding transition T-setx_3_76 (93/666).
Encoding transition T-setx_3_77 (94/666).
Encoding transition T-setx_3_78 (95/666).
Encoding transition T-setx_3_79 (96/666).
Encoding transition T-setx_3_80 (97/666).
Encoding transition T-setx_3_81 (98/666).
Encoding transition T-yne0_4_2 (99/666).
Encoding transition T-yne0_4_3 (100/666).
Encoding transition T-yne0_4_4 (101/666).
Encoding transition T-yne0_4_5 (102/666).
Encoding transition T-yne0_4_6 (103/666).
Encoding transition T-yne0_4_7 (104/666).
Encoding transition T-yne0_4_8 (105/666).
Encoding transition T-yne0_4_9 (106/666).
Encoding transition T-yne0_4_11 (107/666).
Encoding transition T-yne0_4_12 (108/666).
Encoding transition T-yne0_4_13 (109/666).
Encoding transition T-yne0_4_14 (110/666).
Encoding transition T-yne0_4_15 (111/666).
Encoding transition T-yne0_4_16 (112/666).
Encoding transition T-yne0_4_17 (113/666).
Encoding transition T-yne0_4_18 (114/666).
Encoding transition T-yne0_4_20 (115/666).
Encoding transition T-yne0_4_21 (116/666).
Encoding transition T-yne0_4_22 (117/666).
Encoding transition T-yne0_4_23 (118/666).
Encoding transition T-yne0_4_24 (119/666).
Encoding transition T-yne0_4_25 (120/666).
Encoding transition T-yne0_4_26 (121/666).
Encoding transition T-yne0_4_27 (122/666).
Encoding transition T-yne0_4_29 (123/666).
Encoding transition T-yne0_4_30 (124/666).
Encoding transition T-yne0_4_31 (125/666).
Encoding transition T-yne0_4_32 (126/666).
Encoding transition T-yne0_4_33 (127/666).
Encoding transition T-yne0_4_34 (128/666).
Encoding transition T-yne0_4_35 (129/666).
Encoding transition T-yne0_4_36 (130/666).
Encoding transition T-yne0_4_38 (131/666).
Encoding transition T-yne0_4_39 (132/666).
Encoding transition T-yne0_4_40 (133/666).
Encoding transition T-yne0_4_41 (134/666).
Encoding transition T-yne0_4_42 (135/666).
Encoding transition T-yne0_4_43 (136/666).
Encoding transition T-yne0_4_44 (137/666).
Encoding transition T-yne0_4_45 (138/666).
Encoding transition T-yne0_4_47 (139/666).
Encoding transition T-yne0_4_48 (140/666).
Encoding transition T-yne0_4_49 (141/666).
Encoding transition T-yne0_4_50 (142/666).
Encoding transition T-yne0_4_51 (143/666).
Encoding transition T-yne0_4_52 (144/666).
Encoding transition T-yne0_4_53 (145/666).
Encoding transition T-yne0_4_54 (146/666).
Encoding transition T-yne0_4_56 (147/666).
Encoding transition T-yne0_4_57 (148/666).
Encoding transition T-yne0_4_58 (149/666).
Encoding transition T-yne0_4_59 (150/666).
Encoding transition T-yne0_4_60 (151/666).
Encoding transition T-yne0_4_61 (152/666).
Encoding transition T-yne0_4_62 (153/666).
Encoding transition T-yne0_4_63 (154/666).
Encoding transition T-yne0_4_65 (155/666).
Encoding transition T-yne0_4_66 (156/666).
Encoding transition T-yne0_4_67 (157/666).
Encoding transition T-yne0_4_68 (158/666).
Encoding transition T-yne0_4_69 (159/666).
Encoding transition T-yne0_4_70 (160/666).
Encoding transition T-yne0_4_71 (161/666).
Encoding transition T-yne0_4_72 (162/666).
Encoding transition T-yne0_4_74 (163/666).
Encoding transition T-yne0_4_75 (164/666).
Encoding transition T-yne0_4_76 (165/666).
Encoding transition T-yne0_4_77 (166/666).
Encoding transition T-yne0_4_78 (167/666).
Encoding transition T-yne0_4_79 (168/666).
Encoding transition T-yne0_4_80 (169/666).
Encoding transition T-yne0_4_81 (170/666).
Encoding transition T-setbi_5_1 (171/666).
Encoding transition T-setbi_5_2 (172/666).
Encoding transition T-setbi_5_3 (173/666).
Encoding transition T-setbi_5_4 (174/666).
Encoding transition T-setbi_5_5 (175/666).
Encoding transition T-setbi_5_6 (176/666).
Encoding transition T-setbi_5_7 (177/666).
Encoding transition T-setbi_5_8 (178/666).
Encoding transition T-setbi_5_9 (179/666).
Encoding transition T-setbi_5_10 (180/666).
Encoding transition T-setbi_5_11 (181/666).
Encoding transition T-setbi_5_12 (182/666).
Encoding transition T-setbi_5_13 (183/666).
Encoding transition T-setbi_5_14 (184/666).
Encoding transition T-setbi_5_15 (185/666).
Encoding transition T-setbi_5_16 (186/666).
Encoding transition T-setbi_5_17 (187/666).
Encoding transition T-setbi_5_18 (188/666).
Encoding transition T-awaity_1 (189/666).
Encoding transition T-awaity_2 (190/666).
Encoding transition T-awaity_3 (191/666).
Encoding transition T-awaity_4 (192/666).
Encoding transition T-awaity_5 (193/666).
Encoding transition T-awaity_6 (194/666).
Encoding transition T-awaity_7 (195/666).
Encoding transition T-awaity_8 (196/666).
Encoding transition T-awaity_9 (197/666).
Encoding transition T-yeq0_4_1 (198/666).
Encoding transition T-yeq0_4_2 (199/666).
Encoding transition T-yeq0_4_3 (200/666).
Encoding transition T-yeq0_4_4 (201/666).
Encoding transition T-yeq0_4_5 (202/666).
Encoding transition T-yeq0_4_6 (203/666).
Encoding transition T-yeq0_4_7 (204/666).
Encoding transition T-yeq0_4_8 (205/666).
Encoding transition T-yeq0_4_9 (206/666).
Encoding transition T-sety_9_1 (207/666).
Encoding transition T-sety_9_2 (208/666).
Encoding transition T-sety_9_3 (209/666).
Encoding transition T-sety_9_4 (210/666).
Encoding transition T-sety_9_5 (211/666).
Encoding transition T-sety_9_6 (212/666).
Encoding transition T-sety_9_7 (213/666).
Encoding transition T-sety_9_8 (214/666).
Encoding transition T-sety_9_9 (215/666).
Encoding transition T-sety_9_10 (216/666).
Encoding transition T-sety_9_11 (217/666).
Encoding transition T-sety_9_12 (218/666).
Encoding transition T-sety_9_13 (219/666).
Encoding transition T-sety_9_14 (220/666).
Encoding transition T-sety_9_15 (221/666).
Encoding transition T-sety_9_16 (222/666).
Encoding transition T-sety_9_17 (223/666).
Encoding transition T-sety_9_18 (224/666).
Encoding transition T-sety_9_19 (225/666).
Encoding transition T-sety_9_20 (226/666).
Encoding transition T-sety_9_21 (227/666).
Encoding transition T-sety_9_22 (228/666).
Encoding transition T-sety_9_23 (229/666).
Encoding transition T-sety_9_24 (230/666).
Encoding transition T-sety_9_25 (231/666).
Encoding transition T-sety_9_26 (232/666).
Encoding transition T-sety_9_27 (233/666).
Encoding transition T-sety_9_28 (234/666).
Encoding transition T-sety_9_29 (235/666).
Encoding transition T-sety_9_30 (236/666).
Encoding transition T-sety_9_31 (237/666).
Encoding transition T-sety_9_32 (238/666).
Encoding transition T-sety_9_33 (239/666).
Encoding transition T-sety_9_34 (240/666).
Encoding transition T-sety_9_35 (241/666).
Encoding transition T-sety_9_36 (242/666).
Encoding transition T-sety_9_37 (243/666).
Encoding transition T-sety_9_38 (244/666).
Encoding transition T-sety_9_39 (245/666).
Encoding transition T-sety_9_40 (246/666).
Encoding transition T-sety_9_41 (247/666).
Encoding transition T-sety_9_42 (248/666).
Encoding transition T-sety_9_43 (249/666).
Encoding transition T-sety_9_44 (250/666).
Encoding transition T-sety_9_45 (251/666).
Encoding transition T-sety_9_46 (252/666).
Encoding transition T-sety_9_47 (253/666).
Encoding transition T-sety_9_48 (254/666).
Encoding transition T-sety_9_49 (255/666).
Encoding transition T-sety_9_50 (256/666).
Encoding transition T-sety_9_51 (257/666).
Encoding transition T-sety_9_52 (258/666).
Encoding transition T-sety_9_53 (259/666).
Encoding transition T-sety_9_54 (260/666).
Encoding transition T-sety_9_55 (261/666).
Encoding transition T-sety_9_56 (262/666).
Encoding transition T-sety_9_57 (263/666).
Encoding transition T-sety_9_58 (264/666).
Encoding transition T-sety_9_59 (265/666).
Encoding transition T-sety_9_60 (266/666).
Encoding transition T-sety_9_61 (267/666).
Encoding transition T-sety_9_62 (268/666).
Encoding transition T-sety_9_63 (269/666).
Encoding transition T-sety_9_64 (270/666).
Encoding transition T-sety_9_65 (271/666).
Encoding transition T-sety_9_66 (272/666).
Encoding transition T-sety_9_67 (273/666).
Encoding transition T-sety_9_68 (274/666).
Encoding transition T-sety_9_69 (275/666).
Encoding transition T-sety_9_70 (276/666).
Encoding transition T-sety_9_71 (277/666).
Encoding transition T-sety_9_72 (278/666).
Encoding transition T-sety_9_73 (279/666).
Encoding transition T-sety_9_74 (280/666).
Encoding transition T-sety_9_75 (281/666).
Encoding transition T-sety_9_76 (282/666).
Encoding transition T-sety_9_77 (283/666).
Encoding transition T-sety_9_78 (284/666).
Encoding transition T-sety_9_79 (285/666).
Encoding transition T-sety_9_80 (286/666).
Encoding transition T-sety_9_81 (287/666).
Encoding transition T-xnei_10_2 (288/666).
Encoding transition T-xnei_10_3 (289/666).
Encoding transition T-xnei_10_4 (290/666).
Encoding transition T-xnei_10_5 (291/666).
Encoding transition T-xnei_10_6 (292/666).
Encoding transition T-xnei_10_7 (293/666).
Encoding transition T-xnei_10_8 (294/666).
Encoding transition T-xnei_10_9 (295/666).
Encoding transition T-xnei_10_10 (296/666).
Encoding transition T-xnei_10_12 (297/666).
Encoding transition T-xnei_10_13 (298/666).
Encoding transition T-xnei_10_14 (299/666).
Encoding transition T-xnei_10_15 (300/666).
Encoding transition T-xnei_10_16 (301/666).
Encoding transition T-xnei_10_17 (302/666).
Encoding transition T-xnei_10_18 (303/666).
Encoding transition T-xnei_10_19 (304/666).
Encoding transition T-xnei_10_20 (305/666).
Encoding transition T-xnei_10_22 (306/666).
Encoding transition T-xnei_10_23 (307/666).
Encoding transition T-xnei_10_24 (308/666).
Encoding transition T-xnei_10_25 (309/666).
Encoding transition T-xnei_10_26 (310/666).
Encoding transition T-xnei_10_27 (311/666).
Encoding transition T-xnei_10_28 (312/666).
Encoding transition T-xnei_10_29 (313/666).
Encoding transition T-xnei_10_30 (314/666).
Encoding transition T-xnei_10_32 (315/666).
Encoding transition T-xnei_10_33 (316/666).
Encoding transition T-xnei_10_34 (317/666).
Encoding transition T-xnei_10_35 (318/666).
Encoding transition T-xnei_10_36 (319/666).
Encoding transition T-xnei_10_37 (320/666).
Encoding transition T-xnei_10_38 (321/666).
Encoding transition T-xnei_10_39 (322/666).
Encoding transition T-xnei_10_40 (323/666).
Encoding transition T-xnei_10_42 (324/666).
Encoding transition T-xnei_10_43 (325/666).
Encoding transition T-xnei_10_44 (326/666).
Encoding transition T-xnei_10_45 (327/666).
Encoding transition T-xnei_10_46 (328/666).
Encoding transition T-xnei_10_47 (329/666).
Encoding transition T-xnei_10_48 (330/666).
Encoding transition T-xnei_10_49 (331/666).
Encoding transition T-xnei_10_50 (332/666).
Encoding transition T-xnei_10_52 (333/666).
Encoding transition T-xnei_10_53 (334/666).
Encoding transition T-xnei_10_54 (335/666).
Encoding transition T-xnei_10_55 (336/666).
Encoding transition T-xnei_10_56 (337/666).
Encoding transition T-xnei_10_57 (338/666).
Encoding transition T-xnei_10_58 (339/666).
Encoding transition T-xnei_10_59 (340/666).
Encoding transition T-xnei_10_60 (341/666).
Encoding transition T-xnei_10_62 (342/666).
Encoding transition T-xnei_10_63 (343/666).
Encoding transition T-xnei_10_64 (344/666).
Encoding transition T-xnei_10_65 (345/666).
Encoding transition T-xnei_10_66 (346/666).
Encoding transition T-xnei_10_67 (347/666).
Encoding transition T-xnei_10_68 (348/666).
Encoding transition T-xnei_10_69 (349/666).
Encoding transition T-xnei_10_70 (350/666).
Encoding transition T-xnei_10_72 (351/666).
Encoding transition T-xnei_10_73 (352/666).
Encoding transition T-xnei_10_74 (353/666).
Encoding transition T-xnei_10_75 (354/666).
Encoding transition T-xnei_10_76 (355/666).
Encoding transition T-xnei_10_77 (356/666).
Encoding transition T-xnei_10_78 (357/666).
Encoding transition T-xnei_10_79 (358/666).
Encoding transition T-xnei_10_80 (359/666).
Encoding transition T-setbi_11_1 (360/666).
Encoding transition T-setbi_11_2 (361/666).
Encoding transition T-setbi_11_3 (362/666).
Encoding transition T-setbi_11_4 (363/666).
Encoding transition T-setbi_11_5 (364/666).
Encoding transition T-setbi_11_6 (365/666).
Encoding transition T-setbi_11_7 (366/666).
Encoding transition T-setbi_11_8 (367/666).
Encoding transition T-setbi_11_9 (368/666).
Encoding transition T-setbi_11_10 (369/666).
Encoding transition T-setbi_11_11 (370/666).
Encoding transition T-setbi_11_12 (371/666).
Encoding transition T-setbi_11_13 (372/666).
Encoding transition T-setbi_11_14 (373/666).
Encoding transition T-setbi_11_15 (374/666).
Encoding transition T-setbi_11_16 (375/666).
Encoding transition T-setbi_11_17 (376/666).
Encoding transition T-setbi_11_18 (377/666).
Encoding transition T-fordo_12_1 (378/666).
Encoding transition T-fordo_12_2 (379/666).
Encoding transition T-fordo_12_3 (380/666).
Encoding transition T-fordo_12_4 (381/666).
Encoding transition T-fordo_12_5 (382/666).
Encoding transition T-fordo_12_6 (383/666).
Encoding transition T-fordo_12_7 (384/666).
Encoding transition T-fordo_12_8 (385/666).
Encoding transition T-fordo_12_9 (386/666).
Encoding transition T-await_13_1 (387/666).
Encoding transition T-await_13_2 (388/666).
Encoding transition T-await_13_3 (389/666).
Encoding transition T-await_13_4 (390/666).
Encoding transition T-await_13_5 (391/666).
Encoding transition T-await_13_6 (392/666).
Encoding transition T-await_13_7 (393/666).
Encoding transition T-await_13_8 (394/666).
Encoding transition T-await_13_9 (395/666).
Encoding transition T-await_13_10 (396/666).
Encoding transition T-await_13_11 (397/666).
Encoding transition T-await_13_12 (398/666).
Encoding transition T-await_13_13 (399/666).
Encoding transition T-await_13_14 (400/666).
Encoding transition T-await_13_15 (401/666).
Encoding transition T-await_13_16 (402/666).
Encoding transition T-await_13_17 (403/666).
Encoding transition T-await_13_18 (404/666).
Encoding transition T-await_13_19 (405/666).
Encoding transition T-await_13_20 (406/666).
Encoding transition T-await_13_21 (407/666).
Encoding transition T-await_13_22 (408/666).
Encoding transition T-await_13_23 (409/666).
Encoding transition T-await_13_24 (410/666).
Encoding transition T-await_13_25 (411/666).
Encoding transition T-await_13_26 (412/666).
Encoding transition T-await_13_27 (413/666).
Encoding transition T-await_13_28 (414/666).
Encoding transition T-await_13_29 (415/666).
Encoding transition T-await_13_30 (416/666).
Encoding transition T-await_13_31 (417/666).
Encoding transition T-await_13_32 (418/666).
Encoding transition T-await_13_33 (419/666).
Encoding transition T-await_13_34 (420/666).
Encoding transition T-await_13_35 (421/666).
Encoding transition T-await_13_36 (422/666).
Encoding transition T-await_13_37 (423/666).
Encoding transition T-await_13_38 (424/666).
Encoding transition T-await_13_39 (425/666).
Encoding transition T-await_13_40 (426/666).
Encoding transition T-await_13_41 (427/666).
Encoding transition T-await_13_42 (428/666).
Encoding transition T-await_13_43 (429/666).
Encoding transition T-await_13_44 (430/666).
Encoding transition T-await_13_45 (431/666).
Encoding transition T-await_13_46 (432/666).
Encoding transition T-await_13_47 (433/666).
Encoding transition T-await_13_48 (434/666).
Encoding transition T-await_13_49 (435/666).
Encoding transition T-await_13_50 (436/666).
Encoding transition T-await_13_51 (437/666).
Encoding transition T-await_13_52 (438/666).
Encoding transition T-await_13_53 (439/666).
Encoding transition T-await_13_54 (440/666).
Encoding transition T-await_13_55 (441/666).
Encoding transition T-await_13_56 (442/666).
Encoding transition T-await_13_57 (443/666).
Encoding transition T-await_13_58 (444/666).
Encoding transition T-await_13_59 (445/666).
Encoding transition T-await_13_60 (446/666).
Encoding transition T-await_13_61 (447/666).
Encoding transition T-await_13_62 (448/666).
Encoding transition T-await_13_63 (449/666).
Encoding transition T-await_13_64 (450/666).
Encoding transition T-await_13_65 (451/666).
Encoding transition T-await_13_66 (452/666).
Encoding transition T-await_13_67 (453/666).
Encoding transition T-await_13_68 (454/666).
Encoding transition T-await_13_69 (455/666).
Encoding transition T-await_13_70 (456/666).
Encoding transition T-await_13_71 (457/666).
Encoding transition T-await_13_72 (458/666).
Encoding transition T-await_13_73 (459/666).
Encoding transition T-await_13_74 (460/666).
Encoding transition T-await_13_75 (461/666).
Encoding transition T-await_13_76 (462/666).
Encoding transition T-await_13_77 (463/666).
Encoding transition T-await_13_78 (464/666).
Encoding transition T-await_13_79 (465/666).
Encoding transition T-await_13_80 (466/666).
Encoding transition T-await_13_81 (467/666).
Encoding transition T-forod_13_1 (468/666).
Encoding transition T-forod_13_2 (469/666).
Encoding transition T-forod_13_3 (470/666).
Encoding transition T-forod_13_4 (471/666).
Encoding transition T-forod_13_5 (472/666).
Encoding transition T-forod_13_6 (473/666).
Encoding transition T-forod_13_7 (474/666).
Encoding transition T-forod_13_8 (475/666).
Encoding transition T-forod_13_9 (476/666).
Encoding transition T-ynei_15_2 (477/666).
Encoding transition T-ynei_15_3 (478/666).
Encoding transition T-ynei_15_4 (479/666).
Encoding transition T-ynei_15_5 (480/666).
Encoding transition T-ynei_15_6 (481/666).
Encoding transition T-ynei_15_7 (482/666).
Encoding transition T-ynei_15_8 (483/666).
Encoding transition T-ynei_15_9 (484/666).
Encoding transition T-ynei_15_10 (485/666).
Encoding transition T-ynei_15_12 (486/666).
Encoding transition T-ynei_15_13 (487/666).
Encoding transition T-ynei_15_14 (488/666).
Encoding transition T-ynei_15_15 (489/666).
Encoding transition T-ynei_15_16 (490/666).
Encoding transition T-ynei_15_17 (491/666).
Encoding transition T-ynei_15_18 (492/666).
Encoding transition T-ynei_15_19 (493/666).
Encoding transition T-ynei_15_20 (494/666).
Encoding transition T-ynei_15_22 (495/666).
Encoding transition T-ynei_15_23 (496/666).
Encoding transition T-ynei_15_24 (497/666).
Encoding transition T-ynei_15_25 (498/666).
Encoding transition T-ynei_15_26 (499/666).
Encoding transition T-ynei_15_27 (500/666).
Encoding transition T-ynei_15_28 (501/666).
Encoding transition T-ynei_15_29 (502/666).
Encoding transition T-ynei_15_30 (503/666).
Encoding transition T-ynei_15_32 (504/666).
Encoding transition T-ynei_15_33 (505/666).
Encoding transition T-ynei_15_34 (506/666).
Encoding transition T-ynei_15_35 (507/666).
Encoding transition T-ynei_15_36 (508/666).
Encoding transition T-ynei_15_37 (509/666).
Encoding transition T-ynei_15_38 (510/666).
Encoding transition T-ynei_15_39 (511/666).
Encoding transition T-ynei_15_40 (512/666).
Encoding transition T-ynei_15_42 (513/666).
Encoding transition T-ynei_15_43 (514/666).
Encoding transition T-ynei_15_44 (515/666).
Encoding transition T-ynei_15_45 (516/666).
Encoding transition T-ynei_15_46 (517/666).
Encoding transition T-ynei_15_47 (518/666).
Encoding transition T-ynei_15_48 (519/666).
Encoding transition T-ynei_15_49 (520/666).
Encoding transition T-ynei_15_50 (521/666).
Encoding transition T-ynei_15_52 (522/666).
Encoding transition T-ynei_15_53 (523/666).
Encoding transition T-ynei_15_54 (524/666).
Encoding transition T-ynei_15_55 (525/666).
Encoding transition T-ynei_15_56 (526/666).
Encoding transition T-ynei_15_57 (527/666).
Encoding transition T-ynei_15_58 (528/666).
Encoding transition T-ynei_15_59 (529/666).
Encoding transition T-ynei_15_60 (530/666).
Encoding transition T-ynei_15_62 (531/666).
Encoding transition T-ynei_15_63 (532/666).
Encoding transition T-ynei_15_64 (533/666).
Encoding transition T-ynei_15_65 (534/666).
Encoding transition T-ynei_15_66 (535/666).
Encoding transition T-ynei_15_67 (536/666).
Encoding transition T-ynei_15_68 (537/666).
Encoding transition T-ynei_15_69 (538/666).
Encoding transition T-ynei_15_70 (539/666).
Encoding transition T-ynei_15_72 (540/666).
Encoding transition T-ynei_15_73 (541/666).
Encoding transition T-ynei_15_74 (542/666).
Encoding transition T-ynei_15_75 (543/666).
Encoding transition T-ynei_15_76 (544/666).
Encoding transition T-ynei_15_77 (545/666).
Encoding transition T-ynei_15_78 (546/666).
Encoding transition T-ynei_15_79 (547/666).
Encoding transition T-ynei_15_80 (548/666).
Encoding transition T-yeqi_15_1 (549/666).
Encoding transition T-yeqi_15_11 (550/666).
Encoding transition T-yeqi_15_21 (551/666).
Encoding transition T-yeqi_15_31 (552/666).
Encoding transition T-yeqi_15_41 (553/666).
Encoding transition T-yeqi_15_51 (554/666).
Encoding transition T-yeqi_15_61 (555/666).
Encoding transition T-yeqi_15_71 (556/666).
Encoding transition T-yeqi_15_81 (557/666).
Encoding transition T-xeqi_10_1 (558/666).
Encoding transition T-xeqi_10_11 (559/666).
Encoding transition T-xeqi_10_21 (560/666).
Encoding transition T-xeqi_10_31 (561/666).
Encoding transition T-xeqi_10_41 (562/666).
Encoding transition T-xeqi_10_51 (563/666).
Encoding transition T-xeqi_10_61 (564/666).
Encoding transition T-xeqi_10_71 (565/666).
Encoding transition T-xeqi_10_81 (566/666).
Encoding transition T-sety0_23_1 (567/666).
Encoding transition T-sety0_23_2 (568/666).
Encoding transition T-sety0_23_3 (569/666).
Encoding transition T-sety0_23_4 (570/666).
Encoding transition T-sety0_23_5 (571/666).
Encoding transition T-sety0_23_6 (572/666).
Encoding transition T-sety0_23_7 (573/666).
Encoding transition T-sety0_23_8 (574/666).
Encoding transition T-sety0_23_9 (575/666).
Encoding transition T-sety0_23_10 (576/666).
Encoding transition T-sety0_23_11 (577/666).
Encoding transition T-sety0_23_12 (578/666).
Encoding transition T-sety0_23_13 (579/666).
Encoding transition T-sety0_23_14 (580/666).
Encoding transition T-sety0_23_15 (581/666).
Encoding transition T-sety0_23_16 (582/666).
Encoding transition T-sety0_23_17 (583/666).
Encoding transition T-sety0_23_18 (584/666).
Encoding transition T-sety0_23_19 (585/666).
Encoding transition T-sety0_23_20 (586/666).
Encoding transition T-sety0_23_21 (587/666).
Encoding transition T-sety0_23_22 (588/666).
Encoding transition T-sety0_23_23 (589/666).
Encoding transition T-sety0_23_24 (590/666).
Encoding transition T-sety0_23_25 (591/666).
Encoding transition T-sety0_23_26 (592/666).
Encoding transition T-sety0_23_27 (593/666).
Encoding transition T-sety0_23_28 (594/666).
Encoding transition T-sety0_23_29 (595/666).
Encoding transition T-sety0_23_30 (596/666).
Encoding transition T-sety0_23_31 (597/666).
Encoding transition T-sety0_23_32 (598/666).
Encoding transition T-sety0_23_33 (599/666).
Encoding transition T-sety0_23_34 (600/666).
Encoding transition T-sety0_23_35 (601/666).
Encoding transition T-sety0_23_36 (602/666).
Encoding transition T-sety0_23_37 (603/666).
Encoding transition T-sety0_23_38 (604/666).
Encoding transition T-sety0_23_39 (605/666).
Encoding transition T-sety0_23_40 (606/666).
Encoding transition T-sety0_23_41 (607/666).
Encoding transition T-sety0_23_42 (608/666).
Encoding transition T-sety0_23_43 (609/666).
Encoding transition T-sety0_23_44 (610/666).
Encoding transition T-sety0_23_45 (611/666).
Encoding transition T-sety0_23_46 (612/666).
Encoding transition T-sety0_23_47 (613/666).
Encoding transition T-sety0_23_48 (614/666).
Encoding transition T-sety0_23_49 (615/666).
Encoding transition T-sety0_23_50 (616/666).
Encoding transition T-sety0_23_51 (617/666).
Encoding transition T-sety0_23_52 (618/666).
Encoding transition T-sety0_23_53 (619/666).
Encoding transition T-sety0_23_54 (620/666).
Encoding transition T-sety0_23_55 (621/666).
Encoding transition T-sety0_23_56 (622/666).
Encoding transition T-sety0_23_57 (623/666).
Encoding transition T-sety0_23_58 (624/666).
Encoding transition T-sety0_23_59 (625/666).
Encoding transition T-sety0_23_60 (626/666).
Encoding transition T-sety0_23_61 (627/666).
Encoding transition T-sety0_23_62 (628/666).
Encoding transition T-sety0_23_63 (629/666).
Encoding transition T-sety0_23_64 (630/666).
Encoding transition T-sety0_23_65 (631/666).
Encoding transition T-sety0_23_66 (632/666).
Encoding transition T-sety0_23_67 (633/666).
Encoding transition T-sety0_23_68 (634/666).
Encoding transition T-sety0_23_69 (635/666).
Encoding transition T-sety0_23_70 (636/666).
Encoding transition T-sety0_23_71 (637/666).
Encoding transition T-sety0_23_72 (638/666).
Encoding transition T-sety0_23_73 (639/666).
Encoding transition T-sety0_23_74 (640/666).
Encoding transition T-sety0_23_75 (641/666).
Encoding transition T-sety0_23_76 (642/666).
Encoding transition T-sety0_23_77 (643/666).
Encoding transition T-sety0_23_78 (644/666).
Encoding transition T-sety0_23_79 (645/666).
Encoding transition T-sety0_23_80 (646/666).
Encoding transition T-sety0_23_81 (647/666).
Encoding transition T-setbi_24_1 (648/666).
Encoding transition T-setbi_24_2 (649/666).
Encoding transition T-setbi_24_3 (650/666).
Encoding transition T-setbi_24_4 (651/666).
Encoding transition T-setbi_24_5 (652/666).
Encoding transition T-setbi_24_6 (653/666).
Encoding transition T-setbi_24_7 (654/666).
Encoding transition T-setbi_24_8 (655/666).
Encoding transition T-setbi_24_9 (656/666).
Encoding transition T-setbi_24_10 (657/666).
Encoding transition T-setbi_24_11 (658/666).
Encoding transition T-setbi_24_12 (659/666).
Encoding transition T-setbi_24_13 (660/666).
Encoding transition T-setbi_24_14 (661/666).
Encoding transition T-setbi_24_15 (662/666).
Encoding transition T-setbi_24_16 (663/666).
Encoding transition T-setbi_24_17 (664/666).
Encoding transition T-setbi_24_18 (665/666).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 43972KB

BK_TIME_CONFINEMENT_REACHED

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

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="SurpriseLamportFastMutEx-PT-8"
export BK_EXAMINATION="CTLFireability"
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/SurpriseLamportFastMutEx-PT-8.tgz
mv SurpriseLamportFastMutEx-PT-8 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 SurpriseLamportFastMutEx-PT-8, examination is CTLFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r08ks-qhx2-140068993901219"
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 ;