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

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

BK_START 1401988768397

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: 216 NrTr: 977)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


RS generation: 3m17sec


-> reachability set: #nodes 14051 (1.4e+04) #states 4,759,924,249 (9)


STATE_SPACE 4759924249 77248039202 8 1 TECHNIQUES DECISION_DIAGRAMS


total processing time: 3m38sec


BK_STOP 1401988987204

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

471 642 655 723 794 899 864 865 734 827 819 764 766 920 928 1008 1302 1349 1302 1334 1289 1297 1289 1132 1147 1009 1296 1343 1313 1322 1283 1291 1283 1126 1009 1271 1344 1322 1283 1286 1286 1264 1127 1021 1241 1368 1343 1347 1310 1310 1308 1151 1022 1181 1221 1372 1360 1368 1356 1358 1344 1444 1477 1453 1452 1377 1515 1478 1454 1454 1404 1344 1500 1468 1444 1443 1388 1323 1600 1609 1634 1717 1740 1669 1619 1641 1622 1524 1515 1517 1767 1749 1773 1806 1826 1781 1753 1752 1708 1691 1515 1445 1696 1703 1729 1811 1834 1761 1708 1727 1708 1577 1445 1804 1786 1800 1843 1807 1818 1796 1745 1745 1743 1552 1458 1787 1648 1686 2188 2226 2191 2159 2205 2154 2112 1947 1963 1972 1978 1972 1976 2005 1990 1994 2008 2047 2016 2059 2074 2072 2137 2141 2205 2200 2299 2347 2343 2318 2299 2241 2179 2270 2318 2314 2289 2270 2178 2328 2311 2308 2282 2281 2206 2127 2257 2213 2235 2206 2213 2154 2077 2077 2164 2173 1699 2209 2237 2202 2212 2168 2174 2166 1957 1971 1982 1980 1984 1988 1996 2022 2031 2052 2024 2064 2069 2036 2106 2090 2110 2116 2213 2378 2361 2361 2332 2331 2256 2194 2349 2338 2332 2303 2302 2227 2347 2307 2325 2296 2303 2244 2178 2102 2260 2249 2246 2220 2211 2144 1835 1700 2220 2219 2177 2219 2167 2207 2165 2024 1967 1971 1988 1994 2000 2010 2021 2005 2051 2023 2027 2068 2035 2095 2085 2111 2115 2205 2382 2338 2360 2331 2330 2277 2235 2353 2312 2331 2302 2301 2248 2184 2305 2324 2320 2295 2276 2177 2101 2265 2255 2248 2219 2218 2143 2090 1700 1717 2221 2259 2224 2192 2238 2187 2145 1980 1996 2005 2011 2005 2009 2038 2023 2027 2041 2080 2049 2092 2107 2105 2170 2174 2238 2233 2332 2380 2376 2351 2332 2274 2212 2303 2351 2347 2322 2303 2211 2361 2344 2341 2315 2314 2239 2160 2290 2246 2268 2239 2246 2187 2110 1854 1807 1910 2200 2168 2144 2143 2088 2073 2079 2083 2089 2093 2101 2106 2133 2132 2145 2152 2186 2196 2055 2295 2304 2280 2268 2206 2213 2217 2220 2226 2236 2239 2243 2273 2243 2252 2208 2056 2335 2303 2279 2278 2223 2208 2214 2218 2224 2228 2236 2241 2268 2250 2252 2259 2056 2043 2284 2269 2269 2257 2195 2202 2206 2212 2216 2225 2228 2232 2263 2232 2239 2197 2039 2470 2533 2559 2641 2670 2591 2538 2590 2544 2407 2353 2354 2367 2371 2375 2381 2389 2371 2409 2411 2382 2420 2386 2416 2393 2398 2401 2475 2470 2584 2617 2593 2592 2517 2516 2674 2648 2624 2623 2568 2513 2638 2623 2623 2602 2513 2704 2667 2643 2649 2593 2522 2528 2434 2448 2449 2478 2192 2625 2688 2749 2802 2825 2746 2693 2745 2710 2566 2506 2502 2503 2515 2517 2519 2503 2526 2503 2535 2503 2539 2541 2526 2506 2507 2548 2572 2555 2728 2702 2678 2677 2602 2633 2765 2733 2709 2708 2653 2598 2723 2708 2708 2696 2632 2789 2743 2728 2728 2678 2607 2590 2494 2286 2194 2624 2687 2713 2795 2821 2745 2692 2744 2696 2561 2505 2501 2512 2514 2516 2518 2523 2502 2533 2502 2502 2538 2498 2528 2498 2506 2507 2581 2579 2668 2701 2677 2676 2601 2600 2758 2732 2708 2707 2632 2597 2722 2707 2707 2686 2597 2788 2751 2727 2733 2673 2606 2587 2493 2285 2206 2644 2707 2768 2821 2844 2765 2712 2766 2729 2585 2525 2521 2522 2534 2536 2538 2522 2545 2522 2554 2522 2558 2560 2545 2525 2526 2567 2591 2574 2747 2721 2697 2696 2621 2652 2784 2752 2728 2727 2672 2617 2742 2727 2727 2715 2651 2808 2762 2747 2747 2697 2626 2609 2513 2305 2207 6338 6456 6441 6349 6349 6366 6226 6222 6125 6396 6522 6446 6427 6541 6522 6421 6409 6554 6582 6591 6612 6608 6644 6657 6687 6662 6729 6765 6842 6853 6875 6886 6902 6919 6931 6953 7119 7061 7096 7258 7443 7384 7388 7524 7406 7525 7407 7351 7440 7352 7442 7434 7434 7565 7468 7577 7520 7434 7366 7275 7218 7108 7384 7406 7687 7772 7738 7698 7742 7697 7675 7512 7515 7485 7752 7836 7796 7763 7807 7762 7720 7551 7827 7798 7840 7802 7768 7815 7764 7722 7517 7867 7838 7881 7841 7809 7855 7804 7762 7546 7505 7913 7906 7936 7988 8011 7938 7924 7932 7876 7755 7697 7713 7635 7880 7893 7904 7962 8022 7957 7898 7915 7896 7705 7635 7937 7930 7960 8012 8035 7964 7948 7956 7900 7862 7705 7656 7927 7936 7962 8044 8067 7994 7941 7960 7941 7810 7748 8149 8294 8298 8306 8310 8314 8320 8314 8328 8340 8327 8349 8358 8339 8363 8532 8517 8547 8552 8563 8579 8550 8598 8617 8626 8623 8588 8648 8644 8735 8706 8781 8714 9030 9078 9662 9661 9667 9661 9607 9655 9609 9471 9401 9398 9408 9410 9412 9416 9398 9421 9398 9430 9398 9435 9436 9452 9430 9436 9438 9523 9705 9665 9683 9654 9661 9602 9559 9676 9632 9654 9625 9624 9571 9507 9599 9647 9643 9618 9599 9500 9424 9588 9574 9571 9542 9541 9466 9413 9411 9409 9409 9104 9599 9683 9643 9610 9654 9609 9567 9399 9398 9407 9409 9411 9413 9418 9398 9398 9398 9432 9398 9398 9450 9468 9475 9477 9541 9536 9694 9683 9679 9654 9635 9577 9516 9606 9654 9650 9625 9606 9514 9664 9654 9647 9618 9617 9542 9463 9424 9549 9571 9542 9542 9494 9413 9141 9096 9537 9664 9634 9636 9595 9601 9593 9384 9388 9384 9384 9397 9399 9384 9384 9408 9384 9384 9419 9384 9384 9454 9412 9420 9470 9522 9686 9669 9666 9640 9639 9564 9502 9651 9640 9637 9611 9602 9535 9655 9614 9635 9604 9603 9550 9503 9410 9509 9557 9553 9528 9509 9452 9128 9090 8811 8774 9326 9325 9283 9325 9273 9313 9271 9130 9065 9062 9072 9074 9076 9080 9083 9062 9093 9094 9062 9099 9062 9122 9087 9100 9102 9192 9369 9325 9347 9318 9317 9264 9223 9340 9299 9320 9289 9288 9235 9171 9295 9311 9307 9282 9263 9164 9088 9252 9242 9235 9206 9205 9130 9077 8508 8593 8568 8659 8685 8719 8818 9185 9165 9141 9129 9067 9074 9078 9084 9088 9097 9100 9104 9135 9129 9135 9051 9176 9185 9426 9369 9334 9322 9262 9245 9251 9254 9261 9265 9273 9276 9280 9314 9284 9292 8994 8994 9359 9339 9315 9303 9241 9248 9252 9258 9262 9271 9274 9278 9309 9278 9279 9197 8994 9416 9366 9327 9315 9255 9238 9244 9248 9254 9258 9266 9269 9273 9307 9277 9285 9191 8993 9806 9770 9799 9846 9858 9814 9776 9766 9705 9667 9513 9508 9513 9513 9495 9491 9509 9486 9483 9477 9509 9472 9509 9492 9501 9514 9516 9564 9597 9736 9699 9675 9681 9621 9595 9724 9678 9663 9663 9642 9554 9712 9686 9662 9661 9586 9560 9692 9677 9677 9665 9601 9534 9401 9401 9420 9427 9406 9991 9955 9984 10027 10037 9999 9956 9934 9890 9873 9698 9689 9690 9688 9684 9666 9661 9637 9657 9615 9639 9599 9597 9583 9617 9627 9617 9573 9696 9813 9776 9752 9758 9702 9672 9631 9755 9740 9740 9719 9631 9789 9763 9739 9738 9683 9632 9745 9778 9754 9753 9678 9598 9453 9332 9205 9878 9842 9867 9904 9930 9886 9848 9838 9777 9739 9585 9580 9577 9575 9540 9532 9548 9522 9516 9502 9526 9486 9522 9495 9477 9514 9504 9550 9583 9696 9666 9639 9645 9585 9559 9688 9647 9627 9627 9606 9518 9676 9650 9626 9625 9550 9524 9656 9641 9641 9629 9565 9485 9340 9219 9041 7870 7887 8425 8384 8395 8441 8416 8416 8380 8314 8314 8297 8123 8123 8114 8123 8121 8105 8085 8083 8105 8071 8097 8097 8059 8046 8080 8091 8038 8043 8166 8283 8243 8222 8222 8201 8160 8144 8268 8253 8253 8232 8177 8308 8276 8252 8251 8196 8150 8263 8296 8272 8271 8196 8148 8078 7914 6809 10741 10745 10983 11019 10943 10167 9589 9451 13657 13639 13699 13735 13795 13845 13633 14063 14522 14436 14408 14408 14813 14578 14408 14804 14581 14408 14820 14585 14514 14499 14811 14845 14902 15189 14981 14803 15186 14981 14803 15198 14986 14910 15044 15103 15107 15115 15119 15123 15121 15123 15143 15149 15136 15158 15167 15148 15172 15233 15233 15247 15222 15264 15280 15251 15299 15318 15327 15324 15289 15349 15301 15436 15456 15482 15504 15570 15648 16454 16212 16138 16138 16138 16138 16138 16138 16138 16138 16223 16186 16194 16216 16310 16288 16256 16366 16279 16213 16360 16273 16206 16073 16167 16145 16062 16334 16336 16403 16024 16611 16542 16474 16474 16474 16474 16474 16474 16474 16551 16569 16533 16538 16713 16626 16575 16531 16617 16595 16523 16610 16558 16383 16544 16457 16425 16117 16022 16754 16531 16460 16460 16460 16460 16460 16460 16460 16460 16555 16514 16522 16704 16619 16580 16518 16664 16582 16516 16596 16575 16495 16535 16450 16411 16104 16010 15850 15804 16564 16340 16248 16248 16248 16248 16248 16248 16248 16248 16327 16303 16304 16345 16420 16398 16348 16463 16372 16339 16451 16364 16290 16157 16251 16230 16146 15781 15765 15791 15831 15857 15838 15970 16249 16158 16126 16126 16085 16146 16156 16344 16249 16210 16210 16216 16169 16075 16263 16240 16209 16209 16168 16075 16337 16236 16203 16203 16209 16062 16074 16855 16650 16577 16577 16577 16577 16577 16577 16581 16537 16649 16789 16688 16655 16611 16766 16674 16610 16696 16673 16608 16754 16663 16585 16568 16530 16570 16573 16597 17226 17032 16938 16914 16881 16860 16833 16810 16782 16715 16821 16813 16889 16865 16831 16957 16856 16823 16956 16855 16822 16945 16850 16811 16763 16649 16591 16408 16958 16892 16804 16788 16750 16732 16703 16688 16604 16694 16675 16845 16754 16718 16677 16764 16740 16843 16748 16709 16657 16752 16728 16652 16538 16478 16309 15702 15710 16370 16158 16073 16052 16022 16001 15969 15948 15926 15861 15973 16113 16018 15979 15978 16139 16042 15977 16132 16041 15975 16132 16035 16003 15937 15828 15524 16236 16276 16058 11613 14774 14824 14778 14717 14831 14812 14711 14646 14618 14598 14364 14630 14678 14733 14729 14641 14641 14633 14490 14630 14645 14784 14811 14855 14544 14962 14968 14971 14977 14980 14983 14995 14990 15003 15015 15027 15024 15031 15039 15038 15149 15163 15164 15169 15163 15199 15208 15185 15234 15193 15250 15254 15265 15317 15372 15323 15420 15331 15776 15790 16304 16431 16420 16418 16375 16381 16353 16253 16218 16211 16217 16262 16209 16365 16440 16381 16399 16704 16656 16699 16675 16642 16686 16635 16611 16484 16418 16455 16507 16493 16417 16154 16068 16668 16677 16661 16667 16621 16627 16599 16511 16466 16439 16463 16508 16455 16403 16062 15846 15800 15800 16374 16409 16393 16360 16404 16353 16329 16202 16136 16173 16225 16211 16187 15755 15669 15780 15729 15846 15733 15945 16233 16117 16147 16155 16230 16231 16118 16294 16271 16284 16253 16119 16366 16253 16282 16290 16119 16110 16287 16265 16277 16246 16106 16147 16789 16800 16823 16906 16931 16850 16808 16808 16775 16771 16648 16621 16645 16683 16697 16609 16649 16652 16676 17245 17182 17162 17156 17214 17241 17195 17153 17132 17116 17029 16987 16960 16919 16935 16880 16714 16492 17132 17075 17102 17135 17157 17112 17076 17063 17019 17001 16880 16816 16801 16835 16755 16767 16506 16354 15732 15723 16320 16263 16290 16323 16345 16300 16264 16251 16207 16189 16068 16004 15989 16023 15943 15955 15533 15374 17184 17209 15527 12917 14440 14484 14479 14377 14377 14394 14373 14323 14286 14054 14392 14436 14390 14324 14415 14398 14303 14026 13986 14010 14022 14027 14044 14076 14091 14104 14113 14095 14134 14155 14115 14131 14235 14243 14249 14256 14263 14269 14306 14300 14374 14457 14353 14493 14589 14629 14735 14711 14697 14773 14697 14771 14697 14834 14721 14815 14740 14748 14857 14798 14715 14812 14715 14711 14635 14666 14629 14583 14389 14589 14957 14923 14951 14928 14895 14939 14888 14864 14737 14671 14700 14670 14930 15015 15000 14956 14998 14953 14929 14826 14736 14670 14934 15011 15002 14958 15000 14955 14931 14828 14796 14670 15042 15051 15011 15044 14995 15035 14973 14969 14840 14731 14777 14968 15031 15055 15137 15168 15089 15047 15097 15031 15027 14904 14858 14862 15118 15078 15097 15058 15110 15137 15099 15057 15057 15041 14946 14912 14784 15098 15080 15108 15160 15185 15114 15093 15115 15059 15041 14918 14854 14805 15023 15086 15110 15192 15223 15144 15102 15152 15086 15082 14961 14897 14792 15202 15378 15420 15421 15427 15437 15410 15469 15418 14748 14652 16569 16528 15368 14045 14046 14051
iterations count:2122061 (2172), effective:23208 (23)

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