fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r04kn-qhx2-140043541400866
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
4455.63 1296064 146.7 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 Philosophers-PT-000050, examination is CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541400866
=====================================================================


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

BK_START 1400438247801
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Philosophers (PT), instance 000050
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 -P -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLCardinality.rgmedd-ctl
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition End_2 (0/250).
Encoding transition End_3 (1/250).
Encoding transition End_1 (2/250).
Encoding transition End_23 (3/250).
Encoding transition End_22 (4/250).
Encoding transition End_21 (5/250).
Encoding transition End_20 (6/250).
Encoding transition End_27 (7/250).
Encoding transition End_26 (8/250).
Encoding transition End_25 (9/250).
Encoding transition End_24 (10/250).
Encoding transition End_31 (11/250).
Encoding transition End_30 (12/250).
Encoding transition End_29 (13/250).
Encoding transition End_28 (14/250).
Encoding transition End_35 (15/250).
Encoding transition End_34 (16/250).
Encoding transition End_33 (17/250).
Encoding transition End_32 (18/250).
Encoding transition End_6 (19/250).
Encoding transition End_7 (20/250).
Encoding transition End_4 (21/250).
Encoding transition End_5 (22/250).
Encoding transition End_10 (23/250).
Encoding transition End_11 (24/250).
Encoding transition End_8 (25/250).
Encoding transition End_9 (26/250).
Encoding transition End_14 (27/250).
Encoding transition End_15 (28/250).
Encoding transition End_12 (29/250).
Encoding transition End_13 (30/250).
Encoding transition End_18 (31/250).
Encoding transition End_19 (32/250).
Encoding transition End_16 (33/250).
Encoding transition End_17 (34/250).
Encoding transition FF2b_3 (35/250).
Encoding transition FF2b_2 (36/250).
Encoding transition FF2b_5 (37/250).
Encoding transition FF2b_4 (38/250).
Encoding transition FF2b_7 (39/250).
Encoding transition FF2b_6 (40/250).
Encoding transition FF2b_9 (41/250).
Encoding transition FF2b_8 (42/250).
Encoding transition FF2b_11 (43/250).
Encoding transition FF2b_10 (44/250).
Encoding transition FF2b_13 (45/250).
Encoding transition FF2b_12 (46/250).
Encoding transition FF2b_15 (47/250).
Encoding transition FF2b_14 (48/250).
Encoding transition FF2b_17 (49/250).
Encoding transition FF2b_16 (50/250).
Encoding transition End_36 (51/250).
Encoding transition End_37 (52/250).
Encoding transition End_38 (53/250).
Encoding transition End_39 (54/250).
Encoding transition End_40 (55/250).
Encoding transition End_41 (56/250).
Encoding transition End_42 (57/250).
Encoding transition End_43 (58/250).
Encoding transition End_44 (59/250).
Encoding transition End_45 (60/250).
Encoding transition End_46 (61/250).
Encoding transition End_47 (62/250).
Encoding transition End_48 (63/250).
Encoding transition End_49 (64/250).
Encoding transition End_50 (65/250).
Encoding transition FF2b_1 (66/250).
Encoding transition FF2b_41 (67/250).
Encoding transition FF2b_40 (68/250).
Encoding transition FF2b_39 (69/250).
Encoding transition FF2b_38 (70/250).
Encoding transition FF2b_37 (71/250).
Encoding transition FF2b_36 (72/250).
Encoding transition FF2b_35 (73/250).
Encoding transition FF2b_34 (74/250).
Encoding transition FF2b_49 (75/250).
Encoding transition FF2b_48 (76/250).
Encoding transition FF2b_47 (77/250).
Encoding transition FF2b_46 (78/250).
Encoding transition FF2b_45 (79/250).
Encoding transition FF2b_44 (80/250).
Encoding transition FF2b_43 (81/250).
Encoding transition FF2b_42 (82/250).
Encoding transition FF2b_24 (83/250).
Encoding transition FF2b_25 (84/250).
Encoding transition FF2b_22 (85/250).
Encoding transition FF2b_23 (86/250).
Encoding transition FF2b_20 (87/250).
Encoding transition FF2b_21 (88/250).
Encoding transition FF2b_18 (89/250).
Encoding transition FF2b_19 (90/250).
Encoding transition FF2b_32 (91/250).
Encoding transition FF2b_33 (92/250).
Encoding transition FF2b_30 (93/250).
Encoding transition FF2b_31 (94/250).
Encoding transition FF2b_28 (95/250).
Encoding transition FF2b_29 (96/250).
Encoding transition FF2b_26 (97/250).
Encoding transition FF2b_27 (98/250).
Encoding transition FF2a_21 (99/250).
Encoding transition FF2a_20 (100/250).
Encoding transition FF2a_23 (101/250).
Encoding transition FF2a_22 (102/250).
Encoding transition FF2a_17 (103/250).
Encoding transition FF2a_16 (104/250).
Encoding transition FF2a_19 (105/250).
Encoding transition FF2a_18 (106/250).
Encoding transition FF2a_29 (107/250).
Encoding transition FF2a_28 (108/250).
Encoding transition FF2a_31 (109/250).
Encoding transition FF2a_30 (110/250).
Encoding transition FF2a_25 (111/250).
Encoding transition FF2a_24 (112/250).
Encoding transition FF2a_27 (113/250).
Encoding transition FF2a_26 (114/250).
Encoding transition FF2a_4 (115/250).
Encoding transition FF2a_5 (116/250).
Encoding transition FF2a_6 (117/250).
Encoding transition FF2a_7 (118/250).
Encoding transition FF2b_50 (119/250).
Encoding transition FF2a_1 (120/250).
Encoding transition FF2a_2 (121/250).
Encoding transition FF2a_3 (122/250).
Encoding transition FF2a_12 (123/250).
Encoding transition FF2a_13 (124/250).
Encoding transition FF2a_14 (125/250).
Encoding transition FF2a_15 (126/250).
Encoding transition FF2a_8 (127/250).
Encoding transition FF2a_9 (128/250).
Encoding transition FF2a_10 (129/250).
Encoding transition FF2a_11 (130/250).
Encoding transition FF1b_8 (131/250).
Encoding transition FF1b_9 (132/250).
Encoding transition FF1b_6 (133/250).
Encoding transition FF1b_7 (134/250).
Encoding transition FF1b_12 (135/250).
Encoding transition FF1b_13 (136/250).
Encoding transition FF1b_10 (137/250).
Encoding transition FF1b_11 (138/250).
Encoding transition FF2a_50 (139/250).
Encoding transition FF1b_1 (140/250).
Encoding transition FF2a_48 (141/250).
Encoding transition FF2a_49 (142/250).
Encoding transition FF1b_4 (143/250).
Encoding transition FF1b_5 (144/250).
Encoding transition FF1b_2 (145/250).
Encoding transition FF1b_3 (146/250).
Encoding transition FF2a_43 (147/250).
Encoding transition FF2a_42 (148/250).
Encoding transition FF2a_41 (149/250).
Encoding transition FF2a_40 (150/250).
Encoding transition FF2a_47 (151/250).
Encoding transition FF2a_46 (152/250).
Encoding transition FF2a_45 (153/250).
Encoding transition FF2a_44 (154/250).
Encoding transition FF2a_35 (155/250).
Encoding transition FF2a_34 (156/250).
Encoding transition FF2a_33 (157/250).
Encoding transition FF2a_32 (158/250).
Encoding transition FF2a_39 (159/250).
Encoding transition FF2a_38 (160/250).
Encoding transition FF2a_37 (161/250).
Encoding transition FF2a_36 (162/250).
Encoding transition FF1b_38 (163/250).
Encoding transition FF1b_39 (164/250).
Encoding transition FF1b_40 (165/250).
Encoding transition FF1b_41 (166/250).
Encoding transition FF1b_42 (167/250).
Encoding transition FF1b_43 (168/250).
Encoding transition FF1b_44 (169/250).
Encoding transition FF1b_45 (170/250).
Encoding transition FF1b_30 (171/250).
Encoding transition FF1b_31 (172/250).
Encoding transition FF1b_32 (173/250).
Encoding transition FF1b_33 (174/250).
Encoding transition FF1b_34 (175/250).
Encoding transition FF1b_35 (176/250).
Encoding transition FF1b_36 (177/250).
Encoding transition FF1b_37 (178/250).
Encoding transition FF1b_23 (179/250).
Encoding transition FF1b_22 (180/250).
Encoding transition FF1b_25 (181/250).
Encoding transition FF1b_24 (182/250).
Encoding transition FF1b_27 (183/250).
Encoding transition FF1b_26 (184/250).
Encoding transition FF1b_29 (185/250).
Encoding transition FF1b_28 (186/250).
Encoding transition FF1b_15 (187/250).
Encoding transition FF1b_14 (188/250).
Encoding transition FF1b_17 (189/250).
Encoding transition FF1b_16 (190/250).
Encoding transition FF1b_19 (191/250).
Encoding transition FF1b_18 (192/250).
Encoding transition FF1b_21 (193/250).
Encoding transition FF1b_20 (194/250).
Encoding transition FF1a_26 (195/250).
Encoding transition FF1a_27 (196/250).
Encoding transition FF1a_24 (197/250).
Encoding transition FF1a_25 (198/250).
Encoding transition FF1a_22 (199/250).
Encoding transition FF1a_23 (200/250).
Encoding transition FF1a_20 (201/250).
Encoding transition FF1a_21 (202/250).
Encoding transition FF1a_18 (203/250).
Encoding transition FF1a_19 (204/250).
Encoding transition FF1a_16 (205/250).
Encoding transition FF1a_17 (206/250).
Encoding transition FF1a_14 (207/250).
Encoding transition FF1a_15 (208/250).
Encoding transition FF1a_12 (209/250).
Encoding transition FF1a_13 (210/250).
Encoding transition FF1a_11 (211/250).
Encoding transition FF1a_10 (212/250).
Encoding transition FF1a_9 (213/250).
Encoding transition FF1a_8 (214/250).
Encoding transition FF1a_7 (215/250).
Encoding transition FF1a_6 (216/250).
Encoding transition FF1a_5 (217/250).
Encoding transition FF1a_4 (218/250).
Encoding transition FF1a_3 (219/250).
Encoding transition FF1a_2 (220/250).
Encoding transition FF1a_1 (221/250).
Encoding transition FF1b_50 (222/250).
Encoding transition FF1b_49 (223/250).
Encoding transition FF1b_48 (224/250).
Encoding transition FF1b_47 (225/250).
Encoding transition FF1b_46 (226/250).
Encoding transition FF1a_48 (227/250).
Encoding transition FF1a_49 (228/250).
Encoding transition FF1a_50 (229/250).
Encoding transition FF1a_44 (230/250).
Encoding transition FF1a_45 (231/250).
Encoding transition FF1a_46 (232/250).
Encoding transition FF1a_47 (233/250).
Encoding transition FF1a_41 (234/250).
Encoding transition FF1a_40 (235/250).
Encoding transition FF1a_43 (236/250).
Encoding transition FF1a_42 (237/250).
Encoding transition FF1a_37 (238/250).
Encoding transition FF1a_36 (239/250).
Encoding transition FF1a_39 (240/250).
Encoding transition FF1a_38 (241/250).
Encoding transition FF1a_33 (242/250).
Encoding transition FF1a_32 (243/250).
Encoding transition FF1a_35 (244/250).
Encoding transition FF1a_34 (245/250).
Encoding transition FF1a_29 (246/250).
Encoding transition FF1a_28 (247/250).
Encoding transition FF1a_31 (248/250).
Encoding transition FF1a_30 (249/250).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 11016KB
RS size: -9223372036854775808 (7.17898e+23)
----------------------------------------
End RS generation
----------------------------------------


BK_STOP 1400439544581

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

createEGMDD: MEDDLY Error: Insufficient memory
Assertion failed at WN/SOURCE/CTL/CTL.cpp:1657
terminate called after throwing an instance of 'int'
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 167: 1693 Aborted ~/BenchKit/bin/bin/RGMEDD model ${PLACE_ORDER} ${MEDDLY_CACHE} ${BOUND} -C -f ${NEW_FRM}

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