fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r06ks-qhx2-140066506402185
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 SurpriseEcho-PT-d02r19, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r06ks-qhx2-140066506402185
=====================================================================


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

BK_START 1400687227330

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: 3455 NrTr: 2730)

net check time: 0m0sec

place and transition orderings generation:0m19sec

init dd package: 0m5sec


before gc: list nodes free: 1333044

after gc: idd nodes used:51015, unused:15948985; list nodes free:66876931

before gc: list nodes free: 1277577

after gc: idd nodes used:51644, unused:15948356; list nodes free:66873902

before gc: list nodes free: 1224216

after gc: idd nodes used:57535, unused:15942465; list nodes free:66847982

before gc: list nodes free: 1242723

after gc: idd nodes used:57635, unused:15942365; list nodes free:66847233

before gc: list nodes free: 1069109

after gc: idd nodes used:75937, unused:15924063; list nodes free:66768254

before gc: list nodes free: 1215807

after gc: idd nodes used:76547, unused:15923453; list nodes free:66765231

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

14526 31400 34028 36495 43777 44051 43857 44423 43957 44756 44618 44778 44657 44495 44980 45236 45421 45109 45304 45531 45479 45518 46028 46227 46192 45535 46212 45749 45962 46176 46149 46069 46473 46280 46873 46207 46432 46570 46139 46400 46336 47321 47145 50039 46269 46930 46946 46935 46954 49083 46643 47025 46927 46689 47457 46939 47264 46965 47165 46645 47638 47509 48075 47279 48579 47569 47340 47315 47446 47976 47381 47357 47624 46972 47329 47085 47329 47651 47415 47611 47038 47477 47589 48520 48102 51279 47247 47792 47775 47476 47681 47686 49177 48004 48177 48011 48042 48553 49415 48299 48276 48365 47928 48483 48323 47948 48258 48295 48382 47951 48317 47856 48189 47977 48850 48020 49150 47952 47740 48486 48093 48504 47952 48605 48284 48793 48391 50191 48466 49385 48863 48284 48192 48669 52000 49020 48469 48518 48340 49257 48821 52105 48942 49000 48296 48721 49176 51949 48400 48999 48853 47972 48613 49012 48550 49109 48520 48357 48127 48477 48803 49244 49139 48927 49189 48883 48307 48766 48696 49033 48559 48692 49178 48747 49113 48900 49053 48794 49121 48929 48432 49016 48450 49050 49583 50016 49644 50141 49880 49717 49487 49617 49976 49851 50596 50246 53533 49460 49663 49646 49601 49620 52003 49510 49892 49681 49443 50633 49655 53136 49259 49634 51499 49614 49748 50081 49423 49948 49330 53256 49258 50862 50325 50338 50793 50611 50072 50207 50112 50032 50277 50113 49619 50126 50056 50194 50167 50300 50326 49871 50084 49950 50150 49630 53130 53441 53308 53641 53023 53842 53218 56924 53146 53704 53488 53198 53328 53727 53794 54092 53401 53248 53110 54002 57173 54253 53404 53346 53646 53349 53907 53270 53770 57455 53434 54546 53557 53660 54451 54112 57226 53387 53870 55644 54128 54383 53815 53535 54232 53613 57057 54370 53829 53866 53620 54537 55841 53637 54010 54058 53515 54549 54146 53780 54190 53977 54927 53589 54022 53675 54002 54053 57872 53944 54725 54693 54007 54505 54052 53828 54828 54157 57803 54025 54549 57709 53897 54880 54019 55284 54374 58143 54266 54631 54899 54350 55230 54374 54246 55229 54640 58062 54513 54997 56866 54385 55368 54507 54531 55583 55008 54209 54011 54469 54451 54152 54357 54205 54759 54462 55020 54383 54637 54748 54055 54582 54092 57167 57062 56850 57184 56764 56294 56753 56724 57021 56547 56680 57268 57204 57203 57123 56788 56989 70259 70316 70169 70751 70275 70520 70870 70418 72470 70249 70862 70879 70868 70887 73207 70849 71149 70917 72008 72419 71984 71226 71681 71324 71419 71696 71529 71926 71260 71874 75255 72307 71750 71747 71569 72608 72090 73441 72124 75546 71768 72758 71891 72045 72482 72346 74215 71721 72127 73864 71942 72237 72149 71869 72389 71947 73903 72609 72151 72201 71955 72654 73859 71956 72355 71980 71917 72377 72094 72131 72021 72318 72538 71929 72299 72016 72317 75739 71961 72944 72083 72238 72588 72539 74410 71899 72729 72202 72109 72514 73424 72036 72556 72120 74007 72311 72267 72317 72071 72684 73970 72067 72466 72091 71910 72370 72087 73232 72014 72311 72531 71917 72402 72009 71547 73580 71440 72033 71557 71720 72070 71618 73583 71417 71899 72397 71905 72788 72288 72022 72261 72029 72493 73136 73044 72432 72739 72469 76217 72439 72565 73008 72268 73057 76414 73395 72838 72790 72606 73645 73119 76363 73766 72857 73366 72964 74764 73031 72990 74192 72849 73358 73758 75022 73958 73102 72974 73268 72971 73411 72884 73645 74568 73093 73942 73179 73029 73324 73147 73097 72772 75574

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="SurpriseEcho-PT-d02r19"
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/SurpriseEcho-PT-d02r19.tgz
mv SurpriseEcho-PT-d02r19 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 SurpriseEcho-PT-d02r19, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r06ks-qhx2-140066506402185"
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 ;