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 LamportFastMutEx-PT-5, examination is ReachabilityFireabilitySimple
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r02kn-qhx2-140031221901176
=====================================================================

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

BK_START 1400327400460
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running LamportFastMutEx (PT), instance 5
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireabilitySimple.xml INTO /home/mcc/execution/ReachabilityFireabilitySimple.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 1 -C -f /home/mcc/execution/ReachabilityFireabilitySimple.rgmedd-ctl
Using FORCE Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition T-setbi_2_1 (0/318).
Encoding transition T-setbi_2_2 (1/318).
Encoding transition T-setbi_2_3 (2/318).
Encoding transition T-setbi_2_4 (3/318).
Encoding transition T-setbi_2_5 (4/318).
Encoding transition T-setbi_2_6 (5/318).
Encoding transition T-setbi_2_7 (6/318).
Encoding transition T-setbi_2_8 (7/318).
Encoding transition T-setbi_2_9 (8/318).
Encoding transition T-setbi_2_10 (9/318).
Encoding transition T-setbi_2_11 (10/318).
Encoding transition T-setbi_2_12 (11/318).
Encoding transition T-setx_3_1 (12/318).
Encoding transition T-setx_3_2 (13/318).
Encoding transition T-setx_3_3 (14/318).
Encoding transition T-setx_3_4 (15/318).
Encoding transition T-setx_3_5 (16/318).
Encoding transition T-setx_3_6 (17/318).
Encoding transition T-setx_3_7 (18/318).
Encoding transition T-setx_3_8 (19/318).
Encoding transition T-setx_3_9 (20/318).
Encoding transition T-setx_3_10 (21/318).
Encoding transition T-setx_3_11 (22/318).
Encoding transition T-setx_3_12 (23/318).
Encoding transition T-setx_3_13 (24/318).
Encoding transition T-setx_3_14 (25/318).
Encoding transition T-setx_3_15 (26/318).
Encoding transition T-setx_3_16 (27/318).
Encoding transition T-setx_3_17 (28/318).
Encoding transition T-setx_3_18 (29/318).
Encoding transition T-setx_3_19 (30/318).
Encoding transition T-setx_3_20 (31/318).
Encoding transition T-setx_3_21 (32/318).
Encoding transition T-setx_3_22 (33/318).
Encoding transition T-setx_3_23 (34/318).
Encoding transition T-setx_3_24 (35/318).
Encoding transition T-setx_3_25 (36/318).
Encoding transition T-setx_3_26 (37/318).
Encoding transition T-setx_3_27 (38/318).
Encoding transition T-setx_3_28 (39/318).
Encoding transition T-setx_3_29 (40/318).
Encoding transition T-setx_3_30 (41/318).
Encoding transition T-setx_3_31 (42/318).
Encoding transition T-setx_3_32 (43/318).
Encoding transition T-setx_3_33 (44/318).
Encoding transition T-setx_3_34 (45/318).
Encoding transition T-setx_3_35 (46/318).
Encoding transition T-setx_3_36 (47/318).
Encoding transition T-yne0_4_2 (48/318).
Encoding transition T-yne0_4_3 (49/318).
Encoding transition T-yne0_4_4 (50/318).
Encoding transition T-yne0_4_5 (51/318).
Encoding transition T-yne0_4_6 (52/318).
Encoding transition T-yne0_4_8 (53/318).
Encoding transition T-yne0_4_9 (54/318).
Encoding transition T-yne0_4_10 (55/318).
Encoding transition T-yne0_4_11 (56/318).
Encoding transition T-yne0_4_12 (57/318).
Encoding transition T-yne0_4_14 (58/318).
Encoding transition T-yne0_4_15 (59/318).
Encoding transition T-yne0_4_16 (60/318).
Encoding transition T-yne0_4_17 (61/318).
Encoding transition T-yne0_4_18 (62/318).
Encoding transition T-yne0_4_20 (63/318).
Encoding transition T-yne0_4_21 (64/318).
Encoding transition T-yne0_4_22 (65/318).
Encoding transition T-yne0_4_23 (66/318).
Encoding transition T-yne0_4_24 (67/318).
Encoding transition T-yne0_4_26 (68/318).
Encoding transition T-yne0_4_27 (69/318).
Encoding transition T-yne0_4_28 (70/318).
Encoding transition T-yne0_4_29 (71/318).
Encoding transition T-yne0_4_30 (72/318).
Encoding transition T-yne0_4_32 (73/318).
Encoding transition T-yne0_4_33 (74/318).
Encoding transition T-yne0_4_34 (75/318).
Encoding transition T-yne0_4_35 (76/318).
Encoding transition T-yne0_4_36 (77/318).
Encoding transition T-setbi_5_1 (78/318).
Encoding transition T-setbi_5_2 (79/318).
Encoding transition T-setbi_5_3 (80/318).
Encoding transition T-setbi_5_4 (81/318).
Encoding transition T-setbi_5_5 (82/318).
Encoding transition T-setbi_5_6 (83/318).
Encoding transition T-setbi_5_7 (84/318).
Encoding transition T-setbi_5_8 (85/318).
Encoding transition T-setbi_5_9 (86/318).
Encoding transition T-setbi_5_10 (87/318).
Encoding transition T-setbi_5_11 (88/318).
Encoding transition T-setbi_5_12 (89/318).
Encoding transition T-awaity_1 (90/318).
Encoding transition T-awaity_2 (91/318).
Encoding transition T-awaity_3 (92/318).
Encoding transition T-awaity_4 (93/318).
Encoding transition T-awaity_5 (94/318).
Encoding transition T-awaity_6 (95/318).
Encoding transition T-yeq0_4_1 (96/318).
Encoding transition T-yeq0_4_2 (97/318).
Encoding transition T-yeq0_4_3 (98/318).
Encoding transition T-yeq0_4_4 (99/318).
Encoding transition T-yeq0_4_5 (100/318).
Encoding transition T-yeq0_4_6 (101/318).
Encoding transition T-sety_9_1 (102/318).
Encoding transition T-sety_9_2 (103/318).
Encoding transition T-sety_9_3 (104/318).
Encoding transition T-sety_9_4 (105/318).
Encoding transition T-sety_9_5 (106/318).
Encoding transition T-sety_9_6 (107/318).
Encoding transition T-sety_9_7 (108/318).
Encoding transition T-sety_9_8 (109/318).
Encoding transition T-sety_9_9 (110/318).
Encoding transition T-sety_9_10 (111/318).
Encoding transition T-sety_9_11 (112/318).
Encoding transition T-sety_9_12 (113/318).
Encoding transition T-sety_9_13 (114/318).
Encoding transition T-sety_9_14 (115/318).
Encoding transition T-sety_9_15 (116/318).
Encoding transition T-sety_9_16 (117/318).
Encoding transition T-sety_9_17 (118/318).
Encoding transition T-sety_9_18 (119/318).
Encoding transition T-sety_9_19 (120/318).
Encoding transition T-sety_9_20 (121/318).
Encoding transition T-sety_9_21 (122/318).
Encoding transition T-sety_9_22 (123/318).
Encoding transition T-sety_9_23 (124/318).
Encoding transition T-sety_9_24 (125/318).
Encoding transition T-sety_9_25 (126/318).
Encoding transition T-sety_9_26 (127/318).
Encoding transition T-sety_9_27 (128/318).
Encoding transition T-sety_9_28 (129/318).
Encoding transition T-sety_9_29 (130/318).
Encoding transition T-sety_9_30 (131/318).
Encoding transition T-sety_9_31 (132/318).
Encoding transition T-sety_9_32 (133/318).
Encoding transition T-sety_9_33 (134/318).
Encoding transition T-sety_9_34 (135/318).
Encoding transition T-sety_9_35 (136/318).
Encoding transition T-sety_9_36 (137/318).
Encoding transition T-xnei_10_2 (138/318).
Encoding transition T-xnei_10_3 (139/318).
Encoding transition T-xnei_10_4 (140/318).
Encoding transition T-xnei_10_5 (141/318).
Encoding transition T-xnei_10_6 (142/318).
Encoding transition T-xnei_10_7 (143/318).
Encoding transition T-xnei_10_9 (144/318).
Encoding transition T-xnei_10_10 (145/318).
Encoding transition T-xnei_10_11 (146/318).
Encoding transition T-xnei_10_12 (147/318).
Encoding transition T-xnei_10_13 (148/318).
Encoding transition T-xnei_10_14 (149/318).
Encoding transition T-xnei_10_16 (150/318).
Encoding transition T-xnei_10_17 (151/318).
Encoding transition T-xnei_10_18 (152/318).
Encoding transition T-xnei_10_19 (153/318).
Encoding transition T-xnei_10_20 (154/318).
Encoding transition T-xnei_10_21 (155/318).
Encoding transition T-xnei_10_23 (156/318).
Encoding transition T-xnei_10_24 (157/318).
Encoding transition T-xnei_10_25 (158/318).
Encoding transition T-xnei_10_26 (159/318).
Encoding transition T-xnei_10_27 (160/318).
Encoding transition T-xnei_10_28 (161/318).
Encoding transition T-xnei_10_30 (162/318).
Encoding transition T-xnei_10_31 (163/318).
Encoding transition T-xnei_10_32 (164/318).
Encoding transition T-xnei_10_33 (165/318).
Encoding transition T-xnei_10_34 (166/318).
Encoding transition T-xnei_10_35 (167/318).
Encoding transition T-setbi_11_1 (168/318).
Encoding transition T-setbi_11_2 (169/318).
Encoding transition T-setbi_11_3 (170/318).
Encoding transition T-setbi_11_4 (171/318).
Encoding transition T-setbi_11_5 (172/318).
Encoding transition T-setbi_11_6 (173/318).
Encoding transition T-setbi_11_7 (174/318).
Encoding transition T-setbi_11_8 (175/318).
Encoding transition T-setbi_11_9 (176/318).
Encoding transition T-setbi_11_10 (177/318).
Encoding transition T-setbi_11_11 (178/318).
Encoding transition T-setbi_11_12 (179/318).
Encoding transition T-fordo_12_1 (180/318).
Encoding transition T-fordo_12_2 (181/318).
Encoding transition T-fordo_12_3 (182/318).
Encoding transition T-fordo_12_4 (183/318).
Encoding transition T-fordo_12_5 (184/318).
Encoding transition T-fordo_12_6 (185/318).
Encoding transition T-await_13_1 (186/318).
Encoding transition T-await_13_2 (187/318).
Encoding transition T-await_13_3 (188/318).
Encoding transition T-await_13_4 (189/318).
Encoding transition T-await_13_5 (190/318).
Encoding transition T-await_13_6 (191/318).
Encoding transition T-await_13_7 (192/318).
Encoding transition T-await_13_8 (193/318).
Encoding transition T-await_13_9 (194/318).
Encoding transition T-await_13_10 (195/318).
Encoding transition T-await_13_11 (196/318).
Encoding transition T-await_13_12 (197/318).
Encoding transition T-await_13_13 (198/318).
Encoding transition T-await_13_14 (199/318).
Encoding transition T-await_13_15 (200/318).
Encoding transition T-await_13_16 (201/318).
Encoding transition T-await_13_17 (202/318).
Encoding transition T-await_13_18 (203/318).
Encoding transition T-await_13_19 (204/318).
Encoding transition T-await_13_20 (205/318).
Encoding transition T-await_13_21 (206/318).
Encoding transition T-await_13_22 (207/318).
Encoding transition T-await_13_23 (208/318).
Encoding transition T-await_13_24 (209/318).
Encoding transition T-await_13_25 (210/318).
Encoding transition T-await_13_26 (211/318).
Encoding transition T-await_13_27 (212/318).
Encoding transition T-await_13_28 (213/318).
Encoding transition T-await_13_29 (214/318).
Encoding transition T-await_13_30 (215/318).
Encoding transition T-await_13_31 (216/318).
Encoding transition T-await_13_32 (217/318).
Encoding transition T-await_13_33 (218/318).
Encoding transition T-await_13_34 (219/318).
Encoding transition T-await_13_35 (220/318).
Encoding transition T-await_13_36 (221/318).
Encoding transition T-forod_13_1 (222/318).
Encoding transition T-forod_13_2 (223/318).
Encoding transition T-forod_13_3 (224/318).
Encoding transition T-forod_13_4 (225/318).
Encoding transition T-forod_13_5 (226/318).
Encoding transition T-forod_13_6 (227/318).
Encoding transition T-ynei_15_2 (228/318).
Encoding transition T-ynei_15_3 (229/318).
Encoding transition T-ynei_15_4 (230/318).
Encoding transition T-ynei_15_5 (231/318).
Encoding transition T-ynei_15_6 (232/318).
Encoding transition T-ynei_15_7 (233/318).
Encoding transition T-ynei_15_9 (234/318).
Encoding transition T-ynei_15_10 (235/318).
Encoding transition T-ynei_15_11 (236/318).
Encoding transition T-ynei_15_12 (237/318).
Encoding transition T-ynei_15_13 (238/318).
Encoding transition T-ynei_15_14 (239/318).
Encoding transition T-ynei_15_16 (240/318).
Encoding transition T-ynei_15_17 (241/318).
Encoding transition T-ynei_15_18 (242/318).
Encoding transition T-ynei_15_19 (243/318).
Encoding transition T-ynei_15_20 (244/318).
Encoding transition T-ynei_15_21 (245/318).
Encoding transition T-ynei_15_23 (246/318).
Encoding transition T-ynei_15_24 (247/318).
Encoding transition T-ynei_15_25 (248/318).
Encoding transition T-ynei_15_26 (249/318).
Encoding transition T-ynei_15_27 (250/318).
Encoding transition T-ynei_15_28 (251/318).
Encoding transition T-ynei_15_30 (252/318).
Encoding transition T-ynei_15_31 (253/318).
Encoding transition T-ynei_15_32 (254/318).
Encoding transition T-ynei_15_33 (255/318).
Encoding transition T-ynei_15_34 (256/318).
Encoding transition T-ynei_15_35 (257/318).
Encoding transition T-yeqi_15_1 (258/318).
Encoding transition T-yeqi_15_8 (259/318).
Encoding transition T-yeqi_15_15 (260/318).
Encoding transition T-yeqi_15_22 (261/318).
Encoding transition T-yeqi_15_29 (262/318).
Encoding transition T-yeqi_15_36 (263/318).
Encoding transition T-xeqi_10_1 (264/318).
Encoding transition T-xeqi_10_8 (265/318).
Encoding transition T-xeqi_10_15 (266/318).
Encoding transition T-xeqi_10_22 (267/318).
Encoding transition T-xeqi_10_29 (268/318).
Encoding transition T-xeqi_10_36 (269/318).
Encoding transition T-sety0_23_1 (270/318).
Encoding transition T-sety0_23_2 (271/318).
Encoding transition T-sety0_23_3 (272/318).
Encoding transition T-sety0_23_4 (273/318).
Encoding transition T-sety0_23_5 (274/318).
Encoding transition T-sety0_23_6 (275/318).
Encoding transition T-sety0_23_7 (276/318).
Encoding transition T-sety0_23_8 (277/318).
Encoding transition T-sety0_23_9 (278/318).
Encoding transition T-sety0_23_10 (279/318).
Encoding transition T-sety0_23_11 (280/318).
Encoding transition T-sety0_23_12 (281/318).
Encoding transition T-sety0_23_13 (282/318).
Encoding transition T-sety0_23_14 (283/318).
Encoding transition T-sety0_23_15 (284/318).
Encoding transition T-sety0_23_16 (285/318).
Encoding transition T-sety0_23_17 (286/318).
Encoding transition T-sety0_23_18 (287/318).
Encoding transition T-sety0_23_19 (288/318).
Encoding transition T-sety0_23_20 (289/318).
Encoding transition T-sety0_23_21 (290/318).
Encoding transition T-sety0_23_22 (291/318).
Encoding transition T-sety0_23_23 (292/318).
Encoding transition T-sety0_23_24 (293/318).
Encoding transition T-sety0_23_25 (294/318).
Encoding transition T-sety0_23_26 (295/318).
Encoding transition T-sety0_23_27 (296/318).
Encoding transition T-sety0_23_28 (297/318).
Encoding transition T-sety0_23_29 (298/318).
Encoding transition T-sety0_23_30 (299/318).
Encoding transition T-sety0_23_31 (300/318).
Encoding transition T-sety0_23_32 (301/318).
Encoding transition T-sety0_23_33 (302/318).
Encoding transition T-sety0_23_34 (303/318).
Encoding transition T-sety0_23_35 (304/318).
Encoding transition T-sety0_23_36 (305/318).
Encoding transition T-setbi_24_1 (306/318).
Encoding transition T-setbi_24_2 (307/318).
Encoding transition T-setbi_24_3 (308/318).
Encoding transition T-setbi_24_4 (309/318).
Encoding transition T-setbi_24_5 (310/318).
Encoding transition T-setbi_24_6 (311/318).
Encoding transition T-setbi_24_7 (312/318).
Encoding transition T-setbi_24_8 (313/318).
Encoding transition T-setbi_24_9 (314/318).
Encoding transition T-setbi_24_10 (315/318).
Encoding transition T-setbi_24_11 (316/318).
Encoding transition T-setbi_24_12 (317/318).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 11652KB

BK_TIME_CONFINEMENT_REACHED

--------------------
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="LamportFastMutEx-PT-5"
export BK_EXAMINATION="ReachabilityFireabilitySimple"
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/LamportFastMutEx-PT-5.tgz
mv LamportFastMutEx-PT-5 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 LamportFastMutEx-PT-5, examination is ReachabilityFireabilitySimple"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r02kn-qhx2-140031221901176"
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 ;