fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198149900534
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
2660.71 717010 20 45274257328051640582702088538742081937252294837706668420660 15561604026325287516868456563065117610593251089945407638056000 100 100 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-D10N100, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198149900534
=====================================================================


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

BK_START 1401984396581

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


-> reachability set: #nodes 10000 (1.0e+04) #states 45,274,257,328,051,640,582,702,088,538,742,081,937,252,294,837,706,668,420,660 (58)


STATE_SPACE 45274257328051640582702088538742081937252294837706668420660 15561604026325287516868456563065117610593251089945407638056000 100 100 TECHNIQUES DECISION_DIAGRAMS


total processing time: 11m57sec


BK_STOP 1401985114473

--------------------
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 4006 4016 4025 4034 4043 4052 4061 4070 4079 4088 4097 4106 4116 4125 4134 4143 4152 4161 4170 4179 4188 4197 4206 4216 4225 4234 4243 4252 4261 4271 4280 4289 4298 4312 4328 4343 4359 4374 4390 4406 4421 4437 4453 4468 4484 4499 4514 4529 4544 4558 4573 4588 4611 4694 4758 4803 4810 4818 4825 4833 4840 4848 4855 4863 4870 4877 4885 4892 4900 4911 4922 4933 4945 4956 4968 4979 4990 5003 5033 5062 5092 5105 5112 5118 5125 5132 5138 5145 5152 5158 5165 5172 5178 5185 5192 5198 5207 5217 5226 5236 5246 5255 5265 5274 5284 5294 5307 5332 5357 5382 5407 5432 5457 5482 5502 5508 5514 5519 5525 5531 5537 5543 5549 5554 5560 5566 5572 5578 5583 5589 5595 5601 5609 5617 5625 5633 5641 5649 5656 5664 5672 5680 5688 5696 5710 5731 5751 5772 5793 5814 5835 5855 5876 5897 5918 5939 5959 5980 6001 6006 6011 6015 6020 6025 6030 6035 6040 6045 6050 6055 6060 6065 6070 6075 6080 6085 6090 6095 6100 6106 6112 6119 6125 6131 6138 6144 6151 6157 6163 6170 6176 6183 6189 6195 6204 6222 6240 6258 6276 6293 6311 6329 6347 6365 6383 6400 6418 6436 6454 6472 6490 6507 6525 6543 6561 6579 6597 6604 6608 6612 6616 6620 6625 6629 6633 6637 6641 6645 6650 6654 6658 6662 6666 6670 6675 6679 6683 6687 6691 6695 6700 6704 6710 6715 6720 6725 6730 6735 6741 6746 6751 6756 6761 6766 6771 6777 6782 6787 6792 6797 6806 6822 6837 6853 6869 6884 6900 6915 6931 6947 6962 6978 6993 7009 7025 7040 7056 7071 7087 7103 7118 7134 7149 7165 7181 7196 7212 7227 7243 7259 7274 7290 7302 7305 7309 7312 7316 7319 7323 7326 7330 7333 7337 7340 7344 7347 7351 7354 7358 7361 7365 7368 7372 7375 7379 7382 7386 7389 7393 7396 7400 7403 7408 7412 7416 7420 7424 7428 7433 7437 7441 7445 7449 7453 7458 7462 7466 7470 7474 7478 7483 7487 7491 7495 7499 7510 7524 7538 7552 7566 7580 7594 7607 7621 7635 7649 7663 7677 7691 7705 7718 7732 7746 7760 7774 7788 7802 7816 7829 7843 7857 7871 7885 7899 7913 7927 7940 7954 7968 7982 7996 8010 8024 8038 8051 8065 8079 8093 8102 8105 8108 8111 8114 8117 8120 8123 8125 8128 8131 8134 8137 8140 8143 8146 8149 8152 8155 8158 8161 8164 8167 8170 8173 8176 8179 8182 8184 8187 8190 8193 8196 8199 8202 8206 8209 8213 8216 8220 8223 8227 8230 8234 8237 8241 8244 8248 8251 8255 8258 8262 8265 8269 8272 8276 8279 8283 8286 8290 8293 8297 8300 8304 8307 8311 8314 8318 8321 8325 8328 8331 8335 8338 8342 8345 8349 8352 8356 8359 8363 8366 8370 8373 8376 8380 8383 8387 8390 8394 8397 8401 8404 8407 8411 8414 8417 8420 8424 8427 8430 8434 8437 8440 8443 8447 8450 8453 8457 8460 8463 8466 8470 8473 8476 8480 8483 8486 8489 8493 8496 8499 8522 8555 8588 8607 8617 8627 8637 8648 8658 8668 8678 8689 8699 8730 8765 8801 8810 8819 8829 8838 8848 8857 8867 8876 8885 8895 8915 8950 8986 9006 9014 9023 9032 9041 9050 9058 9067 9076 9085 9093 9107 9143 9178 9204 9212 9220 9228 9236 9245 9253 9261 9269 9277 9286 9294 9306 9342 9378 9403 9411 9419 9426 9434 9442 9449 9457 9465 9473 9480 9488 9496 9513 9549 9584 9604 9612 9619 9626 9633 9641 9648 9655 9662 9670 9677 9684 9691 9699 9706 9713 9720 9727 9734 9741 9749 9756 9763 9770 9777 9784 9791 9799 9822 9851 9881 9913 9951 9990
iterations count:826284 (1208), effective:9900 (14)

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