fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150801600
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
- - - DNF timeout

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 PolyORBNT-PT-S05J60, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198150801600
=====================================================================


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

BK_START 1401988362648

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: 909 NrTr: 1970)

net check time: 0m0sec

place and transition orderings generation:0m6sec

init dd package: 0m0sec


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

1700 2406 3767 6378 11393 12673 13366 13820 13503 13948 13629 14062 13897 14162 13983 14248 14051 13977 14372 14032 14418 14088 14462 14489 14880 15216 15394 15793 16049 16453 16626 17005 17277 17637 17829 18314 18371 18996 19064 19714 19840 20418 20550 21298 21868 22140 22794 23040 23653 23857 24507 24861 25343 25746 26428 26612 27236 27427 28196 28392 29029 29234 29876 30086 30764 30983 31615 31841 32552 32785 33533 34312 34442 35256 35396 36226 36368 37214 37371 38185 38375 39211 39391 40279 40481 41345 41515 42394 42571 43523 43783 44717 45255 45853 46381 46987 47433 48074 48601 49412 49754 50638 50991 51747 52106 53020 53386 54265 54636 55600 55977 56946 57331 58229 59322 59441 59848 60646 61054 61989 63136 63290 99070 104205 104218 104348 104352 104356 104360 104364 104368 104371 104374 104378 104381 104384 104387 104390 104393 104395 104402 104414 104422 104431 104440 104448 104531 104544 104552 104925 104932 104941 105265 114399 131473 133989 165860 167032 167151 167602 167461 167726 167574 167516 167940 167613 168028 167830 168095 168145 167805 168187 167964 168229 167896 167887 167887 167887 167887 168046 167887 167931 167890 167943 167893 167897 167901 167902 168035 167930 168088 167983 168052 168089 168139 168187 168237 168454 168349 168577

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="PolyORBNT-PT-S05J60"
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/PolyORBNT-PT-S05J60.tgz
mv PolyORBNT-PT-S05J60 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 PolyORBNT-PT-S05J60, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198150801600"
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 ;