About the Execution
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-D05N200, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198149900456
=====================================================================
--------------------
content from stdout:
BK_START 1401984275184
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: 0m23sec
-> reachability set: #nodes 4825 (4.8e+03) #states 114,386,128,575,629,019,874,142,761,713,876 (32)
STATE_SPACE 114386128575629019874142761713876 14706787959723731126675497934641200 200 200 TECHNIQUES DECISION_DIAGRAMS
total processing time: 4m19sec
BK_STOP 1401984534715
--------------------
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 2645 2667 2688 2709 2730 2752 2773 2794 2816 2841 2872 2902 2932 2963 2993 3023 3040 3055 3070 3086 3101 3117 3132 3147 3163 3178 3193 3209 3224 3243 3263 3283 3302 3322 3341 3361 3381 3400 3420 3438 3457 3475 3493 3511 3529 3547 3566 3584 3602 3620 3635 3649 3663 3676 3690 3704 3717 3731 3745 3758 3772 3786 3799 3813 3829 3863 3898 3932 3967 4001 4031 4048 4066 4083 4101 4118 4136 4153 4171 4188 4206 4223 4240 4257 4274 4291 4308 4325 4342 4359 4376 4393 4410 4428 4458 4488 4519 4549 4579 4609 4644 4684 4724 4764 4804
iterations count:155544 (1080), effective:4800 (33)
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-D05N200"
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-D05N200.tgz
mv Diffusion2D-PT-D05N200 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-D05N200, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198149900456"
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 ;