About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
4727.63 | 1481563 | 116.3 | 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 QuasiCertifProtocol-PT-28, examination is ReachabilityFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541701216
=====================================================================
--------------------
content from stdout:
BK_START 1400447486912
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running QuasiCertifProtocol (PT), instance 28
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireability.xml INTO /home/mcc/execution/ReachabilityFireability.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 10 -C -f /home/mcc/execution/ReachabilityFireability.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 SsendTS_17 (0/446).
Encoding transition SsendTS_18 (1/446).
Encoding transition SsendTS_19 (2/446).
Encoding transition SsendTS_20 (3/446).
Encoding transition SsendTS_13 (4/446).
Encoding transition SsendTS_14 (5/446).
Encoding transition SsendTS_15 (6/446).
Encoding transition SsendTS_16 (7/446).
Encoding transition SsendTS_25 (8/446).
Encoding transition SsendTS_26 (9/446).
Encoding transition SsendTS_27 (10/446).
Encoding transition SsendTS_28 (11/446).
Encoding transition SsendTS_21 (12/446).
Encoding transition SsendTS_22 (13/446).
Encoding transition SsendTS_23 (14/446).
Encoding transition SsendTS_24 (15/446).
Encoding transition SsendTS_2 (16/446).
Encoding transition SsendTS_1 (17/446).
Encoding transition SsendTS_4 (18/446).
Encoding transition SsendTS_3 (19/446).
Encoding transition CsendTS1_27 (20/446).
Encoding transition CsendTS1_26 (21/446).
Encoding transition SsendTS_0 (22/446).
Encoding transition CsendTS1_28 (23/446).
Encoding transition SsendTS_10 (24/446).
Encoding transition SsendTS_9 (25/446).
Encoding transition SsendTS_12 (26/446).
Encoding transition SsendTS_11 (27/446).
Encoding transition SsendTS_6 (28/446).
Encoding transition SsendTS_5 (29/446).
Encoding transition SsendTS_8 (30/446).
Encoding transition SsendTS_7 (31/446).
Encoding transition SackCS_22 (32/446).
Encoding transition SackCS_23 (33/446).
Encoding transition SackCS_20 (34/446).
Encoding transition SackCS_21 (35/446).
Encoding transition SackCS_18 (36/446).
Encoding transition SackCS_19 (37/446).
Encoding transition SackCS_16 (38/446).
Encoding transition SackCS_17 (39/446).
Encoding transition Sperform_1 (40/446).
Encoding transition Sperform_2 (41/446).
Encoding transition SackCS_28 (42/446).
Encoding transition Sperform_0 (43/446).
Encoding transition SackCS_26 (44/446).
Encoding transition SackCS_27 (45/446).
Encoding transition SackCS_24 (46/446).
Encoding transition SackCS_25 (47/446).
Encoding transition SackCS_7 (48/446).
Encoding transition SackCS_6 (49/446).
Encoding transition SackCS_5 (50/446).
Encoding transition SackCS_4 (51/446).
Encoding transition SackCS_3 (52/446).
Encoding transition SackCS_2 (53/446).
Encoding transition SackCS_1 (54/446).
Encoding transition SackCS_0 (55/446).
Encoding transition SackCS_15 (56/446).
Encoding transition SackCS_14 (57/446).
Encoding transition SackCS_13 (58/446).
Encoding transition SackCS_12 (59/446).
Encoding transition SackCS_11 (60/446).
Encoding transition SackCS_10 (61/446).
Encoding transition SackCS_9 (62/446).
Encoding transition SackCS_8 (63/446).
Encoding transition CgenCertif_7 (64/446).
Encoding transition CgenCertif_8 (65/446).
Encoding transition CgenCertif_9 (66/446).
Encoding transition CgenCertif_10 (67/446).
Encoding transition CgenCertif_11 (68/446).
Encoding transition CgenCertif_12 (69/446).
Encoding transition CgenCertif_13 (70/446).
Encoding transition CgenCertif_14 (71/446).
Encoding transition CgenCertif_15 (72/446).
Encoding transition CgenCertif_16 (73/446).
Encoding transition CgenCertif_17 (74/446).
Encoding transition CgenCertif_18 (75/446).
Encoding transition CgenCertif_19 (76/446).
Encoding transition CgenCertif_20 (77/446).
Encoding transition CgenCertif_21 (78/446).
Encoding transition CgenCertif_22 (79/446).
Encoding transition malS1_26 (80/446).
Encoding transition malS1_25 (81/446).
Encoding transition malS1_28 (82/446).
Encoding transition malS1_27 (83/446).
Encoding transition malA3 (84/446).
Encoding transition malA5 (85/446).
Encoding transition malA2 (86/446).
Encoding transition malA4 (87/446).
Encoding transition CgenCertif_0 (88/446).
Encoding transition malA1 (89/446).
Encoding transition CgenCertif_2 (90/446).
Encoding transition CgenCertif_1 (91/446).
Encoding transition CgenCertif_4 (92/446).
Encoding transition CgenCertif_3 (93/446).
Encoding transition CgenCertif_6 (94/446).
Encoding transition CgenCertif_5 (95/446).
Encoding transition CsendTS1_12 (96/446).
Encoding transition CsendTS1_13 (97/446).
Encoding transition CsendTS1_10 (98/446).
Encoding transition CsendTS1_11 (99/446).
Encoding transition CsendTS1_16 (100/446).
Encoding transition CsendTS1_17 (101/446).
Encoding transition CsendTS1_14 (102/446).
Encoding transition CsendTS1_15 (103/446).
Encoding transition CsendTS1_20 (104/446).
Encoding transition CsendTS1_21 (105/446).
Encoding transition CsendTS1_18 (106/446).
Encoding transition CsendTS1_19 (107/446).
Encoding transition CsendTS1_24 (108/446).
Encoding transition CsendTS1_25 (109/446).
Encoding transition CsendTS1_22 (110/446).
Encoding transition CsendTS1_23 (111/446).
Encoding transition CgenCertif_26 (112/446).
Encoding transition CgenCertif_25 (113/446).
Encoding transition CgenCertif_24 (114/446).
Encoding transition CgenCertif_23 (115/446).
Encoding transition CsendTS1_1 (116/446).
Encoding transition CsendTS1_0 (117/446).
Encoding transition CgenCertif_28 (118/446).
Encoding transition CgenCertif_27 (119/446).
Encoding transition CsendTS1_5 (120/446).
Encoding transition CsendTS1_4 (121/446).
Encoding transition CsendTS1_3 (122/446).
Encoding transition CsendTS1_2 (123/446).
Encoding transition CsendTS1_9 (124/446).
Encoding transition CsendTS1_8 (125/446).
Encoding transition CsendTS1_7 (126/446).
Encoding transition CsendTS1_6 (127/446).
Encoding transition malS2_19 (128/446).
Encoding transition malS2_18 (129/446).
Encoding transition malS2_21 (130/446).
Encoding transition malS2_20 (131/446).
Encoding transition malS2_15 (132/446).
Encoding transition malS2_14 (133/446).
Encoding transition malS2_17 (134/446).
Encoding transition malS2_16 (135/446).
Encoding transition malS2_11 (136/446).
Encoding transition malS2_10 (137/446).
Encoding transition malS2_13 (138/446).
Encoding transition malS2_12 (139/446).
Encoding transition malS2_7 (140/446).
Encoding transition malS2_6 (141/446).
Encoding transition malS2_9 (142/446).
Encoding transition malS2_8 (143/446).
Encoding transition malS2_2 (144/446).
Encoding transition malS2_3 (145/446).
Encoding transition malS2_4 (146/446).
Encoding transition malS2_5 (147/446).
Encoding transition malS3_27 (148/446).
Encoding transition malS3_28 (149/446).
Encoding transition malS2_0 (150/446).
Encoding transition malS2_1 (151/446).
Encoding transition malS3_23 (152/446).
Encoding transition malS3_24 (153/446).
Encoding transition malS3_25 (154/446).
Encoding transition malS3_26 (155/446).
Encoding transition malS3_19 (156/446).
Encoding transition malS3_20 (157/446).
Encoding transition malS3_21 (158/446).
Encoding transition malS3_22 (159/446).
Encoding transition malS1_24 (160/446).
Encoding transition malS1_23 (161/446).
Encoding transition malS1_22 (162/446).
Encoding transition malS1_21 (163/446).
Encoding transition malS1_20 (164/446).
Encoding transition malS1_19 (165/446).
Encoding transition malS1_18 (166/446).
Encoding transition malS1_17 (167/446).
Encoding transition malS1_16 (168/446).
Encoding transition malS1_15 (169/446).
Encoding transition malS1_14 (170/446).
Encoding transition malS1_13 (171/446).
Encoding transition malS1_12 (172/446).
Encoding transition malS1_11 (173/446).
Encoding transition malS1_10 (174/446).
Encoding transition malS1_9 (175/446).
Encoding transition malS1_7 (176/446).
Encoding transition malS1_8 (177/446).
Encoding transition malS1_5 (178/446).
Encoding transition malS1_6 (179/446).
Encoding transition malS1_3 (180/446).
Encoding transition malS1_4 (181/446).
Encoding transition malS1_1 (182/446).
Encoding transition malS1_2 (183/446).
Encoding transition malS2_28 (184/446).
Encoding transition malS1_0 (185/446).
Encoding transition malS2_26 (186/446).
Encoding transition malS2_27 (187/446).
Encoding transition malS2_24 (188/446).
Encoding transition malS2_25 (189/446).
Encoding transition malS2_22 (190/446).
Encoding transition malS2_23 (191/446).
Encoding transition malS4_9 (192/446).
Encoding transition malS4_8 (193/446).
Encoding transition malS4_11 (194/446).
Encoding transition malS4_10 (195/446).
Encoding transition malS4_13 (196/446).
Encoding transition malS4_12 (197/446).
Encoding transition malS4_15 (198/446).
Encoding transition malS4_14 (199/446).
Encoding transition malS4_1 (200/446).
Encoding transition malS4_0 (201/446).
Encoding transition malS4_3 (202/446).
Encoding transition malS4_2 (203/446).
Encoding transition malS4_5 (204/446).
Encoding transition malS4_4 (205/446).
Encoding transition malS4_7 (206/446).
Encoding transition malS4_6 (207/446).
Encoding transition malS5_21 (208/446).
Encoding transition malS5_22 (209/446).
Encoding transition malS5_23 (210/446).
Encoding transition malS5_24 (211/446).
Encoding transition malS5_25 (212/446).
Encoding transition malS5_26 (213/446).
Encoding transition malS5_27 (214/446).
Encoding transition malS5_28 (215/446).
Encoding transition malS5_13 (216/446).
Encoding transition malS5_14 (217/446).
Encoding transition malS5_15 (218/446).
Encoding transition malS5_16 (219/446).
Encoding transition malS5_17 (220/446).
Encoding transition malS5_18 (221/446).
Encoding transition malS5_19 (222/446).
Encoding transition malS5_20 (223/446).
Encoding transition malS3_14 (224/446).
Encoding transition malS3_13 (225/446).
Encoding transition malS3_12 (226/446).
Encoding transition malS3_11 (227/446).
Encoding transition malS3_18 (228/446).
Encoding transition malS3_17 (229/446).
Encoding transition malS3_16 (230/446).
Encoding transition malS3_15 (231/446).
Encoding transition malS3_6 (232/446).
Encoding transition malS3_5 (233/446).
Encoding transition malS3_4 (234/446).
Encoding transition malS3_3 (235/446).
Encoding transition malS3_10 (236/446).
Encoding transition malS3_9 (237/446).
Encoding transition malS3_8 (238/446).
Encoding transition malS3_7 (239/446).
Encoding transition malS4_26 (240/446).
Encoding transition malS4_27 (241/446).
Encoding transition malS4_24 (242/446).
Encoding transition malS4_25 (243/446).
Encoding transition malS3_1 (244/446).
Encoding transition malS3_2 (245/446).
Encoding transition malS4_28 (246/446).
Encoding transition malS3_0 (247/446).
Encoding transition malS4_18 (248/446).
Encoding transition malS4_19 (249/446).
Encoding transition malS4_16 (250/446).
Encoding transition malS4_17 (251/446).
Encoding transition malS4_22 (252/446).
Encoding transition malS4_23 (253/446).
Encoding transition malS4_20 (254/446).
Encoding transition malS4_21 (255/446).
Encoding transition malC1_3 (256/446).
Encoding transition malC1_4 (257/446).
Encoding transition malC1_5 (258/446).
Encoding transition malC1_6 (259/446).
Encoding transition malC1_0 (260/446).
Encoding transition malC1_1 (261/446).
Encoding transition malC1_2 (262/446).
Encoding transition malS6_19 (263/446).
Encoding transition malS6_18 (264/446).
Encoding transition malS6_21 (265/446).
Encoding transition malS6_20 (266/446).
Encoding transition malS6_23 (267/446).
Encoding transition malS6_22 (268/446).
Encoding transition malS6_25 (269/446).
Encoding transition malS6_24 (270/446).
Encoding transition malS6_11 (271/446).
Encoding transition malS6_10 (272/446).
Encoding transition malS6_13 (273/446).
Encoding transition malS6_12 (274/446).
Encoding transition malS6_15 (275/446).
Encoding transition malS6_14 (276/446).
Encoding transition malS6_17 (277/446).
Encoding transition malS6_16 (278/446).
Encoding transition malS5_5 (279/446).
Encoding transition malS5_6 (280/446).
Encoding transition malS5_7 (281/446).
Encoding transition malS5_8 (282/446).
Encoding transition malS5_9 (283/446).
Encoding transition malS5_10 (284/446).
Encoding transition malS5_11 (285/446).
Encoding transition malS5_12 (286/446).
Encoding transition malS6_26 (287/446).
Encoding transition malS6_27 (288/446).
Encoding transition malS6_28 (289/446).
Encoding transition malS5_0 (290/446).
Encoding transition malS5_1 (291/446).
Encoding transition malS5_2 (292/446).
Encoding transition malS5_3 (293/446).
Encoding transition malS5_4 (294/446).
Encoding transition malC1_18 (295/446).
Encoding transition malC1_17 (296/446).
Encoding transition malC1_16 (297/446).
Encoding transition malC1_15 (298/446).
Encoding transition malC1_22 (299/446).
Encoding transition malC1_21 (300/446).
Encoding transition malC1_20 (301/446).
Encoding transition malC1_19 (302/446).
Encoding transition malC1_10 (303/446).
Encoding transition malC1_9 (304/446).
Encoding transition malC1_8 (305/446).
Encoding transition malC1_7 (306/446).
Encoding transition malC1_14 (307/446).
Encoding transition malC1_13 (308/446).
Encoding transition malC1_12 (309/446).
Encoding transition malC1_11 (310/446).
Encoding transition malS6_4 (311/446).
Encoding transition malS6_5 (312/446).
Encoding transition malS6_2 (313/446).
Encoding transition malS6_3 (314/446).
Encoding transition malS6_8 (315/446).
Encoding transition malS6_9 (316/446).
Encoding transition malS6_6 (317/446).
Encoding transition malS6_7 (318/446).
Encoding transition malC1_25 (319/446).
Encoding transition malC1_26 (320/446).
Encoding transition malC1_23 (321/446).
Encoding transition malC1_24 (322/446).
Encoding transition malS6_0 (323/446).
Encoding transition malS6_1 (324/446).
Encoding transition malC1_27 (325/446).
Encoding transition malC1_28 (326/446).
Encoding transition SgetTS_23 (327/446).
Encoding transition SgetTS_24 (328/446).
Encoding transition SgetTS_21 (329/446).
Encoding transition SgetTS_22 (330/446).
Encoding transition SgetTS_19 (331/446).
Encoding transition SgetTS_20 (332/446).
Encoding transition SgetTS_17 (333/446).
Encoding transition SgetTS_18 (334/446).
Encoding transition SgetTS_15 (335/446).
Encoding transition SgetTS_16 (336/446).
Encoding transition SgetTS_13 (337/446).
Encoding transition SgetTS_14 (338/446).
Encoding transition SgetTS_11 (339/446).
Encoding transition SgetTS_12 (340/446).
Encoding transition SgetTS_9 (341/446).
Encoding transition SgetTS_10 (342/446).
Encoding transition ScertCS_11 (343/446).
Encoding transition ScertCS_10 (344/446).
Encoding transition ScertCS_9 (345/446).
Encoding transition ScertCS_8 (346/446).
Encoding transition ScertCS_7 (347/446).
Encoding transition ScertCS_6 (348/446).
Encoding transition ScertCS_5 (349/446).
Encoding transition ScertCS_4 (350/446).
Encoding transition ScertCS_3 (351/446).
Encoding transition ScertCS_2 (352/446).
Encoding transition ScertCS_1 (353/446).
Encoding transition ScertCS_0 (354/446).
Encoding transition SgetTS_28 (355/446).
Encoding transition SgetTS_27 (356/446).
Encoding transition SgetTS_26 (357/446).
Encoding transition SgetTS_25 (358/446).
Encoding transition ScertCS_24 (359/446).
Encoding transition ScertCS_25 (360/446).
Encoding transition ScertCS_26 (361/446).
Encoding transition ScertCS_27 (362/446).
Encoding transition ScertCS_20 (363/446).
Encoding transition ScertCS_21 (364/446).
Encoding transition ScertCS_22 (365/446).
Encoding transition ScertCS_23 (366/446).
Encoding transition ScertCS_16 (367/446).
Encoding transition ScertCS_17 (368/446).
Encoding transition ScertCS_18 (369/446).
Encoding transition ScertCS_19 (370/446).
Encoding transition ScertCS_12 (371/446).
Encoding transition ScertCS_13 (372/446).
Encoding transition ScertCS_14 (373/446).
Encoding transition ScertCS_15 (374/446).
Encoding transition AgetTS (375/446).
Encoding transition AreqCS (376/446).
Encoding transition AreqTS (377/446).
Encoding transition AendCS (378/446).
Encoding transition ScertCS_28 (379/446).
Encoding transition AackCS (380/446).
Encoding transition AstartCS (381/446).
Encoding transition Sperform_13 (382/446).
Encoding transition Sperform_14 (383/446).
Encoding transition Sperform_11 (384/446).
Encoding transition Sperform_12 (385/446).
Encoding transition Sperform_17 (386/446).
Encoding transition Sperform_18 (387/446).
Encoding transition Sperform_15 (388/446).
Encoding transition Sperform_16 (389/446).
Encoding transition Sperform_5 (390/446).
Encoding transition Sperform_6 (391/446).
Encoding transition Sperform_3 (392/446).
Encoding transition Sperform_4 (393/446).
Encoding transition Sperform_9 (394/446).
Encoding transition Sperform_10 (395/446).
Encoding transition Sperform_7 (396/446).
Encoding transition Sperform_8 (397/446).
Encoding transition SreqTS_1 (398/446).
Encoding transition SreqTS_0 (399/446).
Encoding transition Sperform_28 (400/446).
Encoding transition Sperform_27 (401/446).
Encoding transition SreqTS_5 (402/446).
Encoding transition SreqTS_4 (403/446).
Encoding transition SreqTS_3 (404/446).
Encoding transition SreqTS_2 (405/446).
Encoding transition Sperform_22 (406/446).
Encoding transition Sperform_21 (407/446).
Encoding transition Sperform_20 (408/446).
Encoding transition Sperform_19 (409/446).
Encoding transition Sperform_26 (410/446).
Encoding transition Sperform_25 (411/446).
Encoding transition Sperform_24 (412/446).
Encoding transition Sperform_23 (413/446).
Encoding transition SreqTS_14 (414/446).
Encoding transition SreqTS_15 (415/446).
Encoding transition SreqTS_16 (416/446).
Encoding transition SreqTS_17 (417/446).
Encoding transition SreqTS_18 (418/446).
Encoding transition SreqTS_19 (419/446).
Encoding transition SreqTS_20 (420/446).
Encoding transition SreqTS_21 (421/446).
Encoding transition SreqTS_6 (422/446).
Encoding transition SreqTS_7 (423/446).
Encoding transition SreqTS_8 (424/446).
Encoding transition SreqTS_9 (425/446).
Encoding transition SreqTS_10 (426/446).
Encoding transition SreqTS_11 (427/446).
Encoding transition SreqTS_12 (428/446).
Encoding transition SreqTS_13 (429/446).
Encoding transition SgetTS_2 (430/446).
Encoding transition SgetTS_1 (431/446).
Encoding transition SgetTS_4 (432/446).
Encoding transition SgetTS_3 (433/446).
Encoding transition SgetTS_6 (434/446).
Encoding transition SgetTS_5 (435/446).
Encoding transition SgetTS_8 (436/446).
Encoding transition SgetTS_7 (437/446).
Encoding transition SreqTS_23 (438/446).
Encoding transition SreqTS_22 (439/446).
Encoding transition SreqTS_25 (440/446).
Encoding transition SreqTS_24 (441/446).
Encoding transition SreqTS_27 (442/446).
Encoding transition SreqTS_26 (443/446).
Encoding transition SgetTS_0 (444/446).
Encoding transition SreqTS_28 (445/446).
----------------------------------------
End firing rule encoding
----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------
Total Used Memory: 1514020KB
CANNOT_COMPUTE
BK_STOP 1400448968797
--------------------
content from stderr:
Cannot read input file model.bnd
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="QuasiCertifProtocol-PT-28"
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/QuasiCertifProtocol-PT-28.tgz
mv QuasiCertifProtocol-PT-28 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 QuasiCertifProtocol-PT-28, examination is ReachabilityFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541701216"
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 ;