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 CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r01kn-qhx2-140025665600749
=====================================================================

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

BK_START 1400263840897
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Dekker (PT), instance 010
MODEL_DIR = /home/mcc/execution
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 1 -C -f /home/mcc/execution/CTLCardinality.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: 5424KB
RS size: 6144 (6144)
----------------------------------------
End RS generation
----------------------------------------

FORMULA Dekker-PT-010-CTLCardinality-1 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-2 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-3 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-4 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-5 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-6 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-7 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-8 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-9 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Dekker-PT-010-CTLCardinality-10 TRUE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400263842059

--------------------
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="CTLCardinality"
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 CTLCardinality"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r01kn-qhx2-140025665600749"
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 ;