fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r04kn-qhx2-140043541701256
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
4052.84 1134994 212.2 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 Railroad-PT-010, examination is CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541701256
=====================================================================


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

BK_START 1400449158868
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Railroad (PT), instance 010
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/CTLCardinality.xml INTO /home/mcc/execution/CTLCardinality.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLCardinality.rgmedd-ctl
Using FORCE-PINV Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition tr_T0_1 (0/156).
Encoding transition tr_T10_1 (1/156).
Encoding transition tr_T11_1 (2/156).
Encoding transition tr_T12_1 (3/156).
Encoding transition tr_T13_1 (4/156).
Encoding transition tr_T14_12 (5/156).
Encoding transition tr_T14_13 (6/156).
Encoding transition tr_T14_14 (7/156).
Encoding transition tr_T14_15 (8/156).
Encoding transition tr_T14_16 (9/156).
Encoding transition tr_T14_17 (10/156).
Encoding transition tr_T14_18 (11/156).
Encoding transition tr_T14_19 (12/156).
Encoding transition tr_T14_20 (13/156).
Encoding transition tr_T14_21 (14/156).
Encoding transition tr_T14_22 (15/156).
Encoding transition tr_T15_1 (16/156).
Encoding transition tr_T16_1 (17/156).
Encoding transition tr_T17_1 (18/156).
Encoding transition tr_T18_1 (19/156).
Encoding transition tr_T19_1 (20/156).
Encoding transition tr_T1_1 (21/156).
Encoding transition tr_T20_1 (22/156).
Encoding transition tr_T21_1 (23/156).
Encoding transition tr_T22_1 (24/156).
Encoding transition tr_T23_1 (25/156).
Encoding transition tr_T24_1 (26/156).
Encoding transition tr_T25_1 (27/156).
Encoding transition tr_T26_1 (28/156).
Encoding transition tr_T27_1 (29/156).
Encoding transition tr_T28_1 (30/156).
Encoding transition tr_T29_1 (31/156).
Encoding transition tr_T2_1 (32/156).
Encoding transition tr_T30_1 (33/156).
Encoding transition tr_T31_1 (34/156).
Encoding transition tr_T32_1 (35/156).
Encoding transition tr_T33_100 (36/156).
Encoding transition tr_T33_101 (37/156).
Encoding transition tr_T33_102 (38/156).
Encoding transition tr_T33_103 (39/156).
Encoding transition tr_T33_104 (40/156).
Encoding transition tr_T33_105 (41/156).
Encoding transition tr_T33_106 (42/156).
Encoding transition tr_T33_107 (43/156).
Encoding transition tr_T33_108 (44/156).
Encoding transition tr_T33_109 (45/156).
Encoding transition tr_T33_110 (46/156).
Encoding transition tr_T33_111 (47/156).
Encoding transition tr_T33_112 (48/156).
Encoding transition tr_T33_113 (49/156).
Encoding transition tr_T33_114 (50/156).
Encoding transition tr_T33_115 (51/156).
Encoding transition tr_T33_116 (52/156).
Encoding transition tr_T33_117 (53/156).
Encoding transition tr_T33_118 (54/156).
Encoding transition tr_T33_119 (55/156).
Encoding transition tr_T33_120 (56/156).
Encoding transition tr_T33_121 (57/156).
Encoding transition tr_T33_23 (58/156).
Encoding transition tr_T33_24 (59/156).
Encoding transition tr_T33_25 (60/156).
Encoding transition tr_T33_26 (61/156).
Encoding transition tr_T33_27 (62/156).
Encoding transition tr_T33_28 (63/156).
Encoding transition tr_T33_29 (64/156).
Encoding transition tr_T33_30 (65/156).
Encoding transition tr_T33_31 (66/156).
Encoding transition tr_T33_32 (67/156).
Encoding transition tr_T33_33 (68/156).
Encoding transition tr_T33_34 (69/156).
Encoding transition tr_T33_35 (70/156).
Encoding transition tr_T33_36 (71/156).
Encoding transition tr_T33_37 (72/156).
Encoding transition tr_T33_38 (73/156).
Encoding transition tr_T33_39 (74/156).
Encoding transition tr_T33_40 (75/156).
Encoding transition tr_T33_41 (76/156).
Encoding transition tr_T33_42 (77/156).
Encoding transition tr_T33_43 (78/156).
Encoding transition tr_T33_44 (79/156).
Encoding transition tr_T33_45 (80/156).
Encoding transition tr_T33_46 (81/156).
Encoding transition tr_T33_47 (82/156).
Encoding transition tr_T33_48 (83/156).
Encoding transition tr_T33_49 (84/156).
Encoding transition tr_T33_50 (85/156).
Encoding transition tr_T33_51 (86/156).
Encoding transition tr_T33_52 (87/156).
Encoding transition tr_T33_53 (88/156).
Encoding transition tr_T33_54 (89/156).
Encoding transition tr_T33_55 (90/156).
Encoding transition tr_T33_56 (91/156).
Encoding transition tr_T33_57 (92/156).
Encoding transition tr_T33_58 (93/156).
Encoding transition tr_T33_59 (94/156).
Encoding transition tr_T33_60 (95/156).
Encoding transition tr_T33_61 (96/156).
Encoding transition tr_T33_62 (97/156).
Encoding transition tr_T33_63 (98/156).
Encoding transition tr_T33_64 (99/156).
Encoding transition tr_T33_65 (100/156).
Encoding transition tr_T33_66 (101/156).
Encoding transition tr_T33_67 (102/156).
Encoding transition tr_T33_68 (103/156).
Encoding transition tr_T33_69 (104/156).
Encoding transition tr_T33_70 (105/156).
Encoding transition tr_T33_71 (106/156).
Encoding transition tr_T33_72 (107/156).
Encoding transition tr_T33_73 (108/156).
Encoding transition tr_T33_74 (109/156).
Encoding transition tr_T33_75 (110/156).
Encoding transition tr_T33_76 (111/156).
Encoding transition tr_T33_77 (112/156).
Encoding transition tr_T33_78 (113/156).
Encoding transition tr_T33_79 (114/156).
Encoding transition tr_T33_80 (115/156).
Encoding transition tr_T33_81 (116/156).
Encoding transition tr_T33_82 (117/156).
Encoding transition tr_T33_83 (118/156).
Encoding transition tr_T33_84 (119/156).
Encoding transition tr_T33_85 (120/156).
Encoding transition tr_T33_86 (121/156).
Encoding transition tr_T33_87 (122/156).
Encoding transition tr_T33_88 (123/156).
Encoding transition tr_T33_89 (124/156).
Encoding transition tr_T33_90 (125/156).
Encoding transition tr_T33_91 (126/156).
Encoding transition tr_T33_92 (127/156).
Encoding transition tr_T33_93 (128/156).
Encoding transition tr_T33_94 (129/156).
Encoding transition tr_T33_95 (130/156).
Encoding transition tr_T33_96 (131/156).
Encoding transition tr_T33_97 (132/156).
Encoding transition tr_T33_98 (133/156).
Encoding transition tr_T33_99 (134/156).
Encoding transition tr_T34_1 (135/156).
Encoding transition tr_T35_1 (136/156).
Encoding transition tr_T36_1 (137/156).
Encoding transition tr_T37_10 (138/156).
Encoding transition tr_T37_2 (139/156).
Encoding transition tr_T37_3 (140/156).
Encoding transition tr_T37_4 (141/156).
Encoding transition tr_T37_5 (142/156).
Encoding transition tr_T37_6 (143/156).
Encoding transition tr_T37_7 (144/156).
Encoding transition tr_T37_8 (145/156).
Encoding transition tr_T37_9 (146/156).
Encoding transition tr_T38_1 (147/156).
Encoding transition tr_T39_1 (148/156).
Encoding transition tr_T3_1 (149/156).
Encoding transition tr_T4_1 (150/156).
Encoding transition tr_T5_1 (151/156).
Encoding transition tr_T6_1 (152/156).
Encoding transition tr_T7_1 (153/156).
Encoding transition tr_T8_1 (154/156).
Encoding transition tr_T9_1 (155/156).
----------------------------------------
End firing rule encoding

----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------

Total Used Memory: 12680KB
CANNOT_COMPUTE

BK_STOP 1400450294441

--------------------
content from stderr:

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="Railroad-PT-010"
export BK_EXAMINATION="CTLCardinality"
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/Railroad-PT-010.tgz
mv Railroad-PT-010 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 Railroad-PT-010, examination is CTLCardinality"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541701256"
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 ;