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

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

BK_START 1401988720674

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: 50 NrTr: 84)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


RS generation: 1m39sec


-> reachability set: #nodes 64614 (6.5e+04) #states 16,098,428 (7)


STATE_SPACE 16098428 213958152 25 1 TECHNIQUES DECISION_DIAGRAMS


total processing time: 1m51sec


BK_STOP 1401988831894

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

393 827 1414 1346 1360 1592 2248 3059 5342 4537 4421 4067 4836 6270 5618 5818 5686 5704 7827 11951 11360 10685 10452 9071 8824 8465 8521 10108 11921 15975 14828 14464 14651 14938 14870 15169 15492 15452 15352 14892 14930 15058 11506 15894 20961 23122 23940 24366 24626 23751 23944 24120 22339 26884 27406 23266 31957 34891 36014 38295 37411 36230 35924 74173 89405 88295 89373 89050 91615 93574 89308 89961 89397 78577 76736 76401 71625 75206 75598 77536 76793 76743 76733 74149 79337 76389 77636 83361 83373 83495 83359 84983 84842 84696 73320 73082 72355 71083 72368 71516 71709 74528 74805 74965 73937 73934 73248 66863 66855 67526 66994 67054 65765 64638 65239 67387 67299 66675 65825 65123 60354 60848 59598 58628 58050 57227 56799 56921 57346 56823 57316 56655 56747 56812 55961 54852 54706 54874 54691 54858 54042 53847 54190 54066 54041 53972 53757 53674 52023 52069 51487 50757 50276 57607 60467 60373 61171 60490 73080 84156 83189 85792 88375 89386 87444 85072 91573 90749 90966 93473 93742 93308 86486 82742 82948 82553 81354 81473 81250 76475 76615 76139 75228 75606 80408 83072 85012 85502 83991 84346 83690 83702 85098 85129 85130 85327 85064 74975 75182 76021 75735 75360 70523 70181 68010 67706 68576 68696 69421 69375 69697 70109 70615 70086 70217 70106 70236 70363 70925 70856 70785 70704 70518 70173 70370 70539 70697 70745 69967 70123 70290 70229 70233 70305 69360 68964 69095 69098 68943 68918 68404 66575 66546 66140 65542
iterations count:245784 (2926), effective:19013 (226)

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="Solitaire-PT-SqrNC5x5"
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/Solitaire-PT-SqrNC5x5.tgz
mv Solitaire-PT-SqrNC5x5 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 Solitaire-PT-SqrNC5x5, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198150901769"
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 ;