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 SurprisePlanning-PT-none, examination is ReachabilityBounds
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r10ks-qhx2-140069022601043
=====================================================================

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

BK_START 1400844798797
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurprisePlanning (PT), instance none
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityBounds.xml INTO /home/mcc/execution/ReachabilityBounds.rgmedd-ctl
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-P -h 2000000000 -B 0 -C -f /home/mcc/execution/ReachabilityBounds.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 t1 (0/128).
Encoding transition t10 (1/128).
Encoding transition t100 (2/128).
Encoding transition t101 (3/128).
Encoding transition t102 (4/128).
Encoding transition t103 (5/128).
Encoding transition t104 (6/128).
Encoding transition t105 (7/128).
Encoding transition t106 (8/128).
Encoding transition t107 (9/128).
Encoding transition t108 (10/128).
Encoding transition t109 (11/128).
Encoding transition t11 (12/128).
Encoding transition t110 (13/128).
Encoding transition t111 (14/128).
Encoding transition t112 (15/128).
Encoding transition t113 (16/128).
Encoding transition t114 (17/128).
Encoding transition t115 (18/128).
Encoding transition t116 (19/128).
Encoding transition t117 (20/128).
Encoding transition t118 (21/128).
Encoding transition t119 (22/128).
Encoding transition t12 (23/128).
Encoding transition t120 (24/128).
Encoding transition t121 (25/128).
Encoding transition t122 (26/128).
Encoding transition t123 (27/128).
Encoding transition t124 (28/128).
Encoding transition t125 (29/128).
Encoding transition t126 (30/128).
Encoding transition t127 (31/128).
Encoding transition t128 (32/128).
Encoding transition t13 (33/128).
Encoding transition t14 (34/128).
Encoding transition t15 (35/128).
Encoding transition t16 (36/128).
Encoding transition t17 (37/128).
Encoding transition t18 (38/128).
Encoding transition t19 (39/128).
Encoding transition t2 (40/128).
Encoding transition t20 (41/128).
Encoding transition t21 (42/128).
Encoding transition t22 (43/128).
Encoding transition t23 (44/128).
Encoding transition t24 (45/128).
Encoding transition t25 (46/128).
Encoding transition t26 (47/128).
Encoding transition t27 (48/128).
Encoding transition t28 (49/128).
Encoding transition t29 (50/128).
Encoding transition t3 (51/128).
Encoding transition t30 (52/128).
Encoding transition t31 (53/128).
Encoding transition t32 (54/128).
Encoding transition t33 (55/128).
Encoding transition t34 (56/128).
Encoding transition t35 (57/128).
Encoding transition t36 (58/128).
Encoding transition t37 (59/128).
Encoding transition t38 (60/128).
Encoding transition t39 (61/128).
Encoding transition t4 (62/128).
Encoding transition t40 (63/128).
Encoding transition t41 (64/128).
Encoding transition t42 (65/128).
Encoding transition t43 (66/128).
Encoding transition t44 (67/128).
Encoding transition t45 (68/128).
Encoding transition t46 (69/128).
Encoding transition t47 (70/128).
Encoding transition t48 (71/128).
Encoding transition t49 (72/128).
Encoding transition t5 (73/128).
Encoding transition t50 (74/128).
Encoding transition t51 (75/128).
Encoding transition t52 (76/128).
Encoding transition t53 (77/128).
Encoding transition t54 (78/128).
Encoding transition t55 (79/128).
Encoding transition t56 (80/128).
Encoding transition t57 (81/128).
Encoding transition t58 (82/128).
Encoding transition t59 (83/128).
Encoding transition t6 (84/128).
Encoding transition t60 (85/128).
Encoding transition t61 (86/128).
Encoding transition t62 (87/128).
Encoding transition t63 (88/128).
Encoding transition t64 (89/128).
Encoding transition t65 (90/128).
Encoding transition t66 (91/128).
Encoding transition t67 (92/128).
Encoding transition t68 (93/128).
Encoding transition t69 (94/128).
Encoding transition t7 (95/128).
Encoding transition t70 (96/128).
Encoding transition t71 (97/128).
Encoding transition t72 (98/128).
Encoding transition t73 (99/128).
Encoding transition t74 (100/128).
Encoding transition t75 (101/128).
Encoding transition t76 (102/128).
Encoding transition t77 (103/128).
Encoding transition t78 (104/128).
Encoding transition t79 (105/128).
Encoding transition t8 (106/128).
Encoding transition t80 (107/128).
Encoding transition t81 (108/128).
Encoding transition t82 (109/128).
Encoding transition t83 (110/128).
Encoding transition t84 (111/128).
Encoding transition t85 (112/128).
Encoding transition t86 (113/128).
Encoding transition t87 (114/128).
Encoding transition t88 (115/128).
Encoding transition t89 (116/128).
Encoding transition t9 (117/128).
Encoding transition t90 (118/128).
Encoding transition t91 (119/128).
Encoding transition t92 (120/128).
Encoding transition t93 (121/128).
Encoding transition t94 (122/128).
Encoding transition t95 (123/128).
Encoding transition t96 (124/128).
Encoding transition t97 (125/128).
Encoding transition t98 (126/128).
Encoding transition t99 (127/128).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 5640KB
RS size: 19327352832 (1.93274e+10)
----------------------------------------
End RS generation
----------------------------------------

FORMULA Planning-PT-none-ReachabilityBounds-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-2 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-3 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-4 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-5 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-6 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-7 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-8 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-9 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Planning-PT-none-ReachabilityBounds-10 TRUE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400844856006

--------------------
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="SurprisePlanning-PT-none"
export BK_EXAMINATION="ReachabilityBounds"
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/SurprisePlanning-PT-none.tgz
mv SurprisePlanning-PT-none 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 SurprisePlanning-PT-none, examination is ReachabilityBounds"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r10ks-qhx2-140069022601043"
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 ;