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 ;