fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r02kn-qhx2-140031222602029
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
1150.64 46301 30.3 6320 116178 18 4 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-1667
Executing tool marcie
Input is GlobalResAllocation-PT-03, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r02kn-qhx2-140031222602029
=====================================================================


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

BK_START 1400336783276

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: 33 NrTr: 4791)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m25sec


-> reachability set: #nodes 3060 (3.1e+03) #states 6,320 (3)


STATE_SPACE 6320 116178 18 4 TECHNIQUES DECISION_DIAGRAMS


total processing time: 0m46sec


BK_STOP 1400336829422

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

129 168 180 186 214 241 249 259 265 275 281 285 289 292 295 300 300 319 319 331 331 340 340 348 351 365 355 359 359 393 397 397 392 397 393 389 410 405 404 400 410 421 422 424 421 425 436 431 428 425 424 421 408 408 418 428 428 446 445 448 459 461 463 465 465 465 470 468 472 475 478 480 479 489 489 503 499 499 513 509 509 522 523 519 519 544 544 548 545 544 540 539 539 547 548 549 547 553 554 555 555 572 572 591 590 589 608 608 606 606 620 625 628 630 623 655 655 656 659 663 659 655 655 657 657 666 673 677 677 677 685 686 688 689 693 693 704 696 696 711 699 699 707 706 703 707 707 716 710 719 713 713 717 717 728 728 748 745 742 739 760 756 753 750 750 764 763 762 761 761 768 771 771 777 777 780 780 787 787 799 793 793 797 797 807 800 800 803 803 803 809 809 812 812 812 815 815 815 818 818 818 859 859 859 900 893 893 900 900 904 911 907 915 912 912 912 951 944 950 950 956 956 961 961 965 979 973 976 976 979 979 994 989 997 993 993 997 997 997 1044 1041 1034 1031 1028 1028 1032 1032 1036 1044 1038 1039 1039 1041 1041 1046 1043 1050 1044 1059 1052 1048 1054 1054 1050 1055 1054 1054 1054 1097 1092 1090 1090 1088 1090 1086 1084 1084 1089 1089 1094 1102 1097 1099 1099 1103 1103 1106 1104 1104 1113 1106 1119 1114 1110 1110 1113 1113 1111 1111 1115 1115 1115 1115 1375 1360 1358 1340 1335 1330 1325 1320 1321 1312 1300 1300 1295 1290 1290 1285 1280 1280 1285 1285 1290 1298 1295 1295 1299 1299 1312 1308 1308 1313 1310 1310 1312 1312 1316 1326 1319 1329 1326 1322 1327 1324 1324 1328 1340 1332 1344 1339 1341 1337 1347 1339 1365 1354 1346 1346 1349 1349 1347 1347 1350 1348 1348 1351 1354 1354 1360 1358 1358 1361 1359 1359 1365 1385 1378 1378 1371 1371 1373 1373 1373 1373 1373 1379 1379 1384 1393 1389 1397 1393 1393 1393 1567 1561 1562 1559 1542 1543 1533 1528 1523 1534 1548 1547 1538 1532 1521 1518 1514 1496 1486 1465 1465 1465 1458 1460 1460 1464 1464 1465 1465 1473 1469 1469 1473 1475 1469 1490 1477 1482 1478 1466 1466 1469 1471 1464 1479 1477 1472 1473 1475 1463 1463 1466 1468 1461 1461 1464 1459 1459 1462 1474 1474 1464 1464 1474 1462 1475 1474 1474 1462 1462 1469 1463 1463 1468 1468 1464 1466 1466 1479 1479 1467 1467 1479 1476 1464 1482 1478 1477 1477 1461 1461 1469 1469 1462 1462 1467 1467 1463 1463 1463 1478 1474 1460 1460 1460 1469 1458 1458 1460 1479 1474 1470 1458 1458 1458 1458 1456 1456 1456 1466 1453 1454 1454 1465 1465 1450 1450 1447 1447 1447 1453 1459 1459 1462 1462 1473 1468 1476 1472 1485 1480 1488 1484 1484 1497 1494 1494 1500 1498 1498 1502 1502 1500 1500 1500 1496 1496 1496 1482 1482 1482 1525 1519 1518 1518 1517 1520 1516 1519 1515 1515 1520 1520 1525 1527 1527 1534 1534 1533 1541 1536 1554 1542 1551 1545 1545 1557 1557 1554 1561 1559 1561 1558 1563 1562 1562 1562 1820 1817 1813 1809 1809 1801 1798 1793 1784 1785 1776 1771 1775 1776 1774 1771 1767 1753 1753 1751 1752 1748 1745 1745 1742 1739 1739 1740 1741 1741 1745 1745 1741 1747 1742 1759 1749 1743 1743 1746 1748 1742 1745 1741 1741 1743 1743 1744 1744 1748 1750 1744 1747 1749 1743 1744 1744 1753 1753 1744 1744 1748 1748 1751 1751 1754 1754 1758 1758 1756 1756 1773 1767 1762 1770 1766 1768 1764 1768 1770 1766 1766 1768 1768 1776 1770 1770 1778 1778 1772 1779 1779 1774 1774 1778 1778 1781 1781 1781 1785 1785 1786 1793 1787 1789 1789 1789 1792 1792 1792 1792 1832 1831 1830 1829 1830 1827 1827 1828 1825 1826 1823 1823 1821 1821 1821 1825 1825 1829 1835 1831 1831 1835 1831 1831 1833 1833 1854 1843 1843 1837 1844 1844 1839 1845 1843 1845 1839 1845 1841 1845 1841 1841 1841 1878 1876 1876 1874 1874 1872 1872 1870 1870 1875 1875 1877 1877 1879 1879 1882 1882 1882 1908 1908 1908 1946 1946 1939 1932 1932 1932 1937 1939 1939 1942 1942 1940 1943 1941 1941 1941 1985 1979 1972 1965 1965 1967 1972 1972 1979 1979 1974 1976 1976 1987 1988 1977 1979 1979 1982 1982 1976 1986 1986 1981 1981 1984 1982 1982 1985 1979 1979 1979 2025 2021 2017 2010 2010 2010 2003 2007 2007 2012 2012 2016 2012 2012 2014 2023 2023 2015 2015 2016 2016 2019 2019 2015 2025 2024 2020 2017 2017 2020 2020 2018 2018 2021 2017 2017 2017 2164 2149 2144 2131 2131 2133 2127 2109 2109 2107 2104 2096 2096 2089 2081 2081 2083 2083 2087 2095 2091 2091 2095 2091 2091 2104 2099 2092 2092 2095 2095 2090 2090 2093 2088 2088 2090 2100 2100 2091 2102 2101 2101 2090 2090 2095 2095 2091 2091 2091 2099 2088 2088 2085 2085 2085 2087 2087 2089 2096 2096 2090 2090 2095 2089 2089 2089 2133 2129 2125 2125 2120 2120 2115 2115 2117 2117 2120 2120 2121 2129 2124 2124 2128 2132 2123 2133 2133 2126 2126 2130 2126 2126 2140 2135 2135 2128 2134 2133 2134 2127 2127 2125 2125 2125 2125 2161 2157 2154 2154 2151 2151 2151 2155 2156 2156 2160 2160 2156 2160 2156 2156 2156 2177 2177 2177 2177 2217 2214 2210 2200 2200 2200 2203 2211 2206 2209 2209 2207 2207 2210 2205 2205 2205 2245 2242 2238 2228 2228 2231 2231 2236 2243 2243 2238 2249 2241 2251 2243 2246 2246 2241 2241 2244 2244 2266 2259 2255 2255 2248 2248 2251 2253 2246 2249 2244 2244 2244 2296 2293 2288 2288 2284 2277 2277 2267 2267 2270 2275 2275 2279 2275 2275 2278 2278 2292 2286 2280 2280 2285 2281 2281 2284 2284 2280 2280 2289 2284 2284 2281 2281 2284 2284 2279 2279 2282 2277 2277 2277 2431 2415 2409 2398 2391 2391 2395 2389 2380 2366 2366 2359 2359 2351 2350 2343 2331 2331 2333 2345 2337 2349 2346 2341 2350 2345 2347 2341 2355 2354 2349 2350 2343 2347 2346 2348 2347 2341 2344 2339 2339 2342 2342 2353 2344 2344 2356 2355 2355 2345 2351 2350 2346 2346 2346 2346 2344 2344 2344 2342 2342 2342 2345 2345 2347 2347 2354 2354 2349 2349 2350 2350 2350 2350 2394 2390 2385 2385 2380 2380 2380 2372 2372 2375 2375 2378 2378 2382 2385 2377 2385 2379 2396 2387 2388 2381 2389 2390 2384 2388 2388 2383 2383 2400 2398 2393 2387 2387 2393 2393 2394 2388 2392 2387 2387 2387 2427 2423 2418 2419 2415 2409 2409 2409 2412 2412 2414 2414 2418 2418 2414 2414 2413 2413 2413 2413 2439 2439 2439 2477 2470 2463 2463 2467 2467 2469 2469 2474 2471 2471 2473 2473 2473 2473 2511 2504 2497 2497 2500 2504 2504 2506 2506 2508 2508 2511 2511 2516 2513 2521 2515 2515 2538 2527 2520 2520 2525 2519 2519 2518 2518 2518 2568 2554 2549 2544 2544 2544 2547 2556 2549 2557 2558 2551 2558 2552 2552 2552 2571 2571 2571 2607 2600 2590 2590 2593 2593 2594 2599 2596 2596 2595 2595 2595 2645 2624 2614 2614 2616 2620 2620 2628 2622 2623 2623 2634 2624 2632 2625 2630 2623 2623 2632 2627 2632 2626 2626 2624 2624 2624 2624 2656 2643 2643 2643 2645 2645 2647 2655 2648 2648 2647 2647 2647 2647 2669 2669 2669 2714 2706 2702 2699 2690 2690 2690 2694 2699 2695 2699 2698 2699 2696 2696 2699 2695 2695 2695 2740 2732 2728 2725 2716 2716 2718 2723 2723 2731 2727 2731 2731 2727 2727 2730 2733 2733 2729 2729 2734 2730 2749 2748 2742 2742 2739 2739 2732 2736 2735 2736 2729 2729 2726 2726 2726 2726 2760 2760 2758 2755 2748 2748 2748 2750 2750 2753 2753 2760 2760 2761 2754 2758 2752 2752 2752 2776 2776 2776 2776 2797 2797 2799 2799 2798 2806 2801 2806 2806 2806 2806 2826 2826 2826 2856 2846 2846 2849 2849 2851 2860 2855 2855 2856 2856 2856 2877 2877 2877 2925 2917 2910 2910 2899 2899 2901 2901 2905 2908 2908 2906 2906 2903 2903 2903 2903 2924 2924 2924 2962 2955 2944 2944 2946 2946 2949 2949 2951 2951 2956 2949 2949 2949 2949 2977 2977 2977 2977 2999 2999 2999 2999 3020 3020 3020 3020 3040 3040 3040 3040 3060 3060 3060 3060 3060
iterations count:1494449 (311), effective:2213 (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="GlobalResAllocation-PT-03"
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/GlobalResAllocation-PT-03.tgz
mv GlobalResAllocation-PT-03 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 GlobalResAllocation-PT-03, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r02kn-qhx2-140031222602029"
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 ;