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-1668
Executing tool greatspn
Input is ResAllocation-PT-R003C100, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r05kn-ovh1-140043890501050
=====================================================================

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

BK_START 1400453040315
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running ResAllocation (PT), instance R003C100
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/CTLFireability.xml INTO /home/mcc/execution/CTLFireability.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -P -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLFireability.rgmedd-ctl
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition t_18_3 (0/400).
Encoding transition t_18_2 (1/400).
Encoding transition t_18_1 (2/400).
Encoding transition t_18_0 (3/400).
Encoding transition t_60_3 (4/400).
Encoding transition t_60_2 (5/400).
Encoding transition t_60_1 (6/400).
Encoding transition t_60_0 (7/400).
Encoding transition t_1_3 (8/400).
Encoding transition t_1_2 (9/400).
Encoding transition t_1_1 (10/400).
Encoding transition t_1_0 (11/400).
Encoding transition t_99_3 (12/400).
Encoding transition t_99_2 (13/400).
Encoding transition t_99_1 (14/400).
Encoding transition t_99_0 (15/400).
Encoding transition t_88_3 (16/400).
Encoding transition t_88_2 (17/400).
Encoding transition t_88_1 (18/400).
Encoding transition t_88_0 (19/400).
Encoding transition t_77_3 (20/400).
Encoding transition t_77_2 (21/400).
Encoding transition t_77_1 (22/400).
Encoding transition t_77_0 (23/400).
Encoding transition t_66_3 (24/400).
Encoding transition t_66_2 (25/400).
Encoding transition t_66_1 (26/400).
Encoding transition t_66_0 (27/400).
Encoding transition t_55_3 (28/400).
Encoding transition t_55_2 (29/400).
Encoding transition t_55_1 (30/400).
Encoding transition t_55_0 (31/400).
Encoding transition t_44_3 (32/400).
Encoding transition t_44_2 (33/400).
Encoding transition t_44_1 (34/400).
Encoding transition t_44_0 (35/400).
Encoding transition t_33_3 (36/400).
Encoding transition t_33_2 (37/400).
Encoding transition t_33_1 (38/400).
Encoding transition t_33_0 (39/400).
Encoding transition t_22_3 (40/400).
Encoding transition t_22_2 (41/400).
Encoding transition t_22_1 (42/400).
Encoding transition t_22_0 (43/400).
Encoding transition t_7_3 (44/400).
Encoding transition t_7_2 (45/400).
Encoding transition t_7_1 (46/400).
Encoding transition t_7_0 (47/400).
Encoding transition t_11_3 (48/400).
Encoding transition t_11_2 (49/400).
Encoding transition t_11_1 (50/400).
Encoding transition t_11_0 (51/400).
Encoding transition t_92_3 (52/400).
Encoding transition t_92_2 (53/400).
Encoding transition t_92_1 (54/400).
Encoding transition t_92_0 (55/400).
Encoding transition t_39_3 (56/400).
Encoding transition t_39_2 (57/400).
Encoding transition t_39_1 (58/400).
Encoding transition t_39_0 (59/400).
Encoding transition t_81_3 (60/400).
Encoding transition t_81_2 (61/400).
Encoding transition t_81_1 (62/400).
Encoding transition t_81_0 (63/400).
Encoding transition t_28_3 (64/400).
Encoding transition t_28_2 (65/400).
Encoding transition t_28_1 (66/400).
Encoding transition t_28_0 (67/400).
Encoding transition t_70_3 (68/400).
Encoding transition t_70_2 (69/400).
Encoding transition t_70_1 (70/400).
Encoding transition t_70_0 (71/400).
Encoding transition t_17_3 (72/400).
Encoding transition t_17_2 (73/400).
Encoding transition t_17_1 (74/400).
Encoding transition t_17_0 (75/400).
Encoding transition t_0_3 (76/400).
Encoding transition t_0_2 (77/400).
Encoding transition t_0_1 (78/400).
Encoding transition t_0_0 (79/400).
Encoding transition t_98_3 (80/400).
Encoding transition t_98_2 (81/400).
Encoding transition t_98_1 (82/400).
Encoding transition t_98_0 (83/400).
Encoding transition t_87_3 (84/400).
Encoding transition t_87_2 (85/400).
Encoding transition t_87_1 (86/400).
Encoding transition t_87_0 (87/400).
Encoding transition t_76_3 (88/400).
Encoding transition t_76_2 (89/400).
Encoding transition t_76_1 (90/400).
Encoding transition t_76_0 (91/400).
Encoding transition t_65_3 (92/400).
Encoding transition t_65_2 (93/400).
Encoding transition t_65_1 (94/400).
Encoding transition t_65_0 (95/400).
Encoding transition t_54_3 (96/400).
Encoding transition t_54_2 (97/400).
Encoding transition t_54_1 (98/400).
Encoding transition t_54_0 (99/400).
Encoding transition t_43_3 (100/400).
Encoding transition t_43_2 (101/400).
Encoding transition t_43_1 (102/400).
Encoding transition t_43_0 (103/400).
Encoding transition t_32_3 (104/400).
Encoding transition t_32_2 (105/400).
Encoding transition t_32_1 (106/400).
Encoding transition t_32_0 (107/400).
Encoding transition t_21_3 (108/400).
Encoding transition t_21_2 (109/400).
Encoding transition t_21_1 (110/400).
Encoding transition t_21_0 (111/400).
Encoding transition t_6_3 (112/400).
Encoding transition t_6_2 (113/400).
Encoding transition t_6_1 (114/400).
Encoding transition t_6_0 (115/400).
Encoding transition t_10_3 (116/400).
Encoding transition t_10_2 (117/400).
Encoding transition t_10_1 (118/400).
Encoding transition t_10_0 (119/400).
Encoding transition t_49_3 (120/400).
Encoding transition t_49_2 (121/400).
Encoding transition t_49_1 (122/400).
Encoding transition t_49_0 (123/400).
Encoding transition t_91_3 (124/400).
Encoding transition t_91_2 (125/400).
Encoding transition t_91_1 (126/400).
Encoding transition t_91_0 (127/400).
Encoding transition t_38_3 (128/400).
Encoding transition t_38_2 (129/400).
Encoding transition t_38_1 (130/400).
Encoding transition t_38_0 (131/400).
Encoding transition t_80_3 (132/400).
Encoding transition t_80_2 (133/400).
Encoding transition t_80_1 (134/400).
Encoding transition t_80_0 (135/400).
Encoding transition t_27_3 (136/400).
Encoding transition t_27_2 (137/400).
Encoding transition t_27_1 (138/400).
Encoding transition t_27_0 (139/400).
Encoding transition t_16_3 (140/400).
Encoding transition t_16_2 (141/400).
Encoding transition t_16_1 (142/400).
Encoding transition t_16_0 (143/400).
Encoding transition t_97_3 (144/400).
Encoding transition t_97_2 (145/400).
Encoding transition t_97_1 (146/400).
Encoding transition t_97_0 (147/400).
Encoding transition t_86_3 (148/400).
Encoding transition t_86_2 (149/400).
Encoding transition t_86_1 (150/400).
Encoding transition t_86_0 (151/400).
Encoding transition t_75_3 (152/400).
Encoding transition t_75_2 (153/400).
Encoding transition t_75_1 (154/400).
Encoding transition t_75_0 (155/400).
Encoding transition t_64_3 (156/400).
Encoding transition t_64_2 (157/400).
Encoding transition t_64_1 (158/400).
Encoding transition t_64_0 (159/400).
Encoding transition t_53_3 (160/400).
Encoding transition t_53_2 (161/400).
Encoding transition t_53_1 (162/400).
Encoding transition t_53_0 (163/400).
Encoding transition t_42_3 (164/400).
Encoding transition t_42_2 (165/400).
Encoding transition t_42_1 (166/400).
Encoding transition t_42_0 (167/400).
Encoding transition t_31_3 (168/400).
Encoding transition t_31_2 (169/400).
Encoding transition t_31_1 (170/400).
Encoding transition t_31_0 (171/400).
Encoding transition t_20_3 (172/400).
Encoding transition t_20_2 (173/400).
Encoding transition t_20_1 (174/400).
Encoding transition t_20_0 (175/400).
Encoding transition t_5_3 (176/400).
Encoding transition t_5_2 (177/400).
Encoding transition t_5_1 (178/400).
Encoding transition t_5_0 (179/400).
Encoding transition t_59_3 (180/400).
Encoding transition t_59_2 (181/400).
Encoding transition t_59_1 (182/400).
Encoding transition t_59_0 (183/400).
Encoding transition t_48_3 (184/400).
Encoding transition t_48_2 (185/400).
Encoding transition t_48_1 (186/400).
Encoding transition t_48_0 (187/400).
Encoding transition t_90_3 (188/400).
Encoding transition t_90_2 (189/400).
Encoding transition t_90_1 (190/400).
Encoding transition t_90_0 (191/400).
Encoding transition t_37_3 (192/400).
Encoding transition t_37_2 (193/400).
Encoding transition t_37_1 (194/400).
Encoding transition t_37_0 (195/400).
Encoding transition t_26_3 (196/400).
Encoding transition t_26_2 (197/400).
Encoding transition t_26_1 (198/400).
Encoding transition t_26_0 (199/400).
Encoding transition t_15_3 (200/400).
Encoding transition t_15_2 (201/400).
Encoding transition t_15_1 (202/400).
Encoding transition t_15_0 (203/400).
Encoding transition t_96_3 (204/400).
Encoding transition t_96_2 (205/400).
Encoding transition t_96_1 (206/400).
Encoding transition t_96_0 (207/400).
Encoding transition t_85_3 (208/400).
Encoding transition t_85_2 (209/400).
Encoding transition t_85_1 (210/400).
Encoding transition t_85_0 (211/400).
Encoding transition t_74_3 (212/400).
Encoding transition t_74_2 (213/400).
Encoding transition t_74_1 (214/400).
Encoding transition t_74_0 (215/400).
Encoding transition t_63_3 (216/400).
Encoding transition t_63_2 (217/400).
Encoding transition t_63_1 (218/400).
Encoding transition t_63_0 (219/400).
Encoding transition t_52_3 (220/400).
Encoding transition t_52_2 (221/400).
Encoding transition t_52_1 (222/400).
Encoding transition t_52_0 (223/400).
Encoding transition t_41_3 (224/400).
Encoding transition t_41_2 (225/400).
Encoding transition t_41_1 (226/400).
Encoding transition t_41_0 (227/400).
Encoding transition t_30_3 (228/400).
Encoding transition t_30_2 (229/400).
Encoding transition t_30_1 (230/400).
Encoding transition t_30_0 (231/400).
Encoding transition t_4_3 (232/400).
Encoding transition t_4_2 (233/400).
Encoding transition t_4_1 (234/400).
Encoding transition t_4_0 (235/400).
Encoding transition t_69_3 (236/400).
Encoding transition t_69_2 (237/400).
Encoding transition t_69_1 (238/400).
Encoding transition t_69_0 (239/400).
Encoding transition t_58_3 (240/400).
Encoding transition t_58_2 (241/400).
Encoding transition t_58_1 (242/400).
Encoding transition t_58_0 (243/400).
Encoding transition t_47_3 (244/400).
Encoding transition t_47_2 (245/400).
Encoding transition t_47_1 (246/400).
Encoding transition t_47_0 (247/400).
Encoding transition t_36_3 (248/400).
Encoding transition t_36_2 (249/400).
Encoding transition t_36_1 (250/400).
Encoding transition t_36_0 (251/400).
Encoding transition t_25_3 (252/400).
Encoding transition t_25_2 (253/400).
Encoding transition t_25_1 (254/400).
Encoding transition t_25_0 (255/400).
Encoding transition t_14_3 (256/400).
Encoding transition t_14_2 (257/400).
Encoding transition t_14_1 (258/400).
Encoding transition t_14_0 (259/400).
Encoding transition t_95_3 (260/400).
Encoding transition t_95_2 (261/400).
Encoding transition t_95_1 (262/400).
Encoding transition t_95_0 (263/400).
Encoding transition t_84_3 (264/400).
Encoding transition t_84_2 (265/400).
Encoding transition t_84_1 (266/400).
Encoding transition t_84_0 (267/400).
Encoding transition t_73_3 (268/400).
Encoding transition t_73_2 (269/400).
Encoding transition t_73_1 (270/400).
Encoding transition t_73_0 (271/400).
Encoding transition t_62_3 (272/400).
Encoding transition t_62_2 (273/400).
Encoding transition t_62_1 (274/400).
Encoding transition t_62_0 (275/400).
Encoding transition t_51_3 (276/400).
Encoding transition t_51_2 (277/400).
Encoding transition t_51_1 (278/400).
Encoding transition t_51_0 (279/400).
Encoding transition t_40_3 (280/400).
Encoding transition t_40_2 (281/400).
Encoding transition t_40_1 (282/400).
Encoding transition t_40_0 (283/400).
Encoding transition t_3_3 (284/400).
Encoding transition t_3_2 (285/400).
Encoding transition t_3_1 (286/400).
Encoding transition t_3_0 (287/400).
Encoding transition t_79_3 (288/400).
Encoding transition t_79_2 (289/400).
Encoding transition t_79_1 (290/400).
Encoding transition t_79_0 (291/400).
Encoding transition t_68_3 (292/400).
Encoding transition t_68_2 (293/400).
Encoding transition t_68_1 (294/400).
Encoding transition t_68_0 (295/400).
Encoding transition t_57_3 (296/400).
Encoding transition t_57_2 (297/400).
Encoding transition t_57_1 (298/400).
Encoding transition t_57_0 (299/400).
Encoding transition t_46_3 (300/400).
Encoding transition t_46_2 (301/400).
Encoding transition t_46_1 (302/400).
Encoding transition t_46_0 (303/400).
Encoding transition t_35_3 (304/400).
Encoding transition t_35_2 (305/400).
Encoding transition t_35_1 (306/400).
Encoding transition t_35_0 (307/400).
Encoding transition t_24_3 (308/400).
Encoding transition t_24_2 (309/400).
Encoding transition t_24_1 (310/400).
Encoding transition t_24_0 (311/400).
Encoding transition t_9_3 (312/400).
Encoding transition t_9_2 (313/400).
Encoding transition t_9_1 (314/400).
Encoding transition t_9_0 (315/400).
Encoding transition t_13_3 (316/400).
Encoding transition t_13_2 (317/400).
Encoding transition t_13_1 (318/400).
Encoding transition t_13_0 (319/400).
Encoding transition t_94_3 (320/400).
Encoding transition t_94_2 (321/400).
Encoding transition t_94_1 (322/400).
Encoding transition t_94_0 (323/400).
Encoding transition t_83_3 (324/400).
Encoding transition t_83_2 (325/400).
Encoding transition t_83_1 (326/400).
Encoding transition t_83_0 (327/400).
Encoding transition t_72_3 (328/400).
Encoding transition t_72_2 (329/400).
Encoding transition t_72_1 (330/400).
Encoding transition t_72_0 (331/400).
Encoding transition t_19_3 (332/400).
Encoding transition t_19_2 (333/400).
Encoding transition t_19_1 (334/400).
Encoding transition t_19_0 (335/400).
Encoding transition t_61_3 (336/400).
Encoding transition t_61_2 (337/400).
Encoding transition t_61_1 (338/400).
Encoding transition t_61_0 (339/400).
Encoding transition t_50_3 (340/400).
Encoding transition t_50_2 (341/400).
Encoding transition t_50_1 (342/400).
Encoding transition t_50_0 (343/400).
Encoding transition t_2_3 (344/400).
Encoding transition t_2_2 (345/400).
Encoding transition t_2_1 (346/400).
Encoding transition t_2_0 (347/400).
Encoding transition t_89_3 (348/400).
Encoding transition t_89_2 (349/400).
Encoding transition t_89_1 (350/400).
Encoding transition t_89_0 (351/400).
Encoding transition t_78_3 (352/400).
Encoding transition t_78_2 (353/400).
Encoding transition t_78_1 (354/400).
Encoding transition t_78_0 (355/400).
Encoding transition t_67_3 (356/400).
Encoding transition t_67_2 (357/400).
Encoding transition t_67_1 (358/400).
Encoding transition t_67_0 (359/400).
Encoding transition t_56_3 (360/400).
Encoding transition t_56_2 (361/400).
Encoding transition t_56_1 (362/400).
Encoding transition t_56_0 (363/400).
Encoding transition t_45_3 (364/400).
Encoding transition t_45_2 (365/400).
Encoding transition t_45_1 (366/400).
Encoding transition t_45_0 (367/400).
Encoding transition t_34_3 (368/400).
Encoding transition t_34_2 (369/400).
Encoding transition t_34_1 (370/400).
Encoding transition t_34_0 (371/400).
Encoding transition t_23_3 (372/400).
Encoding transition t_23_2 (373/400).
Encoding transition t_23_1 (374/400).
Encoding transition t_23_0 (375/400).
Encoding transition t_8_3 (376/400).
Encoding transition t_8_2 (377/400).
Encoding transition t_8_1 (378/400).
Encoding transition t_8_0 (379/400).
Encoding transition t_12_3 (380/400).
Encoding transition t_12_2 (381/400).
Encoding transition t_12_1 (382/400).
Encoding transition t_12_0 (383/400).
Encoding transition t_93_3 (384/400).
Encoding transition t_93_2 (385/400).
Encoding transition t_93_1 (386/400).
Encoding transition t_93_0 (387/400).
Encoding transition t_82_3 (388/400).
Encoding transition t_82_2 (389/400).
Encoding transition t_82_1 (390/400).
Encoding transition t_82_0 (391/400).
Encoding transition t_29_3 (392/400).
Encoding transition t_29_2 (393/400).
Encoding transition t_29_1 (394/400).
Encoding transition t_29_0 (395/400).
Encoding transition t_71_3 (396/400).
Encoding transition t_71_2 (397/400).
Encoding transition t_71_1 (398/400).
Encoding transition t_71_0 (399/400).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 29560KB
CANNOT_COMPUTE

BK_STOP 1400453580691

--------------------
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="ResAllocation-PT-R003C100"
export BK_EXAMINATION="CTLFireability"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/srv/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/ResAllocation-PT-R003C100.tgz
mv ResAllocation-PT-R003C100 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is ResAllocation-PT-R003C100, examination is CTLFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r05kn-ovh1-140043890501050"
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 ;