fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r01kn-qhx2-140025665600745
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
98.60 2039 189.6 TF________ normal

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 Dekker-PT-010, examination is ReachabilityDeadlock
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r01kn-qhx2-140025665600745
=====================================================================


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

BK_START 1400263803468
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Dekker (PT), instance 010
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 -FORCE-WES1 -h 2000000000 -B 1 -C -f /home/mcc/execution/ReachabilityDeadlock.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 withdraw_0_1 (0/120).
Encoding transition withdraw_0_2 (1/120).
Encoding transition withdraw_0_3 (2/120).
Encoding transition withdraw_0_4 (3/120).
Encoding transition withdraw_0_5 (4/120).
Encoding transition withdraw_0_6 (5/120).
Encoding transition withdraw_0_7 (6/120).
Encoding transition withdraw_0_8 (7/120).
Encoding transition withdraw_0_9 (8/120).
Encoding transition try_0 (9/120).
Encoding transition enter_0 (10/120).
Encoding transition exit_0 (11/120).
Encoding transition withdraw_1_0 (12/120).
Encoding transition withdraw_1_2 (13/120).
Encoding transition withdraw_1_3 (14/120).
Encoding transition withdraw_1_4 (15/120).
Encoding transition withdraw_1_5 (16/120).
Encoding transition withdraw_1_6 (17/120).
Encoding transition withdraw_1_7 (18/120).
Encoding transition withdraw_1_8 (19/120).
Encoding transition withdraw_1_9 (20/120).
Encoding transition try_1 (21/120).
Encoding transition enter_1 (22/120).
Encoding transition exit_1 (23/120).
Encoding transition withdraw_2_0 (24/120).
Encoding transition withdraw_2_1 (25/120).
Encoding transition withdraw_2_3 (26/120).
Encoding transition withdraw_2_4 (27/120).
Encoding transition withdraw_2_5 (28/120).
Encoding transition withdraw_2_6 (29/120).
Encoding transition withdraw_2_7 (30/120).
Encoding transition withdraw_2_8 (31/120).
Encoding transition withdraw_2_9 (32/120).
Encoding transition try_2 (33/120).
Encoding transition enter_2 (34/120).
Encoding transition exit_2 (35/120).
Encoding transition withdraw_3_0 (36/120).
Encoding transition withdraw_3_1 (37/120).
Encoding transition withdraw_3_2 (38/120).
Encoding transition withdraw_3_4 (39/120).
Encoding transition withdraw_3_5 (40/120).
Encoding transition withdraw_3_6 (41/120).
Encoding transition withdraw_3_7 (42/120).
Encoding transition withdraw_3_8 (43/120).
Encoding transition withdraw_3_9 (44/120).
Encoding transition try_3 (45/120).
Encoding transition enter_3 (46/120).
Encoding transition exit_3 (47/120).
Encoding transition withdraw_4_0 (48/120).
Encoding transition withdraw_4_1 (49/120).
Encoding transition withdraw_4_2 (50/120).
Encoding transition withdraw_4_3 (51/120).
Encoding transition withdraw_4_5 (52/120).
Encoding transition withdraw_4_6 (53/120).
Encoding transition withdraw_4_7 (54/120).
Encoding transition withdraw_4_8 (55/120).
Encoding transition withdraw_4_9 (56/120).
Encoding transition try_4 (57/120).
Encoding transition enter_4 (58/120).
Encoding transition exit_4 (59/120).
Encoding transition withdraw_5_0 (60/120).
Encoding transition withdraw_5_1 (61/120).
Encoding transition withdraw_5_2 (62/120).
Encoding transition withdraw_5_3 (63/120).
Encoding transition withdraw_5_4 (64/120).
Encoding transition withdraw_5_6 (65/120).
Encoding transition withdraw_5_7 (66/120).
Encoding transition withdraw_5_8 (67/120).
Encoding transition withdraw_5_9 (68/120).
Encoding transition try_5 (69/120).
Encoding transition enter_5 (70/120).
Encoding transition exit_5 (71/120).
Encoding transition withdraw_6_0 (72/120).
Encoding transition withdraw_6_1 (73/120).
Encoding transition withdraw_6_2 (74/120).
Encoding transition withdraw_6_3 (75/120).
Encoding transition withdraw_6_4 (76/120).
Encoding transition withdraw_6_5 (77/120).
Encoding transition withdraw_6_7 (78/120).
Encoding transition withdraw_6_8 (79/120).
Encoding transition withdraw_6_9 (80/120).
Encoding transition try_6 (81/120).
Encoding transition enter_6 (82/120).
Encoding transition exit_6 (83/120).
Encoding transition withdraw_7_0 (84/120).
Encoding transition withdraw_7_1 (85/120).
Encoding transition withdraw_7_2 (86/120).
Encoding transition withdraw_7_3 (87/120).
Encoding transition withdraw_7_4 (88/120).
Encoding transition withdraw_7_5 (89/120).
Encoding transition withdraw_7_6 (90/120).
Encoding transition withdraw_7_8 (91/120).
Encoding transition withdraw_7_9 (92/120).
Encoding transition try_7 (93/120).
Encoding transition enter_7 (94/120).
Encoding transition exit_7 (95/120).
Encoding transition withdraw_8_0 (96/120).
Encoding transition withdraw_8_1 (97/120).
Encoding transition withdraw_8_2 (98/120).
Encoding transition withdraw_8_3 (99/120).
Encoding transition withdraw_8_4 (100/120).
Encoding transition withdraw_8_5 (101/120).
Encoding transition withdraw_8_6 (102/120).
Encoding transition withdraw_8_7 (103/120).
Encoding transition withdraw_8_9 (104/120).
Encoding transition try_8 (105/120).
Encoding transition enter_8 (106/120).
Encoding transition exit_8 (107/120).
Encoding transition withdraw_9_0 (108/120).
Encoding transition withdraw_9_1 (109/120).
Encoding transition withdraw_9_2 (110/120).
Encoding transition withdraw_9_3 (111/120).
Encoding transition withdraw_9_4 (112/120).
Encoding transition withdraw_9_5 (113/120).
Encoding transition withdraw_9_6 (114/120).
Encoding transition withdraw_9_7 (115/120).
Encoding transition withdraw_9_8 (116/120).
Encoding transition try_9 (117/120).
Encoding transition enter_9 (118/120).
Encoding transition exit_9 (119/120).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 5432KB
RS size: 6144 (6144)
----------------------------------------
End RS generation
----------------------------------------

FORMULA Dekker-PT-010-ReachabilityDeadlock-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-ReachabilityDeadlock-2 FALSE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400263805374

--------------------
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="Dekker-PT-010"
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/Dekker-PT-010.tgz
mv Dekker-PT-010 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 Dekker-PT-010, examination is ReachabilityDeadlock"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r01kn-qhx2-140025665600745"
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 ;