About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
5862.11 | 720089 | 397.8 | MOVF | 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 SurprisePeterson-PT-4, examination is ReachabilityFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r09ks-qhx2-140069008201099
=====================================================================
--------------------
content from stdout:
BK_START 1400798045685
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurprisePeterson (PT), instance 4
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireability.xml INTO /home/mcc/execution/ReachabilityFireability.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 12 -C -f /home/mcc/execution/ReachabilityFireability.rgmedd-ctl
Using FORCE-PINV Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition NoIdentity_0_3_2 (0/690).
Encoding transition NoIdentity_1_3_2 (1/690).
Encoding transition NoIdentity_2_3_2 (2/690).
Encoding transition NoIdentity_4_3_2 (3/690).
Encoding transition NoIdentity_0_2_2 (4/690).
Encoding transition NoIdentity_1_2_2 (5/690).
Encoding transition NoIdentity_3_2_2 (6/690).
Encoding transition NoIdentity_4_2_2 (7/690).
Encoding transition NoIdentity_0_1_2 (8/690).
Encoding transition NoIdentity_2_1_2 (9/690).
Encoding transition NoIdentity_3_1_2 (10/690).
Encoding transition NoIdentity_4_1_2 (11/690).
Encoding transition NoIdentity_1_0_2 (12/690).
Encoding transition NoIdentity_2_0_2 (13/690).
Encoding transition NoIdentity_3_0_2 (14/690).
Encoding transition NoIdentity_4_0_2 (15/690).
Encoding transition NoIdentity_1_2_3 (16/690).
Encoding transition NoIdentity_0_2_3 (17/690).
Encoding transition NoIdentity_4_2_3 (18/690).
Encoding transition NoIdentity_3_2_3 (19/690).
Encoding transition NoIdentity_2_1_3 (20/690).
Encoding transition NoIdentity_0_1_3 (21/690).
Encoding transition NoIdentity_4_1_3 (22/690).
Encoding transition NoIdentity_3_1_3 (23/690).
Encoding transition NoIdentity_2_0_3 (24/690).
Encoding transition NoIdentity_1_0_3 (25/690).
Encoding transition NoIdentity_4_0_3 (26/690).
Encoding transition NoIdentity_3_0_3 (27/690).
Encoding transition NoIdentity_1_4_2 (28/690).
Encoding transition NoIdentity_0_4_2 (29/690).
Encoding transition NoIdentity_3_4_2 (30/690).
Encoding transition NoIdentity_2_4_2 (31/690).
Encoding transition Identity_1_1 (32/690).
Encoding transition Identity_2_1 (33/690).
Encoding transition Identity_4_0 (34/690).
Encoding transition Identity_0_1 (35/690).
Encoding transition Identity_2_0 (36/690).
Encoding transition Identity_3_0 (37/690).
Encoding transition Identity_0_0 (38/690).
Encoding transition Identity_1_0 (39/690).
Encoding transition NoIdentity_2_4_3 (40/690).
Encoding transition NoIdentity_3_4_3 (41/690).
Encoding transition NoIdentity_0_4_3 (42/690).
Encoding transition NoIdentity_1_4_3 (43/690).
Encoding transition NoIdentity_2_3_3 (44/690).
Encoding transition NoIdentity_4_3_3 (45/690).
Encoding transition NoIdentity_0_3_3 (46/690).
Encoding transition NoIdentity_1_3_3 (47/690).
Encoding transition ProgressTurn_3_0 (48/690).
Encoding transition ProgressTurn_2_0 (49/690).
Encoding transition ProgressTurn_1_0 (50/690).
Encoding transition ProgressTurn_0_0 (51/690).
Encoding transition Identity_4_3 (52/690).
Encoding transition Identity_3_3 (53/690).
Encoding transition Identity_2_3 (54/690).
Encoding transition Identity_1_3 (55/690).
Encoding transition Identity_0_3 (56/690).
Encoding transition Identity_4_2 (57/690).
Encoding transition Identity_3_2 (58/690).
Encoding transition Identity_2_2 (59/690).
Encoding transition Identity_1_2 (60/690).
Encoding transition Identity_0_2 (61/690).
Encoding transition Identity_4_1 (62/690).
Encoding transition Identity_3_1 (63/690).
Encoding transition UpdateTurn_4_1_3 (64/690).
Encoding transition UpdateTurn_0_2_3 (65/690).
Encoding transition UpdateTurn_1_2_3 (66/690).
Encoding transition UpdateTurn_2_2_3 (67/690).
Encoding transition UpdateTurn_3_2_3 (68/690).
Encoding transition UpdateTurn_4_2_3 (69/690).
Encoding transition UpdateTurn_0_3_3 (70/690).
Encoding transition UpdateTurn_1_3_3 (71/690).
Encoding transition UpdateTurn_1_0_3 (72/690).
Encoding transition UpdateTurn_2_0_3 (73/690).
Encoding transition UpdateTurn_3_0_3 (74/690).
Encoding transition UpdateTurn_4_0_3 (75/690).
Encoding transition UpdateTurn_0_1_3 (76/690).
Encoding transition UpdateTurn_1_1_3 (77/690).
Encoding transition UpdateTurn_2_1_3 (78/690).
Encoding transition UpdateTurn_3_1_3 (79/690).
Encoding transition NoIdentity_2_0_0 (80/690).
Encoding transition NoIdentity_1_0_0 (81/690).
Encoding transition NoIdentity_4_0_0 (82/690).
Encoding transition NoIdentity_3_0_0 (83/690).
Encoding transition NoIdentity_2_1_0 (84/690).
Encoding transition NoIdentity_0_1_0 (85/690).
Encoding transition NoIdentity_4_1_0 (86/690).
Encoding transition NoIdentity_3_1_0 (87/690).
Encoding transition UpdateTurn_3_3_3 (88/690).
Encoding transition UpdateTurn_2_3_3 (89/690).
Encoding transition UpdateTurn_0_4_3 (90/690).
Encoding transition UpdateTurn_4_3_3 (91/690).
Encoding transition UpdateTurn_2_4_3 (92/690).
Encoding transition UpdateTurn_1_4_3 (93/690).
Encoding transition UpdateTurn_4_4_3 (94/690).
Encoding transition UpdateTurn_3_4_3 (95/690).
Encoding transition NoIdentity_2_4_0 (96/690).
Encoding transition NoIdentity_3_4_0 (97/690).
Encoding transition NoIdentity_0_4_0 (98/690).
Encoding transition NoIdentity_1_4_0 (99/690).
Encoding transition NoIdentity_3_0_1 (100/690).
Encoding transition NoIdentity_4_0_1 (101/690).
Encoding transition NoIdentity_1_0_1 (102/690).
Encoding transition NoIdentity_2_0_1 (103/690).
Encoding transition NoIdentity_3_2_0 (104/690).
Encoding transition NoIdentity_4_2_0 (105/690).
Encoding transition NoIdentity_0_2_0 (106/690).
Encoding transition NoIdentity_1_2_0 (107/690).
Encoding transition NoIdentity_2_3_0 (108/690).
Encoding transition NoIdentity_4_3_0 (109/690).
Encoding transition NoIdentity_0_3_0 (110/690).
Encoding transition NoIdentity_1_3_0 (111/690).
Encoding transition NoIdentity_4_3_1 (112/690).
Encoding transition NoIdentity_2_3_1 (113/690).
Encoding transition NoIdentity_1_3_1 (114/690).
Encoding transition NoIdentity_0_3_1 (115/690).
Encoding transition NoIdentity_3_4_1 (116/690).
Encoding transition NoIdentity_2_4_1 (117/690).
Encoding transition NoIdentity_1_4_1 (118/690).
Encoding transition NoIdentity_0_4_1 (119/690).
Encoding transition NoIdentity_4_1_1 (120/690).
Encoding transition NoIdentity_3_1_1 (121/690).
Encoding transition NoIdentity_2_1_1 (122/690).
Encoding transition NoIdentity_0_1_1 (123/690).
Encoding transition NoIdentity_4_2_1 (124/690).
Encoding transition NoIdentity_3_2_1 (125/690).
Encoding transition NoIdentity_1_2_1 (126/690).
Encoding transition NoIdentity_0_2_1 (127/690).
Encoding transition ProgressTurn_0_1 (128/690).
Encoding transition ProgressTurn_4_0 (129/690).
Encoding transition ProgressTurn_2_1 (130/690).
Encoding transition ProgressTurn_1_1 (131/690).
Encoding transition ProgressTurn_4_1 (132/690).
Encoding transition ProgressTurn_3_1 (133/690).
Encoding transition ProgressTurn_1_2 (134/690).
Encoding transition ProgressTurn_0_2 (135/690).
Encoding transition ProgressTurn_3_2 (136/690).
Encoding transition ProgressTurn_2_2 (137/690).
Encoding transition AccessCS_0 (138/690).
Encoding transition ProgressTurn_4_2 (139/690).
Encoding transition AccessCS_2 (140/690).
Encoding transition AccessCS_1 (141/690).
Encoding transition AccessCS_4 (142/690).
Encoding transition AccessCS_3 (143/690).
Encoding transition BecomeIdle_0 (144/690).
Encoding transition BecomeIdle_1 (145/690).
Encoding transition BecomeIdle_2 (146/690).
Encoding transition BecomeIdle_3 (147/690).
Encoding transition BecomeIdle_4 (148/690).
Encoding transition Loop_0_1_0 (149/690).
Encoding transition Loop_1_1_0 (150/690).
Encoding transition Loop_2_1_0 (151/690).
Encoding transition Loop_3_1_0 (152/690).
Encoding transition Loop_1_0_0 (153/690).
Encoding transition Loop_2_0_0 (154/690).
Encoding transition Loop_3_0_0 (155/690).
Encoding transition Loop_4_0_0 (156/690).
Encoding transition EndLoop_2_3 (157/690).
Encoding transition EndLoop_3_3 (158/690).
Encoding transition EndLoop_4_3 (159/690).
Encoding transition Loop_0_0_0 (160/690).
Encoding transition EndLoop_3_2 (161/690).
Encoding transition EndLoop_4_2 (162/690).
Encoding transition EndLoop_0_3 (163/690).
Encoding transition EndLoop_1_3 (164/690).
Encoding transition EndLoop_0_2 (165/690).
Encoding transition EndLoop_4_1 (166/690).
Encoding transition EndLoop_2_2 (167/690).
Encoding transition EndLoop_1_2 (168/690).
Encoding transition EndLoop_1_1 (169/690).
Encoding transition EndLoop_0_1 (170/690).
Encoding transition EndLoop_3_1 (171/690).
Encoding transition EndLoop_2_1 (172/690).
Encoding transition EndLoop_2_0 (173/690).
Encoding transition EndLoop_1_0 (174/690).
Encoding transition EndLoop_4_0 (175/690).
Encoding transition EndLoop_3_0 (176/690).
Encoding transition EndLoop_0_0 (177/690).
Encoding transition Loop_2_1_2 (178/690).
Encoding transition Loop_3_1_2 (179/690).
Encoding transition Loop_0_1_2 (180/690).
Encoding transition Loop_1_1_2 (181/690).
Encoding transition Loop_3_0_2 (182/690).
Encoding transition Loop_4_0_2 (183/690).
Encoding transition Loop_1_0_2 (184/690).
Encoding transition Loop_2_0_2 (185/690).
Encoding transition Loop_0_3_2 (186/690).
Encoding transition Loop_1_3_2 (187/690).
Encoding transition Loop_3_2_2 (188/690).
Encoding transition Loop_4_2_2 (189/690).
Encoding transition Loop_1_2_2 (190/690).
Encoding transition Loop_2_2_2 (191/690).
Encoding transition Loop_4_1_2 (192/690).
Encoding transition Loop_0_2_2 (193/690).
Encoding transition Loop_4_0_3 (194/690).
Encoding transition Loop_3_0_3 (195/690).
Encoding transition Loop_2_0_3 (196/690).
Encoding transition Loop_1_0_3 (197/690).
Encoding transition Loop_0_0_3 (198/690).
Encoding transition Loop_4_3_2 (199/690).
Encoding transition Loop_3_3_2 (200/690).
Encoding transition Loop_2_3_2 (201/690).
Encoding transition Loop_2_2_3 (202/690).
Encoding transition Loop_1_2_3 (203/690).
Encoding transition Loop_0_2_3 (204/690).
Encoding transition Loop_4_1_3 (205/690).
Encoding transition Loop_3_1_3 (206/690).
Encoding transition Loop_2_1_3 (207/690).
Encoding transition Loop_1_1_3 (208/690).
Encoding transition Loop_0_1_3 (209/690).
Encoding transition Loop_3_2_0 (210/690).
Encoding transition Loop_4_2_0 (211/690).
Encoding transition Loop_0_3_0 (212/690).
Encoding transition Loop_1_3_0 (213/690).
Encoding transition Loop_4_1_0 (214/690).
Encoding transition Loop_0_2_0 (215/690).
Encoding transition Loop_1_2_0 (216/690).
Encoding transition Loop_2_2_0 (217/690).
Encoding transition Loop_1_0_1 (218/690).
Encoding transition Loop_2_0_1 (219/690).
Encoding transition Loop_3_0_1 (220/690).
Encoding transition Loop_4_0_1 (221/690).
Encoding transition Loop_2_3_0 (222/690).
Encoding transition Loop_3_3_0 (223/690).
Encoding transition Loop_4_3_0 (224/690).
Encoding transition Loop_0_0_1 (225/690).
Encoding transition Loop_0_2_1 (226/690).
Encoding transition Loop_4_1_1 (227/690).
Encoding transition Loop_2_2_1 (228/690).
Encoding transition Loop_1_2_1 (229/690).
Encoding transition Loop_1_1_1 (230/690).
Encoding transition Loop_0_1_1 (231/690).
Encoding transition Loop_3_1_1 (232/690).
Encoding transition Loop_2_1_1 (233/690).
Encoding transition Loop_3_3_1 (234/690).
Encoding transition Loop_2_3_1 (235/690).
Encoding transition Loop_0_0_2 (236/690).
Encoding transition Loop_4_3_1 (237/690).
Encoding transition Loop_4_2_1 (238/690).
Encoding transition Loop_3_2_1 (239/690).
Encoding transition Loop_1_3_1 (240/690).
Encoding transition Loop_0_3_1 (241/690).
Encoding transition Alone1_4_1_1 (242/690).
Encoding transition Alone1_0_2_1 (243/690).
Encoding transition Alone1_2_1_1 (244/690).
Encoding transition Alone1_3_1_1 (245/690).
Encoding transition Alone1_4_2_1 (246/690).
Encoding transition Alone1_0_3_1 (247/690).
Encoding transition Alone1_1_2_1 (248/690).
Encoding transition Alone1_3_2_1 (249/690).
Encoding transition Alone1_4_3_1 (250/690).
Encoding transition Alone1_0_4_1 (251/690).
Encoding transition Alone1_1_3_1 (252/690).
Encoding transition Alone1_2_3_1 (253/690).
Encoding transition Alone1_3_4_1 (254/690).
Encoding transition Alone1_1_0_2 (255/690).
Encoding transition Alone1_1_4_1 (256/690).
Encoding transition Alone1_2_4_1 (257/690).
Encoding transition Alone1_0_1_2 (258/690).
Encoding transition Alone1_4_0_2 (259/690).
Encoding transition Alone1_3_0_2 (260/690).
Encoding transition Alone1_2_0_2 (261/690).
Encoding transition Alone1_0_2_2 (262/690).
Encoding transition Alone1_4_1_2 (263/690).
Encoding transition Alone1_3_1_2 (264/690).
Encoding transition Alone1_2_1_2 (265/690).
Encoding transition Alone1_0_3_2 (266/690).
Encoding transition Alone1_4_2_2 (267/690).
Encoding transition Alone1_3_2_2 (268/690).
Encoding transition Alone1_1_2_2 (269/690).
Encoding transition Alone1_0_4_2 (270/690).
Encoding transition Alone1_4_3_2 (271/690).
Encoding transition Alone1_2_3_2 (272/690).
Encoding transition Alone1_1_3_2 (273/690).
Encoding transition Loop_3_2_3 (274/690).
Encoding transition Loop_4_2_3 (275/690).
Encoding transition Loop_0_3_3 (276/690).
Encoding transition Loop_1_3_3 (277/690).
Encoding transition Loop_2_3_3 (278/690).
Encoding transition Loop_3_3_3 (279/690).
Encoding transition Loop_4_3_3 (280/690).
Encoding transition Alone1_1_0_0 (281/690).
Encoding transition Alone1_2_0_0 (282/690).
Encoding transition Alone1_3_0_0 (283/690).
Encoding transition Alone1_4_0_0 (284/690).
Encoding transition Alone1_0_1_0 (285/690).
Encoding transition Alone1_2_1_0 (286/690).
Encoding transition Alone1_3_1_0 (287/690).
Encoding transition Alone1_4_1_0 (288/690).
Encoding transition Alone1_0_2_0 (289/690).
Encoding transition Alone1_3_2_0 (290/690).
Encoding transition Alone1_1_2_0 (291/690).
Encoding transition Alone1_0_3_0 (292/690).
Encoding transition Alone1_4_2_0 (293/690).
Encoding transition Alone1_2_3_0 (294/690).
Encoding transition Alone1_1_3_0 (295/690).
Encoding transition Alone1_0_4_0 (296/690).
Encoding transition Alone1_4_3_0 (297/690).
Encoding transition Alone1_2_4_0 (298/690).
Encoding transition Alone1_1_4_0 (299/690).
Encoding transition Alone1_1_0_1 (300/690).
Encoding transition Alone1_3_4_0 (301/690).
Encoding transition Alone1_3_0_1 (302/690).
Encoding transition Alone1_2_0_1 (303/690).
Encoding transition Alone1_0_1_1 (304/690).
Encoding transition Alone1_4_0_1 (305/690).
Encoding transition NotAlone_0_1_1 (306/690).
Encoding transition NotAlone_4_0_1 (307/690).
Encoding transition NotAlone_3_0_1 (308/690).
Encoding transition NotAlone_2_0_1 (309/690).
Encoding transition NotAlone_1_0_1 (310/690).
Encoding transition NotAlone_3_4_0 (311/690).
Encoding transition NotAlone_2_4_0 (312/690).
Encoding transition NotAlone_1_4_0 (313/690).
Encoding transition NotAlone_0_4_0 (314/690).
Encoding transition NotAlone_4_3_0 (315/690).
Encoding transition NotAlone_2_3_0 (316/690).
Encoding transition NotAlone_1_3_0 (317/690).
Encoding transition NotAlone_0_3_0 (318/690).
Encoding transition NotAlone_4_2_0 (319/690).
Encoding transition NotAlone_3_2_0 (320/690).
Encoding transition NotAlone_1_2_0 (321/690).
Encoding transition NotAlone_3_4_1 (322/690).
Encoding transition NotAlone_1_0_2 (323/690).
Encoding transition NotAlone_1_4_1 (324/690).
Encoding transition NotAlone_2_4_1 (325/690).
Encoding transition NotAlone_4_3_1 (326/690).
Encoding transition NotAlone_0_4_1 (327/690).
Encoding transition NotAlone_1_3_1 (328/690).
Encoding transition NotAlone_2_3_1 (329/690).
Encoding transition NotAlone_4_2_1 (330/690).
Encoding transition NotAlone_0_3_1 (331/690).
Encoding transition NotAlone_1_2_1 (332/690).
Encoding transition NotAlone_3_2_1 (333/690).
Encoding transition NotAlone_4_1_1 (334/690).
Encoding transition NotAlone_0_2_1 (335/690).
Encoding transition NotAlone_2_1_1 (336/690).
Encoding transition NotAlone_3_1_1 (337/690).
Encoding transition Alone1_3_2_3 (338/690).
Encoding transition Alone1_1_2_3 (339/690).
Encoding transition Alone1_0_3_3 (340/690).
Encoding transition Alone1_4_2_3 (341/690).
Encoding transition Alone1_3_1_3 (342/690).
Encoding transition Alone1_2_1_3 (343/690).
Encoding transition Alone1_0_2_3 (344/690).
Encoding transition Alone1_4_1_3 (345/690).
Encoding transition Alone1_3_0_3 (346/690).
Encoding transition Alone1_2_0_3 (347/690).
Encoding transition Alone1_0_1_3 (348/690).
Encoding transition Alone1_4_0_3 (349/690).
Encoding transition Alone1_2_4_2 (350/690).
Encoding transition Alone1_1_4_2 (351/690).
Encoding transition Alone1_1_0_3 (352/690).
Encoding transition Alone1_3_4_2 (353/690).
Encoding transition NotAlone_2_1_0 (354/690).
Encoding transition NotAlone_3_1_0 (355/690).
Encoding transition NotAlone_4_1_0 (356/690).
Encoding transition NotAlone_0_2_0 (357/690).
Encoding transition NotAlone_2_0_0 (358/690).
Encoding transition NotAlone_3_0_0 (359/690).
Encoding transition NotAlone_4_0_0 (360/690).
Encoding transition NotAlone_0_1_0 (361/690).
Encoding transition Alone1_1_4_3 (362/690).
Encoding transition Alone1_2_4_3 (363/690).
Encoding transition Alone1_3_4_3 (364/690).
Encoding transition NotAlone_1_0_0 (365/690).
Encoding transition Alone1_1_3_3 (366/690).
Encoding transition Alone1_2_3_3 (367/690).
Encoding transition Alone1_4_3_3 (368/690).
Encoding transition Alone1_0_4_3 (369/690).
Encoding transition ContinueLoop_4_0_0 (370/690).
Encoding transition ContinueLoop_3_0_0 (371/690).
Encoding transition ContinueLoop_2_0_0 (372/690).
Encoding transition ContinueLoop_1_0_0 (373/690).
Encoding transition ContinueLoop_3_1_0 (374/690).
Encoding transition ContinueLoop_2_1_0 (375/690).
Encoding transition ContinueLoop_1_1_0 (376/690).
Encoding transition ContinueLoop_0_1_0 (377/690).
Encoding transition NotAlone_0_4_3 (378/690).
Encoding transition NotAlone_4_3_3 (379/690).
Encoding transition NotAlone_2_3_3 (380/690).
Encoding transition NotAlone_1_3_3 (381/690).
Encoding transition ContinueLoop_0_0_0 (382/690).
Encoding transition NotAlone_3_4_3 (383/690).
Encoding transition NotAlone_2_4_3 (384/690).
Encoding transition NotAlone_1_4_3 (385/690).
Encoding transition ContinueLoop_4_3_0 (386/690).
Encoding transition ContinueLoop_0_4_0 (387/690).
Encoding transition ContinueLoop_2_3_0 (388/690).
Encoding transition ContinueLoop_3_3_0 (389/690).
Encoding transition ContinueLoop_3_4_0 (390/690).
Encoding transition ContinueLoop_4_4_0 (391/690).
Encoding transition ContinueLoop_1_4_0 (392/690).
Encoding transition ContinueLoop_2_4_0 (393/690).
Encoding transition ContinueLoop_1_2_0 (394/690).
Encoding transition ContinueLoop_2_2_0 (395/690).
Encoding transition ContinueLoop_4_1_0 (396/690).
Encoding transition ContinueLoop_0_2_0 (397/690).
Encoding transition ContinueLoop_0_3_0 (398/690).
Encoding transition ContinueLoop_1_3_0 (399/690).
Encoding transition ContinueLoop_3_2_0 (400/690).
Encoding transition ContinueLoop_4_2_0 (401/690).
Encoding transition NotAlone_3_2_2 (402/690).
Encoding transition NotAlone_1_2_2 (403/690).
Encoding transition NotAlone_0_3_2 (404/690).
Encoding transition NotAlone_4_2_2 (405/690).
Encoding transition NotAlone_2_3_2 (406/690).
Encoding transition NotAlone_1_3_2 (407/690).
Encoding transition NotAlone_0_4_2 (408/690).
Encoding transition NotAlone_4_3_2 (409/690).
Encoding transition NotAlone_3_0_2 (410/690).
Encoding transition NotAlone_2_0_2 (411/690).
Encoding transition NotAlone_0_1_2 (412/690).
Encoding transition NotAlone_4_0_2 (413/690).
Encoding transition NotAlone_3_1_2 (414/690).
Encoding transition NotAlone_2_1_2 (415/690).
Encoding transition NotAlone_0_2_2 (416/690).
Encoding transition NotAlone_4_1_2 (417/690).
Encoding transition NotAlone_2_1_3 (418/690).
Encoding transition NotAlone_3_1_3 (419/690).
Encoding transition NotAlone_4_1_3 (420/690).
Encoding transition NotAlone_0_2_3 (421/690).
Encoding transition NotAlone_1_2_3 (422/690).
Encoding transition NotAlone_3_2_3 (423/690).
Encoding transition NotAlone_4_2_3 (424/690).
Encoding transition NotAlone_0_3_3 (425/690).
Encoding transition NotAlone_1_4_2 (426/690).
Encoding transition NotAlone_2_4_2 (427/690).
Encoding transition NotAlone_3_4_2 (428/690).
Encoding transition NotAlone_1_0_3 (429/690).
Encoding transition NotAlone_2_0_3 (430/690).
Encoding transition NotAlone_3_0_3 (431/690).
Encoding transition NotAlone_4_0_3 (432/690).
Encoding transition NotAlone_0_1_3 (433/690).
Encoding transition ContinueLoop_3_0_3 (434/690).
Encoding transition ContinueLoop_2_0_3 (435/690).
Encoding transition ContinueLoop_0_1_3 (436/690).
Encoding transition ContinueLoop_4_0_3 (437/690).
Encoding transition ContinueLoop_4_4_2 (438/690).
Encoding transition ContinueLoop_3_4_2 (439/690).
Encoding transition ContinueLoop_1_0_3 (440/690).
Encoding transition ContinueLoop_0_0_3 (441/690).
Encoding transition ContinueLoop_1_2_3 (442/690).
Encoding transition ContinueLoop_0_2_3 (443/690).
Encoding transition ContinueLoop_3_2_3 (444/690).
Encoding transition ContinueLoop_2_2_3 (445/690).
Encoding transition ContinueLoop_2_1_3 (446/690).
Encoding transition ContinueLoop_1_1_3 (447/690).
Encoding transition ContinueLoop_4_1_3 (448/690).
Encoding transition ContinueLoop_3_1_3 (449/690).
Encoding transition ContinueLoop_1_2_2 (450/690).
Encoding transition ContinueLoop_2_2_2 (451/690).
Encoding transition ContinueLoop_3_2_2 (452/690).
Encoding transition ContinueLoop_4_2_2 (453/690).
Encoding transition ContinueLoop_2_1_2 (454/690).
Encoding transition ContinueLoop_3_1_2 (455/690).
Encoding transition ContinueLoop_4_1_2 (456/690).
Encoding transition ContinueLoop_0_2_2 (457/690).
Encoding transition ContinueLoop_4_3_2 (458/690).
Encoding transition ContinueLoop_0_4_2 (459/690).
Encoding transition ContinueLoop_1_4_2 (460/690).
Encoding transition ContinueLoop_2_4_2 (461/690).
Encoding transition ContinueLoop_0_3_2 (462/690).
Encoding transition ContinueLoop_1_3_2 (463/690).
Encoding transition ContinueLoop_2_3_2 (464/690).
Encoding transition ContinueLoop_3_3_2 (465/690).
Encoding transition ContinueLoop_3_4_1 (466/690).
Encoding transition ContinueLoop_2_4_1 (467/690).
Encoding transition ContinueLoop_1_4_1 (468/690).
Encoding transition ContinueLoop_0_4_1 (469/690).
Encoding transition ContinueLoop_4_3_1 (470/690).
Encoding transition ContinueLoop_3_3_1 (471/690).
Encoding transition ContinueLoop_2_3_1 (472/690).
Encoding transition ContinueLoop_1_3_1 (473/690).
Encoding transition ContinueLoop_1_1_2 (474/690).
Encoding transition ContinueLoop_0_1_2 (475/690).
Encoding transition ContinueLoop_4_0_2 (476/690).
Encoding transition ContinueLoop_3_0_2 (477/690).
Encoding transition ContinueLoop_2_0_2 (478/690).
Encoding transition ContinueLoop_1_0_2 (479/690).
Encoding transition ContinueLoop_0_0_2 (480/690).
Encoding transition ContinueLoop_4_4_1 (481/690).
Encoding transition ContinueLoop_1_1_1 (482/690).
Encoding transition ContinueLoop_2_1_1 (483/690).
Encoding transition ContinueLoop_4_0_1 (484/690).
Encoding transition ContinueLoop_0_1_1 (485/690).
Encoding transition ContinueLoop_2_0_1 (486/690).
Encoding transition ContinueLoop_3_0_1 (487/690).
Encoding transition ContinueLoop_0_0_1 (488/690).
Encoding transition ContinueLoop_1_0_1 (489/690).
Encoding transition ContinueLoop_4_2_1 (490/690).
Encoding transition ContinueLoop_0_3_1 (491/690).
Encoding transition ContinueLoop_2_2_1 (492/690).
Encoding transition ContinueLoop_3_2_1 (493/690).
Encoding transition ContinueLoop_0_2_1 (494/690).
Encoding transition ContinueLoop_1_2_1 (495/690).
Encoding transition ContinueLoop_3_1_1 (496/690).
Encoding transition ContinueLoop_4_1_1 (497/690).
Encoding transition TurnDiff_2_4_1 (498/690).
Encoding transition TurnDiff_1_4_1 (499/690).
Encoding transition TurnDiff_1_0_2 (500/690).
Encoding transition TurnDiff_3_4_1 (501/690).
Encoding transition TurnDiff_3_0_2 (502/690).
Encoding transition TurnDiff_2_0_2 (503/690).
Encoding transition TurnDiff_0_1_2 (504/690).
Encoding transition TurnDiff_4_0_2 (505/690).
Encoding transition TurnDiff_3_1_2 (506/690).
Encoding transition TurnDiff_2_1_2 (507/690).
Encoding transition TurnDiff_0_2_2 (508/690).
Encoding transition TurnDiff_4_1_2 (509/690).
Encoding transition TurnDiff_3_2_2 (510/690).
Encoding transition TurnDiff_1_2_2 (511/690).
Encoding transition TurnDiff_0_3_2 (512/690).
Encoding transition TurnDiff_4_2_2 (513/690).
Encoding transition TurnDiff_2_0_1 (514/690).
Encoding transition TurnDiff_3_0_1 (515/690).
Encoding transition TurnDiff_4_0_1 (516/690).
Encoding transition TurnDiff_0_1_1 (517/690).
Encoding transition TurnDiff_2_1_1 (518/690).
Encoding transition TurnDiff_3_1_1 (519/690).
Encoding transition TurnDiff_4_1_1 (520/690).
Encoding transition TurnDiff_0_2_1 (521/690).
Encoding transition TurnDiff_1_2_1 (522/690).
Encoding transition TurnDiff_3_2_1 (523/690).
Encoding transition TurnDiff_4_2_1 (524/690).
Encoding transition TurnDiff_0_3_1 (525/690).
Encoding transition TurnDiff_1_3_1 (526/690).
Encoding transition TurnDiff_2_3_1 (527/690).
Encoding transition TurnDiff_4_3_1 (528/690).
Encoding transition TurnDiff_0_4_1 (529/690).
Encoding transition TurnDiff_0_2_0 (530/690).
Encoding transition TurnDiff_4_1_0 (531/690).
Encoding transition TurnDiff_3_1_0 (532/690).
Encoding transition TurnDiff_2_1_0 (533/690).
Encoding transition TurnDiff_0_3_0 (534/690).
Encoding transition TurnDiff_4_2_0 (535/690).
Encoding transition TurnDiff_3_2_0 (536/690).
Encoding transition TurnDiff_1_2_0 (537/690).
Encoding transition TurnDiff_0_4_0 (538/690).
Encoding transition TurnDiff_4_3_0 (539/690).
Encoding transition TurnDiff_2_3_0 (540/690).
Encoding transition TurnDiff_1_3_0 (541/690).
Encoding transition TurnDiff_1_0_1 (542/690).
Encoding transition TurnDiff_3_4_0 (543/690).
Encoding transition TurnDiff_2_4_0 (544/690).
Encoding transition TurnDiff_1_4_0 (545/690).
Encoding transition ContinueLoop_1_3_3 (546/690).
Encoding transition ContinueLoop_2_3_3 (547/690).
Encoding transition ContinueLoop_4_2_3 (548/690).
Encoding transition ContinueLoop_0_3_3 (549/690).
Encoding transition ContinueLoop_0_4_3 (550/690).
Encoding transition ContinueLoop_1_4_3 (551/690).
Encoding transition ContinueLoop_3_3_3 (552/690).
Encoding transition ContinueLoop_4_3_3 (553/690).
Encoding transition ContinueLoop_4_4_3 (554/690).
Encoding transition TurnDiff_1_0_0 (555/690).
Encoding transition ContinueLoop_2_4_3 (556/690).
Encoding transition ContinueLoop_3_4_3 (557/690).
Encoding transition TurnDiff_4_0_0 (558/690).
Encoding transition TurnDiff_0_1_0 (559/690).
Encoding transition TurnDiff_2_0_0 (560/690).
Encoding transition TurnDiff_3_0_0 (561/690).
Encoding transition UpdateTurn_3_1_0 (562/690).
Encoding transition UpdateTurn_4_1_0 (563/690).
Encoding transition UpdateTurn_0_2_0 (564/690).
Encoding transition UpdateTurn_1_2_0 (565/690).
Encoding transition UpdateTurn_4_0_0 (566/690).
Encoding transition UpdateTurn_0_1_0 (567/690).
Encoding transition UpdateTurn_1_1_0 (568/690).
Encoding transition UpdateTurn_2_1_0 (569/690).
Encoding transition UpdateTurn_0_0_0 (570/690).
Encoding transition UpdateTurn_1_0_0 (571/690).
Encoding transition UpdateTurn_2_0_0 (572/690).
Encoding transition UpdateTurn_3_0_0 (573/690).
Encoding transition Ask_1 (574/690).
Encoding transition Ask_2 (575/690).
Encoding transition Ask_3 (576/690).
Encoding transition Ask_4 (577/690).
Encoding transition TurnEqual_3_3 (578/690).
Encoding transition TurnEqual_2_3 (579/690).
Encoding transition Ask_0 (580/690).
Encoding transition TurnEqual_4_3 (581/690).
Encoding transition TurnEqual_4_2 (582/690).
Encoding transition TurnEqual_3_2 (583/690).
Encoding transition TurnEqual_1_3 (584/690).
Encoding transition TurnEqual_0_3 (585/690).
Encoding transition TurnEqual_0_2 (586/690).
Encoding transition TurnEqual_4_1 (587/690).
Encoding transition TurnEqual_2_2 (588/690).
Encoding transition TurnEqual_1_2 (589/690).
Encoding transition TurnEqual_1_1 (590/690).
Encoding transition TurnEqual_0_1 (591/690).
Encoding transition TurnEqual_3_1 (592/690).
Encoding transition TurnEqual_2_1 (593/690).
Encoding transition TurnEqual_3_0 (594/690).
Encoding transition TurnEqual_4_0 (595/690).
Encoding transition TurnEqual_1_0 (596/690).
Encoding transition TurnEqual_2_0 (597/690).
Encoding transition TurnDiff_3_4_3 (598/690).
Encoding transition TurnEqual_0_0 (599/690).
Encoding transition TurnDiff_1_4_3 (600/690).
Encoding transition TurnDiff_2_4_3 (601/690).
Encoding transition TurnDiff_4_3_3 (602/690).
Encoding transition TurnDiff_0_4_3 (603/690).
Encoding transition TurnDiff_1_3_3 (604/690).
Encoding transition TurnDiff_2_3_3 (605/690).
Encoding transition TurnDiff_4_2_3 (606/690).
Encoding transition TurnDiff_0_3_3 (607/690).
Encoding transition TurnDiff_1_2_3 (608/690).
Encoding transition TurnDiff_3_2_3 (609/690).
Encoding transition TurnDiff_0_2_3 (610/690).
Encoding transition TurnDiff_4_1_3 (611/690).
Encoding transition TurnDiff_3_1_3 (612/690).
Encoding transition TurnDiff_2_1_3 (613/690).
Encoding transition TurnDiff_0_1_3 (614/690).
Encoding transition TurnDiff_4_0_3 (615/690).
Encoding transition TurnDiff_3_0_3 (616/690).
Encoding transition TurnDiff_2_0_3 (617/690).
Encoding transition TurnDiff_1_0_3 (618/690).
Encoding transition TurnDiff_3_4_2 (619/690).
Encoding transition TurnDiff_2_4_2 (620/690).
Encoding transition TurnDiff_1_4_2 (621/690).
Encoding transition TurnDiff_0_4_2 (622/690).
Encoding transition TurnDiff_4_3_2 (623/690).
Encoding transition TurnDiff_2_3_2 (624/690).
Encoding transition TurnDiff_1_3_2 (625/690).
Encoding transition UpdateTurn_3_3_2 (626/690).
Encoding transition UpdateTurn_4_3_2 (627/690).
Encoding transition UpdateTurn_0_4_2 (628/690).
Encoding transition UpdateTurn_1_4_2 (629/690).
Encoding transition UpdateTurn_2_4_2 (630/690).
Encoding transition UpdateTurn_3_4_2 (631/690).
Encoding transition UpdateTurn_4_4_2 (632/690).
Encoding transition UpdateTurn_0_0_3 (633/690).
Encoding transition UpdateTurn_0_2_2 (634/690).
Encoding transition UpdateTurn_1_2_2 (635/690).
Encoding transition UpdateTurn_2_2_2 (636/690).
Encoding transition UpdateTurn_3_2_2 (637/690).
Encoding transition UpdateTurn_4_2_2 (638/690).
Encoding transition UpdateTurn_0_3_2 (639/690).
Encoding transition UpdateTurn_1_3_2 (640/690).
Encoding transition UpdateTurn_2_3_2 (641/690).
Encoding transition UpdateTurn_3_0_2 (642/690).
Encoding transition UpdateTurn_2_0_2 (643/690).
Encoding transition UpdateTurn_0_1_2 (644/690).
Encoding transition UpdateTurn_4_0_2 (645/690).
Encoding transition UpdateTurn_2_1_2 (646/690).
Encoding transition UpdateTurn_1_1_2 (647/690).
Encoding transition UpdateTurn_4_1_2 (648/690).
Encoding transition UpdateTurn_3_1_2 (649/690).
Encoding transition UpdateTurn_0_4_1 (650/690).
Encoding transition UpdateTurn_4_3_1 (651/690).
Encoding transition UpdateTurn_2_4_1 (652/690).
Encoding transition UpdateTurn_1_4_1 (653/690).
Encoding transition UpdateTurn_4_4_1 (654/690).
Encoding transition UpdateTurn_3_4_1 (655/690).
Encoding transition UpdateTurn_1_0_2 (656/690).
Encoding transition UpdateTurn_0_0_2 (657/690).
Encoding transition UpdateTurn_3_2_1 (658/690).
Encoding transition UpdateTurn_4_2_1 (659/690).
Encoding transition UpdateTurn_1_2_1 (660/690).
Encoding transition UpdateTurn_2_2_1 (661/690).
Encoding transition UpdateTurn_2_3_1 (662/690).
Encoding transition UpdateTurn_3_3_1 (663/690).
Encoding transition UpdateTurn_0_3_1 (664/690).
Encoding transition UpdateTurn_1_3_1 (665/690).
Encoding transition UpdateTurn_0_1_1 (666/690).
Encoding transition UpdateTurn_1_1_1 (667/690).
Encoding transition UpdateTurn_3_0_1 (668/690).
Encoding transition UpdateTurn_4_0_1 (669/690).
Encoding transition UpdateTurn_4_1_1 (670/690).
Encoding transition UpdateTurn_0_2_1 (671/690).
Encoding transition UpdateTurn_2_1_1 (672/690).
Encoding transition UpdateTurn_3_1_1 (673/690).
Encoding transition UpdateTurn_3_4_0 (674/690).
Encoding transition UpdateTurn_2_4_0 (675/690).
Encoding transition UpdateTurn_1_4_0 (676/690).
Encoding transition UpdateTurn_0_4_0 (677/690).
Encoding transition UpdateTurn_2_0_1 (678/690).
Encoding transition UpdateTurn_1_0_1 (679/690).
Encoding transition UpdateTurn_0_0_1 (680/690).
Encoding transition UpdateTurn_4_4_0 (681/690).
Encoding transition UpdateTurn_0_3_0 (682/690).
Encoding transition UpdateTurn_4_2_0 (683/690).
Encoding transition UpdateTurn_3_2_0 (684/690).
Encoding transition UpdateTurn_2_2_0 (685/690).
Encoding transition UpdateTurn_4_3_0 (686/690).
Encoding transition UpdateTurn_3_3_0 (687/690).
Encoding transition UpdateTurn_2_3_0 (688/690).
Encoding transition UpdateTurn_1_3_0 (689/690).
----------------------------------------
End firing rule encoding
----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------
Total Used Memory: 411768KB
CANNOT_COMPUTE
BK_STOP 1400798767411
--------------------
content from stderr:
MEDDLY Error: Insufficient memory
Sequence of Actions to be Executed by the VM
This is useful if one wants to reexecute the tool in the VM from the submitted image disk.
set -x
# this is for BenchKit: configuration of major elements for the test
export BK_INPUT="SurprisePeterson-PT-4"
export BK_EXAMINATION="ReachabilityFireability"
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/SurprisePeterson-PT-4.tgz
mv SurprisePeterson-PT-4 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 SurprisePeterson-PT-4, examination is ReachabilityFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r09ks-qhx2-140069008201099"
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 ;