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 SurprisePermAdmissibility-PT-01, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r09ks-qhx2-140069008902055
=====================================================================

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

BK_START 1400807683341

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: 168 NrTr: 592)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m4sec


RS generation: 0m52sec


-> reachability set: #nodes 78999 (7.9e+04) #states 52,537 (4)


STATE_SPACE 52537 54600 9 1 TECHNIQUES DECISION_DIAGRAMS


total processing time: 1m36sec


BK_STOP 1400807779549

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

1341 1583 1759 1881 2113 2098 2236 2320 2571 2607 2759 2792 2790 3006 3050 3145 3285 3371 3536 3542 3562 3550 3583 3868 4026 4058 4347 4376 4721 4749 4834 5176 5219 5334 5412 5456 5638 5677 5695 5738 5782 5836 5872 5992 6023 6078 6141 6339 6327 6315 6490 6468 6471 6615 6575 6571 6562 6993 7032 7080 7379 7434 7438 7794 7772 7767 7864 8335 8332 8350 8575 8604 8619 8620 8678 8712 8785 8786 8817 8854 8975 9011 9019 9051 9093 9135 9186 9245 9245 9344 9327 9393 9561 9546 9555 9595 9586 9615 9660 9677 9722 9744 9803 9953 10004 10043 10146 10185 10224 10200 10226 10239 10283 10329 10457 10471 10511 10547 10580 10627 10657 10685 10690 10692 10684 10787 10820 10873 10856 10865 10889 10888 10894 10861 10914 10944 11047 11081 11139 11166 11177 11178 11164 11156 11151 11138 11140 11553 12279 12817 13156 13553 13718 14234 14507 14738 14929 15181 15435 15575 15994 16434 17133 17291 17499 17619 17736 17812 17898 17974 18319 18406 18628 18689 18693 18875 19041 19465 19815 19826 20005 20126 20141 20244 20360 20441 20616 20729 20804 20984 21182 21289 21483 21658 21950 22325 22321 22577 22825 23004 23143 23215 23553 23791 23990 24200 24475 24398 24698 24719 24945 25135 25217 25401 25513 25654 25678 25902 26061 26308 26476 26508 26676 26710 26806 27029 27120 27218 27235 27244 27400 27542 27638 27605 27893 28146 28128 28211 28262 28388 28478 28852 29057 29276 29374 29650 29775 29861 30003 30079 30334 30461 30634 30688 30754 30822 30861 30946 31219 31229 31335 31436 31661 31812 31818 31996 32054 32143 32383 32545 32664 32839 33026 33113 33236 33443 33463 33483 33497 33557 33724 33900 33893 33917 34005 34195 34313 34378 34426 34498 34625 34787 34860 34893 34905 34940 35022 35262 35408 35494 35567 35728 35822 35827 35965 36101 36054 36213 36142 36181 36330 36277 36278 36427 36436 36529 36562 36575 36604 36614 36666 36723 36744 36745 36875 36936 37040 37101 37120 37157 37173 37304 37275 37308 37317 37487 37500 37619 37761 37821 37929 37973 37978 38000 38109 38031 38093 38228 38174 38294 38312 38230 38379 38486 38546 38558 38558 38613 38679 38729 38750 38750 38751 38939 39069 39086 39176 39212 39326 39591 39490 39510 39669 39603 39782 39933 40035 40116 40217 40300 40363 40507 40474 40635 40601 40702 40727 40760 40790 40933 40885 41102 41264 41403 41495 41604 41644 41718 41805 41867 41922 42091 42026 42037 42186 42133 42147 42302 42391 42513 42617 42653 42825 42810 42781 42868 43013 42946 43147 43205 43305 43381 43428 43499 43543 43647 43565 43736 43794 43707 43850 43731 43871 43829 43824 43931 44042 44085 44156 44189 44187 44261 44404 44319 44401 44524 44436 44441 44634 44489 44504 44699 44715 44722 44770 44845 44984 45097 44942 44970 45114 45057 45238 45354 45382 45442 45433 45498 45519 45623 45670 45793 45739 45825 45755 45772 45851 45929 45884 46061 46182 46252 46223 46291 46343 46414 46426 46447 46521 46631 46531 46579 46658 46587 46628 46769 46852 46868 46923 46972 47165 47149 47087 47128 47287 47218 47369 47438 47504 47551 47544 47602 47642 47646 47823 47862 47714 47849 47806 47744 47880 47885 47778 47949 47976 47968 48033 48034 48075 48131 48314 48218 48361 48320 48267 48378 48276 48298 48433 48411 48414 48451 48467 48486 48663 48647 48545 48543 48560 48596 51455 53653 53968 56240 56879 57982 59116 59740 60821 61150 61452 62311 62712 63147 63492 63678 64532 65091 65468 65817 65981 69182 70653 72886 73847 74445 75044 75611 75991 76328 76644 76892 77296 77504 77733 77922 78089 78181 78296 78405 78501 78566 78739 78874 78943
iterations count:595755 (1006), effective:3264 (5)

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="SurprisePermAdmissibility-PT-01"
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/SurprisePermAdmissibility-PT-01.tgz
mv SurprisePermAdmissibility-PT-01 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 SurprisePermAdmissibility-PT-01, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r09ks-qhx2-140069008902055"
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 ;