About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
5138.05 | 1722968 | 172.4 | TTFTTFTFTF | 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 Eratosthenes-PT-100, examination is ReachabilityBounds
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r01kn-qhx2-140025666001134
=====================================================================
--------------------
content from stdout:
BK_START 1400275587949
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Eratosthenes (PT), instance 100
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityBounds.xml INTO /home/mcc/execution/ReachabilityBounds.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -P -h 2000000000 -B 1 -C -f /home/mcc/execution/ReachabilityBounds.rgmedd-ctl
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition t100.50 (0/283).
Encoding transition t25.5 (1/283).
Encoding transition t60.20 (2/283).
Encoding transition t94.47 (3/283).
Encoding transition t60.15 (4/283).
Encoding transition t60.12 (5/283).
Encoding transition t60.10 (6/283).
Encoding transition t14.7 (7/283).
Encoding transition t14.2 (8/283).
Encoding transition t100.25 (9/283).
Encoding transition t100.20 (10/283).
Encoding transition t100.5 (11/283).
Encoding transition t100.4 (12/283).
Encoding transition t100.2 (13/283).
Encoding transition t51.17 (14/283).
Encoding transition t92.4 (15/283).
Encoding transition t92.2 (16/283).
Encoding transition t100.10 (17/283).
Encoding transition t42.21 (18/283).
Encoding transition t81.9 (19/283).
Encoding transition t81.3 (20/283).
Encoding transition t39.3 (21/283).
Encoding transition t42.14 (22/283).
Encoding transition t85.17 (23/283).
Encoding transition t76.38 (24/283).
Encoding transition t70.7 (25/283).
Encoding transition t28.7 (26/283).
Encoding transition t70.5 (27/283).
Encoding transition t28.4 (28/283).
Encoding transition t70.2 (29/283).
Encoding transition t28.2 (30/283).
Encoding transition t33.11 (31/283).
Encoding transition t76.19 (32/283).
Encoding transition t95.5 (33/283).
Encoding transition t24.12 (34/283).
Encoding transition t84.7 (35/283).
Encoding transition t84.6 (36/283).
Encoding transition t84.4 (37/283).
Encoding transition t84.3 (38/283).
Encoding transition t84.2 (39/283).
Encoding transition t58.29 (40/283).
Encoding transition t82.41 (41/283).
Encoding transition t62.2 (42/283).
Encoding transition t91.13 (43/283).
Encoding transition t51.3 (44/283).
Encoding transition t98.7 (45/283).
Encoding transition t98.2 (46/283).
Encoding transition t40.8 (47/283).
Encoding transition t40.5 (48/283).
Encoding transition t40.4 (49/283).
Encoding transition t40.2 (50/283).
Encoding transition t87.3 (51/283).
Encoding transition t30.15 (52/283).
Encoding transition t30.10 (53/283).
Encoding transition t76.4 (54/283).
Encoding transition t76.2 (55/283).
Encoding transition t64.32 (56/283).
Encoding transition t65.5 (57/283).
Encoding transition t98.49 (58/283).
Encoding transition t64.16 (59/283).
Encoding transition t54.9 (60/283).
Encoding transition t54.6 (61/283).
Encoding transition t54.3 (62/283).
Encoding transition t54.2 (63/283).
Encoding transition t55.11 (64/283).
Encoding transition t98.14 (65/283).
Encoding transition t32.8 (66/283).
Encoding transition t32.4 (67/283).
Encoding transition t32.2 (68/283).
Encoding transition t46.23 (69/283).
Encoding transition t21.7 (70/283).
Encoding transition t21.3 (71/283).
Encoding transition t68.4 (72/283).
Encoding transition t68.2 (73/283).
Encoding transition t70.35 (74/283).
Encoding transition t10.5 (75/283).
Encoding transition t10.2 (76/283).
Encoding transition t57.3 (77/283).
Encoding transition t70.14 (78/283).
Encoding transition t46.2 (79/283).
Encoding transition t70.10 (80/283).
Encoding transition t28.14 (81/283).
Encoding transition t35.7 (82/283).
Encoding transition t35.5 (83/283).
Encoding transition t24.8 (84/283).
Encoding transition t24.6 (85/283).
Encoding transition t24.4 (86/283).
Encoding transition t24.3 (87/283).
Encoding transition t24.2 (88/283).
Encoding transition t52.26 (89/283).
Encoding transition t86.43 (90/283).
Encoding transition t52.13 (91/283).
Encoding transition t6.3 (92/283).
Encoding transition t6.2 (93/283).
Encoding transition t95.19 (94/283).
Encoding transition t91.7 (95/283).
Encoding transition t49.7 (96/283).
Encoding transition t80.8 (97/283).
Encoding transition t80.5 (98/283).
Encoding transition t80.4 (99/283).
Encoding transition t80.2 (100/283).
Encoding transition t38.2 (101/283).
Encoding transition t27.9 (102/283).
Encoding transition t34.17 (103/283).
Encoding transition t27.3 (104/283).
Encoding transition t77.11 (105/283).
Encoding transition t68.34 (106/283).
Encoding transition t16.8 (107/283).
Encoding transition t16.4 (108/283).
Encoding transition t16.2 (109/283).
Encoding transition t9.3 (110/283).
Encoding transition t68.17 (111/283).
Encoding transition t92.46 (112/283).
Encoding transition t94.2 (113/283).
Encoding transition t92.23 (114/283).
Encoding transition t72.9 (115/283).
Encoding transition t72.8 (116/283).
Encoding transition t72.6 (117/283).
Encoding transition t72.4 (118/283).
Encoding transition t72.3 (119/283).
Encoding transition t72.2 (120/283).
Encoding transition t40.20 (121/283).
Encoding transition t40.10 (122/283).
Encoding transition t74.37 (123/283).
Encoding transition t50.5 (124/283).
Encoding transition t50.2 (125/283).
Encoding transition t86.2 (126/283).
Encoding transition t75.5 (127/283).
Encoding transition t75.3 (128/283).
Encoding transition t22.11 (129/283).
Encoding transition t65.13 (130/283).
Encoding transition t64.8 (131/283).
Encoding transition t64.4 (132/283).
Encoding transition t64.2 (133/283).
Encoding transition t99.33 (134/283).
Encoding transition t56.28 (135/283).
Encoding transition t56.14 (136/283).
Encoding transition t80.40 (137/283).
Encoding transition t99.11 (138/283).
Encoding transition t42.7 (139/283).
Encoding transition t42.6 (140/283).
Encoding transition t42.3 (141/283).
Encoding transition t42.2 (142/283).
Encoding transition t80.20 (143/283).
Encoding transition t78.6 (144/283).
Encoding transition t78.3 (145/283).
Encoding transition t78.2 (146/283).
Encoding transition t80.16 (147/283).
Encoding transition t80.10 (148/283).
Encoding transition t20.5 (149/283).
Encoding transition t20.4 (150/283).
Encoding transition t20.2 (151/283).
Encoding transition t38.19 (152/283).
Encoding transition t56.8 (153/283).
Encoding transition t56.7 (154/283).
Encoding transition t56.4 (155/283).
Encoding transition t56.2 (156/283).
Encoding transition t62.31 (157/283).
Encoding transition t45.9 (158/283).
Encoding transition t45.5 (159/283).
Encoding transition t45.3 (160/283).
Encoding transition t96.48 (161/283).
Encoding transition t34.2 (162/283).
Encoding transition t96.32 (163/283).
Encoding transition t96.24 (164/283).
Encoding transition t96.16 (165/283).
Encoding transition t96.12 (166/283).
Encoding transition t12.6 (167/283).
Encoding transition t12.4 (168/283).
Encoding transition t12.3 (169/283).
Encoding transition t12.2 (170/283).
Encoding transition t44.22 (171/283).
Encoding transition t87.29 (172/283).
Encoding transition t44.11 (173/283).
Encoding transition t78.39 (174/283).
Encoding transition t90.9 (175/283).
Encoding transition t48.8 (176/283).
Encoding transition t90.6 (177/283).
Encoding transition t48.6 (178/283).
Encoding transition t90.5 (179/283).
Encoding transition t48.4 (180/283).
Encoding transition t90.3 (181/283).
Encoding transition t48.3 (182/283).
Encoding transition t90.2 (183/283).
Encoding transition t48.2 (184/283).
Encoding transition t78.26 (185/283).
Encoding transition t78.13 (186/283).
Encoding transition t26.2 (187/283).
Encoding transition t69.23 (188/283).
Encoding transition t26.13 (189/283).
Encoding transition t15.5 (190/283).
Encoding transition t15.3 (191/283).
Encoding transition t8.4 (192/283).
Encoding transition t8.2 (193/283).
Encoding transition t93.31 (194/283).
Encoding transition t93.3 (195/283).
Encoding transition t50.25 (196/283).
Encoding transition t84.42 (197/283).
Encoding transition t50.10 (198/283).
Encoding transition t82.2 (199/283).
Encoding transition t84.28 (200/283).
Encoding transition t84.21 (201/283).
Encoding transition t84.14 (202/283).
Encoding transition t84.12 (203/283).
Encoding transition t18.9 (204/283).
Encoding transition t60.6 (205/283).
Encoding transition t18.6 (206/283).
Encoding transition t60.5 (207/283).
Encoding transition t60.4 (208/283).
Encoding transition t60.3 (209/283).
Encoding transition t18.3 (210/283).
Encoding transition t60.2 (211/283).
Encoding transition t18.2 (212/283).
Encoding transition t75.25 (213/283).
Encoding transition t32.16 (214/283).
Encoding transition t96.8 (215/283).
Encoding transition t75.15 (216/283).
Encoding transition t96.6 (217/283).
Encoding transition t96.4 (218/283).
Encoding transition t96.3 (219/283).
Encoding transition t96.2 (220/283).
Encoding transition t66.33 (221/283).
Encoding transition t66.22 (222/283).
Encoding transition t85.5 (223/283).
Encoding transition t66.11 (224/283).
Encoding transition t90.45 (225/283).
Encoding transition t74.2 (226/283).
Encoding transition t90.30 (227/283).
Encoding transition t63.9 (228/283).
Encoding transition t63.7 (229/283).
Encoding transition t63.3 (230/283).
Encoding transition t57.19 (231/283).
Encoding transition t52.4 (232/283).
Encoding transition t52.2 (233/283).
Encoding transition t90.18 (234/283).
Encoding transition t90.15 (235/283).
Encoding transition t48.24 (236/283).
Encoding transition t90.10 (237/283).
Encoding transition t99.9 (238/283).
Encoding transition t99.3 (239/283).
Encoding transition t48.16 (240/283).
Encoding transition t48.12 (241/283).
Encoding transition t81.27 (242/283).
Encoding transition t88.8 (243/283).
Encoding transition t88.4 (244/283).
Encoding transition t88.2 (245/283).
Encoding transition t72.36 (246/283).
Encoding transition t30.6 (247/283).
Encoding transition t30.5 (248/283).
Encoding transition t30.3 (249/283).
Encoding transition t30.2 (250/283).
Encoding transition t77.7 (251/283).
Encoding transition t39.13 (252/283).
Encoding transition t72.24 (253/283).
Encoding transition t72.18 (254/283).
Encoding transition t66.6 (255/283).
Encoding transition t72.12 (256/283).
Encoding transition t66.3 (257/283).
Encoding transition t66.2 (258/283).
Encoding transition t63.21 (259/283).
Encoding transition t55.5 (260/283).
Encoding transition t20.10 (261/283).
Encoding transition t44.4 (262/283).
Encoding transition t44.2 (263/283).
Encoding transition t54.27 (264/283).
Encoding transition t33.3 (265/283).
Encoding transition t88.44 (266/283).
Encoding transition t54.18 (267/283).
Encoding transition t22.2 (268/283).
Encoding transition t69.3 (269/283).
Encoding transition t88.22 (270/283).
Encoding transition t45.15 (271/283).
Encoding transition t88.11 (272/283).
Encoding transition t4.2 (273/283).
Encoding transition t58.2 (274/283).
Encoding transition t36.18 (275/283).
Encoding transition t36.12 (276/283).
Encoding transition t36.9 (277/283).
Encoding transition t36.6 (278/283).
Encoding transition t36.4 (279/283).
Encoding transition t36.3 (280/283).
Encoding transition t36.2 (281/283).
Encoding transition t60.30 (282/283).
----------------------------------------
End firing rule encoding
----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------
Total Used Memory: 3750112KB
RS size: -9223372036854775808 (1.88895e+22)
----------------------------------------
End RS generation
----------------------------------------
FORMULA Eratosthenes-PT-100-ReachabilityBounds-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-2 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-3 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-4 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-5 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-6 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-7 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-8 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-9 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Eratosthenes-PT-100-ReachabilityBounds-10 FALSE TECHNIQUES DECISION_DIAGRAMS
Ok.
BK_STOP 1400277312024
--------------------
content from stderr:
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="Eratosthenes-PT-100"
export BK_EXAMINATION="ReachabilityBounds"
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/Eratosthenes-PT-100.tgz
mv Eratosthenes-PT-100 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 Eratosthenes-PT-100, examination is ReachabilityBounds"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r01kn-qhx2-140025666001134"
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 ;