fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150000560
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
- - - DNF timeout

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


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

BK_START 1401984451346

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


BK_TIME_CONFINEMENT_REACHED

--------------------
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 5739 4339 5997 4482 6157 4627 6319 4774 6483 4923 6859 4969 7029 5121 7522 5275 8023 5539 4351 5698 4390 5859 4429 6022 4690 6299 4843 6580 4998 6751 5155 7039 5314 7215 5359 7510 5521 7809 5685 8231 5851 8659 6019 4819 6310 4858 6483 4897 6658 5059 6959 5223 7139 5514 7447 5557 7632 5727 7819 5899 8137 6073 8459 6249 8916 6296 9379 6607 5287 6789 5326 6973 5365 7159 5539 7347 5715 7811 5893 8143 6073 8340 6255 8539 6439 8740 6625 9227 6671 9434 6860 10075 7051 10579 7389 5794 7585 5833 7783 5872 7983 6207 8334 6397 8689 6589 8897 6783 9107 6979 9472 7024 9841 7223 10214 7424 10747 7627 11286 7832 6262 8197 6301 8407 6340 8619 6539 8994 6740 9211 7105 9593 7148 9815 7355 10039 7564 10431 7775 10827 7988 11395 8035 11969 8420 6730 8639 6769 8860 6808

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