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 Diffusion2D-PT-D10N150, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198149900547
=====================================================================

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

BK_START 1401984427114

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: 100 NrTr: 684)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


RS generation: 39m38sec


-> reachability set: #nodes 14950 (1.5e+04) #states 242,520,983,711,364,275,168,282,666,169,455,781,913,613,043,678,110,346,873,178,692,778,335,084 (71)



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

139 139 194 181 253 225 313 271 379 319 444 364 517 415 594 468 691 523 787 589 490 649 529 711 568 775 619 854 685 937 741 1009 799 1083 843 1159 904 1255 967 1355 1032 1499 1099 1609 1168 958 1261 997 1335 1036 1387 1099 1464 1164 1595 1257 1705 1300 1791 1371 1879 1444 1999 1519 2123 1565 2283 1643 2416 1756 2621 1839 1465 1924 1504 2011 1543 2100 1656 2229 1735 2362 1816 2459 1899 2599 1984 2701 2029 2848 2117 2999 2207 3199 2299 3405 2439 1933 2536 1972 2635 2011 2736 2099 2889 2239 2995 2332 3155 2427 3266 2471 3379 2569 3549 2669 3723 2771 3958 2875 4199 2981 2401 3148 2440 3199 2479 3311 2579 3425 2681 3667 2785 3851 2891 3974 2999 4099 3109 4293 3221 4491 3267 4624 3382 4969 3499 5322 3689 2908 3811 2947 3935 2986 4061 3173 4264 3289 4471 3407 4605 3527 4819 3649 4958 3694 5179 3819 5404 3946 5715 4075 6032 4289 3376 4423 3415 4559 3454 4697 3579 4924 3793 5067 3923 5301 4055 5449 4099 5599 4234 5843 4371 6091 4510 6437 4651 6789 4794 3844 5035 3883 5086 3922 5235 4059 5386 4198 5739 4339 5997 4482 6157 4627 6319 4774 6483 4923 6859 4969 7029 5121 7522 5275 8023 5539 4351 5698 4390 5859 4429 6022 4690 6299 4843 6580 4998 6751 5155 7039 5314 7215 5359 7510 5521 7809 5685 8231 5851 8659 6019 4819 6310 4858 6483 4897 6658 5059 6959 5223 7139 5514 7447 5557 7632 5727 7819 5899 8137 6073 8459 6249 8916 6296 9379 6607 5287 6789 5326 6973 5365 7159 5539 7347 5715 7811 5893 8143 6073 8340 6255 8539 6439 8740 6625 9227 6671 9434 6860 10075 7051 10579 7389 5794 7585 5833 7783 5872 7983 6207 8334 6397 5956 5965 5974 5983 5992 6001 6011 6020 6029 6038 6047 6056 6065 6074 6083 6092 6101 6111 6120 6129 6138 6147 6156 6165 6174 6183 6192 6201 6211 6220 6229 6238 6247 6256 6265 6274 6283 6293 6302 6311 6320 6329 6339 6348 6357 6366 6375 6384 6394 6404 6420 6435 6451 6467 6482 6498 6514 6529 6545 6560 6576 6592 6607 6623 6638 6654 6670 6685 6701 6716 6730 6745 6760 6774 6789 6804 6819 6833 6848 6919 7002 7064 7127 7155 7163 7170 7177 7185 7192 7200 7207 7215 7222 7230 7237 7245 7252 7260 7267 7274 7282 7289 7297 7306 7318 7329 7340 7352 7363 7374 7386 7397 7408 7420 7431 7443 7459 7489 7518 7547 7577 7602 7608 7615 7622 7628 7635 7642 7648 7655 7662 7668 7675 7682 7688 7695 7702 7708 7715 7722 7728 7735 7742 7748 7757 7767 7776 7786 7796 7805 7815 7824 7834 7844 7853 7863 7872 7882 7892 7902 7927 7952 7977 8002 8027 8052 8077 8102 8127 8152 8177 8201 8207 8212 8218 8224 8230 8236 8242 8247 8253 8259 8265 8271 8276 8282 8288 8294 8300 8305 8311 8317 8323 8329 8335 8340 8346 8352 8360 8368 8376 8384 8392 8400 8408 8416 8424 8432 8440 8448 8456 8464 8472 8479 8487 8495 8508 8528 8549 8570 8591 8612 8633 8653 8674 8695 8716 8737 8757 8778 8799 8820 8841 8861 8882 8903 8924 8945 8954 8959 8964 8969 8974 8979 8984 8989 8994 8999 9004 9009 9013 9018 9023 9028 9033 9038 9043 9048 9053 9058 9063 9068 9073 9078 9083 9088 9093 9098 9103 9110 9116 9122 9129 9135 9142 9148 9154 9161 9167 9174 9180 9186 9193 9199 9206 9212 9219 9225 9231 9238 9244 9251 9268 9286 9304 9322 9340 9358 9376 9393 9411 9429 9447 9465 9483 9500 9518 9536 9554 9572 9590 9607 9625 9643 9661 9679 9697 9714 9732 9750 9768 9786 9804 9822 9839 9852 9856 9860 9865 9869 9873 9877 9881 9885 9890 9894 9898 9902 9906 9910 9915 9919 9923 9927 9931 9935 9940 9944 9948 9952 9956 9960 9965 9969 9973 9977 9981 9985 9990 9994 9998 10002 10008 10013 10018 10023 10028 10033 10038 10044 10049 10054 10059 10064 10069 10075 10080 10085 10090 10095 10100 10105 10111 10116 10121 10126 10131 10136 10142 10147 10155 10170 10186 10201 10217 10233 10248 10264 10280 10295 10311 10326 10342 10358 10373 10389 10404 10420 10436 10451 10467 10482 10498 10514 10529 10545 10561 10576 10592 10607 10623 10639 10654 10670 10685 10701 10717 10732 10748 10763 10779 10795 10810 10826 10842 10857 10873 10888 10901 10905 10908 10912 10915 10919 10922 10926 10929 10933 10936 10940 10943 10947 10950 10954 10957 10961 10964 10968 10971 10975 10978 10982 10985 10989 10992 10996 10999 11003 11006 11010 11013 11017 11020 11024 11027 11031 11034 11038 11041 11045 11048 11052 11056 11060 11064 11068 11073 11077 11081 11085 11089 11093 11098 11102 11106 11110 11114 11118 11123 11127 11131 11135 11139 11143 11148 11152 11156 11160 11164 11168 11173 11177 11181 11185 11189 11193 11198 11205 11219 11233 11246 11260 11274 11288 11302 11316 11330 11344 11357 11371 11385 11399 11413 11427 11441 11455 11469 11482 11496 11510 11524 11538 11552 11566 11580 11593 11607 11621 11635 11649 11663 11677 11691 11704 11718 11732 11746 11760 11774 11788 11802 11815 11829 11843 11857 11871 11885 11899 11913 11927 11940 11954 11968 11982 11996 12010 12024 12038 12051 12065 12079 12093 12102 12105 12108 12111 12114 12117 12120 12123 12125 12128 12131 12134 12137 12140 12143 12146 12149 12152 12155 12158 12161 12164 12167 12170 12173 12176 12179 12182 12184 12187 12190 12193 12196 12199 12202 12205 12208 12211 12214 12217 12220 12223 12226 12229 12232 12235 12238 12240 12243 12246 12249 12253 12256 12260 12263 12267 12270 12274 12277 12281 12284 12288 12291 12295 12298 12302 12305 12309 12312 12316 12319 12323 12326 12330 12333 12337 12340 12344 12347 12351 12354 12357 12361 12364 12368 12371 12375 12378 12382 12385 12389 12392 12396 12399 12403 12406 12410 12413 12417 12420 12424 12427 12431 12434 12438 12441 12444 12448 12451 12455 12458 12462 12465 12469 12472 12476 12479 12482 12486 12489 12493 12496 12500 12503 12507 12510 12514 12517 12521 12524 12527 12531 12534 12538 12541 12545 12548 12552 12555 12558 12561 12565 12568 12571 12575 12578 12581 12585 12588 12591 12594 12598 12601 12604 12608 12611 12614 12617 12621 12624 12627 12631 12634 12637 12640 12644 12647 12650 12654 12657 12660 12663 12667 12670 12673 12677 12680 12683 12686 12690 12693 12696 12700 12725 12758 12792 12825 12853 12863 12873 12883 12894 12904 12914 12924 12934 12945 12955 12965 12975 12985 12996 13019 13055 13090 13126 13153 13163 13172 13182 13191 13201 13210 13219 13229 13238 13248 13257 13267 13276 13285 13295 13315 13350 13386 13422 13452 13461 13470 13479 13487 13496 13505 13514 13522 13531 13540 13549 13557 13566 13575 13584 13593 13603 13639 13675 13711 13746 13758 13766 13774 13782 13790 13799 13807 13815 13823 13831 13840 13848 13856 13864 13872 13881 13889 13897 13921 13956 13992 14028 14053 14061 14069 14076 14084 14092 14099 14107 14115 14123 14130 14138 14146 14153 14161 14169 14176 14184 14192 14199 14231 14267 14302 14338 14355 14362 14370 14377 14384 14391 14399 14406 14413 14420 14428 14435 14442 14449 14457 14464 14471 14478 14486 14493 14500 14507 14514 14521 14529 14536 14543 14550 14557 14564 14571 14579 14586 14593 14600 14607 14614 14621 14629 14636 14643 14650 14678 14707 14737 14766 14795 14832 14871 14909 14947
iterations count:1239084 (1811), effective:14850 (21)
limit of 2048MB is reached

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