About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
4104.29 | 1304332 | 165.6 | 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-22, examination is ReachabilityComputeBounds
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541701198
=====================================================================
--------------------
content from stdout:
BK_START 1400447002966
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running QuasiCertifProtocol (PT), instance 22
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityComputeBounds.xml INTO /home/mcc/execution/ReachabilityComputeBounds.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 10 -C -f /home/mcc/execution/ReachabilityComputeBounds.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_19 (0/356).
Encoding transition SsendTS_20 (1/356).
Encoding transition SsendTS_21 (2/356).
Encoding transition SsendTS_22 (3/356).
Encoding transition SackCS_0 (4/356).
Encoding transition SackCS_1 (5/356).
Encoding transition SackCS_2 (6/356).
Encoding transition SackCS_3 (7/356).
Encoding transition SsendTS_11 (8/356).
Encoding transition SsendTS_12 (9/356).
Encoding transition SsendTS_13 (10/356).
Encoding transition SsendTS_14 (11/356).
Encoding transition SsendTS_15 (12/356).
Encoding transition SsendTS_16 (13/356).
Encoding transition SsendTS_17 (14/356).
Encoding transition SsendTS_18 (15/356).
Encoding transition SsendTS_4 (16/356).
Encoding transition SsendTS_3 (17/356).
Encoding transition SsendTS_6 (18/356).
Encoding transition SsendTS_5 (19/356).
Encoding transition SsendTS_8 (20/356).
Encoding transition SsendTS_7 (21/356).
Encoding transition SsendTS_10 (22/356).
Encoding transition SsendTS_9 (23/356).
Encoding transition CsendTS1_19 (24/356).
Encoding transition CsendTS1_18 (25/356).
Encoding transition CsendTS1_21 (26/356).
Encoding transition CsendTS1_20 (27/356).
Encoding transition SsendTS_0 (28/356).
Encoding transition CsendTS1_22 (29/356).
Encoding transition SsendTS_2 (30/356).
Encoding transition SsendTS_1 (31/356).
Encoding transition Sperform_7 (32/356).
Encoding transition Sperform_8 (33/356).
Encoding transition Sperform_5 (34/356).
Encoding transition Sperform_6 (35/356).
Encoding transition Sperform_11 (36/356).
Encoding transition Sperform_12 (37/356).
Encoding transition Sperform_9 (38/356).
Encoding transition Sperform_10 (39/356).
Encoding transition SackCS_22 (40/356).
Encoding transition Sperform_0 (41/356).
Encoding transition SackCS_20 (42/356).
Encoding transition SackCS_21 (43/356).
Encoding transition Sperform_3 (44/356).
Encoding transition Sperform_4 (45/356).
Encoding transition Sperform_1 (46/356).
Encoding transition Sperform_2 (47/356).
Encoding transition SackCS_15 (48/356).
Encoding transition SackCS_14 (49/356).
Encoding transition SackCS_13 (50/356).
Encoding transition SackCS_12 (51/356).
Encoding transition SackCS_19 (52/356).
Encoding transition SackCS_18 (53/356).
Encoding transition SackCS_17 (54/356).
Encoding transition SackCS_16 (55/356).
Encoding transition SackCS_7 (56/356).
Encoding transition SackCS_6 (57/356).
Encoding transition SackCS_5 (58/356).
Encoding transition SackCS_4 (59/356).
Encoding transition SackCS_11 (60/356).
Encoding transition SackCS_10 (61/356).
Encoding transition SackCS_9 (62/356).
Encoding transition SackCS_8 (63/356).
Encoding transition SreqTS_18 (64/356).
Encoding transition SreqTS_19 (65/356).
Encoding transition SreqTS_20 (66/356).
Encoding transition SreqTS_21 (67/356).
Encoding transition SreqTS_14 (68/356).
Encoding transition SreqTS_15 (69/356).
Encoding transition SreqTS_16 (70/356).
Encoding transition SreqTS_17 (71/356).
Encoding transition SreqTS_10 (72/356).
Encoding transition SreqTS_11 (73/356).
Encoding transition SreqTS_12 (74/356).
Encoding transition SreqTS_13 (75/356).
Encoding transition SreqTS_6 (76/356).
Encoding transition SreqTS_7 (77/356).
Encoding transition SreqTS_8 (78/356).
Encoding transition SreqTS_9 (79/356).
Encoding transition SreqTS_3 (80/356).
Encoding transition SreqTS_2 (81/356).
Encoding transition SreqTS_5 (82/356).
Encoding transition SreqTS_4 (83/356).
Encoding transition Sperform_22 (84/356).
Encoding transition Sperform_21 (85/356).
Encoding transition SreqTS_1 (86/356).
Encoding transition SreqTS_0 (87/356).
Encoding transition Sperform_18 (88/356).
Encoding transition Sperform_17 (89/356).
Encoding transition Sperform_20 (90/356).
Encoding transition Sperform_19 (91/356).
Encoding transition Sperform_14 (92/356).
Encoding transition Sperform_13 (93/356).
Encoding transition Sperform_16 (94/356).
Encoding transition Sperform_15 (95/356).
Encoding transition ScertCS_6 (96/356).
Encoding transition ScertCS_7 (97/356).
Encoding transition ScertCS_4 (98/356).
Encoding transition ScertCS_5 (99/356).
Encoding transition ScertCS_2 (100/356).
Encoding transition ScertCS_3 (101/356).
Encoding transition ScertCS_0 (102/356).
Encoding transition ScertCS_1 (103/356).
Encoding transition SgetTS_21 (104/356).
Encoding transition SgetTS_22 (105/356).
Encoding transition SgetTS_19 (106/356).
Encoding transition SgetTS_20 (107/356).
Encoding transition SgetTS_17 (108/356).
Encoding transition SgetTS_18 (109/356).
Encoding transition SgetTS_15 (110/356).
Encoding transition SgetTS_16 (111/356).
Encoding transition SgetTS_14 (112/356).
Encoding transition SgetTS_13 (113/356).
Encoding transition SgetTS_12 (114/356).
Encoding transition SgetTS_11 (115/356).
Encoding transition SgetTS_10 (116/356).
Encoding transition SgetTS_9 (117/356).
Encoding transition SgetTS_8 (118/356).
Encoding transition SgetTS_7 (119/356).
Encoding transition SgetTS_6 (120/356).
Encoding transition SgetTS_5 (121/356).
Encoding transition SgetTS_4 (122/356).
Encoding transition SgetTS_3 (123/356).
Encoding transition SgetTS_2 (124/356).
Encoding transition SgetTS_1 (125/356).
Encoding transition SgetTS_0 (126/356).
Encoding transition SreqTS_22 (127/356).
Encoding transition malS3_4 (128/356).
Encoding transition malS3_3 (129/356).
Encoding transition malS3_6 (130/356).
Encoding transition malS3_5 (131/356).
Encoding transition malS3_8 (132/356).
Encoding transition malS3_7 (133/356).
Encoding transition malS3_10 (134/356).
Encoding transition malS3_9 (135/356).
Encoding transition malS3_12 (136/356).
Encoding transition malS3_11 (137/356).
Encoding transition malS3_14 (138/356).
Encoding transition malS3_13 (139/356).
Encoding transition malS3_16 (140/356).
Encoding transition malS3_15 (141/356).
Encoding transition malS3_18 (142/356).
Encoding transition malS3_17 (143/356).
Encoding transition malS4_10 (144/356).
Encoding transition malS4_11 (145/356).
Encoding transition malS4_12 (146/356).
Encoding transition malS4_13 (147/356).
Encoding transition malS4_14 (148/356).
Encoding transition malS4_15 (149/356).
Encoding transition malS4_16 (150/356).
Encoding transition malS4_17 (151/356).
Encoding transition malS4_18 (152/356).
Encoding transition malS4_19 (153/356).
Encoding transition malS4_20 (154/356).
Encoding transition malS4_21 (155/356).
Encoding transition malS4_22 (156/356).
Encoding transition malS3_0 (157/356).
Encoding transition malS3_1 (158/356).
Encoding transition malS3_2 (159/356).
Encoding transition malS2_15 (160/356).
Encoding transition malS2_14 (161/356).
Encoding transition malS2_13 (162/356).
Encoding transition malS2_12 (163/356).
Encoding transition malS2_19 (164/356).
Encoding transition malS2_18 (165/356).
Encoding transition malS2_17 (166/356).
Encoding transition malS2_16 (167/356).
Encoding transition malS1_0 (168/356).
Encoding transition malS2_22 (169/356).
Encoding transition malS2_21 (170/356).
Encoding transition malS2_20 (171/356).
Encoding transition malS1_4 (172/356).
Encoding transition malS1_3 (173/356).
Encoding transition malS1_2 (174/356).
Encoding transition malS1_1 (175/356).
Encoding transition malS3_21 (176/356).
Encoding transition malS3_22 (177/356).
Encoding transition malS3_19 (178/356).
Encoding transition malS3_20 (179/356).
Encoding transition malS2_2 (180/356).
Encoding transition malS2_3 (181/356).
Encoding transition malS2_0 (182/356).
Encoding transition malS2_1 (183/356).
Encoding transition malS2_6 (184/356).
Encoding transition malS2_7 (185/356).
Encoding transition malS2_4 (186/356).
Encoding transition malS2_5 (187/356).
Encoding transition malS2_10 (188/356).
Encoding transition malS2_11 (189/356).
Encoding transition malS2_8 (190/356).
Encoding transition malS2_9 (191/356).
Encoding transition malA2 (192/356).
Encoding transition malA4 (193/356).
Encoding transition CgenCertif_0 (194/356).
Encoding transition malA1 (195/356).
Encoding transition malS1_22 (196/356).
Encoding transition malS1_21 (197/356).
Encoding transition malA3 (198/356).
Encoding transition malA5 (199/356).
Encoding transition CgenCertif_6 (200/356).
Encoding transition CgenCertif_5 (201/356).
Encoding transition CgenCertif_8 (202/356).
Encoding transition CgenCertif_7 (203/356).
Encoding transition CgenCertif_2 (204/356).
Encoding transition CgenCertif_1 (205/356).
Encoding transition CgenCertif_4 (206/356).
Encoding transition CgenCertif_3 (207/356).
Encoding transition malS1_9 (208/356).
Encoding transition malS1_10 (209/356).
Encoding transition malS1_11 (210/356).
Encoding transition malS1_12 (211/356).
Encoding transition malS1_5 (212/356).
Encoding transition malS1_6 (213/356).
Encoding transition malS1_7 (214/356).
Encoding transition malS1_8 (215/356).
Encoding transition malS1_17 (216/356).
Encoding transition malS1_18 (217/356).
Encoding transition malS1_19 (218/356).
Encoding transition malS1_20 (219/356).
Encoding transition malS1_13 (220/356).
Encoding transition malS1_14 (221/356).
Encoding transition malS1_15 (222/356).
Encoding transition malS1_16 (223/356).
Encoding transition CsendTS1_9 (224/356).
Encoding transition CsendTS1_8 (225/356).
Encoding transition CsendTS1_7 (226/356).
Encoding transition CsendTS1_6 (227/356).
Encoding transition CsendTS1_5 (228/356).
Encoding transition CsendTS1_4 (229/356).
Encoding transition CsendTS1_3 (230/356).
Encoding transition CsendTS1_2 (231/356).
Encoding transition CsendTS1_17 (232/356).
Encoding transition CsendTS1_16 (233/356).
Encoding transition CsendTS1_15 (234/356).
Encoding transition CsendTS1_14 (235/356).
Encoding transition CsendTS1_13 (236/356).
Encoding transition CsendTS1_12 (237/356).
Encoding transition CsendTS1_11 (238/356).
Encoding transition CsendTS1_10 (239/356).
Encoding transition CgenCertif_15 (240/356).
Encoding transition CgenCertif_16 (241/356).
Encoding transition CgenCertif_13 (242/356).
Encoding transition CgenCertif_14 (243/356).
Encoding transition CgenCertif_11 (244/356).
Encoding transition CgenCertif_12 (245/356).
Encoding transition CgenCertif_9 (246/356).
Encoding transition CgenCertif_10 (247/356).
Encoding transition CsendTS1_0 (248/356).
Encoding transition CsendTS1_1 (249/356).
Encoding transition CgenCertif_21 (250/356).
Encoding transition CgenCertif_22 (251/356).
Encoding transition CgenCertif_19 (252/356).
Encoding transition CgenCertif_20 (253/356).
Encoding transition CgenCertif_17 (254/356).
Encoding transition CgenCertif_18 (255/356).
Encoding transition ScertCS_10 (256/356).
Encoding transition malS5_17 (257/356).
Encoding transition ScertCS_11 (258/356).
Encoding transition malS5_18 (259/356).
Encoding transition ScertCS_8 (260/356).
Encoding transition malS5_19 (261/356).
Encoding transition ScertCS_9 (262/356).
Encoding transition malS5_20 (263/356).
Encoding transition ScertCS_14 (264/356).
Encoding transition malS5_21 (265/356).
Encoding transition ScertCS_15 (266/356).
Encoding transition malS5_22 (267/356).
Encoding transition ScertCS_12 (268/356).
Encoding transition malS4_0 (269/356).
Encoding transition ScertCS_13 (270/356).
Encoding transition malS4_1 (271/356).
Encoding transition ScertCS_18 (272/356).
Encoding transition malS4_2 (273/356).
Encoding transition ScertCS_19 (274/356).
Encoding transition malS4_3 (275/356).
Encoding transition ScertCS_16 (276/356).
Encoding transition malS4_4 (277/356).
Encoding transition ScertCS_17 (278/356).
Encoding transition malS4_5 (279/356).
Encoding transition ScertCS_22 (280/356).
Encoding transition malS4_6 (281/356).
Encoding transition AendCS (282/356).
Encoding transition malS4_7 (283/356).
Encoding transition ScertCS_20 (284/356).
Encoding transition malS4_8 (285/356).
Encoding transition ScertCS_21 (286/356).
Encoding transition malS4_9 (287/356).
Encoding transition AgetTS (288/356).
Encoding transition malS5_2 (289/356).
Encoding transition AreqCS (290/356).
Encoding transition malS5_1 (291/356).
Encoding transition AackCS (292/356).
Encoding transition malS5_4 (293/356).
Encoding transition AstartCS (294/356).
Encoding transition malS5_3 (295/356).
Encoding transition malS5_6 (296/356).
Encoding transition malS5_5 (297/356).
Encoding transition malS5_8 (298/356).
Encoding transition AreqTS (299/356).
Encoding transition malS5_7 (300/356).
Encoding transition malS5_10 (301/356).
Encoding transition malS5_9 (302/356).
Encoding transition malS5_12 (303/356).
Encoding transition malS5_11 (304/356).
Encoding transition malS5_14 (305/356).
Encoding transition malS5_13 (306/356).
Encoding transition malS5_16 (307/356).
Encoding transition malS5_15 (308/356).
Encoding transition malS6_10 (309/356).
Encoding transition malS6_11 (310/356).
Encoding transition malS6_8 (311/356).
Encoding transition malS6_9 (312/356).
Encoding transition malS6_14 (313/356).
Encoding transition malS6_15 (314/356).
Encoding transition malS6_12 (315/356).
Encoding transition malS6_13 (316/356).
Encoding transition malS6_18 (317/356).
Encoding transition malS6_19 (318/356).
Encoding transition malS6_16 (319/356).
Encoding transition malS6_17 (320/356).
Encoding transition malS6_22 (321/356).
Encoding transition malS5_0 (322/356).
Encoding transition malS6_20 (323/356).
Encoding transition malS6_21 (324/356).
Encoding transition malC1_18 (325/356).
Encoding transition malC1_17 (326/356).
Encoding transition malC1_16 (327/356).
Encoding transition malC1_15 (328/356).
Encoding transition malC1_22 (329/356).
Encoding transition malC1_21 (330/356).
Encoding transition malC1_20 (331/356).
Encoding transition malC1_19 (332/356).
Encoding transition malS6_3 (333/356).
Encoding transition malS6_2 (334/356).
Encoding transition malS6_1 (335/356).
Encoding transition malS6_0 (336/356).
Encoding transition malS6_7 (337/356).
Encoding transition malS6_6 (338/356).
Encoding transition malS6_5 (339/356).
Encoding transition malS6_4 (340/356).
Encoding transition malC1_3 (341/356).
Encoding transition malC1_4 (342/356).
Encoding transition malC1_5 (343/356).
Encoding transition malC1_6 (344/356).
Encoding transition malC1_0 (345/356).
Encoding transition malC1_1 (346/356).
Encoding transition malC1_2 (347/356).
Encoding transition malC1_11 (348/356).
Encoding transition malC1_12 (349/356).
Encoding transition malC1_13 (350/356).
Encoding transition malC1_14 (351/356).
Encoding transition malC1_7 (352/356).
Encoding transition malC1_8 (353/356).
Encoding transition malC1_9 (354/356).
Encoding transition malC1_10 (355/356).
----------------------------------------
End firing rule encoding
----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------
Total Used Memory: 822632KB
CANNOT_COMPUTE
BK_STOP 1400448308275
--------------------
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-22"
export BK_EXAMINATION="ReachabilityComputeBounds"
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-22.tgz
mv QuasiCertifProtocol-PT-22 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-22, examination is ReachabilityComputeBounds"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541701198"
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 ;