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-7, examination is ReachabilityFireabilitySimple
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r08ks-qhx2-140068993901202
=====================================================================

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

BK_START 1400731407268
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurpriseLamportFastMutEx (PT), instance 7
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireabilitySimple.xml INTO /home/mcc/execution/ReachabilityFireabilitySimple.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 21 -C -f /home/mcc/execution/ReachabilityFireabilitySimple.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/536).
Encoding transition T-setbi_2_2 (1/536).
Encoding transition T-setbi_2_3 (2/536).
Encoding transition T-setbi_2_4 (3/536).
Encoding transition T-setbi_2_5 (4/536).
Encoding transition T-setbi_2_6 (5/536).
Encoding transition T-setbi_2_7 (6/536).
Encoding transition T-setbi_2_8 (7/536).
Encoding transition T-setbi_2_9 (8/536).
Encoding transition T-setbi_2_10 (9/536).
Encoding transition T-setbi_2_11 (10/536).
Encoding transition T-setbi_2_12 (11/536).
Encoding transition T-setbi_2_13 (12/536).
Encoding transition T-setbi_2_14 (13/536).
Encoding transition T-setbi_2_15 (14/536).
Encoding transition T-setbi_2_16 (15/536).
Encoding transition T-setx_3_1 (16/536).
Encoding transition T-setx_3_2 (17/536).
Encoding transition T-setx_3_3 (18/536).
Encoding transition T-setx_3_4 (19/536).
Encoding transition T-setx_3_5 (20/536).
Encoding transition T-setx_3_6 (21/536).
Encoding transition T-setx_3_7 (22/536).
Encoding transition T-setx_3_8 (23/536).
Encoding transition T-setx_3_9 (24/536).
Encoding transition T-setx_3_10 (25/536).
Encoding transition T-setx_3_11 (26/536).
Encoding transition T-setx_3_12 (27/536).
Encoding transition T-setx_3_13 (28/536).
Encoding transition T-setx_3_14 (29/536).
Encoding transition T-setx_3_15 (30/536).
Encoding transition T-setx_3_16 (31/536).
Encoding transition T-setx_3_17 (32/536).
Encoding transition T-setx_3_18 (33/536).
Encoding transition T-setx_3_19 (34/536).
Encoding transition T-setx_3_20 (35/536).
Encoding transition T-setx_3_21 (36/536).
Encoding transition T-setx_3_22 (37/536).
Encoding transition T-setx_3_23 (38/536).
Encoding transition T-setx_3_24 (39/536).
Encoding transition T-setx_3_25 (40/536).
Encoding transition T-setx_3_26 (41/536).
Encoding transition T-setx_3_27 (42/536).
Encoding transition T-setx_3_28 (43/536).
Encoding transition T-setx_3_29 (44/536).
Encoding transition T-setx_3_30 (45/536).
Encoding transition T-setx_3_31 (46/536).
Encoding transition T-setx_3_32 (47/536).
Encoding transition T-setx_3_33 (48/536).
Encoding transition T-setx_3_34 (49/536).
Encoding transition T-setx_3_35 (50/536).
Encoding transition T-setx_3_36 (51/536).
Encoding transition T-setx_3_37 (52/536).
Encoding transition T-setx_3_38 (53/536).
Encoding transition T-setx_3_39 (54/536).
Encoding transition T-setx_3_40 (55/536).
Encoding transition T-setx_3_41 (56/536).
Encoding transition T-setx_3_42 (57/536).
Encoding transition T-setx_3_43 (58/536).
Encoding transition T-setx_3_44 (59/536).
Encoding transition T-setx_3_45 (60/536).
Encoding transition T-setx_3_46 (61/536).
Encoding transition T-setx_3_47 (62/536).
Encoding transition T-setx_3_48 (63/536).
Encoding transition T-setx_3_49 (64/536).
Encoding transition T-setx_3_50 (65/536).
Encoding transition T-setx_3_51 (66/536).
Encoding transition T-setx_3_52 (67/536).
Encoding transition T-setx_3_53 (68/536).
Encoding transition T-setx_3_54 (69/536).
Encoding transition T-setx_3_55 (70/536).
Encoding transition T-setx_3_56 (71/536).
Encoding transition T-setx_3_57 (72/536).
Encoding transition T-setx_3_58 (73/536).
Encoding transition T-setx_3_59 (74/536).
Encoding transition T-setx_3_60 (75/536).
Encoding transition T-setx_3_61 (76/536).
Encoding transition T-setx_3_62 (77/536).
Encoding transition T-setx_3_63 (78/536).
Encoding transition T-setx_3_64 (79/536).
Encoding transition T-yne0_4_2 (80/536).
Encoding transition T-yne0_4_3 (81/536).
Encoding transition T-yne0_4_4 (82/536).
Encoding transition T-yne0_4_5 (83/536).
Encoding transition T-yne0_4_6 (84/536).
Encoding transition T-yne0_4_7 (85/536).
Encoding transition T-yne0_4_8 (86/536).
Encoding transition T-yne0_4_10 (87/536).
Encoding transition T-yne0_4_11 (88/536).
Encoding transition T-yne0_4_12 (89/536).
Encoding transition T-yne0_4_13 (90/536).
Encoding transition T-yne0_4_14 (91/536).
Encoding transition T-yne0_4_15 (92/536).
Encoding transition T-yne0_4_16 (93/536).
Encoding transition T-yne0_4_18 (94/536).
Encoding transition T-yne0_4_19 (95/536).
Encoding transition T-yne0_4_20 (96/536).
Encoding transition T-yne0_4_21 (97/536).
Encoding transition T-yne0_4_22 (98/536).
Encoding transition T-yne0_4_23 (99/536).
Encoding transition T-yne0_4_24 (100/536).
Encoding transition T-yne0_4_26 (101/536).
Encoding transition T-yne0_4_27 (102/536).
Encoding transition T-yne0_4_28 (103/536).
Encoding transition T-yne0_4_29 (104/536).
Encoding transition T-yne0_4_30 (105/536).
Encoding transition T-yne0_4_31 (106/536).
Encoding transition T-yne0_4_32 (107/536).
Encoding transition T-yne0_4_34 (108/536).
Encoding transition T-yne0_4_35 (109/536).
Encoding transition T-yne0_4_36 (110/536).
Encoding transition T-yne0_4_37 (111/536).
Encoding transition T-yne0_4_38 (112/536).
Encoding transition T-yne0_4_39 (113/536).
Encoding transition T-yne0_4_40 (114/536).
Encoding transition T-yne0_4_42 (115/536).
Encoding transition T-yne0_4_43 (116/536).
Encoding transition T-yne0_4_44 (117/536).
Encoding transition T-yne0_4_45 (118/536).
Encoding transition T-yne0_4_46 (119/536).
Encoding transition T-yne0_4_47 (120/536).
Encoding transition T-yne0_4_48 (121/536).
Encoding transition T-yne0_4_50 (122/536).
Encoding transition T-yne0_4_51 (123/536).
Encoding transition T-yne0_4_52 (124/536).
Encoding transition T-yne0_4_53 (125/536).
Encoding transition T-yne0_4_54 (126/536).
Encoding transition T-yne0_4_55 (127/536).
Encoding transition T-yne0_4_56 (128/536).
Encoding transition T-yne0_4_58 (129/536).
Encoding transition T-yne0_4_59 (130/536).
Encoding transition T-yne0_4_60 (131/536).
Encoding transition T-yne0_4_61 (132/536).
Encoding transition T-yne0_4_62 (133/536).
Encoding transition T-yne0_4_63 (134/536).
Encoding transition T-yne0_4_64 (135/536).
Encoding transition T-setbi_5_1 (136/536).
Encoding transition T-setbi_5_2 (137/536).
Encoding transition T-setbi_5_3 (138/536).
Encoding transition T-setbi_5_4 (139/536).
Encoding transition T-setbi_5_5 (140/536).
Encoding transition T-setbi_5_6 (141/536).
Encoding transition T-setbi_5_7 (142/536).
Encoding transition T-setbi_5_8 (143/536).
Encoding transition T-setbi_5_9 (144/536).
Encoding transition T-setbi_5_10 (145/536).
Encoding transition T-setbi_5_11 (146/536).
Encoding transition T-setbi_5_12 (147/536).
Encoding transition T-setbi_5_13 (148/536).
Encoding transition T-setbi_5_14 (149/536).
Encoding transition T-setbi_5_15 (150/536).
Encoding transition T-setbi_5_16 (151/536).
Encoding transition T-awaity_1 (152/536).
Encoding transition T-awaity_2 (153/536).
Encoding transition T-awaity_3 (154/536).
Encoding transition T-awaity_4 (155/536).
Encoding transition T-awaity_5 (156/536).
Encoding transition T-awaity_6 (157/536).
Encoding transition T-awaity_7 (158/536).
Encoding transition T-awaity_8 (159/536).
Encoding transition T-yeq0_4_1 (160/536).
Encoding transition T-yeq0_4_2 (161/536).
Encoding transition T-yeq0_4_3 (162/536).
Encoding transition T-yeq0_4_4 (163/536).
Encoding transition T-yeq0_4_5 (164/536).
Encoding transition T-yeq0_4_6 (165/536).
Encoding transition T-yeq0_4_7 (166/536).
Encoding transition T-yeq0_4_8 (167/536).
Encoding transition T-sety_9_1 (168/536).
Encoding transition T-sety_9_2 (169/536).
Encoding transition T-sety_9_3 (170/536).
Encoding transition T-sety_9_4 (171/536).
Encoding transition T-sety_9_5 (172/536).
Encoding transition T-sety_9_6 (173/536).
Encoding transition T-sety_9_7 (174/536).
Encoding transition T-sety_9_8 (175/536).
Encoding transition T-sety_9_9 (176/536).
Encoding transition T-sety_9_10 (177/536).
Encoding transition T-sety_9_11 (178/536).
Encoding transition T-sety_9_12 (179/536).
Encoding transition T-sety_9_13 (180/536).
Encoding transition T-sety_9_14 (181/536).
Encoding transition T-sety_9_15 (182/536).
Encoding transition T-sety_9_16 (183/536).
Encoding transition T-sety_9_17 (184/536).
Encoding transition T-sety_9_18 (185/536).
Encoding transition T-sety_9_19 (186/536).
Encoding transition T-sety_9_20 (187/536).
Encoding transition T-sety_9_21 (188/536).
Encoding transition T-sety_9_22 (189/536).
Encoding transition T-sety_9_23 (190/536).
Encoding transition T-sety_9_24 (191/536).
Encoding transition T-sety_9_25 (192/536).
Encoding transition T-sety_9_26 (193/536).
Encoding transition T-sety_9_27 (194/536).
Encoding transition T-sety_9_28 (195/536).
Encoding transition T-sety_9_29 (196/536).
Encoding transition T-sety_9_30 (197/536).
Encoding transition T-sety_9_31 (198/536).
Encoding transition T-sety_9_32 (199/536).
Encoding transition T-sety_9_33 (200/536).
Encoding transition T-sety_9_34 (201/536).
Encoding transition T-sety_9_35 (202/536).
Encoding transition T-sety_9_36 (203/536).
Encoding transition T-sety_9_37 (204/536).
Encoding transition T-sety_9_38 (205/536).
Encoding transition T-sety_9_39 (206/536).
Encoding transition T-sety_9_40 (207/536).
Encoding transition T-sety_9_41 (208/536).
Encoding transition T-sety_9_42 (209/536).
Encoding transition T-sety_9_43 (210/536).
Encoding transition T-sety_9_44 (211/536).
Encoding transition T-sety_9_45 (212/536).
Encoding transition T-sety_9_46 (213/536).
Encoding transition T-sety_9_47 (214/536).
Encoding transition T-sety_9_48 (215/536).
Encoding transition T-sety_9_49 (216/536).
Encoding transition T-sety_9_50 (217/536).
Encoding transition T-sety_9_51 (218/536).
Encoding transition T-sety_9_52 (219/536).
Encoding transition T-sety_9_53 (220/536).
Encoding transition T-sety_9_54 (221/536).
Encoding transition T-sety_9_55 (222/536).
Encoding transition T-sety_9_56 (223/536).
Encoding transition T-sety_9_57 (224/536).
Encoding transition T-sety_9_58 (225/536).
Encoding transition T-sety_9_59 (226/536).
Encoding transition T-sety_9_60 (227/536).
Encoding transition T-sety_9_61 (228/536).
Encoding transition T-sety_9_62 (229/536).
Encoding transition T-sety_9_63 (230/536).
Encoding transition T-sety_9_64 (231/536).
Encoding transition T-xnei_10_2 (232/536).
Encoding transition T-xnei_10_3 (233/536).
Encoding transition T-xnei_10_4 (234/536).
Encoding transition T-xnei_10_5 (235/536).
Encoding transition T-xnei_10_6 (236/536).
Encoding transition T-xnei_10_7 (237/536).
Encoding transition T-xnei_10_8 (238/536).
Encoding transition T-xnei_10_9 (239/536).
Encoding transition T-xnei_10_11 (240/536).
Encoding transition T-xnei_10_12 (241/536).
Encoding transition T-xnei_10_13 (242/536).
Encoding transition T-xnei_10_14 (243/536).
Encoding transition T-xnei_10_15 (244/536).
Encoding transition T-xnei_10_16 (245/536).
Encoding transition T-xnei_10_17 (246/536).
Encoding transition T-xnei_10_18 (247/536).
Encoding transition T-xnei_10_20 (248/536).
Encoding transition T-xnei_10_21 (249/536).
Encoding transition T-xnei_10_22 (250/536).
Encoding transition T-xnei_10_23 (251/536).
Encoding transition T-xnei_10_24 (252/536).
Encoding transition T-xnei_10_25 (253/536).
Encoding transition T-xnei_10_26 (254/536).
Encoding transition T-xnei_10_27 (255/536).
Encoding transition T-xnei_10_29 (256/536).
Encoding transition T-xnei_10_30 (257/536).
Encoding transition T-xnei_10_31 (258/536).
Encoding transition T-xnei_10_32 (259/536).
Encoding transition T-xnei_10_33 (260/536).
Encoding transition T-xnei_10_34 (261/536).
Encoding transition T-xnei_10_35 (262/536).
Encoding transition T-xnei_10_36 (263/536).
Encoding transition T-xnei_10_38 (264/536).
Encoding transition T-xnei_10_39 (265/536).
Encoding transition T-xnei_10_40 (266/536).
Encoding transition T-xnei_10_41 (267/536).
Encoding transition T-xnei_10_42 (268/536).
Encoding transition T-xnei_10_43 (269/536).
Encoding transition T-xnei_10_44 (270/536).
Encoding transition T-xnei_10_45 (271/536).
Encoding transition T-xnei_10_47 (272/536).
Encoding transition T-xnei_10_48 (273/536).
Encoding transition T-xnei_10_49 (274/536).
Encoding transition T-xnei_10_50 (275/536).
Encoding transition T-xnei_10_51 (276/536).
Encoding transition T-xnei_10_52 (277/536).
Encoding transition T-xnei_10_53 (278/536).
Encoding transition T-xnei_10_54 (279/536).
Encoding transition T-xnei_10_56 (280/536).
Encoding transition T-xnei_10_57 (281/536).
Encoding transition T-xnei_10_58 (282/536).
Encoding transition T-xnei_10_59 (283/536).
Encoding transition T-xnei_10_60 (284/536).
Encoding transition T-xnei_10_61 (285/536).
Encoding transition T-xnei_10_62 (286/536).
Encoding transition T-xnei_10_63 (287/536).
Encoding transition T-setbi_11_1 (288/536).
Encoding transition T-setbi_11_2 (289/536).
Encoding transition T-setbi_11_3 (290/536).
Encoding transition T-setbi_11_4 (291/536).
Encoding transition T-setbi_11_5 (292/536).
Encoding transition T-setbi_11_6 (293/536).
Encoding transition T-setbi_11_7 (294/536).
Encoding transition T-setbi_11_8 (295/536).
Encoding transition T-setbi_11_9 (296/536).
Encoding transition T-setbi_11_10 (297/536).
Encoding transition T-setbi_11_11 (298/536).
Encoding transition T-setbi_11_12 (299/536).
Encoding transition T-setbi_11_13 (300/536).
Encoding transition T-setbi_11_14 (301/536).
Encoding transition T-setbi_11_15 (302/536).
Encoding transition T-setbi_11_16 (303/536).
Encoding transition T-fordo_12_1 (304/536).
Encoding transition T-fordo_12_2 (305/536).
Encoding transition T-fordo_12_3 (306/536).
Encoding transition T-fordo_12_4 (307/536).
Encoding transition T-fordo_12_5 (308/536).
Encoding transition T-fordo_12_6 (309/536).
Encoding transition T-fordo_12_7 (310/536).
Encoding transition T-fordo_12_8 (311/536).
Encoding transition T-await_13_1 (312/536).
Encoding transition T-await_13_2 (313/536).
Encoding transition T-await_13_3 (314/536).
Encoding transition T-await_13_4 (315/536).
Encoding transition T-await_13_5 (316/536).
Encoding transition T-await_13_6 (317/536).
Encoding transition T-await_13_7 (318/536).
Encoding transition T-await_13_8 (319/536).
Encoding transition T-await_13_9 (320/536).
Encoding transition T-await_13_10 (321/536).
Encoding transition T-await_13_11 (322/536).
Encoding transition T-await_13_12 (323/536).
Encoding transition T-await_13_13 (324/536).
Encoding transition T-await_13_14 (325/536).
Encoding transition T-await_13_15 (326/536).
Encoding transition T-await_13_16 (327/536).
Encoding transition T-await_13_17 (328/536).
Encoding transition T-await_13_18 (329/536).
Encoding transition T-await_13_19 (330/536).
Encoding transition T-await_13_20 (331/536).
Encoding transition T-await_13_21 (332/536).
Encoding transition T-await_13_22 (333/536).
Encoding transition T-await_13_23 (334/536).
Encoding transition T-await_13_24 (335/536).
Encoding transition T-await_13_25 (336/536).
Encoding transition T-await_13_26 (337/536).
Encoding transition T-await_13_27 (338/536).
Encoding transition T-await_13_28 (339/536).
Encoding transition T-await_13_29 (340/536).
Encoding transition T-await_13_30 (341/536).
Encoding transition T-await_13_31 (342/536).
Encoding transition T-await_13_32 (343/536).
Encoding transition T-await_13_33 (344/536).
Encoding transition T-await_13_34 (345/536).
Encoding transition T-await_13_35 (346/536).
Encoding transition T-await_13_36 (347/536).
Encoding transition T-await_13_37 (348/536).
Encoding transition T-await_13_38 (349/536).
Encoding transition T-await_13_39 (350/536).
Encoding transition T-await_13_40 (351/536).
Encoding transition T-await_13_41 (352/536).
Encoding transition T-await_13_42 (353/536).
Encoding transition T-await_13_43 (354/536).
Encoding transition T-await_13_44 (355/536).
Encoding transition T-await_13_45 (356/536).
Encoding transition T-await_13_46 (357/536).
Encoding transition T-await_13_47 (358/536).
Encoding transition T-await_13_48 (359/536).
Encoding transition T-await_13_49 (360/536).
Encoding transition T-await_13_50 (361/536).
Encoding transition T-await_13_51 (362/536).
Encoding transition T-await_13_52 (363/536).
Encoding transition T-await_13_53 (364/536).
Encoding transition T-await_13_54 (365/536).
Encoding transition T-await_13_55 (366/536).
Encoding transition T-await_13_56 (367/536).
Encoding transition T-await_13_57 (368/536).
Encoding transition T-await_13_58 (369/536).
Encoding transition T-await_13_59 (370/536).
Encoding transition T-await_13_60 (371/536).
Encoding transition T-await_13_61 (372/536).
Encoding transition T-await_13_62 (373/536).
Encoding transition T-await_13_63 (374/536).
Encoding transition T-await_13_64 (375/536).
Encoding transition T-forod_13_1 (376/536).
Encoding transition T-forod_13_2 (377/536).
Encoding transition T-forod_13_3 (378/536).
Encoding transition T-forod_13_4 (379/536).
Encoding transition T-forod_13_5 (380/536).
Encoding transition T-forod_13_6 (381/536).
Encoding transition T-forod_13_7 (382/536).
Encoding transition T-forod_13_8 (383/536).
Encoding transition T-ynei_15_2 (384/536).
Encoding transition T-ynei_15_3 (385/536).
Encoding transition T-ynei_15_4 (386/536).
Encoding transition T-ynei_15_5 (387/536).
Encoding transition T-ynei_15_6 (388/536).
Encoding transition T-ynei_15_7 (389/536).
Encoding transition T-ynei_15_8 (390/536).
Encoding transition T-ynei_15_9 (391/536).
Encoding transition T-ynei_15_11 (392/536).
Encoding transition T-ynei_15_12 (393/536).
Encoding transition T-ynei_15_13 (394/536).
Encoding transition T-ynei_15_14 (395/536).
Encoding transition T-ynei_15_15 (396/536).
Encoding transition T-ynei_15_16 (397/536).
Encoding transition T-ynei_15_17 (398/536).
Encoding transition T-ynei_15_18 (399/536).
Encoding transition T-ynei_15_20 (400/536).
Encoding transition T-ynei_15_21 (401/536).
Encoding transition T-ynei_15_22 (402/536).
Encoding transition T-ynei_15_23 (403/536).
Encoding transition T-ynei_15_24 (404/536).
Encoding transition T-ynei_15_25 (405/536).
Encoding transition T-ynei_15_26 (406/536).
Encoding transition T-ynei_15_27 (407/536).
Encoding transition T-ynei_15_29 (408/536).
Encoding transition T-ynei_15_30 (409/536).
Encoding transition T-ynei_15_31 (410/536).
Encoding transition T-ynei_15_32 (411/536).
Encoding transition T-ynei_15_33 (412/536).
Encoding transition T-ynei_15_34 (413/536).
Encoding transition T-ynei_15_35 (414/536).
Encoding transition T-ynei_15_36 (415/536).
Encoding transition T-ynei_15_38 (416/536).
Encoding transition T-ynei_15_39 (417/536).
Encoding transition T-ynei_15_40 (418/536).
Encoding transition T-ynei_15_41 (419/536).
Encoding transition T-ynei_15_42 (420/536).
Encoding transition T-ynei_15_43 (421/536).
Encoding transition T-ynei_15_44 (422/536).
Encoding transition T-ynei_15_45 (423/536).
Encoding transition T-ynei_15_47 (424/536).
Encoding transition T-ynei_15_48 (425/536).
Encoding transition T-ynei_15_49 (426/536).
Encoding transition T-ynei_15_50 (427/536).
Encoding transition T-ynei_15_51 (428/536).
Encoding transition T-ynei_15_52 (429/536).
Encoding transition T-ynei_15_53 (430/536).
Encoding transition T-ynei_15_54 (431/536).
Encoding transition T-ynei_15_56 (432/536).
Encoding transition T-ynei_15_57 (433/536).
Encoding transition T-ynei_15_58 (434/536).
Encoding transition T-ynei_15_59 (435/536).
Encoding transition T-ynei_15_60 (436/536).
Encoding transition T-ynei_15_61 (437/536).
Encoding transition T-ynei_15_62 (438/536).
Encoding transition T-ynei_15_63 (439/536).
Encoding transition T-yeqi_15_1 (440/536).
Encoding transition T-yeqi_15_10 (441/536).
Encoding transition T-yeqi_15_19 (442/536).
Encoding transition T-yeqi_15_28 (443/536).
Encoding transition T-yeqi_15_37 (444/536).
Encoding transition T-yeqi_15_46 (445/536).
Encoding transition T-yeqi_15_55 (446/536).
Encoding transition T-yeqi_15_64 (447/536).
Encoding transition T-xeqi_10_1 (448/536).
Encoding transition T-xeqi_10_10 (449/536).
Encoding transition T-xeqi_10_19 (450/536).
Encoding transition T-xeqi_10_28 (451/536).
Encoding transition T-xeqi_10_37 (452/536).
Encoding transition T-xeqi_10_46 (453/536).
Encoding transition T-xeqi_10_55 (454/536).
Encoding transition T-xeqi_10_64 (455/536).
Encoding transition T-sety0_23_1 (456/536).
Encoding transition T-sety0_23_2 (457/536).
Encoding transition T-sety0_23_3 (458/536).
Encoding transition T-sety0_23_4 (459/536).
Encoding transition T-sety0_23_5 (460/536).
Encoding transition T-sety0_23_6 (461/536).
Encoding transition T-sety0_23_7 (462/536).
Encoding transition T-sety0_23_8 (463/536).
Encoding transition T-sety0_23_9 (464/536).
Encoding transition T-sety0_23_10 (465/536).
Encoding transition T-sety0_23_11 (466/536).
Encoding transition T-sety0_23_12 (467/536).
Encoding transition T-sety0_23_13 (468/536).
Encoding transition T-sety0_23_14 (469/536).
Encoding transition T-sety0_23_15 (470/536).
Encoding transition T-sety0_23_16 (471/536).
Encoding transition T-sety0_23_17 (472/536).
Encoding transition T-sety0_23_18 (473/536).
Encoding transition T-sety0_23_19 (474/536).
Encoding transition T-sety0_23_20 (475/536).
Encoding transition T-sety0_23_21 (476/536).
Encoding transition T-sety0_23_22 (477/536).
Encoding transition T-sety0_23_23 (478/536).
Encoding transition T-sety0_23_24 (479/536).
Encoding transition T-sety0_23_25 (480/536).
Encoding transition T-sety0_23_26 (481/536).
Encoding transition T-sety0_23_27 (482/536).
Encoding transition T-sety0_23_28 (483/536).
Encoding transition T-sety0_23_29 (484/536).
Encoding transition T-sety0_23_30 (485/536).
Encoding transition T-sety0_23_31 (486/536).
Encoding transition T-sety0_23_32 (487/536).
Encoding transition T-sety0_23_33 (488/536).
Encoding transition T-sety0_23_34 (489/536).
Encoding transition T-sety0_23_35 (490/536).
Encoding transition T-sety0_23_36 (491/536).
Encoding transition T-sety0_23_37 (492/536).
Encoding transition T-sety0_23_38 (493/536).
Encoding transition T-sety0_23_39 (494/536).
Encoding transition T-sety0_23_40 (495/536).
Encoding transition T-sety0_23_41 (496/536).
Encoding transition T-sety0_23_42 (497/536).
Encoding transition T-sety0_23_43 (498/536).
Encoding transition T-sety0_23_44 (499/536).
Encoding transition T-sety0_23_45 (500/536).
Encoding transition T-sety0_23_46 (501/536).
Encoding transition T-sety0_23_47 (502/536).
Encoding transition T-sety0_23_48 (503/536).
Encoding transition T-sety0_23_49 (504/536).
Encoding transition T-sety0_23_50 (505/536).
Encoding transition T-sety0_23_51 (506/536).
Encoding transition T-sety0_23_52 (507/536).
Encoding transition T-sety0_23_53 (508/536).
Encoding transition T-sety0_23_54 (509/536).
Encoding transition T-sety0_23_55 (510/536).
Encoding transition T-sety0_23_56 (511/536).
Encoding transition T-sety0_23_57 (512/536).
Encoding transition T-sety0_23_58 (513/536).
Encoding transition T-sety0_23_59 (514/536).
Encoding transition T-sety0_23_60 (515/536).
Encoding transition T-sety0_23_61 (516/536).
Encoding transition T-sety0_23_62 (517/536).
Encoding transition T-sety0_23_63 (518/536).
Encoding transition T-sety0_23_64 (519/536).
Encoding transition T-setbi_24_1 (520/536).
Encoding transition T-setbi_24_2 (521/536).
Encoding transition T-setbi_24_3 (522/536).
Encoding transition T-setbi_24_4 (523/536).
Encoding transition T-setbi_24_5 (524/536).
Encoding transition T-setbi_24_6 (525/536).
Encoding transition T-setbi_24_7 (526/536).
Encoding transition T-setbi_24_8 (527/536).
Encoding transition T-setbi_24_9 (528/536).
Encoding transition T-setbi_24_10 (529/536).
Encoding transition T-setbi_24_11 (530/536).
Encoding transition T-setbi_24_12 (531/536).
Encoding transition T-setbi_24_13 (532/536).
Encoding transition T-setbi_24_14 (533/536).
Encoding transition T-setbi_24_15 (534/536).
Encoding transition T-setbi_24_16 (535/536).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 24756KB

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