fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r05kn-ovh1-140043892103082
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
1453.32 913680 340 2024 12240 1020 1 normal

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 RwMutex-PT-r0010w1000, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r05kn-ovh1-140043892103082
=====================================================================


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

BK_START 1400461057861

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: 2030 NrTr: 2020)

net check time: 0m0sec

place and transition orderings generation:0m10sec

init dd package: 0m0sec


RS generation: 13m34sec


-> reachability set: #nodes 425663 (4.3e+05) #states 2,024 (3)


STATE_SPACE 2024 12240 1020 1 TECHNIQUES DECISION_DIAGRAMS


total processing time: 15m13sec


BK_STOP 1400461971743

--------------------
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

423043 423056 423066 423074 423081 423088 423094 423100 423105 423110 423115 423120 423124 423129 423133 423137 423141 423145 423148 423152 423155 423159 423162 423165 423168 423172 423175 423178 423181 423184 423186 423189 423192 423195 423197 423200 423203 423206 423209 423215 423221 423224 423232 423238 423241 423247 423253 423256 423261 423269 423272 423278 423284 423287 423293 423294 423302 423308 423311 423317 423320 423326 423335 423338 423344 423347 423353 423356 423362 423368 423371 423377 423380 423386 423389 423395 423396 423405 423408 423414 423420 423423 423429 423430 423438 423441 423447 423450 423456 423459 423463 423469 423475 423478 423481 423487 423490 423496 423497 423505 423508 423514 423517 423523 423526 423529 423535 423539 423545 423548 423554 423557 423560 423564 423569 423575 423578 423584 423587 423590 423596 423597 423602 423609 423612 423618 423621 423624 423630 423631 423639 423642 423645 423651 423654 423657 423663 423664 423665 423675 423679 423682 423688 423691 423694 423700 423701 423706 423712 423715 423718 423724 423727 423730 423734 423739 423742 423749 423752 423755 423758 423764 423767 423768 423776 423779 423782 423788 423791 423794 423797 423801 423806 423809 423812 423816 423817 423821 423827 423830 423833 423836 423839 423845 423848 423851 423854 423860 423863 423866 423869 423872 423878 423881 423884 423887 423890 423896 423899 423902 423905 423908 423914 423917 423920 423923 423926 423929 423935 423938 423941 423944 423947 423950 423953 423959 423962 423965 423968 423971 423974 423977 423980 423983 423989 423992 423995 423998 424001 424004 424007 424010 424013 424016 424019 424025 424028 424031 424034 424037 424040 424043 424046 424049 424052 424055 424058 424061 424064 424067 424070 424073 424079 424082 424085 424088 424091 424094 424097 424100 424103 424106 424109 424112 424115 424118 424121 424124 424127 424130 424133 424136 424139 424142 424145 424148 424151 424154 424157 424160 424163 424166 424169 424172 424175 424178 424181 424184 424184 424187 424190 424193 424196 424199 424202 424205 424208 424211 424214 424217 424220 424223 424226 424229 424232 424235 424238 424238 424241 424244 424247 424250 424253 424256 424259 424262 424265 424268 424271 424274 424274 424277 424280 424283 424286 424289 424292 424295 424298 424301 424304 424304 424307 424310 424313 424316 424319 424322 424325 424328 424328 424331 424334 424337 424340 424343 424346 424349 424349 424352 424355 424358 424361 424364 424367 424367 424370 424373 424376 424379 424382 424385 424385 424388 424391 424394 424397 424400 424403 424403 424406 424409 424412 424415 424418 424418 424421 424424 424427 424430 424433 424436 424436 424439 424442 424445 424448 424448 424451 424454 424457 424460 424463 424463 424466 424469 424472 424475 424475 424478 424481 424484 424487 424490 424490 424493 424496 424499 424502 424502 424505 424508 424511 424514 424514 424517 424520 424523 424526 424526 424529 424532 424535 424535 424538 424541 424544 424547 424547 424550 424553 424556 424559 424559 424562 424565 424568 424568 424571 424574 424577 424577 424580 424583 424586 424589 424589 424592 424595 424598 424598 424601 424604 424607 424607 424610 424613 424616 424616 424619 424622 424625 424625 424628 424631 424634 424634 424637 424640 424643 424643 424646 424649 424652 424652 424655 424658 424661 424661 424664 424667 424670 424670 424673 424676 424679 424679 424682 424685 424685 424688 424691 424694 424694 424697 424700 424703 424703 424706 424709 424709 424712 424715 424718 424718 424721 424724 424724 424727 424730 424733 424733 424736 424739 424739 424742 424745 424748 424748 424751 424754 424754 424757 424760 424760 424763 424766 424769 424769 424772 424775 424775 424778 424781 424784 424784 424787 424790 424790 424793 424796 424796 424799 424802 424802 424805 424808 424811 424811 424814 424817 424817 424820 424823 424823 424826 424829 424829 424832 424835 424835 424838 424841 424841 424844 424847 424847 424850 424853 424853 424856 424859 424862 424862 424865 424868 424868 424871 424874 424874 424877 424880 424880 424883 424886 424886 424889 424892 424892 424895 424898 424898 424901 424904 424904 424907 424907 424910 424913 424913 424916 424919 424919 424922 424925 424925 424928 424931 424931 424934 424937 424937 424940 424943 424943 424946 424949 424949 424952 424952 424955 424958 424958 424961 424964 424964 424967 424970 424970 424973 424976 424976 424979 424979 424982 424985 424985 424988 424991 424991 424994 424997 424997 425000 425000 425003 425006 425006 425009 425012 425012 425015 425015 425018 425021 425021 425024 425027 425027 425030 425033 425033 425036 425036 425039 425042 425042 425045 425045 425048 425051 425051 425054 425057 425057 425060 425060 425063 425066 425066 425069 425072 425072 425075 425075 425078 425081 425081 425084 425084 425087 425090 425090 425093 425093 425096 425099 425099 425102 425105 425105 425108 425108 425111 425114 425114 425117 425117 425120 425123 425123 425126 425126 425129 425132 425132 425135 425135 425138 425141 425141 425144 425144 425147 425150 425150 425153 425153 425156 425159 425159 425162 425162 425165 425165 425168 425171 425171 425174 425174 425177 425180 425180 425183 425183 425186 425189 425189 425192 425192 425195 425195 425198 425201 425201 425204 425204 425207 425210 425210 425213 425213 425216 425216 425219 425222 425222 425225 425225 425228 425228 425231 425234 425234 425237 425237 425240 425243 425243 425246 425246 425249 425249 425252 425255 425255 425258 425258 425261 425261 425264 425267 425267 425270 425270 425273 425273 425276 425279 425279 425282 425282 425285 425285 425288 425288 425291 425294 425294 425297 425297 425300 425300 425303 425306 425306 425309 425309 425312 425312 425315 425315 425318 425321 425321 425324 425324 425327 425327 425330 425330 425333 425336 425336 425339 425339 425342 425342 425345 425345 425348 425351 425351 425354 425354 425357 425357 425360 425360 425363 425363 425366 425369 425369 425372 425372 425375 425375 425378 425378 425381 425384 425384 425387 425387 425390 425390 425393 425393 425396 425396 425399 425399 425402 425405 425405 425408 425408 425411 425411 425414 425414 425417 425417 425420 425420 425423 425426 425426 425429 425429 425432 425432 425435 425435 425438 425438 425441 425441 425444 425447 425447 425450 425450 425453 425453 425456 425456 425459 425459 425462 425462 425465 425465 425468 425468 425471 425474 425474 425477 425477 425480 425480 425483 425483 425486 425486 425489 425489 425492 425492 425495 425495 425498 425498 425501 425504 425504 425507 425507 425510 425510 425513 425513 425516 425516 425519 425519 425522 425522 425525 425525 425528 425528 425531 425531 425534 425534 425537 425537 425540 425540 425543 425543 425546 425549 425549 425552 425552 425555 425555 425558 425558 425561 425561 425564 425564 425567 425567 425570 425570 425573 425573 425576 425576 425579 425579 425582 425582 425585 425585 425588 425588 425591 425591 425594 425594 425597 425597 425600 425600 425603 425603 425606 425606 425609 425609 425612 425612 425615 425615 425618 425618 425621 425621 425624 425624 425627 425627 425630 425630 425633 425633 425636 425636 425639 425639 425642 425642 425645 425645 425648 425648 425651 425651 425654 425654 425657 425657 425660 425660 425663 425663
iterations count:1043313 (516), effective:1010 (0)

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