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 CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r21sr-ovh1-140191459900372
=====================================================================

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

BK_START 1401924826717
======================================================
== 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/CTLCardinality.xml INTO /home/mcc/execution/CTLCardinality.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 30 -C -f /home/mcc/execution/CTLCardinality.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 1401926640567

--------------------
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: 1752 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="CTLCardinality"
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 CTLCardinality"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r21sr-ovh1-140191459900372"
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 ;