fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150000664
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 Diffusion2D-PT-D30N150, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198150000664
=====================================================================


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

BK_START 1401984583482

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: 900 NrTr: 6844)

net check time: 0m0sec

place and transition orderings generation:0m3sec

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

942 942 1001 987 1062 1034 1125 1080 1190 1130 1262 1177 1326 1224 1404 1278 1478 1326 1554 1383 1632 1442 1723 1503 1806 1554 1917 1618 2006 1698 1979 1752 1572 1822 1614 1894 1656 1968 1716 2044 1778 2102 1842 2181 1887 2240 1954 2322 2000 2430 2070 2492 2117 2606 2164 2697 2238 2818 2286 2914 2334 2982 2412 3143 2492 3246 2574 3351 2658 3526 2710 3707 2832 2412 2922 2454 3014 2496 3108 2538 3204 2619 3262 2702 3361 2787 3420 2832 3522 2920 3626 2966 3732 3057 3886 3104 3997 3198 4110 3246 4225 3294 4342 3392 4461 3492 4634 3594 4811 3645 4992 3750 5177 3912 3252 3966 3294 4077 3336 4248 3378 4305 3479 4422 3582 4480 3687 4600 3732 4659 3840 4846 3886 4972 3997 5034 4044 5230 4091 5362 4206 5565 4254 5702 4302 5841 4421 6054 4542 6198 4665 6492 4790 6642 4842 7022 5046 4134 5177 4176 5310 4218 5445 4260 5582 4382 5640 4506 5780 4632 5839 4760 5982 4806 6127 4852 6274 4984 6510 5031 6662 5166 6816 5214 6972 5262 7130 5401 7290 5542 7638 5685 7804 5830 8067 5882 8334 6126 4974 6180 5016 6430 5058 6585 5100 6642 5242 6800 5386 6960 5532 7019 5577 7182 5726 7347 5772 7514 5924 7790 5971 7854 6018 8136 6174 8312 6222 8490 6381 8670 6542 8965 6705 9150 6756 9567 6922 9758 7206 9591 7260 5856 7432 5898 7606 5940 7782 6102 7960 6266 8018 6432 8199 6477 8258 6646 8442 6692 8754 6864 8816 6911 9134 6958 9327 7134 9652 7182 9850 7230 9918 7410 10385 7592 10590 7776 10797 7962 11278 8014 11765 8340 6696 8532 6738 8726 6780 8922 6822 9120 7005 9178 7190 9379 7377 9438 7422 9642 7612 9848 7658 10056 7851 10414 7898 10627 7945 7205 7217 7229 7241 7253 7265 7277 7289 7302 7314 7326 7338 7350 7362 7375 7388 7400 7413 7426 7438 7451 7463 7476 7489 7502 7522 7543

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