fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198149900521
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
1508.02 65009 20 13419107273154621529493489587286210498760 3080090394240859438313270764330123483608000 50 50 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-D10N050, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198149900521
=====================================================================


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

BK_START 1401984370298

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: 0m35sec


-> reachability set: #nodes 5050 (5.0e+03) #states 13,419,107,273,154,621,529,493,489,587,286,210,498,760 (40)


STATE_SPACE 13419107273154621529493489587286210498760 3080090394240859438313270764330123483608000 50 50 TECHNIQUES DECISION_DIAGRAMS


total processing time: 1m5sec


BK_STOP 1401984435419

--------------------
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 2057 2066 2075 2084 2093 2102 2111 2121 2130 2139 2148 2157 2166 2175 2184 2194 2204 2220 2235 2251 2267 2282 2298 2313 2327 2342 2386 2451 2458 2466 2473 2480 2488 2495 2504 2515 2527 2538 2549 2577 2602 2608 2615 2622 2628 2635 2642 2648 2657 2667 2676 2686 2696 2712 2737 2762 2787 2803 2809 2815 2821 2826 2832 2838 2844 2850 2857 2865 2873 2881 2889 2897 2912 2933 2953 2974 2995 3016 3036 3052 3057 3062 3067 3072 3077 3082 3087 3092 3097 3102 3108 3115 3121 3128 3134 3140 3147 3158 3176 3193 3211 3229 3247 3265 3282 3300 3318 3336 3351 3355 3360 3364 3368 3372 3376 3380 3385 3389 3393 3397 3401 3407 3412 3417 3422 3427 3432 3437 3443 3448 3458 3473 3489 3504 3520 3536 3551 3567 3582 3598 3614 3629 3645 3660 3676 3692 3702 3705 3709 3712 3716 3719 3723 3726 3730 3733 3737 3740 3744 3747 3751 3755 3759 3763 3768 3772 3776 3780 3784 3788 3793 3797 3802 3816 3830 3844 3857 3871 3885 3899 3913 3927 3941 3954 3968 3982 3996 4010 4024 4038 4051 4065 4079 4093 4102 4105 4108 4111 4114 4117 4120 4123 4125 4128 4131 4134 4137 4140 4143 4146 4149 4152 4156 4159 4163 4166 4170 4173 4177 4180 4184 4187 4191 4194 4198 4201 4205 4208 4212 4215 4218 4222 4225 4229 4232 4236 4239 4243 4246 4250 4253 4256 4260 4263 4266 4269 4273 4276 4279 4283 4286 4289 4292 4296 4299 4318 4351 4361 4371 4381 4392 4405 4440 4457 4467 4476 4485 4495 4515 4550 4559 4568 4577 4586 4594 4611 4646 4658 4666 4674 4682 4690 4699 4728 4753 4761 4769 4776 4784 4792 4799 4831 4854 4861 4868 4875 4883 4890 4897 4904 4911 4919 4926 4933 4940 4947 4966 4995 5032
iterations count:413484 (604), effective:4950 (7)

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