fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150000573
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
1530.91 92969 30.3 32308197757577553240 2341356923067478430400 10 10 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 Diffusion2D-PT-D20N010, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198150000573
=====================================================================


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

BK_START 1401984469153

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: 400 NrTr: 2964)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


RS generation: 1m2sec


-> reachability set: #nodes 4390 (4.4e+03) #states 32,308,197,757,577,553,240 (19)


STATE_SPACE 32308197757577553240 2341356923067478430400 10 10 TECHNIQUES DECISION_DIAGRAMS


total processing time: 1m32sec


BK_STOP 1401984562061

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

474 509 538 566 587 610 627 640 660 679 693 709 731 739 747 756 767 787 800 812 824 836 854 886 903 911 916 922 927 932 937 943 953 965 972 978 984 990 1004 1019 1033 1053 1076 1086 1091 1097 1102 1107 1112 1117 1121 1126 1130 1134 1138 1149 1169 1187 1210 1244 1266 1286 1298 1302 1305 1308 1310 1313 1315 1317 1319 1321 1323 1325 1327 1329 1331 1332 1334 1336 1338 1339 1341 1342 1344 1346 1347 1349 1350 1358 1370 1376 1381 1383 1386 1388 1390 1392 1394 1396 1398 1400 1402 1403 1405 1407 1408 1410 1412 1413 1415 1416 1418 1419 1423 1434 1446 1455 1464 1473 1482 1495 1508 1518 1529 1543 1559 1572 1592 1612 1621 1623 1624 1625 1626 1627 1628 1630 1631 1632 1633 1634 1635 1637 1638 1639 1640 1644 1648 1653 1658 1664 1672 1680 1691 1703 1711 1713 1716 1718 1720 1722 1724 1726 1728 1730 1732 1734 1735 1737 1739 1741 1743 1745 1746 1748 1750 1752 1753 1755 1756 1758 1760 1761 1763 1764 1765 1766 1768 1769 1770 1772 1773 1774 1775 1776 1778 1779 1780 1781 1782 1783 1784 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1832 1843 1854 1864 1875 1885 1896 1907 1917 1929 1941 1953 1964 1976 1987 1999 2010 2024 2037 2050 2063 2075 2088 2103 2118 2132 2146 2160 2178 2194 2210 2228 2247 2265 2288 2321 2342 2362 2377 2384 2389 2394 2398 2402 2405 2409 2412 2414 2417 2420 2422 2424 2426 2428 2431 2438 2451 2456 2462 2466 2470 2474 2477 2481 2483 2486 2489 2492 2494 2496 2499 2502 2512 2525 2534 2543 2552 2561 2573 2587 2597 2608 2621 2637 2650 2670 2689 2701 2701 2702 2703 2703 2704 2704 2705 2706 2706 2707 2707 2708 2709 2709 2710 2710 2712 2713 2715 2716 2718 2719 2722 2726 2730 2736 2741 2748 2756 2766 2777 2790 2821 2836 2848 2857 2866 2871 2871 2872 2872 2873 2874 2874 2875 2875 2876 2876 2877 2877 2878 2879 2879 2880 2880 2881 2881 2882 2882 2883 2884 2884 2885 2885 2886 2886 2887 2887 2888 2889 2889 2890 2890 2891 2891 2892 2892 2893 2894 2894 2895 2895 2896 2896 2897 2897 2898 2898 2899 2900 2900 2901 2901 2902 2902 2903 2903 2904 2905 2905 2906 2906 2907 2907 2908 2908 2909 2910 2910 2911 2912 2913 2914 2915 2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 2955 2956 2957 2958 2959 2960 2961 2962 2963 2964 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2983 2984 2985 2986 2987 2988 2989 2990 2992 2998 3005 3011 3017 3023 3029 3035 3041 3047 3053 3059 3065 3071 3078 3084 3090 3096 3102 3108 3114 3120 3126 3132 3138 3144 3150 3156 3163 3169 3175 3181 3187 3193 3199 3206 3212 3218 3224 3230 3236 3242 3248 3254 3260 3266 3273 3279 3285 3291 3297 3303 3309 3315 3321 3327 3333 3339 3345 3351 3357 3364 3370 3376 3382 3388 3394 3400 3407 3413 3419 3425 3431 3437 3443 3449 3455 3461 3467 3474 3480 3486 3492 3498 3504 3510 3516 3522 3528 3534 3540 3546 3552 3558 3565 3571 3577 3583 3589 3595 3601 3608 3614 3620 3626 3632 3638 3644 3650 3656 3662 3668 3675 3681 3687 3693 3699 3705 3711 3717 3723 3729 3735 3741 3747 3753 3760 3766 3772 3778 3784 3790 3796 3803 3809 3815 3821 3827 3833 3839 3845 3851 3857 3863 3869 3876 3882 3888 3894 3900 3906 3912 3918 3924 3930 3936 3942 3948 3954 3960 3967 3973 3979 3985 3991 3997 4004 4010 4034 4039 4053 4059 4072 4078 4091 4096 4107 4115 4120 4133 4138 4151 4156 4160 4173 4177 4191 4195 4199 4212 4216 4220 4233 4237 4241 4253 4257 4264 4274 4277 4284 4293 4297 4302 4313 4317 4320 4333 4336 4339 4352 4355 4358 4371 4374 4377 4380
iterations count:730334 (246), effective:3990 (1)

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