fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r01kn-qhx2-140025666601873
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-1667
Executing tool marcie
Input is CSRepetitions-PT-05, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r01kn-qhx2-140025666601873
=====================================================================


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

BK_START 1400279598075

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: 206 NrTr: 325)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m6sec


before gc: list nodes free: 333675

after gc: idd nodes used:116887, unused:15883113; list nodes free:70774686

before gc: list nodes free: 2034057

after gc: idd nodes used:169922, unused:15830078; list nodes free:72612650

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 1213 2218 4836 4645 4454 4579 6650 6772 6321 5612 11315 11244 10627 13911 13090 12967 11215 11300 11313 11724 11179 11075 10709 12006 11790 11097 17798 17895 16938 16572 18951 18188 18192 17269 15870 18425 18253 19027 18288 23083 23768 26106 24878 25901 26671 23200 24366 24332 22239 26544 25479 26761 23439 23396 25737 24232 22647 17473 27556 30153 29779 30760 32903 31472 31547 28583 30081 30187 28813 26889 31067 31641 31263 30445 29059 31804 29732 28596 28792 28001 21506 41615 38036 36786 36869 36388 36883 36591 35897 37343 37009 38400 37246 36774 39521 47230 45298 45273 47485 48073 48327 48029 47467 50543 49809 49116 46773 46406 37196 40683 39596 40133 42545 42918 43502 42777 44041 45758 45292 44371 41896 41635 38727 40035 39063 39616 41710 42095 42816 42098 43269 44970 44295 43523 41297 40891 39032 42021 41897 41691 41692 43305 41736 41756 42145 43546 42137 42049 44231 51129 50185 47937 48123 49955 48591 47832 47822 48098 47889 49159 47903 47755 46336 50198 49794 49252 49164 48136 50374 48771 47944 48715 48160 47977 47927 47761 45157 51926 50650 48916 48560 50336 48972 48213 48260 48040 49188 47794 47586 44567 63724 71149 69349 73441 71121 61438 63632 64383 63054 78077 84478 81169 84636 84666 77698 118873 114007 110463 111426 107230 110904 109211 105367 110570 106588 107154 104196 102519 102058 103021 96708 97006 98505 100991 99466 119095 123511 123766 119709 118954 124269 120155 116021 122536 119874 119053 119635 116576 115290 114410 105597 102259 103747 103014 102600 112747 115053 115974 118212 115976 120903 117746 115845 121320 119745 118403 118395 116980 115533 116685 100933 104703 103629 108012 112241 110916 111108 108745 98578 96247 102517 103838 87370 86943 87162 87439 79920 71947 72409 71932 68871 60376 60155 60010 57092 54887 53757 90265 98703 96947 101989 107607 104299 102251 103105 102556 88884 115218 120817 118466 125120 127398 113604 155334 199498 178167 168934 167091 168218 171376 170043 169992 168696 166839 167318 160113 158601 160537 159259 154774 154071 153622 162574 162536 159732 158917 158894 157070 156366 156792 155851 151060 148228 145850 135015 129688 145677 148070 149938 152280 141020 166914 192699 188244 173620 177647 185718 181728 178566 186239 181688 178715 182021 174150 172777 176691 175097 173265 173256 172159 178212 178118 175481 174765 174758 172752 172372 172026 173049 166515 162934 160769 153000 153636 153993 155078 154774 154042 165108 177118 170667 171857 173452 170851 174340 173082 168943 176405 173979 174563 172897 170489 173924 174498 172996 172623 171768 175764 175765 173539 173415 172812 171142 171539 171661 171435 165284 162939 160692 154037 152624 150195 154313

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="CSRepetitions-PT-05"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="marcie"
export BK_RESULT_DIR="/home/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/CSRepetitions-PT-05.tgz
mv CSRepetitions-PT-05 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1667"
echo " Executing tool marcie"
echo " Input is CSRepetitions-PT-05, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r01kn-qhx2-140025666601873"
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 ;