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 SurpriseLamportFastMutEx-PT-3, examination is ReachabilityFireabilitySimple
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r08ks-qhx2-140068993901150
=====================================================================

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

BK_START 1400729911616
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurpriseLamportFastMutEx (PT), instance 3
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityFireabilitySimple.xml INTO /home/mcc/execution/ReachabilityFireabilitySimple.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 9 -C -f /home/mcc/execution/ReachabilityFireabilitySimple.rgmedd-ctl
Using FORCE-PINV 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/156).
Encoding transition T-setbi_2_2 (1/156).
Encoding transition T-setbi_2_3 (2/156).
Encoding transition T-setbi_2_4 (3/156).
Encoding transition T-setbi_2_5 (4/156).
Encoding transition T-setbi_2_6 (5/156).
Encoding transition T-setbi_2_7 (6/156).
Encoding transition T-setbi_2_8 (7/156).
Encoding transition T-setx_3_1 (8/156).
Encoding transition T-setx_3_2 (9/156).
Encoding transition T-setx_3_3 (10/156).
Encoding transition T-setx_3_4 (11/156).
Encoding transition T-setx_3_5 (12/156).
Encoding transition T-setx_3_6 (13/156).
Encoding transition T-setx_3_7 (14/156).
Encoding transition T-setx_3_8 (15/156).
Encoding transition T-setx_3_9 (16/156).
Encoding transition T-setx_3_10 (17/156).
Encoding transition T-setx_3_11 (18/156).
Encoding transition T-setx_3_12 (19/156).
Encoding transition T-setx_3_13 (20/156).
Encoding transition T-setx_3_14 (21/156).
Encoding transition T-setx_3_15 (22/156).
Encoding transition T-setx_3_16 (23/156).
Encoding transition T-yne0_4_2 (24/156).
Encoding transition T-yne0_4_3 (25/156).
Encoding transition T-yne0_4_4 (26/156).
Encoding transition T-yne0_4_6 (27/156).
Encoding transition T-yne0_4_7 (28/156).
Encoding transition T-yne0_4_8 (29/156).
Encoding transition T-yne0_4_10 (30/156).
Encoding transition T-yne0_4_11 (31/156).
Encoding transition T-yne0_4_12 (32/156).
Encoding transition T-yne0_4_14 (33/156).
Encoding transition T-yne0_4_15 (34/156).
Encoding transition T-yne0_4_16 (35/156).
Encoding transition T-setbi_5_1 (36/156).
Encoding transition T-setbi_5_2 (37/156).
Encoding transition T-setbi_5_3 (38/156).
Encoding transition T-setbi_5_4 (39/156).
Encoding transition T-setbi_5_5 (40/156).
Encoding transition T-setbi_5_6 (41/156).
Encoding transition T-setbi_5_7 (42/156).
Encoding transition T-setbi_5_8 (43/156).
Encoding transition T-awaity_1 (44/156).
Encoding transition T-awaity_2 (45/156).
Encoding transition T-awaity_3 (46/156).
Encoding transition T-awaity_4 (47/156).
Encoding transition T-yeq0_4_1 (48/156).
Encoding transition T-yeq0_4_2 (49/156).
Encoding transition T-yeq0_4_3 (50/156).
Encoding transition T-yeq0_4_4 (51/156).
Encoding transition T-sety_9_1 (52/156).
Encoding transition T-sety_9_2 (53/156).
Encoding transition T-sety_9_3 (54/156).
Encoding transition T-sety_9_4 (55/156).
Encoding transition T-sety_9_5 (56/156).
Encoding transition T-sety_9_6 (57/156).
Encoding transition T-sety_9_7 (58/156).
Encoding transition T-sety_9_8 (59/156).
Encoding transition T-sety_9_9 (60/156).
Encoding transition T-sety_9_10 (61/156).
Encoding transition T-sety_9_11 (62/156).
Encoding transition T-sety_9_12 (63/156).
Encoding transition T-sety_9_13 (64/156).
Encoding transition T-sety_9_14 (65/156).
Encoding transition T-sety_9_15 (66/156).
Encoding transition T-sety_9_16 (67/156).
Encoding transition T-xnei_10_2 (68/156).
Encoding transition T-xnei_10_3 (69/156).
Encoding transition T-xnei_10_4 (70/156).
Encoding transition T-xnei_10_5 (71/156).
Encoding transition T-xnei_10_7 (72/156).
Encoding transition T-xnei_10_8 (73/156).
Encoding transition T-xnei_10_9 (74/156).
Encoding transition T-xnei_10_10 (75/156).
Encoding transition T-xnei_10_12 (76/156).
Encoding transition T-xnei_10_13 (77/156).
Encoding transition T-xnei_10_14 (78/156).
Encoding transition T-xnei_10_15 (79/156).
Encoding transition T-setbi_11_1 (80/156).
Encoding transition T-setbi_11_2 (81/156).
Encoding transition T-setbi_11_3 (82/156).
Encoding transition T-setbi_11_4 (83/156).
Encoding transition T-setbi_11_5 (84/156).
Encoding transition T-setbi_11_6 (85/156).
Encoding transition T-setbi_11_7 (86/156).
Encoding transition T-setbi_11_8 (87/156).
Encoding transition T-fordo_12_1 (88/156).
Encoding transition T-fordo_12_2 (89/156).
Encoding transition T-fordo_12_3 (90/156).
Encoding transition T-fordo_12_4 (91/156).
Encoding transition T-await_13_1 (92/156).
Encoding transition T-await_13_2 (93/156).
Encoding transition T-await_13_3 (94/156).
Encoding transition T-await_13_4 (95/156).
Encoding transition T-await_13_5 (96/156).
Encoding transition T-await_13_6 (97/156).
Encoding transition T-await_13_7 (98/156).
Encoding transition T-await_13_8 (99/156).
Encoding transition T-await_13_9 (100/156).
Encoding transition T-await_13_10 (101/156).
Encoding transition T-await_13_11 (102/156).
Encoding transition T-await_13_12 (103/156).
Encoding transition T-await_13_13 (104/156).
Encoding transition T-await_13_14 (105/156).
Encoding transition T-await_13_15 (106/156).
Encoding transition T-await_13_16 (107/156).
Encoding transition T-forod_13_1 (108/156).
Encoding transition T-forod_13_2 (109/156).
Encoding transition T-forod_13_3 (110/156).
Encoding transition T-forod_13_4 (111/156).
Encoding transition T-ynei_15_2 (112/156).
Encoding transition T-ynei_15_3 (113/156).
Encoding transition T-ynei_15_4 (114/156).
Encoding transition T-ynei_15_5 (115/156).
Encoding transition T-ynei_15_7 (116/156).
Encoding transition T-ynei_15_8 (117/156).
Encoding transition T-ynei_15_9 (118/156).
Encoding transition T-ynei_15_10 (119/156).
Encoding transition T-ynei_15_12 (120/156).
Encoding transition T-ynei_15_13 (121/156).
Encoding transition T-ynei_15_14 (122/156).
Encoding transition T-ynei_15_15 (123/156).
Encoding transition T-yeqi_15_1 (124/156).
Encoding transition T-yeqi_15_6 (125/156).
Encoding transition T-yeqi_15_11 (126/156).
Encoding transition T-yeqi_15_16 (127/156).
Encoding transition T-xeqi_10_1 (128/156).
Encoding transition T-xeqi_10_6 (129/156).
Encoding transition T-xeqi_10_11 (130/156).
Encoding transition T-xeqi_10_16 (131/156).
Encoding transition T-sety0_23_1 (132/156).
Encoding transition T-sety0_23_2 (133/156).
Encoding transition T-sety0_23_3 (134/156).
Encoding transition T-sety0_23_4 (135/156).
Encoding transition T-sety0_23_5 (136/156).
Encoding transition T-sety0_23_6 (137/156).
Encoding transition T-sety0_23_7 (138/156).
Encoding transition T-sety0_23_8 (139/156).
Encoding transition T-sety0_23_9 (140/156).
Encoding transition T-sety0_23_10 (141/156).
Encoding transition T-sety0_23_11 (142/156).
Encoding transition T-sety0_23_12 (143/156).
Encoding transition T-sety0_23_13 (144/156).
Encoding transition T-sety0_23_14 (145/156).
Encoding transition T-sety0_23_15 (146/156).
Encoding transition T-sety0_23_16 (147/156).
Encoding transition T-setbi_24_1 (148/156).
Encoding transition T-setbi_24_2 (149/156).
Encoding transition T-setbi_24_3 (150/156).
Encoding transition T-setbi_24_4 (151/156).
Encoding transition T-setbi_24_5 (152/156).
Encoding transition T-setbi_24_6 (153/156).
Encoding transition T-setbi_24_7 (154/156).
Encoding transition T-setbi_24_8 (155/156).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 18292KB
RS size: 19742 (19742)
----------------------------------------
End RS generation
----------------------------------------

FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-2 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-3 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-4 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-5 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-6 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-7 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-8 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-9 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA LamportFastMutEx-COL-3-ReachabilityFireabilitySimple-10 TRUE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400729921807

--------------------
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="SurpriseLamportFastMutEx-PT-3"
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/SurpriseLamportFastMutEx-PT-3.tgz
mv SurpriseLamportFastMutEx-PT-3 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 SurpriseLamportFastMutEx-PT-3, examination is ReachabilityFireabilitySimple"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r08ks-qhx2-140068993901150"
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 ;