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

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

BK_START 1401984309213

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: 25 NrTr: 144)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


RS generation: 1m46sec


-> reachability set: #nodes 7225 (7.2e+03) #states 1,205,415,014,974,454,321,389,844,651,253,260,376 (36)


STATE_SPACE 1205415014974454321389844651253260376 160722001996593909518645953500434716800 300 300 TECHNIQUES DECISION_DIAGRAMS


total processing time: 42m47sec


BK_STOP 1401986877073

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

80 136 192 248 304 360 416 472 528 584 640 696 752 808 864 920 976 1032 1088 1144 1200 1256 1312 1368 1424 1480 1536 1592 1648 1704 1760 1816 1872 1928 1984 2040 2096 2152 2208 2264 2320 2376 2432 2488 2544 2600 2656 2712 2768 2824 2880 2936 2992 3048 3104 3160 3216 3272 3328 3384 3440 3496 3552 3608 3664 3720 3776 3832 3888 3944 4000 4056 4112 4168 4224 3945 3967 3988 4009 4030 4052 4073 4094 4116 4137 4158 4179 4201 4222 4251 4281 4311 4341 4372 4402 4432 4463 4493 4523 4540 4555 4570 4586 4601 4617 4632 4647 4663 4678 4693 4709 4724 4740 4755 4770 4786 4801 4817 4834 4853 4873 4892 4912 4932 4951 4971 4990 5010 5030 5049 5069 5088 5108 5127 5146 5164 5182 5200 5218 5237 5255 5273 5291 5309 5327 5346 5364 5382 5400 5418 5434 5447 5461 5475 5489 5502 5516 5530 5543 5557 5571 5584 5598 5612 5626 5639 5653 5667 5680 5694 5708 5721 5749 5784 5818 5853 5887 5922 5956 5991 6025 6043 6060 6078 6095 6113 6131 6148 6166 6183 6201 6218 6236 6253 6271 6288 6306 6323 6340 6357 6374 6391 6408 6425 6442 6459 6476 6493 6510 6527 6544 6561 6578 6595 6612 6631 6661 6691 6722 6752 6782 6812 6843 6873 6903 6936 6976 7016 7056 7096 7136 7176 7216
iterations count:233244 (1619), effective:7200 (50)

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