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-4, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r02kn-qhx2-140031221901167
=====================================================================

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

BK_START 1400327346181
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running LamportFastMutEx (PT), instance 4
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 -FORCE-WES1 -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLFireability.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/230).
Encoding transition T-setbi_2_2 (1/230).
Encoding transition T-setbi_2_3 (2/230).
Encoding transition T-setbi_2_4 (3/230).
Encoding transition T-setbi_2_5 (4/230).
Encoding transition T-setbi_2_6 (5/230).
Encoding transition T-setbi_2_7 (6/230).
Encoding transition T-setbi_2_8 (7/230).
Encoding transition T-setbi_2_9 (8/230).
Encoding transition T-setbi_2_10 (9/230).
Encoding transition T-setx_3_1 (10/230).
Encoding transition T-setx_3_2 (11/230).
Encoding transition T-setx_3_3 (12/230).
Encoding transition T-setx_3_4 (13/230).
Encoding transition T-setx_3_5 (14/230).
Encoding transition T-setx_3_6 (15/230).
Encoding transition T-setx_3_7 (16/230).
Encoding transition T-setx_3_8 (17/230).
Encoding transition T-setx_3_9 (18/230).
Encoding transition T-setx_3_10 (19/230).
Encoding transition T-setx_3_11 (20/230).
Encoding transition T-setx_3_12 (21/230).
Encoding transition T-setx_3_13 (22/230).
Encoding transition T-setx_3_14 (23/230).
Encoding transition T-setx_3_15 (24/230).
Encoding transition T-setx_3_16 (25/230).
Encoding transition T-setx_3_17 (26/230).
Encoding transition T-setx_3_18 (27/230).
Encoding transition T-setx_3_19 (28/230).
Encoding transition T-setx_3_20 (29/230).
Encoding transition T-setx_3_21 (30/230).
Encoding transition T-setx_3_22 (31/230).
Encoding transition T-setx_3_23 (32/230).
Encoding transition T-setx_3_24 (33/230).
Encoding transition T-setx_3_25 (34/230).
Encoding transition T-yne0_4_2 (35/230).
Encoding transition T-yne0_4_3 (36/230).
Encoding transition T-yne0_4_4 (37/230).
Encoding transition T-yne0_4_5 (38/230).
Encoding transition T-yne0_4_7 (39/230).
Encoding transition T-yne0_4_8 (40/230).
Encoding transition T-yne0_4_9 (41/230).
Encoding transition T-yne0_4_10 (42/230).
Encoding transition T-yne0_4_12 (43/230).
Encoding transition T-yne0_4_13 (44/230).
Encoding transition T-yne0_4_14 (45/230).
Encoding transition T-yne0_4_15 (46/230).
Encoding transition T-yne0_4_17 (47/230).
Encoding transition T-yne0_4_18 (48/230).
Encoding transition T-yne0_4_19 (49/230).
Encoding transition T-yne0_4_20 (50/230).
Encoding transition T-yne0_4_22 (51/230).
Encoding transition T-yne0_4_23 (52/230).
Encoding transition T-yne0_4_24 (53/230).
Encoding transition T-yne0_4_25 (54/230).
Encoding transition T-setbi_5_1 (55/230).
Encoding transition T-setbi_5_2 (56/230).
Encoding transition T-setbi_5_3 (57/230).
Encoding transition T-setbi_5_4 (58/230).
Encoding transition T-setbi_5_5 (59/230).
Encoding transition T-setbi_5_6 (60/230).
Encoding transition T-setbi_5_7 (61/230).
Encoding transition T-setbi_5_8 (62/230).
Encoding transition T-setbi_5_9 (63/230).
Encoding transition T-setbi_5_10 (64/230).
Encoding transition T-awaity_1 (65/230).
Encoding transition T-awaity_2 (66/230).
Encoding transition T-awaity_3 (67/230).
Encoding transition T-awaity_4 (68/230).
Encoding transition T-awaity_5 (69/230).
Encoding transition T-yeq0_4_1 (70/230).
Encoding transition T-yeq0_4_2 (71/230).
Encoding transition T-yeq0_4_3 (72/230).
Encoding transition T-yeq0_4_4 (73/230).
Encoding transition T-yeq0_4_5 (74/230).
Encoding transition T-sety_9_1 (75/230).
Encoding transition T-sety_9_2 (76/230).
Encoding transition T-sety_9_3 (77/230).
Encoding transition T-sety_9_4 (78/230).
Encoding transition T-sety_9_5 (79/230).
Encoding transition T-sety_9_6 (80/230).
Encoding transition T-sety_9_7 (81/230).
Encoding transition T-sety_9_8 (82/230).
Encoding transition T-sety_9_9 (83/230).
Encoding transition T-sety_9_10 (84/230).
Encoding transition T-sety_9_11 (85/230).
Encoding transition T-sety_9_12 (86/230).
Encoding transition T-sety_9_13 (87/230).
Encoding transition T-sety_9_14 (88/230).
Encoding transition T-sety_9_15 (89/230).
Encoding transition T-sety_9_16 (90/230).
Encoding transition T-sety_9_17 (91/230).
Encoding transition T-sety_9_18 (92/230).
Encoding transition T-sety_9_19 (93/230).
Encoding transition T-sety_9_20 (94/230).
Encoding transition T-sety_9_21 (95/230).
Encoding transition T-sety_9_22 (96/230).
Encoding transition T-sety_9_23 (97/230).
Encoding transition T-sety_9_24 (98/230).
Encoding transition T-sety_9_25 (99/230).
Encoding transition T-xnei_10_2 (100/230).
Encoding transition T-xnei_10_3 (101/230).
Encoding transition T-xnei_10_4 (102/230).
Encoding transition T-xnei_10_5 (103/230).
Encoding transition T-xnei_10_6 (104/230).
Encoding transition T-xnei_10_8 (105/230).
Encoding transition T-xnei_10_9 (106/230).
Encoding transition T-xnei_10_10 (107/230).
Encoding transition T-xnei_10_11 (108/230).
Encoding transition T-xnei_10_12 (109/230).
Encoding transition T-xnei_10_14 (110/230).
Encoding transition T-xnei_10_15 (111/230).
Encoding transition T-xnei_10_16 (112/230).
Encoding transition T-xnei_10_17 (113/230).
Encoding transition T-xnei_10_18 (114/230).
Encoding transition T-xnei_10_20 (115/230).
Encoding transition T-xnei_10_21 (116/230).
Encoding transition T-xnei_10_22 (117/230).
Encoding transition T-xnei_10_23 (118/230).
Encoding transition T-xnei_10_24 (119/230).
Encoding transition T-setbi_11_1 (120/230).
Encoding transition T-setbi_11_2 (121/230).
Encoding transition T-setbi_11_3 (122/230).
Encoding transition T-setbi_11_4 (123/230).
Encoding transition T-setbi_11_5 (124/230).
Encoding transition T-setbi_11_6 (125/230).
Encoding transition T-setbi_11_7 (126/230).
Encoding transition T-setbi_11_8 (127/230).
Encoding transition T-setbi_11_9 (128/230).
Encoding transition T-setbi_11_10 (129/230).
Encoding transition T-fordo_12_1 (130/230).
Encoding transition T-fordo_12_2 (131/230).
Encoding transition T-fordo_12_3 (132/230).
Encoding transition T-fordo_12_4 (133/230).
Encoding transition T-fordo_12_5 (134/230).
Encoding transition T-await_13_1 (135/230).
Encoding transition T-await_13_2 (136/230).
Encoding transition T-await_13_3 (137/230).
Encoding transition T-await_13_4 (138/230).
Encoding transition T-await_13_5 (139/230).
Encoding transition T-await_13_6 (140/230).
Encoding transition T-await_13_7 (141/230).
Encoding transition T-await_13_8 (142/230).
Encoding transition T-await_13_9 (143/230).
Encoding transition T-await_13_10 (144/230).
Encoding transition T-await_13_11 (145/230).
Encoding transition T-await_13_12 (146/230).
Encoding transition T-await_13_13 (147/230).
Encoding transition T-await_13_14 (148/230).
Encoding transition T-await_13_15 (149/230).
Encoding transition T-await_13_16 (150/230).
Encoding transition T-await_13_17 (151/230).
Encoding transition T-await_13_18 (152/230).
Encoding transition T-await_13_19 (153/230).
Encoding transition T-await_13_20 (154/230).
Encoding transition T-await_13_21 (155/230).
Encoding transition T-await_13_22 (156/230).
Encoding transition T-await_13_23 (157/230).
Encoding transition T-await_13_24 (158/230).
Encoding transition T-await_13_25 (159/230).
Encoding transition T-forod_13_1 (160/230).
Encoding transition T-forod_13_2 (161/230).
Encoding transition T-forod_13_3 (162/230).
Encoding transition T-forod_13_4 (163/230).
Encoding transition T-forod_13_5 (164/230).
Encoding transition T-ynei_15_2 (165/230).
Encoding transition T-ynei_15_3 (166/230).
Encoding transition T-ynei_15_4 (167/230).
Encoding transition T-ynei_15_5 (168/230).
Encoding transition T-ynei_15_6 (169/230).
Encoding transition T-ynei_15_8 (170/230).
Encoding transition T-ynei_15_9 (171/230).
Encoding transition T-ynei_15_10 (172/230).
Encoding transition T-ynei_15_11 (173/230).
Encoding transition T-ynei_15_12 (174/230).
Encoding transition T-ynei_15_14 (175/230).
Encoding transition T-ynei_15_15 (176/230).
Encoding transition T-ynei_15_16 (177/230).
Encoding transition T-ynei_15_17 (178/230).
Encoding transition T-ynei_15_18 (179/230).
Encoding transition T-ynei_15_20 (180/230).
Encoding transition T-ynei_15_21 (181/230).
Encoding transition T-ynei_15_22 (182/230).
Encoding transition T-ynei_15_23 (183/230).
Encoding transition T-ynei_15_24 (184/230).
Encoding transition T-yeqi_15_1 (185/230).
Encoding transition T-yeqi_15_7 (186/230).
Encoding transition T-yeqi_15_13 (187/230).
Encoding transition T-yeqi_15_19 (188/230).
Encoding transition T-yeqi_15_25 (189/230).
Encoding transition T-xeqi_10_1 (190/230).
Encoding transition T-xeqi_10_7 (191/230).
Encoding transition T-xeqi_10_13 (192/230).
Encoding transition T-xeqi_10_19 (193/230).
Encoding transition T-xeqi_10_25 (194/230).
Encoding transition T-sety0_23_1 (195/230).
Encoding transition T-sety0_23_2 (196/230).
Encoding transition T-sety0_23_3 (197/230).
Encoding transition T-sety0_23_4 (198/230).
Encoding transition T-sety0_23_5 (199/230).
Encoding transition T-sety0_23_6 (200/230).
Encoding transition T-sety0_23_7 (201/230).
Encoding transition T-sety0_23_8 (202/230).
Encoding transition T-sety0_23_9 (203/230).
Encoding transition T-sety0_23_10 (204/230).
Encoding transition T-sety0_23_11 (205/230).
Encoding transition T-sety0_23_12 (206/230).
Encoding transition T-sety0_23_13 (207/230).
Encoding transition T-sety0_23_14 (208/230).
Encoding transition T-sety0_23_15 (209/230).
Encoding transition T-sety0_23_16 (210/230).
Encoding transition T-sety0_23_17 (211/230).
Encoding transition T-sety0_23_18 (212/230).
Encoding transition T-sety0_23_19 (213/230).
Encoding transition T-sety0_23_20 (214/230).
Encoding transition T-sety0_23_21 (215/230).
Encoding transition T-sety0_23_22 (216/230).
Encoding transition T-sety0_23_23 (217/230).
Encoding transition T-sety0_23_24 (218/230).
Encoding transition T-sety0_23_25 (219/230).
Encoding transition T-setbi_24_1 (220/230).
Encoding transition T-setbi_24_2 (221/230).
Encoding transition T-setbi_24_3 (222/230).
Encoding transition T-setbi_24_4 (223/230).
Encoding transition T-setbi_24_5 (224/230).
Encoding transition T-setbi_24_6 (225/230).
Encoding transition T-setbi_24_7 (226/230).
Encoding transition T-setbi_24_8 (227/230).
Encoding transition T-setbi_24_9 (228/230).
Encoding transition T-setbi_24_10 (229/230).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 8124KB
RS size: 1914784 (1.91478e+06)
----------------------------------------
End RS generation
----------------------------------------


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