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 ReachabilityDeadlock
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541400862
=====================================================================

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

BK_START 1400438231966
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Philosophers (PT), instance 000050
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityDeadlock.xml INTO /home/mcc/execution/ReachabilityDeadlock.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -P -h 2000000000 -B 1 -C -f /home/mcc/execution/ReachabilityDeadlock.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
----------------------------------------

FORMULA Philosophers-COL-000050-ReachabilityDeadlock-1 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000050-ReachabilityDeadlock-2 TRUE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400438242532

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

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="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/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 ReachabilityDeadlock"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541400862"
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 ;