fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r21sr-ovh1-140191459900367
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
4783.28 1823451 123.6 CC normal

Execution Chart

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

Trace from the execution

Waiting for the VM to be ready (probing ssh)
.......................
=====================================================================
Generated by BenchKit 2-1668
Executing tool greatspn
Input is DatabaseWithMutex-PT-10, examination is ReachabilityBounds
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r21sr-ovh1-140191459900367
=====================================================================


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

BK_START 1401924809364
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running DatabaseWithMutex (PT), instance 10
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityBounds.xml INTO /home/mcc/execution/ReachabilityBounds.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 30 -C -f /home/mcc/execution/ReachabilityBounds.rgmedd-ctl
Using FORCE Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition Update_6_3 (0/800).
Encoding transition Release_6_4 (1/800).
Encoding transition Release_4_5 (2/800).
Encoding transition SendReply_9_2 (3/800).
Encoding transition SendReply_5_10 (4/800).
Encoding transition Release_8_8 (5/800).
Encoding transition Start_3_8 (6/800).
Encoding transition SendMsg_1_10 (7/800).
Encoding transition Update_1_3 (8/800).
Encoding transition SendReply_5_1 (9/800).
Encoding transition SendMsg_4_5 (10/800).
Encoding transition Update_5_4 (11/800).
Encoding transition Update_2_2 (12/800).
Encoding transition Start_4_4 (13/800).
Encoding transition SendReply_4_3 (14/800).
Encoding transition Start_5_5 (15/800).
Encoding transition SendMsg_1_7 (16/800).
Encoding transition Release_9_6 (17/800).
Encoding transition Update_8_7 (18/800).
Encoding transition Start_7_2 (19/800).
Encoding transition SendMsg_5_1 (20/800).
Encoding transition Release_1_4 (21/800).
Encoding transition Update_9_5 (22/800).
Encoding transition SendReply_7_9 (23/800).
Encoding transition Release_7_1 (24/800).
Encoding transition Acquire_7_6 (25/800).
Encoding transition Release_10_5 (26/800).
Encoding transition Start_1_1 (27/800).
Encoding transition Release_3_8 (28/800).
Encoding transition Change_7_2 (29/800).
Encoding transition SendReply_10_8 (30/800).
Encoding transition Change_10_2 (31/800).
Encoding transition Change_3_10 (32/800).
Encoding transition Change_10_3 (33/800).
Encoding transition SendReply_3_4 (34/800).
Encoding transition Release_5_5 (35/800).
Encoding transition Change_5_7 (36/800).
Encoding transition SendMsg_3_4 (37/800).
Encoding transition Acquire_5_6 (38/800).
Encoding transition Change_6_1 (39/800).
Encoding transition Acquire_8_5 (40/800).
Encoding transition SendReply_8_4 (41/800).
Encoding transition Release_2_3 (42/800).
Encoding transition SendMsg_9_1 (43/800).
Encoding transition Change_4_5 (44/800).
Encoding transition Change_1_4 (45/800).
Encoding transition Acquire_8_10 (46/800).
Encoding transition Start_2_7 (47/800).
Encoding transition Acquire_2_7 (48/800).
Encoding transition SendMsg_7_5 (49/800).
Encoding transition Start_5_10 (50/800).
Encoding transition end_update_5_6 (51/800).
Encoding transition Update_4_6 (52/800).
Encoding transition Change_3_5 (53/800).
Encoding transition Update_3_7 (54/800).
Encoding transition SendReply_9_8 (55/800).
Encoding transition Change_9_9 (56/800).
Encoding transition end_update_10_4 (57/800).
Encoding transition Update_10_4 (58/800).
Encoding transition SendReply_7_7 (59/800).
Encoding transition SendMsg_7_8 (60/800).
Encoding transition Release_8_6 (61/800).
Encoding transition SendMsg_7_4 (62/800).
Encoding transition end_update_9_7 (63/800).
Encoding transition end_update_10_9 (64/800).
Encoding transition SendMsg_5_10 (65/800).
Encoding transition Acquire_7_2 (66/800).
Encoding transition end_update_5_9 (67/800).
Encoding transition end_update_6_8 (68/800).
Encoding transition Change_2_7 (69/800).
Encoding transition SendReply_2_6 (70/800).
Encoding transition Acquire_6_1 (71/800).
Encoding transition Update_1_10 (72/800).
Encoding transition end_update_9_10 (73/800).
Encoding transition Acquire_8_3 (74/800).
Encoding transition SendMsg_6_2 (75/800).
Encoding transition Start_6_1 (76/800).
Encoding transition Update_4_1 (77/800).
Encoding transition SendReply_6_8 (78/800).
Encoding transition end_update_2_2 (79/800).
Encoding transition end_update_1_5 (80/800).
Encoding transition SendMsg_5_6 (81/800).
Encoding transition Update_7_8 (82/800).
Encoding transition SendMsg_2_9 (83/800).
Encoding transition Start_5_6 (84/800).
Encoding transition Release_2_10 (85/800).
Encoding transition Release_2_8 (86/800).
Encoding transition SendMsg_2_7 (87/800).
Encoding transition SendMsg_8_7 (88/800).
Encoding transition Update_6_10 (89/800).
Encoding transition SendMsg_4_4 (90/800).
Encoding transition SendReply_10_10 (91/800).
Encoding transition Release_10_3 (92/800).
Encoding transition end_update_7_3 (93/800).
Encoding transition Acquire_5_5 (94/800).
Encoding transition Acquire_3_3 (95/800).
Encoding transition Change_4_4 (96/800).
Encoding transition Start_9_9 (97/800).
Encoding transition Change_1_8 (98/800).
Encoding transition SendReply_8_5 (99/800).
Encoding transition Release_4_2 (100/800).
Encoding transition Release_4_7 (101/800).
Encoding transition Acquire_5_9 (102/800).
Encoding transition Update_2_9 (103/800).
Encoding transition Acquire_1_4 (104/800).
Encoding transition Start_2_10 (105/800).
Encoding transition Update_2_4 (106/800).
Encoding transition Start_3_6 (107/800).
Encoding transition Release_9_9 (108/800).
Encoding transition Update_9_3 (109/800).
Encoding transition Change_2_2 (110/800).
Encoding transition Acquire_8_7 (111/800).
Encoding transition Change_1_7 (112/800).
Encoding transition end_update_1_7 (113/800).
Encoding transition SendMsg_8_1 (114/800).
Encoding transition Start_8_6 (115/800).
Encoding transition Update_5_2 (116/800).
Encoding transition Start_2_8 (117/800).
Encoding transition Update_7_6 (118/800).
Encoding transition Start_6_2 (119/800).
Encoding transition SendMsg_5_5 (120/800).
Encoding transition SendReply_1_5 (121/800).
Encoding transition SendMsg_7_2 (122/800).
Encoding transition Release_7_4 (123/800).
Encoding transition Change_2_6 (124/800).
Encoding transition Update_8_2 (125/800).
Encoding transition SendReply_3_2 (126/800).
Encoding transition SendMsg_6_4 (127/800).
Encoding transition end_update_4_6 (128/800).
Encoding transition Release_9_8 (129/800).
Encoding transition Release_3_3 (130/800).
Encoding transition end_update_6_3 (131/800).
Encoding transition Start_8_8 (132/800).
Encoding transition Release_1_6 (133/800).
Encoding transition Acquire_10_2 (134/800).
Encoding transition Start_9_4 (135/800).
Encoding transition SendReply_2_10 (136/800).
Encoding transition Acquire_4_4 (137/800).
Encoding transition Start_1_2 (138/800).
Encoding transition SendMsg_7_3 (139/800).
Encoding transition SendMsg_6_1 (140/800).
Encoding transition Change_3_1 (141/800).
Encoding transition Start_4_5 (142/800).
Encoding transition end_update_6_1 (143/800).
Encoding transition SendReply_10_2 (144/800).
Encoding transition Change_4_3 (145/800).
Encoding transition Acquire_3_1 (146/800).
Encoding transition end_update_8_7 (147/800).
Encoding transition Change_7_1 (148/800).
Encoding transition Acquire_9_5 (149/800).
Encoding transition SendReply_2_7 (150/800).
Encoding transition Update_1_8 (151/800).
Encoding transition end_update_3_4 (152/800).
Encoding transition Change_8_9 (153/800).
Encoding transition SendMsg_4_8 (154/800).
Encoding transition Update_6_5 (155/800).
Encoding transition Acquire_7_1 (156/800).
Encoding transition SendMsg_6_3 (157/800).
Encoding transition Start_5_3 (158/800).
Encoding transition Release_4_9 (159/800).
Encoding transition SendReply_3_3 (160/800).
Encoding transition end_update_4_4 (161/800).
Encoding transition Start_10_3 (162/800).
Encoding transition end_update_1_10 (163/800).
Encoding transition Change_3_4 (164/800).
Encoding transition Release_7_2 (165/800).
Encoding transition Acquire_6_6 (166/800).
Encoding transition Acquire_2_2 (167/800).
Encoding transition SendReply_2_1 (168/800).
Encoding transition Acquire_5_3 (169/800).
Encoding transition Release_8_4 (170/800).
Encoding transition Release_8_1 (171/800).
Encoding transition SendReply_9_6 (172/800).
Encoding transition SendReply_10_7 (173/800).
Encoding transition end_update_4_9 (174/800).
Encoding transition end_update_2_9 (175/800).
Encoding transition Change_2_1 (176/800).
Encoding transition end_update_8_10 (177/800).
Encoding transition Acquire_6_10 (178/800).
Encoding transition Change_10_7 (179/800).
Encoding transition Update_9_10 (180/800).
Encoding transition SendMsg_3_7 (181/800).
Encoding transition Release_5_8 (182/800).
Encoding transition Release_9_3 (183/800).
Encoding transition end_update_2_6 (184/800).
Encoding transition SendReply_7_8 (185/800).
Encoding transition SendReply_8_6 (186/800).
Encoding transition end_update_7_8 (187/800).
Encoding transition SendReply_7_10 (188/800).
Encoding transition SendMsg_7_7 (189/800).
Encoding transition Change_10_8 (190/800).
Encoding transition Release_7_5 (191/800).
Encoding transition end_update_3_5 (192/800).
Encoding transition SendMsg_5_4 (193/800).
Encoding transition end_update_5_1 (194/800).
Encoding transition Change_2_5 (195/800).
Encoding transition Acquire_4_9 (196/800).
Encoding transition SendReply_10_3 (197/800).
Encoding transition Release_6_2 (198/800).
Encoding transition Start_7_7 (199/800).
Encoding transition SendReply_8_9 (200/800).
Encoding transition Change_1_9 (201/800).
Encoding transition end_update_4_3 (202/800).
Encoding transition Update_3_5 (203/800).
Encoding transition Acquire_10_3 (204/800).
Encoding transition Change_2_3 (205/800).
Encoding transition Change_8_10 (206/800).
Encoding transition Acquire_5_4 (207/800).
Encoding transition Release_10_2 (208/800).
Encoding transition SendReply_10_4 (209/800).
Encoding transition SendMsg_8_3 (210/800).
Encoding transition SendReply_1_4 (211/800).
Encoding transition Change_9_10 (212/800).
Encoding transition Release_8_5 (213/800).
Encoding transition Release_9_4 (214/800).
Encoding transition Start_9_8 (215/800).
Encoding transition end_update_1_8 (216/800).
Encoding transition SendMsg_4_2 (217/800).
Encoding transition Start_4_9 (218/800).
Encoding transition end_update_5_2 (219/800).
Encoding transition SendReply_8_8 (220/800).
Encoding transition Update_8_3 (221/800).
Encoding transition Update_5_9 (222/800).
Encoding transition SendMsg_6_7 (223/800).
Encoding transition Release_7_6 (224/800).
Encoding transition SendReply_3_1 (225/800).
Encoding transition SendReply_2_2 (226/800).
Encoding transition Update_6_6 (227/800).
Encoding transition Update_3_3 (228/800).
Encoding transition SendMsg_4_6 (229/800).
Encoding transition Acquire_2_1 (230/800).
Encoding transition SendMsg_4_10 (231/800).
Encoding transition Start_8_1 (232/800).
Encoding transition Acquire_1_8 (233/800).
Encoding transition SendMsg_1_3 (234/800).
Encoding transition Change_5_3 (235/800).
Encoding transition SendReply_5_9 (236/800).
Encoding transition Acquire_10_4 (237/800).
Encoding transition Start_5_8 (238/800).
Encoding transition Release_7_10 (239/800).
Encoding transition end_update_5_3 (240/800).
Encoding transition SendMsg_5_9 (241/800).
Encoding transition SendMsg_7_1 (242/800).
Encoding transition SendMsg_4_9 (243/800).
Encoding transition Update_4_8 (244/800).
Encoding transition Start_6_4 (245/800).
Encoding transition Change_3_6 (246/800).
Encoding transition SendReply_1_6 (247/800).
Encoding transition end_update_2_7 (248/800).
Encoding transition Acquire_7_9 (249/800).
Encoding transition Release_6_8 (250/800).
Encoding transition Start_10_5 (251/800).
Encoding transition Update_1_6 (252/800).
Encoding transition Acquire_2_3 (253/800).
Encoding transition Change_8_2 (254/800).
Encoding transition Change_5_1 (255/800).
Encoding transition Start_2_3 (256/800).
Encoding transition Release_7_9 (257/800).
Encoding transition Change_2_4 (258/800).
Encoding transition end_update_5_4 (259/800).
Encoding transition Update_9_8 (260/800).
Encoding transition Start_2_1 (261/800).
Encoding transition Update_1_1 (262/800).
Encoding transition Release_4_8 (263/800).
Encoding transition end_update_7_1 (264/800).
Encoding transition Release_9_1 (265/800).
Encoding transition SendMsg_5_8 (266/800).
Encoding transition SendReply_9_7 (267/800).
Encoding transition Update_9_7 (268/800).
Encoding transition Change_5_2 (269/800).
Encoding transition Update_7_10 (270/800).
Encoding transition end_update_4_2 (271/800).
Encoding transition Change_10_6 (272/800).
Encoding transition Change_3_2 (273/800).
Encoding transition Acquire_9_6 (274/800).
Encoding transition SendReply_2_3 (275/800).
Encoding transition SendReply_10_6 (276/800).
Encoding transition end_update_2_10 (277/800).
Encoding transition end_update_3_6 (278/800).
Encoding transition Start_4_7 (279/800).
Encoding transition Update_4_9 (280/800).
Encoding transition end_update_2_4 (281/800).
Encoding transition Acquire_9_7 (282/800).
Encoding transition end_update_10_6 (283/800).
Encoding transition Acquire_4_1 (284/800).
Encoding transition Release_6_5 (285/800).
Encoding transition end_update_10_7 (286/800).
Encoding transition Start_1_7 (287/800).
Encoding transition Change_1_10 (288/800).
Encoding transition Acquire_10_5 (289/800).
Encoding transition Acquire_7_8 (290/800).
Encoding transition Start_5_1 (291/800).
Encoding transition end_update_2_5 (292/800).
Encoding transition SendMsg_9_8 (293/800).
Encoding transition Release_8_3 (294/800).
Encoding transition Release_5_1 (295/800).
Encoding transition SendMsg_2_8 (296/800).
Encoding transition Acquire_7_10 (297/800).
Encoding transition Release_6_6 (298/800).
Encoding transition Release_9_5 (299/800).
Encoding transition Start_4_10 (300/800).
Encoding transition Change_10_4 (301/800).
Encoding transition Release_6_7 (302/800).
Encoding transition Release_9_2 (303/800).
Encoding transition Start_10_1 (304/800).
Encoding transition SendMsg_3_10 (305/800).
Encoding transition Start_6_8 (306/800).
Encoding transition Change_6_10 (307/800).
Encoding transition Acquire_6_9 (308/800).
Encoding transition end_update_7_2 (309/800).
Encoding transition SendMsg_5_7 (310/800).
Encoding transition Release_10_1 (311/800).
Encoding transition SendReply_4_7 (312/800).
Encoding transition SendReply_10_5 (313/800).
Encoding transition SendReply_7_6 (314/800).
Encoding transition SendReply_1_8 (315/800).
Encoding transition Start_1_6 (316/800).
Encoding transition end_update_3_7 (317/800).
Encoding transition Update_10_2 (318/800).
Encoding transition Change_3_7 (319/800).
Encoding transition Acquire_9_8 (320/800).
Encoding transition end_update_6_4 (321/800).
Encoding transition end_update_2_3 (322/800).
Encoding transition Start_7_9 (323/800).
Encoding transition SendMsg_5_2 (324/800).
Encoding transition Acquire_5_2 (325/800).
Encoding transition Acquire_3_5 (326/800).
Encoding transition Release_1_3 (327/800).
Encoding transition end_update_10_10 (328/800).
Encoding transition Start_7_10 (329/800).
Encoding transition Release_4_10 (330/800).
Encoding transition Start_3_4 (331/800).
Encoding transition Change_7_8 (332/800).
Encoding transition Update_8_5 (333/800).
Encoding transition Change_2_9 (334/800).
Encoding transition SendMsg_9_3 (335/800).
Encoding transition SendReply_4_10 (336/800).
Encoding transition SendReply_6_9 (337/800).
Encoding transition Update_3_2 (338/800).
Encoding transition Start_8_3 (339/800).
Encoding transition Acquire_3_4 (340/800).
Encoding transition Update_1_4 (341/800).
Encoding transition Update_4_10 (342/800).
Encoding transition Acquire_8_6 (343/800).
Encoding transition SendReply_7_1 (344/800).
Encoding transition end_update_3_10 (345/800).
Encoding transition SendReply_2_5 (346/800).
Encoding transition SendReply_5_4 (347/800).
Encoding transition SendReply_4_2 (348/800).
Encoding transition end_update_9_6 (349/800).
Encoding transition Update_6_7 (350/800).
Encoding transition SendReply_1_3 (351/800).
Encoding transition Acquire_6_7 (352/800).
Encoding transition Start_8_4 (353/800).
Encoding transition SendMsg_10_10 (354/800).
Encoding transition Change_6_3 (355/800).
Encoding transition Change_5_4 (356/800).
Encoding transition Change_1_3 (357/800).
Encoding transition Acquire_1_6 (358/800).
Encoding transition Change_4_1 (359/800).
Encoding transition Update_1_5 (360/800).
Encoding transition SendMsg_3_8 (361/800).
Encoding transition Change_8_4 (362/800).
Encoding transition Update_10_1 (363/800).
Encoding transition end_update_4_7 (364/800).
Encoding transition Start_3_3 (365/800).
Encoding transition end_update_5_5 (366/800).
Encoding transition Update_7_9 (367/800).
Encoding transition Acquire_5_1 (368/800).
Encoding transition Change_4_6 (369/800).
Encoding transition Change_9_5 (370/800).
Encoding transition Update_9_6 (371/800).
Encoding transition Release_4_6 (372/800).
Encoding transition SendMsg_2_5 (373/800).
Encoding transition Release_7_8 (374/800).
Encoding transition end_update_8_1 (375/800).
Encoding transition SendMsg_6_6 (376/800).
Encoding transition end_update_10_5 (377/800).
Encoding transition SendMsg_3_5 (378/800).
Encoding transition SendMsg_6_9 (379/800).
Encoding transition end_update_3_1 (380/800).
Encoding transition Release_2_9 (381/800).
Encoding transition Start_6_6 (382/800).
Encoding transition Release_8_7 (383/800).
Encoding transition SendMsg_7_6 (384/800).
Encoding transition Change_8_7 (385/800).
Encoding transition Release_1_2 (386/800).
Encoding transition Change_7_10 (387/800).
Encoding transition Change_10_1 (388/800).
Encoding transition Acquire_5_10 (389/800).
Encoding transition Update_8_4 (390/800).
Encoding transition SendReply_2_8 (391/800).
Encoding transition SendMsg_2_1 (392/800).
Encoding transition Change_7_3 (393/800).
Encoding transition Update_6_8 (394/800).
Encoding transition Change_10_9 (395/800).
Encoding transition SendReply_9_10 (396/800).
Encoding transition end_update_10_8 (397/800).
Encoding transition Update_3_6 (398/800).
Encoding transition Acquire_1_5 (399/800).
Encoding transition Acquire_7_3 (400/800).
Encoding transition Update_10_10 (401/800).
Encoding transition Acquire_4_10 (402/800).
Encoding transition Acquire_6_5 (403/800).
Encoding transition end_update_1_4 (404/800).
Encoding transition SendReply_5_2 (405/800).
Encoding transition Change_6_8 (406/800).
Encoding transition Start_6_10 (407/800).
Encoding transition Acquire_8_2 (408/800).
Encoding transition SendMsg_8_6 (409/800).
Encoding transition Release_8_2 (410/800).
Encoding transition end_update_3_8 (411/800).
Encoding transition end_update_4_10 (412/800).
Encoding transition Release_4_1 (413/800).
Encoding transition Acquire_2_4 (414/800).
Encoding transition SendReply_4_5 (415/800).
Encoding transition Update_4_5 (416/800).
Encoding transition Acquire_6_8 (417/800).
Encoding transition Start_3_2 (418/800).
Encoding transition Change_9_7 (419/800).
Encoding transition SendReply_8_3 (420/800).
Encoding transition Update_3_1 (421/800).
Encoding transition SendReply_6_1 (422/800).
Encoding transition end_update_6_2 (423/800).
Encoding transition Update_5_10 (424/800).
Encoding transition end_update_9_1 (425/800).
Encoding transition SendReply_3_7 (426/800).
Encoding transition Change_5_6 (427/800).
Encoding transition SendMsg_4_7 (428/800).
Encoding transition Change_3_9 (429/800).
Encoding transition SendReply_9_5 (430/800).
Encoding transition Start_9_6 (431/800).
Encoding transition Acquire_3_2 (432/800).
Encoding transition SendMsg_2_10 (433/800).
Encoding transition end_update_9_9 (434/800).
Encoding transition SendMsg_8_8 (435/800).
Encoding transition Update_1_9 (436/800).
Encoding transition SendReply_4_9 (437/800).
Encoding transition Update_6_2 (438/800).
Encoding transition Change_1_5 (439/800).
Encoding transition end_update_8_6 (440/800).
Encoding transition end_update_4_5 (441/800).
Encoding transition end_update_2_1 (442/800).
Encoding transition Start_6_7 (443/800).
Encoding transition Release_9_10 (444/800).
Encoding transition Update_5_3 (445/800).
Encoding transition end_update_1_6 (446/800).
Encoding transition SendMsg_1_6 (447/800).
Encoding transition SendMsg_1_1 (448/800).
Encoding transition Release_3_9 (449/800).
Encoding transition SendMsg_1_5 (450/800).
Encoding transition Acquire_2_8 (451/800).
Encoding transition end_update_3_9 (452/800).
Encoding transition Change_8_5 (453/800).
Encoding transition Start_9_7 (454/800).
Encoding transition Release_9_7 (455/800).
Encoding transition Change_4_10 (456/800).
Encoding transition Start_1_4 (457/800).
Encoding transition SendMsg_10_3 (458/800).
Encoding transition Update_8_6 (459/800).
Encoding transition Update_9_4 (460/800).
Encoding transition Start_7_1 (461/800).
Encoding transition SendMsg_1_9 (462/800).
Encoding transition SendReply_3_5 (463/800).
Encoding transition Change_7_6 (464/800).
Encoding transition Release_10_4 (465/800).
Encoding transition Start_7_8 (466/800).
Encoding transition Release_5_6 (467/800).
Encoding transition SendReply_9_3 (468/800).
Encoding transition SendMsg_3_3 (469/800).
Encoding transition Update_10_3 (470/800).
Encoding transition Update_6_9 (471/800).
Encoding transition Acquire_7_7 (472/800).
Encoding transition Release_7_3 (473/800).
Encoding transition Update_2_8 (474/800).
Encoding transition SendMsg_8_5 (475/800).
Encoding transition end_update_2_8 (476/800).
Encoding transition Start_1_5 (477/800).
Encoding transition Change_6_2 (478/800).
Encoding transition Update_2_1 (479/800).
Encoding transition Start_1_10 (480/800).
Encoding transition Acquire_2_6 (481/800).
Encoding transition Update_1_2 (482/800).
Encoding transition Start_2_2 (483/800).
Encoding transition Acquire_4_3 (484/800).
Encoding transition Acquire_1_7 (485/800).
Encoding transition Start_10_2 (486/800).
Encoding transition Release_1_5 (487/800).
Encoding transition SendMsg_8_9 (488/800).
Encoding transition Start_2_9 (489/800).
Encoding transition Start_8_5 (490/800).
Encoding transition SendReply_1_1 (491/800).
Encoding transition Release_5_9 (492/800).
Encoding transition SendMsg_7_9 (493/800).
Encoding transition SendReply_1_10 (494/800).
Encoding transition SendReply_6_7 (495/800).
Encoding transition Start_5_9 (496/800).
Encoding transition SendReply_5_5 (497/800).
Encoding transition end_update_8_9 (498/800).
Encoding transition end_update_8_4 (499/800).
Encoding transition Start_1_3 (500/800).
Encoding transition end_update_3_3 (501/800).
Encoding transition Update_7_7 (502/800).
Encoding transition SendMsg_1_4 (503/800).
Encoding transition end_update_7_5 (504/800).
Encoding transition Acquire_5_8 (505/800).
Encoding transition Change_9_4 (506/800).
Encoding transition Change_7_5 (507/800).
Encoding transition end_update_5_10 (508/800).
Encoding transition Start_5_4 (509/800).
Encoding transition SendReply_6_10 (510/800).
Encoding transition Start_3_7 (511/800).
Encoding transition SendReply_5_6 (512/800).
Encoding transition Acquire_9_9 (513/800).
Encoding transition SendMsg_9_6 (514/800).
Encoding transition Release_6_10 (515/800).
Encoding transition SendMsg_3_2 (516/800).
Encoding transition end_update_9_2 (517/800).
Encoding transition end_update_6_7 (518/800).
Encoding transition Update_5_8 (519/800).
Encoding transition Acquire_2_10 (520/800).
Encoding transition end_update_7_4 (521/800).
Encoding transition SendReply_3_9 (522/800).
Encoding transition Start_3_1 (523/800).
Encoding transition Acquire_8_4 (524/800).
Encoding transition SendMsg_10_2 (525/800).
Encoding transition Update_7_5 (526/800).
Encoding transition Change_1_2 (527/800).
Encoding transition SendMsg_2_3 (528/800).
Encoding transition Change_6_7 (529/800).
Encoding transition Release_3_4 (530/800).
Encoding transition end_update_5_7 (531/800).
Encoding transition end_update_10_3 (532/800).
Encoding transition Start_6_3 (533/800).
Encoding transition SendReply_4_4 (534/800).
Encoding transition SendReply_7_3 (535/800).
Encoding transition SendReply_3_8 (536/800).
Encoding transition Acquire_10_8 (537/800).
Encoding transition Release_6_3 (538/800).
Encoding transition end_update_1_1 (539/800).
Encoding transition Acquire_8_8 (540/800).
Encoding transition Update_9_9 (541/800).
Encoding transition Update_3_4 (542/800).
Encoding transition Change_6_6 (543/800).
Encoding transition Update_10_5 (544/800).
Encoding transition Update_8_1 (545/800).
Encoding transition Update_8_8 (546/800).
Encoding transition Start_4_6 (547/800).
Encoding transition Start_8_9 (548/800).
Encoding transition Acquire_3_6 (549/800).
Encoding transition Update_2_3 (550/800).
Encoding transition Release_3_10 (551/800).
Encoding transition Start_9_10 (552/800).
Encoding transition Release_10_8 (553/800).
Encoding transition Change_9_2 (554/800).
Encoding transition Start_4_1 (555/800).
Encoding transition SendMsg_9_5 (556/800).
Encoding transition Start_4_8 (557/800).
Encoding transition Change_4_9 (558/800).
Encoding transition Start_9_5 (559/800).
Encoding transition Release_1_7 (560/800).
Encoding transition Release_4_3 (561/800).
Encoding transition Acquire_10_6 (562/800).
Encoding transition SendReply_9_1 (563/800).
Encoding transition SendReply_7_4 (564/800).
Encoding transition Release_3_1 (565/800).
Encoding transition Start_2_4 (566/800).
Encoding transition Start_8_7 (567/800).
Encoding transition SendMsg_10_5 (568/800).
Encoding transition Update_9_2 (569/800).
Encoding transition Acquire_10_1 (570/800).
Encoding transition Acquire_6_2 (571/800).
Encoding transition end_update_10_1 (572/800).
Encoding transition Release_2_6 (573/800).
Encoding transition Change_7_7 (574/800).
Encoding transition Change_5_8 (575/800).
Encoding transition SendMsg_2_2 (576/800).
Encoding transition Update_1_7 (577/800).
Encoding transition Acquire_8_9 (578/800).
Encoding transition SendMsg_10_8 (579/800).
Encoding transition Acquire_4_7 (580/800).
Encoding transition end_update_5_8 (581/800).
Encoding transition Start_10_4 (582/800).
Encoding transition Release_8_10 (583/800).
Encoding transition Release_5_7 (584/800).
Encoding transition Update_6_4 (585/800).
Encoding transition SendReply_6_2 (586/800).
Encoding transition Update_2_10 (587/800).
Encoding transition Release_4_4 (588/800).
Encoding transition end_update_4_8 (589/800).
Encoding transition SendMsg_10_4 (590/800).
Encoding transition Release_3_5 (591/800).

BK_STOP 1401926633972

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

javax.xml.bind.UnmarshalException: unexpected element (uri:"http://mcc.lip6.fr/", local:"property-set"). Expected elements are <{}all-paths>,<{}before>,<{}boolean-formula>,<{}conjunction>,<{}deadlock>,<{}description>,<{}disjunction>,<{}equivalence>,<{}exclusive-disjunction>,<{}exists-path>,<{}expected-result>,<{}explanation>,<{}false>,<{}finally>,<{}formula>,<{}globally>,<{}id>,<{}if-no-successor>,<{}implication>,<{}impossibility>,<{}integer-constant>,<{}integer-difference>,<{}integer-division>,<{}integer-eq>,<{}integer-expression>,<{}integer-formula>,<{}integer-ge>,<{}integer-gt>,<{}integer-le>,<{}integer-lt>,<{}integer-ne>,<{}integer-product>,<{}integer-sum>,<{}invariant>,<{}is-ctl>,<{}is-fireable>,<{}is-live>,<{}is-ltl>,<{}is-reachability>,<{}is-structural>,<{}level>,<{}negation>,<{}next>,<{}place>,<{}place-bound>,<{}possibility>,<{}property>,<{}property-set>,<{}reach>,<{}steps>,<{}strength>,<{}tags>,<{}tokens-count>,<{}transition>,<{}true>,<{}until>,<{}value>
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext.handleEvent(UnmarshallingContext.java:647)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportError(Loader.java:243)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportError(Loader.java:238)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportUnexpectedChildElement(Loader.java:105)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext$DefaultRootLoader.childElement(UnmarshallingContext.java:1048)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext._startElement(UnmarshallingContext.java:483)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext.startElement(UnmarshallingContext.java:465)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.SAXConnector.startElement(SAXConnector.java:135)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.startElement(AbstractSAXParser.java:506)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.scanStartElement(XMLNSDocumentScannerImpl.java:376)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl$NSContentDriver.scanRootElementHook(XMLNSDocumentScannerImpl.java:602)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl$FragmentContentDriver.next(XMLDocumentFragmentScannerImpl.java:3063)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl$PrologDriver.next(XMLDocumentScannerImpl.java:881)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl.next(XMLDocumentScannerImpl.java:607)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.next(XMLNSDocumentScannerImpl.java:116)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanDocument(XMLDocumentFragmentScannerImpl.java:488)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:835)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:764)
at com.sun.org.apache.xerces.internal.parsers.XMLParser.parse(XMLParser.java:123)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.parse(AbstractSAXParser.java:1210)
at com.sun.org.apache.xerces.internal.jaxp.SAXParserImpl$JAXPSAXParser.parse(SAXParserImpl.java:568)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal0(UnmarshallerImpl.java:202)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal(UnmarshallerImpl.java:174)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:157)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:214)
at Main.convert(Main.java:194)
at Main.main(Main.java:229)
Cannot read input file model.bnd
terminate called after throwing an instance of 'MEDDLY::error'
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 167: 1751 Aborted ~/BenchKit/bin/bin/RGMEDD model ${PLACE_ORDER} ${MEDDLY_CACHE} ${BOUND} -C -f ${NEW_FRM}

Sequence of Actions to be Executed by the VM

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

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

# this is specific to your benchmark or test

export BIN_DIR="$HOME/BenchKit/bin"

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

tar xzf /home/mcc/BenchKit/INPUTS/DatabaseWithMutex-PT-10.tgz
mv DatabaseWithMutex-PT-10 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is DatabaseWithMutex-PT-10, examination is ReachabilityBounds"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r21sr-ovh1-140191459900367"
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 ;