About the Execution
Execution Summary | ||||
Max Memory Used (MB) |
CPU Usage (ms) | I/O Wait (ms) | Competition Result | Execution Status |
5707.49 | 1348833 | 201.4 | 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-10, examination is ReachabilityDeadlock
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541701174
=====================================================================
--------------------
content from stdout:
BK_START 1400445656499
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running QuasiCertifProtocol (PT), instance 10
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityDeadlock.xml INTO /home/mcc/execution/ReachabilityDeadlock.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 10 -C -f /home/mcc/execution/ReachabilityDeadlock.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 malC1_5 (0/176).
Encoding transition malC1_6 (1/176).
Encoding transition malC1_3 (2/176).
Encoding transition malC1_4 (3/176).
Encoding transition malC1_1 (4/176).
Encoding transition malC1_2 (5/176).
Encoding transition malC1_0 (6/176).
Encoding transition malS6_3 (7/176).
Encoding transition malS6_2 (8/176).
Encoding transition malS6_1 (9/176).
Encoding transition malS6_0 (10/176).
Encoding transition malC1_10 (11/176).
Encoding transition malC1_9 (12/176).
Encoding transition malC1_8 (13/176).
Encoding transition malC1_7 (14/176).
Encoding transition malS5_0 (15/176).
Encoding transition malS6_10 (16/176).
Encoding transition malS6_9 (17/176).
Encoding transition malS6_8 (18/176).
Encoding transition malS6_7 (19/176).
Encoding transition malS6_6 (20/176).
Encoding transition malS6_5 (21/176).
Encoding transition malS6_4 (22/176).
Encoding transition malS2_2 (23/176).
Encoding transition malS2_3 (24/176).
Encoding transition malS2_0 (25/176).
Encoding transition malS2_1 (26/176).
Encoding transition malS2_6 (27/176).
Encoding transition malS2_7 (28/176).
Encoding transition malS2_4 (29/176).
Encoding transition malS2_5 (30/176).
Encoding transition malS2_10 (31/176).
Encoding transition malS1_0 (32/176).
Encoding transition malS2_8 (33/176).
Encoding transition malS2_9 (34/176).
Encoding transition malS1_3 (35/176).
Encoding transition malS1_4 (36/176).
Encoding transition malS1_1 (37/176).
Encoding transition malS1_2 (38/176).
Encoding transition malS1_8 (39/176).
Encoding transition malS1_7 (40/176).
Encoding transition malS1_6 (41/176).
Encoding transition malS1_5 (42/176).
Encoding transition malA3 (43/176).
Encoding transition malA5 (44/176).
Encoding transition malS1_10 (45/176).
Encoding transition malS1_9 (46/176).
Encoding transition CgenCertif_0 (47/176).
Encoding transition malA1 (48/176).
Encoding transition malA2 (49/176).
Encoding transition malA4 (50/176).
Encoding transition CgenCertif_4 (51/176).
Encoding transition CgenCertif_3 (52/176).
Encoding transition CgenCertif_2 (53/176).
Encoding transition CgenCertif_1 (54/176).
Encoding transition malS5_1 (55/176).
Encoding transition malS5_2 (56/176).
Encoding transition malS5_3 (57/176).
Encoding transition malS5_4 (58/176).
Encoding transition malS5_5 (59/176).
Encoding transition malS5_6 (60/176).
Encoding transition malS5_7 (61/176).
Encoding transition malS5_8 (62/176).
Encoding transition malS5_9 (63/176).
Encoding transition malS5_10 (64/176).
Encoding transition malS4_0 (65/176).
Encoding transition malS4_1 (66/176).
Encoding transition malS4_2 (67/176).
Encoding transition malS4_3 (68/176).
Encoding transition malS4_4 (69/176).
Encoding transition malS4_5 (70/176).
Encoding transition malS4_7 (71/176).
Encoding transition malS4_6 (72/176).
Encoding transition malS4_9 (73/176).
Encoding transition malS4_8 (74/176).
Encoding transition malS3_0 (75/176).
Encoding transition malS4_10 (76/176).
Encoding transition malS3_2 (77/176).
Encoding transition malS3_1 (78/176).
Encoding transition malS3_4 (79/176).
Encoding transition malS3_3 (80/176).
Encoding transition malS3_6 (81/176).
Encoding transition malS3_5 (82/176).
Encoding transition malS3_8 (83/176).
Encoding transition malS3_7 (84/176).
Encoding transition malS3_10 (85/176).
Encoding transition malS3_9 (86/176).
Encoding transition Sperform_8 (87/176).
Encoding transition Sperform_7 (88/176).
Encoding transition Sperform_6 (89/176).
Encoding transition Sperform_5 (90/176).
Encoding transition Sperform_4 (91/176).
Encoding transition Sperform_3 (92/176).
Encoding transition Sperform_2 (93/176).
Encoding transition Sperform_1 (94/176).
Encoding transition Sperform_0 (95/176).
Encoding transition SackCS_10 (96/176).
Encoding transition SackCS_9 (97/176).
Encoding transition SackCS_8 (98/176).
Encoding transition SackCS_7 (99/176).
Encoding transition SackCS_6 (100/176).
Encoding transition SackCS_5 (101/176).
Encoding transition SackCS_4 (102/176).
Encoding transition SgetTS_1 (103/176).
Encoding transition SgetTS_2 (104/176).
Encoding transition SreqTS_10 (105/176).
Encoding transition SgetTS_0 (106/176).
Encoding transition SreqTS_8 (107/176).
Encoding transition SreqTS_9 (108/176).
Encoding transition SreqTS_6 (109/176).
Encoding transition SreqTS_7 (110/176).
Encoding transition SreqTS_4 (111/176).
Encoding transition SreqTS_5 (112/176).
Encoding transition SreqTS_2 (113/176).
Encoding transition SreqTS_3 (114/176).
Encoding transition SreqTS_0 (115/176).
Encoding transition SreqTS_1 (116/176).
Encoding transition Sperform_9 (117/176).
Encoding transition Sperform_10 (118/176).
Encoding transition CsendTS1_7 (119/176).
Encoding transition CsendTS1_6 (120/176).
Encoding transition CsendTS1_9 (121/176).
Encoding transition CsendTS1_8 (122/176).
Encoding transition CsendTS1_3 (123/176).
Encoding transition CsendTS1_2 (124/176).
Encoding transition CsendTS1_5 (125/176).
Encoding transition CsendTS1_4 (126/176).
Encoding transition CgenCertif_10 (127/176).
Encoding transition CgenCertif_9 (128/176).
Encoding transition CsendTS1_1 (129/176).
Encoding transition CsendTS1_0 (130/176).
Encoding transition CgenCertif_6 (131/176).
Encoding transition CgenCertif_5 (132/176).
Encoding transition CgenCertif_8 (133/176).
Encoding transition CgenCertif_7 (134/176).
Encoding transition SackCS_0 (135/176).
Encoding transition SackCS_1 (136/176).
Encoding transition SackCS_2 (137/176).
Encoding transition SackCS_3 (138/176).
Encoding transition SsendTS_7 (139/176).
Encoding transition SsendTS_8 (140/176).
Encoding transition SsendTS_9 (141/176).
Encoding transition SsendTS_10 (142/176).
Encoding transition SsendTS_3 (143/176).
Encoding transition SsendTS_4 (144/176).
Encoding transition SsendTS_5 (145/176).
Encoding transition SsendTS_6 (146/176).
Encoding transition CsendTS1_10 (147/176).
Encoding transition SsendTS_0 (148/176).
Encoding transition SsendTS_1 (149/176).
Encoding transition SsendTS_2 (150/176).
Encoding transition ScertCS_1 (151/176).
Encoding transition ScertCS_0 (152/176).
Encoding transition ScertCS_3 (153/176).
Encoding transition ScertCS_2 (154/176).
Encoding transition ScertCS_5 (155/176).
Encoding transition ScertCS_4 (156/176).
Encoding transition ScertCS_7 (157/176).
Encoding transition ScertCS_6 (158/176).
Encoding transition SgetTS_4 (159/176).
Encoding transition SgetTS_3 (160/176).
Encoding transition SgetTS_6 (161/176).
Encoding transition SgetTS_5 (162/176).
Encoding transition SgetTS_8 (163/176).
Encoding transition SgetTS_7 (164/176).
Encoding transition SgetTS_10 (165/176).
Encoding transition SgetTS_9 (166/176).
Encoding transition AreqTS (167/176).
Encoding transition ScertCS_8 (168/176).
Encoding transition ScertCS_9 (169/176).
Encoding transition ScertCS_10 (170/176).
Encoding transition AendCS (171/176).
Encoding transition AstartCS (172/176).
Encoding transition AackCS (173/176).
Encoding transition AreqCS (174/176).
Encoding transition AgetTS (175/176).
----------------------------------------
End firing rule encoding
----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------
Total Used Memory: 82924KB
CANNOT_COMPUTE
BK_STOP 1400447006249
--------------------
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-10"
export BK_EXAMINATION="ReachabilityDeadlock"
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-10.tgz
mv QuasiCertifProtocol-PT-10 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-10, examination is ReachabilityDeadlock"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541701174"
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 ;