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


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

BK_START 1401988417768

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: 664 NrTr: 12050)

net check time: 0m0sec

place and transition orderings generation:2m33sec

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: 0m2sec

1296 2429 3921 4827 5148 5304 5614 5783 6154 6309 6687 6832 7102 7400 7744 7916 8217 8651 8959 9430 9682 10279 10582 11281 11559 12159 12312 12843 13494 14046 14694 15046 15970 16325 17088 17280 17928 18676 19333 20094 20523 21614 22052 23108 23528 24468 24615 25315 26116 26531 27676 28135 29270 29419 30257 31200 32017 32950 33430 34796 35237 36454 36630 37569 38616 39142 40574 41109 42496 42583 43596 44739 50793 51153 51482 51453 51630 51599 51453 51587 51455 51636 51461 51480 51605 51502 51687 51514 51527 51623 51546 51735 51564 51577 51642 51592 51779 51607 51683 51721 51927 52078 51901 51975 52163 52374 52600 52423 52520 52780 52751 52955 53121 53234 53538 53525 53764 53970 54108 54654 54478 54788 55070 55376 55842 55665 55836 56308 56301 56666 56996 57198 58033 57750 58161 58537 58915 59582 59405 59638 60300 60283 60785 61247 61511 62414 62237 62782 63290 63719 63848 64368 64776 65195 65213 65244 65352 65408 65481 65563 65542 65635 65755 65958 66189 66229 66481 66757 67063 67396 67748 68298 68694 69118 69244 69707 70192 70707 70893 71442 72017 72613 73234 73882 74732 94413 94835 95164 95499 95789 99166 122792 123503 124246 124311 124370 124376 124381 124387 124392 124397 124402 125567 125888 125415 141588 142756 143570 143570 143570 143571 143577 143582 143588 143593 143570 149611 149761 149919 150022 150064 153025 159866 160521 161008 161060 161119 161125 161131 161136 161141 161146 161086 161232 160233 160271 164623 166580 166903 167119 167183 170358 177788 178398 178865 178907 178966 178972 178978 178983 178988 178993 178933 179067 177156 181174 181483 181811 182077 184313 187236 195701 196170 196659 196691 196750 196756 196761 196767 196772 196777 196717 196841 194808 194630 200171 202254 202312 202232 204992 214283 214444 214711 214722 214779 214799 214805 214810 214816 214821 214761 214877 213436 213982 219622 219992 220340 221966 224687 231946 233673 233754 233773 233809 233841 233849 233854 233860 233865 233870 233911 233799 232149 240122 240363 240621 240755 240812 244448 252773 252696 252730 252741 252788 252794 252802 252807 252812 252817 252931 252661 252204 259007 259317 259664 261024 260952 264670 273420 273114 273135 273135 273180 273185 273191 273196 273204 273209 273146 273223 271485 271409 281785 282087 282315 282180 284317 297166 297591 298190 298190 298208 298228 298234 298239 298244 298250 298254 298261 295314 294195 304675 304999 305310 305175 307098 320351 319663 319734 319753 319753 319785 319793 319799 319804 319809 319814 319828 319337 317085 329890 329959 329932 329809 329719 334026 347551 348124 348220 348220 348236 348242 348250 348255 348261 348265 348298 347688 344197 357282 357490 357574 357646 357514 361738 374708 374587 374667 374667 374667 374667 374667 374672 374680 374685 374865

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