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

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

BK_START 1400837857285
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running SurprisePhilosophers (PT), instance 000020
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 48 -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 FF1a_1 (0/100).
Encoding transition FF1a_8 (1/100).
Encoding transition FF1a_9 (2/100).
Encoding transition FF1a_6 (3/100).
Encoding transition FF1a_7 (4/100).
Encoding transition FF1a_4 (5/100).
Encoding transition FF1a_5 (6/100).
Encoding transition FF1a_2 (7/100).
Encoding transition FF1a_3 (8/100).
Encoding transition FF1a_17 (9/100).
Encoding transition FF1a_16 (10/100).
Encoding transition FF1a_15 (11/100).
Encoding transition FF1a_14 (12/100).
Encoding transition FF1a_13 (13/100).
Encoding transition FF1a_12 (14/100).
Encoding transition FF1a_11 (15/100).
Encoding transition FF1a_10 (16/100).
Encoding transition FF1b_5 (17/100).
Encoding transition FF1b_4 (18/100).
Encoding transition FF1b_3 (19/100).
Encoding transition FF1b_2 (20/100).
Encoding transition FF1b_1 (21/100).
Encoding transition FF1a_20 (22/100).
Encoding transition FF1a_19 (23/100).
Encoding transition FF1a_18 (24/100).
Encoding transition FF1b_15 (25/100).
Encoding transition FF1b_14 (26/100).
Encoding transition FF1b_17 (27/100).
Encoding transition FF1b_16 (28/100).
Encoding transition FF1b_19 (29/100).
Encoding transition FF1b_18 (30/100).
Encoding transition FF2a_1 (31/100).
Encoding transition FF1b_20 (32/100).
Encoding transition FF1b_7 (33/100).
Encoding transition FF1b_6 (34/100).
Encoding transition FF1b_9 (35/100).
Encoding transition FF1b_8 (36/100).
Encoding transition FF1b_11 (37/100).
Encoding transition FF1b_10 (38/100).
Encoding transition FF1b_13 (39/100).
Encoding transition FF1b_12 (40/100).
Encoding transition FF2a_10 (41/100).
Encoding transition FF2a_11 (42/100).
Encoding transition FF2a_12 (43/100).
Encoding transition FF2a_13 (44/100).
Encoding transition FF2a_14 (45/100).
Encoding transition FF2a_15 (46/100).
Encoding transition FF2a_16 (47/100).
Encoding transition FF2a_17 (48/100).
Encoding transition FF2a_2 (49/100).
Encoding transition FF2a_3 (50/100).
Encoding transition FF2a_4 (51/100).
Encoding transition FF2a_5 (52/100).
Encoding transition FF2a_6 (53/100).
Encoding transition FF2a_7 (54/100).
Encoding transition FF2a_8 (55/100).
Encoding transition FF2a_9 (56/100).
Encoding transition FF2b_9 (57/100).
Encoding transition FF2b_8 (58/100).
Encoding transition FF2b_7 (59/100).
Encoding transition FF2b_6 (60/100).
Encoding transition FF2b_13 (61/100).
Encoding transition FF2b_12 (62/100).
Encoding transition FF2b_11 (63/100).
Encoding transition FF2b_10 (64/100).
Encoding transition FF2b_1 (65/100).
Encoding transition FF2a_20 (66/100).
Encoding transition FF2a_19 (67/100).
Encoding transition FF2a_18 (68/100).
Encoding transition FF2b_5 (69/100).
Encoding transition FF2b_4 (70/100).
Encoding transition FF2b_3 (71/100).
Encoding transition FF2b_2 (72/100).
Encoding transition End_4 (73/100).
Encoding transition End_5 (74/100).
Encoding transition End_2 (75/100).
Encoding transition End_3 (76/100).
Encoding transition End_8 (77/100).
Encoding transition End_9 (78/100).
Encoding transition End_6 (79/100).
Encoding transition End_7 (80/100).
Encoding transition FF2b_16 (81/100).
Encoding transition FF2b_17 (82/100).
Encoding transition FF2b_14 (83/100).
Encoding transition FF2b_15 (84/100).
Encoding transition FF2b_20 (85/100).
Encoding transition End_1 (86/100).
Encoding transition FF2b_18 (87/100).
Encoding transition FF2b_19 (88/100).
Encoding transition End_19 (89/100).
Encoding transition End_18 (90/100).
Encoding transition End_20 (91/100).
Encoding transition End_15 (92/100).
Encoding transition End_14 (93/100).
Encoding transition End_17 (94/100).
Encoding transition End_16 (95/100).
Encoding transition End_11 (96/100).
Encoding transition End_10 (97/100).
Encoding transition End_13 (98/100).
Encoding transition End_12 (99/100).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 5352KB
RS size: 3486784401 (3.48678e+09)
----------------------------------------
End RS generation
----------------------------------------

FORMULA Philosophers-COL-000020-ReachabilityBounds-1 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-2 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-3 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-4 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-5 TRUE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-6 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-7 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-8 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-9 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA Philosophers-COL-000020-ReachabilityBounds-10 TRUE TECHNIQUES DECISION_DIAGRAMS
Ok.

BK_STOP 1400838037645

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