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-1668
Executing tool greatspn
Input is SurpriseTokenRing-PT-005, examination is ReachabilityDeadlock
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r07ks-ovh1-140068246201811
=====================================================================

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

BK_START 1400692629517
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurpriseTokenRing (PT), instance 005
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityDeadlock.xml INTO /home/mcc/execution/ReachabilityDeadlock.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 15 -C -f /home/mcc/execution/ReachabilityDeadlock.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 OtherProcess_2_1_5 (0/156).
Encoding transition OtherProcess_5_1_0 (1/156).
Encoding transition OtherProcess_4_1_5 (2/156).
Encoding transition OtherProcess_1_3_5 (3/156).
Encoding transition OtherProcess_5_4_3 (4/156).
Encoding transition OtherProcess_2_2_3 (5/156).
Encoding transition OtherProcess_5_4_2 (6/156).
Encoding transition OtherProcess_1_0_2 (7/156).
Encoding transition OtherProcess_3_4_5 (8/156).
Encoding transition MainProcess_1 (9/156).
Encoding transition OtherProcess_3_5_0 (10/156).
Encoding transition OtherProcess_1_4_2 (11/156).
Encoding transition OtherProcess_1_2_3 (12/156).
Encoding transition OtherProcess_2_0_5 (13/156).
Encoding transition OtherProcess_1_3_0 (14/156).
Encoding transition OtherProcess_5_4_1 (15/156).
Encoding transition OtherProcess_3_2_4 (16/156).
Encoding transition OtherProcess_1_2_1 (17/156).
Encoding transition OtherProcess_2_0_2 (18/156).
Encoding transition OtherProcess_3_5_2 (19/156).
Encoding transition OtherProcess_4_0_3 (20/156).
Encoding transition OtherProcess_5_0_3 (21/156).
Encoding transition OtherProcess_5_3_4 (22/156).
Encoding transition OtherProcess_4_5_0 (23/156).
Encoding transition OtherProcess_4_0_4 (24/156).
Encoding transition OtherProcess_4_1_2 (25/156).
Encoding transition OtherProcess_4_3_1 (26/156).
Encoding transition OtherProcess_4_1_0 (27/156).
Encoding transition OtherProcess_5_1_5 (28/156).
Encoding transition OtherProcess_1_5_4 (29/156).
Encoding transition MainProcess_2 (30/156).
Encoding transition OtherProcess_3_4_0 (31/156).
Encoding transition OtherProcess_4_4_5 (32/156).
Encoding transition OtherProcess_5_5_0 (33/156).
Encoding transition OtherProcess_2_4_3 (34/156).
Encoding transition OtherProcess_4_5_3 (35/156).
Encoding transition OtherProcess_3_0_2 (36/156).
Encoding transition OtherProcess_1_1_3 (37/156).
Encoding transition OtherProcess_1_1_4 (38/156).
Encoding transition OtherProcess_2_4_2 (39/156).
Encoding transition OtherProcess_5_1_3 (40/156).
Encoding transition OtherProcess_5_3_1 (41/156).
Encoding transition OtherProcess_4_4_1 (42/156).
Encoding transition OtherProcess_4_0_5 (43/156).
Encoding transition MainProcess_3 (44/156).
Encoding transition OtherProcess_2_3_0 (45/156).
Encoding transition OtherProcess_5_0_1 (46/156).
Encoding transition OtherProcess_3_1_0 (47/156).
Encoding transition OtherProcess_2_5_2 (48/156).
Encoding transition OtherProcess_1_2_5 (49/156).
Encoding transition OtherProcess_2_4_0 (50/156).
Encoding transition OtherProcess_2_5_1 (51/156).
Encoding transition OtherProcess_2_4_5 (52/156).
Encoding transition OtherProcess_4_1_3 (53/156).
Encoding transition OtherProcess_3_5_3 (54/156).
Encoding transition OtherProcess_1_0_1 (55/156).
Encoding transition OtherProcess_2_1_0 (56/156).
Encoding transition OtherProcess_4_0_2 (57/156).
Encoding transition OtherProcess_2_3_1 (58/156).
Encoding transition OtherProcess_1_0_5 (59/156).
Encoding transition OtherProcess_4_3_4 (60/156).
Encoding transition OtherProcess_3_1_2 (61/156).
Encoding transition OtherProcess_2_1_4 (62/156).
Encoding transition OtherProcess_4_0_1 (63/156).
Encoding transition OtherProcess_2_1_2 (64/156).
Encoding transition OtherProcess_3_0_5 (65/156).
Encoding transition OtherProcess_2_1_3 (66/156).
Encoding transition OtherProcess_4_2_0 (67/156).
Encoding transition OtherProcess_4_3_2 (68/156).
Encoding transition OtherProcess_1_0_4 (69/156).
Encoding transition OtherProcess_5_5_2 (70/156).
Encoding transition OtherProcess_2_2_5 (71/156).
Encoding transition OtherProcess_3_4_3 (72/156).
Encoding transition OtherProcess_1_5_1 (73/156).
Encoding transition OtherProcess_5_0_2 (74/156).
Encoding transition OtherProcess_3_3_4 (75/156).
Encoding transition OtherProcess_4_5_2 (76/156).
Encoding transition OtherProcess_1_1_0 (77/156).
Encoding transition OtherProcess_1_4_5 (78/156).
Encoding transition OtherProcess_3_1_3 (79/156).
Encoding transition OtherProcess_4_1_4 (80/156).
Encoding transition OtherProcess_4_4_0 (81/156).
Encoding transition OtherProcess_5_2_0 (82/156).
Encoding transition OtherProcess_1_1_2 (83/156).
Encoding transition OtherProcess_5_3_2 (84/156).
Encoding transition OtherProcess_3_3_1 (85/156).
Encoding transition OtherProcess_3_0_1 (86/156).
Encoding transition OtherProcess_5_2_3 (87/156).
Encoding transition OtherProcess_3_1_4 (88/156).
Encoding transition OtherProcess_5_5_3 (89/156).
Encoding transition OtherProcess_4_5_4 (90/156).
Encoding transition OtherProcess_2_2_0 (91/156).
Encoding transition OtherProcess_2_4_1 (92/156).
Encoding transition OtherProcess_1_4_3 (93/156).
Encoding transition OtherProcess_4_3_0 (94/156).
Encoding transition MainProcess_5 (95/156).
Encoding transition OtherProcess_1_1_5 (96/156).
Encoding transition OtherProcess_3_2_5 (97/156).
Encoding transition OtherProcess_5_3_5 (98/156).
Encoding transition OtherProcess_2_3_4 (99/156).
Encoding transition OtherProcess_5_1_4 (100/156).
Encoding transition OtherProcess_4_2_1 (101/156).
Encoding transition OtherProcess_4_2_3 (102/156).
Encoding transition OtherProcess_3_2_0 (103/156).
Encoding transition OtherProcess_5_4_0 (104/156).
Encoding transition OtherProcess_1_5_3 (105/156).
Encoding transition OtherProcess_4_3_5 (106/156).
Encoding transition OtherProcess_3_5_1 (107/156).
Encoding transition MainProcess_4 (108/156).
Encoding transition OtherProcess_3_0_4 (109/156).
Encoding transition OtherProcess_2_0_1 (110/156).
Encoding transition OtherProcess_1_4_1 (111/156).
Encoding transition OtherProcess_5_5_4 (112/156).
Encoding transition OtherProcess_1_3_4 (113/156).
Encoding transition OtherProcess_1_3_1 (114/156).
Encoding transition OtherProcess_3_3_0 (115/156).
Encoding transition OtherProcess_1_0_3 (116/156).
Encoding transition OtherProcess_3_3_2 (117/156).
Encoding transition OtherProcess_2_0_3 (118/156).
Encoding transition OtherProcess_5_4_5 (119/156).
Encoding transition OtherProcess_2_3_2 (120/156).
Encoding transition OtherProcess_3_3_5 (121/156).
Encoding transition OtherProcess_4_2_5 (122/156).
Encoding transition OtherProcess_5_2_1 (123/156).
Encoding transition OtherProcess_5_0_5 (124/156).
Encoding transition OtherProcess_3_2_3 (125/156).
Encoding transition OtherProcess_4_5_1 (126/156).
Encoding transition OtherProcess_2_5_4 (127/156).
Encoding transition OtherProcess_1_5_0 (128/156).
Encoding transition OtherProcess_5_2_5 (129/156).
Encoding transition OtherProcess_1_2_4 (130/156).
Encoding transition OtherProcess_3_4_2 (131/156).
Encoding transition OtherProcess_1_3_2 (132/156).
Encoding transition OtherProcess_5_2_4 (133/156).
Encoding transition OtherProcess_2_5_3 (134/156).
Encoding transition OtherProcess_1_4_0 (135/156).
Encoding transition OtherProcess_3_2_1 (136/156).
Encoding transition OtherProcess_3_1_5 (137/156).
Encoding transition MainProcess_0 (138/156).
Encoding transition OtherProcess_2_5_0 (139/156).
Encoding transition OtherProcess_5_5_1 (140/156).
Encoding transition OtherProcess_3_0_3 (141/156).
Encoding transition OtherProcess_2_0_4 (142/156).
Encoding transition OtherProcess_2_2_1 (143/156).
Encoding transition OtherProcess_3_5_4 (144/156).
Encoding transition OtherProcess_4_2_4 (145/156).
Encoding transition OtherProcess_2_2_4 (146/156).
Encoding transition OtherProcess_2_3_5 (147/156).
Encoding transition OtherProcess_5_3_0 (148/156).
Encoding transition OtherProcess_1_2_0 (149/156).
Encoding transition OtherProcess_4_4_2 (150/156).
Encoding transition OtherProcess_5_0_4 (151/156).
Encoding transition OtherProcess_4_4_3 (152/156).
Encoding transition OtherProcess_5_1_2 (153/156).
Encoding transition OtherProcess_3_4_1 (154/156).
Encoding transition OtherProcess_1_5_2 (155/156).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 51460KB
RS size: 166 (166)
----------------------------------------
End RS generation
----------------------------------------

FORMULA TokenRing-COL-005-ReachabilityDeadlock-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA TokenRing-COL-005-ReachabilityDeadlock-2 FALSE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400692639145

--------------------
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="SurpriseTokenRing-PT-005"
export BK_EXAMINATION="ReachabilityDeadlock"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/srv/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/SurpriseTokenRing-PT-005.tgz
mv SurpriseTokenRing-PT-005 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is SurpriseTokenRing-PT-005, examination is ReachabilityDeadlock"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r07ks-ovh1-140068246201811"
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 ;