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-1668
Executing tool greatspn
Input is DatabaseWithMutex-PT-20, examination is ReachabilityDeadlock
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r21sr-ovh1-140191459900381
=====================================================================

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

BK_START 1401924868879
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running DatabaseWithMutex (PT), instance 20
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/ReachabilityDeadlock.xml INTO /home/mcc/execution/ReachabilityDeadlock.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 60 -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 SendMsg_10_7 (0/3200).
Encoding transition SendMsg_15_18 (1/3200).
Encoding transition Change_13_20 (2/3200).
Encoding transition end_update_10_4 (3/3200).
Encoding transition end_update_13_7 (4/3200).
Encoding transition Acquire_10_15 (5/3200).
Encoding transition Acquire_6_5 (6/3200).
Encoding transition Change_12_12 (7/3200).
Encoding transition SendMsg_11_20 (8/3200).
Encoding transition Update_1_6 (9/3200).
Encoding transition Release_19_11 (10/3200).
Encoding transition Change_17_6 (11/3200).
Encoding transition SendReply_12_6 (12/3200).
Encoding transition Start_2_15 (13/3200).
Encoding transition SendReply_3_12 (14/3200).
Encoding transition Acquire_5_13 (15/3200).
Encoding transition SendReply_17_8 (16/3200).
Encoding transition Change_6_14 (17/3200).
Encoding transition SendReply_8_19 (18/3200).
Encoding transition SendMsg_19_9 (19/3200).
Encoding transition Start_17_14 (20/3200).
Encoding transition SendMsg_8_13 (21/3200).
Encoding transition Update_12_3 (22/3200).
Encoding transition Update_9_15 (23/3200).
Encoding transition SendMsg_10_15 (24/3200).
Encoding transition Start_5_11 (25/3200).
Encoding transition SendMsg_3_6 (26/3200).
Encoding transition SendMsg_17_5 (27/3200).
Encoding transition Acquire_19_5 (28/3200).
Encoding transition end_update_13_14 (29/3200).
Encoding transition Acquire_20_20 (30/3200).
Encoding transition Acquire_6_17 (31/3200).
Encoding transition Change_17_18 (32/3200).
Encoding transition Update_18_18 (33/3200).

BK_STOP 1401928167741

--------------------
content from stderr:

Cannot read input file model.bnd
terminate called after throwing an instance of 'MEDDLY::error'
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 167: 1751 Aborted ~/BenchKit/bin/bin/RGMEDD model ${PLACE_ORDER} ${MEDDLY_CACHE} ${BOUND} -C -f ${NEW_FRM}

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="DatabaseWithMutex-PT-20"
export BK_EXAMINATION="ReachabilityDeadlock"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/srv/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/DatabaseWithMutex-PT-20.tgz
mv DatabaseWithMutex-PT-20 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is DatabaseWithMutex-PT-20, examination is ReachabilityDeadlock"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r21sr-ovh1-140191459900381"
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 ;