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-1667
Executing tool marcie
Input is SurpriseEcho-PT-d02r09, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r06ks-qhx2-140066506402146
=====================================================================

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

BK_START 1400687035342

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: 735 NrTr: 570)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m5sec


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

13344 28842 31334 36054 42540 42457 62675 65211 66622 66977 70582 91469 181516 190276 190764 193586 194966 192371 199546 199576 203403 204377 208834 206104 268625 432159 439144 442193 444040 444713 444324 447298 448256 446527 448390 441036 448040 456691 463057 463117 465484 467044 459932 466742 471793 470355 476787 476673 475752 478198 478700 477585 480617 591310 612502 611178 620406 603759 597901 596917 679571 705036 630284 616824 619855 625768 619037 620643 622529 619698 626042 618185 617497 618603 627699 626967 636049 624720 612950 613327 638118 643360 644562 627079 620943 719175 727630 707536 678658 720822 721046 719738 719786 721423 719870 738288 739397 741784 738561 736993 741257 742609 745622 736814 733137 736788 738185 743978 745411 739245 734456 679230 710236 717806 722750 717334 725224 728315 737856 748277 737973 741544 859493 847431 849859 841404 839498 835413 847346 869372 882536 885118 878998 850884 891649 888295 891557 861563 855229 926383

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="SurpriseEcho-PT-d02r09"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="marcie"
export BK_RESULT_DIR="/home/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/SurpriseEcho-PT-d02r09.tgz
mv SurpriseEcho-PT-d02r09 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1667"
echo " Executing tool marcie"
echo " Input is SurpriseEcho-PT-d02r09, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r06ks-qhx2-140066506402146"
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 ;