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-015, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r01kn-qhx2-140025665600764
=====================================================================

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

BK_START 1400263926999
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running Dekker (PT), instance 015
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 withdraw_0_1 (0/255).
Encoding transition withdraw_0_2 (1/255).
Encoding transition withdraw_0_3 (2/255).
Encoding transition withdraw_0_4 (3/255).
Encoding transition withdraw_0_5 (4/255).
Encoding transition withdraw_0_6 (5/255).
Encoding transition withdraw_0_7 (6/255).
Encoding transition withdraw_0_8 (7/255).
Encoding transition withdraw_0_9 (8/255).
Encoding transition withdraw_0_10 (9/255).
Encoding transition withdraw_0_11 (10/255).
Encoding transition withdraw_0_12 (11/255).
Encoding transition withdraw_0_13 (12/255).
Encoding transition withdraw_0_14 (13/255).
Encoding transition try_0 (14/255).
Encoding transition enter_0 (15/255).
Encoding transition exit_0 (16/255).
Encoding transition withdraw_1_0 (17/255).
Encoding transition withdraw_1_2 (18/255).
Encoding transition withdraw_1_3 (19/255).
Encoding transition withdraw_1_4 (20/255).
Encoding transition withdraw_1_5 (21/255).
Encoding transition withdraw_1_6 (22/255).
Encoding transition withdraw_1_7 (23/255).
Encoding transition withdraw_1_8 (24/255).
Encoding transition withdraw_1_9 (25/255).
Encoding transition withdraw_1_10 (26/255).
Encoding transition withdraw_1_11 (27/255).
Encoding transition withdraw_1_12 (28/255).
Encoding transition withdraw_1_13 (29/255).
Encoding transition withdraw_1_14 (30/255).
Encoding transition try_1 (31/255).
Encoding transition enter_1 (32/255).
Encoding transition exit_1 (33/255).
Encoding transition withdraw_2_0 (34/255).
Encoding transition withdraw_2_1 (35/255).
Encoding transition withdraw_2_3 (36/255).
Encoding transition withdraw_2_4 (37/255).
Encoding transition withdraw_2_5 (38/255).
Encoding transition withdraw_2_6 (39/255).
Encoding transition withdraw_2_7 (40/255).
Encoding transition withdraw_2_8 (41/255).
Encoding transition withdraw_2_9 (42/255).
Encoding transition withdraw_2_10 (43/255).
Encoding transition withdraw_2_11 (44/255).
Encoding transition withdraw_2_12 (45/255).
Encoding transition withdraw_2_13 (46/255).
Encoding transition withdraw_2_14 (47/255).
Encoding transition try_2 (48/255).
Encoding transition enter_2 (49/255).
Encoding transition exit_2 (50/255).
Encoding transition withdraw_3_0 (51/255).
Encoding transition withdraw_3_1 (52/255).
Encoding transition withdraw_3_2 (53/255).
Encoding transition withdraw_3_4 (54/255).
Encoding transition withdraw_3_5 (55/255).
Encoding transition withdraw_3_6 (56/255).
Encoding transition withdraw_3_7 (57/255).
Encoding transition withdraw_3_8 (58/255).
Encoding transition withdraw_3_9 (59/255).
Encoding transition withdraw_3_10 (60/255).
Encoding transition withdraw_3_11 (61/255).
Encoding transition withdraw_3_12 (62/255).
Encoding transition withdraw_3_13 (63/255).
Encoding transition withdraw_3_14 (64/255).
Encoding transition try_3 (65/255).
Encoding transition enter_3 (66/255).
Encoding transition exit_3 (67/255).
Encoding transition withdraw_4_0 (68/255).
Encoding transition withdraw_4_1 (69/255).
Encoding transition withdraw_4_2 (70/255).
Encoding transition withdraw_4_3 (71/255).
Encoding transition withdraw_4_5 (72/255).
Encoding transition withdraw_4_6 (73/255).
Encoding transition withdraw_4_7 (74/255).
Encoding transition withdraw_4_8 (75/255).
Encoding transition withdraw_4_9 (76/255).
Encoding transition withdraw_4_10 (77/255).
Encoding transition withdraw_4_11 (78/255).
Encoding transition withdraw_4_12 (79/255).
Encoding transition withdraw_4_13 (80/255).
Encoding transition withdraw_4_14 (81/255).
Encoding transition try_4 (82/255).
Encoding transition enter_4 (83/255).
Encoding transition exit_4 (84/255).
Encoding transition withdraw_5_0 (85/255).
Encoding transition withdraw_5_1 (86/255).
Encoding transition withdraw_5_2 (87/255).
Encoding transition withdraw_5_3 (88/255).
Encoding transition withdraw_5_4 (89/255).
Encoding transition withdraw_5_6 (90/255).
Encoding transition withdraw_5_7 (91/255).
Encoding transition withdraw_5_8 (92/255).
Encoding transition withdraw_5_9 (93/255).
Encoding transition withdraw_5_10 (94/255).
Encoding transition withdraw_5_11 (95/255).
Encoding transition withdraw_5_12 (96/255).
Encoding transition withdraw_5_13 (97/255).
Encoding transition withdraw_5_14 (98/255).
Encoding transition try_5 (99/255).
Encoding transition enter_5 (100/255).
Encoding transition exit_5 (101/255).
Encoding transition withdraw_6_0 (102/255).
Encoding transition withdraw_6_1 (103/255).
Encoding transition withdraw_6_2 (104/255).
Encoding transition withdraw_6_3 (105/255).
Encoding transition withdraw_6_4 (106/255).
Encoding transition withdraw_6_5 (107/255).
Encoding transition withdraw_6_7 (108/255).
Encoding transition withdraw_6_8 (109/255).
Encoding transition withdraw_6_9 (110/255).
Encoding transition withdraw_6_10 (111/255).
Encoding transition withdraw_6_11 (112/255).
Encoding transition withdraw_6_12 (113/255).
Encoding transition withdraw_6_13 (114/255).
Encoding transition withdraw_6_14 (115/255).
Encoding transition try_6 (116/255).
Encoding transition enter_6 (117/255).
Encoding transition exit_6 (118/255).
Encoding transition withdraw_7_0 (119/255).
Encoding transition withdraw_7_1 (120/255).
Encoding transition withdraw_7_2 (121/255).
Encoding transition withdraw_7_3 (122/255).
Encoding transition withdraw_7_4 (123/255).
Encoding transition withdraw_7_5 (124/255).
Encoding transition withdraw_7_6 (125/255).
Encoding transition withdraw_7_8 (126/255).
Encoding transition withdraw_7_9 (127/255).
Encoding transition withdraw_7_10 (128/255).
Encoding transition withdraw_7_11 (129/255).
Encoding transition withdraw_7_12 (130/255).
Encoding transition withdraw_7_13 (131/255).
Encoding transition withdraw_7_14 (132/255).
Encoding transition try_7 (133/255).
Encoding transition enter_7 (134/255).
Encoding transition exit_7 (135/255).
Encoding transition withdraw_8_0 (136/255).
Encoding transition withdraw_8_1 (137/255).
Encoding transition withdraw_8_2 (138/255).
Encoding transition withdraw_8_3 (139/255).
Encoding transition withdraw_8_4 (140/255).
Encoding transition withdraw_8_5 (141/255).
Encoding transition withdraw_8_6 (142/255).
Encoding transition withdraw_8_7 (143/255).
Encoding transition withdraw_8_9 (144/255).
Encoding transition withdraw_8_10 (145/255).
Encoding transition withdraw_8_11 (146/255).
Encoding transition withdraw_8_12 (147/255).
Encoding transition withdraw_8_13 (148/255).
Encoding transition withdraw_8_14 (149/255).
Encoding transition try_8 (150/255).
Encoding transition enter_8 (151/255).
Encoding transition exit_8 (152/255).
Encoding transition withdraw_9_0 (153/255).
Encoding transition withdraw_9_1 (154/255).
Encoding transition withdraw_9_2 (155/255).
Encoding transition withdraw_9_3 (156/255).
Encoding transition withdraw_9_4 (157/255).
Encoding transition withdraw_9_5 (158/255).
Encoding transition withdraw_9_6 (159/255).
Encoding transition withdraw_9_7 (160/255).
Encoding transition withdraw_9_8 (161/255).
Encoding transition withdraw_9_10 (162/255).
Encoding transition withdraw_9_11 (163/255).
Encoding transition withdraw_9_12 (164/255).
Encoding transition withdraw_9_13 (165/255).
Encoding transition withdraw_9_14 (166/255).
Encoding transition try_9 (167/255).
Encoding transition enter_9 (168/255).
Encoding transition exit_9 (169/255).
Encoding transition withdraw_10_0 (170/255).
Encoding transition withdraw_10_1 (171/255).
Encoding transition withdraw_10_2 (172/255).
Encoding transition withdraw_10_3 (173/255).
Encoding transition withdraw_10_4 (174/255).
Encoding transition withdraw_10_5 (175/255).
Encoding transition withdraw_10_6 (176/255).
Encoding transition withdraw_10_7 (177/255).
Encoding transition withdraw_10_8 (178/255).
Encoding transition withdraw_10_9 (179/255).
Encoding transition withdraw_10_11 (180/255).
Encoding transition withdraw_10_12 (181/255).
Encoding transition withdraw_10_13 (182/255).
Encoding transition withdraw_10_14 (183/255).
Encoding transition try_10 (184/255).
Encoding transition enter_10 (185/255).
Encoding transition exit_10 (186/255).
Encoding transition withdraw_11_0 (187/255).
Encoding transition withdraw_11_1 (188/255).
Encoding transition withdraw_11_2 (189/255).
Encoding transition withdraw_11_3 (190/255).
Encoding transition withdraw_11_4 (191/255).
Encoding transition withdraw_11_5 (192/255).
Encoding transition withdraw_11_6 (193/255).
Encoding transition withdraw_11_7 (194/255).
Encoding transition withdraw_11_8 (195/255).
Encoding transition withdraw_11_9 (196/255).
Encoding transition withdraw_11_10 (197/255).
Encoding transition withdraw_11_12 (198/255).
Encoding transition withdraw_11_13 (199/255).
Encoding transition withdraw_11_14 (200/255).
Encoding transition try_11 (201/255).
Encoding transition enter_11 (202/255).
Encoding transition exit_11 (203/255).
Encoding transition withdraw_12_0 (204/255).
Encoding transition withdraw_12_1 (205/255).
Encoding transition withdraw_12_2 (206/255).
Encoding transition withdraw_12_3 (207/255).
Encoding transition withdraw_12_4 (208/255).
Encoding transition withdraw_12_5 (209/255).
Encoding transition withdraw_12_6 (210/255).
Encoding transition withdraw_12_7 (211/255).
Encoding transition withdraw_12_8 (212/255).
Encoding transition withdraw_12_9 (213/255).
Encoding transition withdraw_12_10 (214/255).
Encoding transition withdraw_12_11 (215/255).
Encoding transition withdraw_12_13 (216/255).
Encoding transition withdraw_12_14 (217/255).
Encoding transition try_12 (218/255).
Encoding transition enter_12 (219/255).
Encoding transition exit_12 (220/255).
Encoding transition withdraw_13_0 (221/255).
Encoding transition withdraw_13_1 (222/255).
Encoding transition withdraw_13_2 (223/255).
Encoding transition withdraw_13_3 (224/255).
Encoding transition withdraw_13_4 (225/255).
Encoding transition withdraw_13_5 (226/255).
Encoding transition withdraw_13_6 (227/255).
Encoding transition withdraw_13_7 (228/255).
Encoding transition withdraw_13_8 (229/255).
Encoding transition withdraw_13_9 (230/255).
Encoding transition withdraw_13_10 (231/255).
Encoding transition withdraw_13_11 (232/255).
Encoding transition withdraw_13_12 (233/255).
Encoding transition withdraw_13_14 (234/255).
Encoding transition try_13 (235/255).
Encoding transition enter_13 (236/255).
Encoding transition exit_13 (237/255).
Encoding transition withdraw_14_0 (238/255).
Encoding transition withdraw_14_1 (239/255).
Encoding transition withdraw_14_2 (240/255).
Encoding transition withdraw_14_3 (241/255).
Encoding transition withdraw_14_4 (242/255).
Encoding transition withdraw_14_5 (243/255).
Encoding transition withdraw_14_6 (244/255).
Encoding transition withdraw_14_7 (245/255).
Encoding transition withdraw_14_8 (246/255).
Encoding transition withdraw_14_9 (247/255).
Encoding transition withdraw_14_10 (248/255).
Encoding transition withdraw_14_11 (249/255).
Encoding transition withdraw_14_12 (250/255).
Encoding transition withdraw_14_13 (251/255).
Encoding transition try_14 (252/255).
Encoding transition enter_14 (253/255).
Encoding transition exit_14 (254/255).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 8964KB
RS size: 278528 (278528)
----------------------------------------
End RS generation
----------------------------------------

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

BK_STOP 1400263934018

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