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


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

BK_START 1401988325957

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: 489 NrTr: 1400)

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

956 1338 1327 1990 2005 4592 5930 6581 7007 7310 7779 8045 8172 8505 8642 8995 9182 9322 9729 10162 10371 10790 10990 11214 11638 11816 12281 12556 12753 13228 13726 13978 14372 14549 14846 15288 15532 15937 16468 16796 17306 17547 17856 18381 18641 18987 19630 20294 20755 21302 21553 22014 22561 22824 23362 24026 24494 25109 25390 25829 26425 26688 27138 27753 28045 28522 29164 29703 30293 30921 31216 31856 32532 32845 33518 34291 34912 35624 36004 36610 37304 37623 38226 38925 39513 40245 40998 41347 42095 42723 43033 43785 44430 44748 45797 45741 47649 48508 48801 48838 48804 48806 48808 48808 48808 48809 48817 48812 48867 48812 48898 48812 48812 48812 48820 48824 48833 48840 48882 49059 48984 49089 49163 49275 49330 49427 49639 49599 49937 49851 50011 50089 50225 50389 50550 50844 50797 50994 51091 51274 51488 51684 52030 51994 52233 52350 52573 52827 53065 53412 53438 54132 53981 54278 54425 54704 55100 55431 55748 55753 56093 56261 56585 57032 57411 57743 57790 58233 58930 59086 59087 59087 59089 59168 59093 59093 59093 59094 59183 59096 59101 59096 59096 59232 59134 59306 59245 59319 59412 59457 59564 59685 59941 59880 60110 60165 60238 60402 60480 60652 60833 61126 61118 61402 61425 61640 61871 61985 62230 62482 62866 62873 63225 63432 63575 63881 64032 64640 64665 65106 65165 65585 65819 66098 66543 66735 67004 67159 67321 67494 67681 68061 68105 68355 68640 68912 69204 69569 69901 70239 70622 70972 71323 71701 72373 72811 73288 73757 74206 74658 75165 75645 76142 97556 97578 115132 115140 115148 115154 115159 115175 115189 116004 116240 116255 120038 132179 132179 132179 132179 132179 132179 132179 132199 132347 145760 146015 152318 157479 157479 157479 157479 157479 157479 157549 157616 157633 159157 160235 169828 170353 174730 179944 179944 179944 179944 179944 179944 180008 180070 180086 180773 180984 191687 191709 201289 201289 201289 201289 201289 201289 201289 201395 201411 201718 202394 213520 213484 218166 223572 223572 223572 223572 223572 223572 223748 223666 223681 224405 224187 235469 236951 246381 246381 246381 246381 246381 246381 246384 246448 246468 247253 249185 260198 260116 268756 269859 269859 269859 269859 269859 269859 269996 269923 269909 270112 281852 281440 285556 289954 289954 289954 289954 289954 289954 289976 289993 290010 290139 290939 302952 302714 313450 313522 313522 313522 313522 313522 313522 313636 313556 313540 313224 324572 323622 326811 331380 331380 331380 331380 331380 331380 331390 331399 331415 330902 330688 343115 342730 353543 353600 353600 353600 353600 353600 353600 353719 353637 353680 351820 366268 365253 369738 376815 376815 376815 376815 376815 376815 376815 376828 376830 375718 374592 387721 386449 394697 394702 394702 394702 394702 394702 394702 394782 394724 394732 394114 407390 406960 408903 414387 414387 414387 414387 414387 414387 414387 414399 414400 413234 412368 427124 425398 435114 435670 435670 435670 435670 435670 435670 435805 435682 435704 434836 433746 446367 445594 455303 455303 455303 455303 455303 455303 455303

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