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 marcie
Input is SharedMemory-PT-000100, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r05kn-ovh1-140043892403407
=====================================================================

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

BK_START 1400461634820

Marcie rev. 1291 (build: mcc on 2014-04-30)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 10301 NrTr: 20100)

net check time: 0m0sec

place and transition orderings generation:7m58sec

init dd package: 0m0sec


before gc: list nodes free: 688966

after gc: idd nodes used:5657, unused:15994343; list nodes free:64971819

before gc: list nodes free: 608804

after gc: idd nodes used:7999, unused:15992001; list nodes free:64955367

before gc: list nodes free: 648163

after gc: idd nodes used:9796, unused:15990204; list nodes free:64942748

BK_TIME_CONFINEMENT_REACHED

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

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

19546 22057 23443 24784 26353 28013 29764 29764 31606 33539 33539 35563 35563 37677 37677 39883 39883 42179 42179 42179 44944 46258 46321 46482 46563 49495 49495 49516 49517 49518 52617 52617 52654 52662 52669 52685 55953 55953 55954 55954 55954 55955 59412 59415 59419 59440 59440 59450 59456 63062 63063 63063 63068 63073 63073 63087 66862 66862 66862 66862 66862 66862 66864 66864 70810 70811 70811 70811 70811 70811 70811 70811 70816 74616 74616 74616 74616 74616 75548 75549 75891 75893 80025 80025 80215 80217 80217 80218 80219 80220 80220 80222 80226 84255 84259 84267 84275 84279 84283 84283 84283 84283 84283 84283 88774 88778 88778 88778 88778 88778 88787 88787 88788 88788 88799 88799 93254 93299 93343 93431 93475 93563 93607 93607 93607 93607 93760 93760 93760 93760 177540 177549 177588 177588 177588 177588 177588 177588 177617 177617 177617 177617 177617 177769 186407 186407 186407 186407 186407 186407 186407 186535 186535 186535 186535 186535 186535 186535 186535 186535 365194 365207 365248 365248 365248 365248 365248

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="SharedMemory-PT-000100"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="marcie"
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/SharedMemory-PT-000100.tgz
mv SharedMemory-PT-000100 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool marcie"
echo " Input is SharedMemory-PT-000100, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r05kn-ovh1-140043892403407"
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 ;