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 SurpriseLamportFastMutEx-PT-8, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r08ks-qhx2-140068994902432
=====================================================================

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

BK_START 1400739539781

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: 315 NrTr: 666)

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

648 1046 1135 1326 1564 1732 1663 1578 1576 1783 2213 2418 2821 2921 2978 3049 3290 3257 3373 3329 3251 3230 3407 3587 3595 3597 3635 3637 3567 3539 4241 4540 4619 4718 4810 4874 4835 4944 5022 4934 4841 4754 4734 4636 5063 5606 5593 5934 5826 5564 5423 6637 6664 6720 6714 6597 6752 7105 7259 7266 7154 6981 6974 7464 7828 7812 8371 8511 8748 8653 8847 8850 8867 8822 8683 8771 9135 9271 9382 9441 9477 9475 9419 9366 12767 15087 15092 17771 17685 17266 18449 18789 18816 20124 20186 20343 20369 19958 19788 20013 21419 22442 22203 22984 23073 22974 23058 22889 22883 22805 22701 23085 22983 22750 23430 23473 23066 22407 22464 23275 22902 22982 22507 22156 21720 21382 21071 21185 20725 22762 23580 23731 23390 23780 23786 23603 23494 23627 23602 23851 23826 23690 23349 23050 23135 22915 22444 24037 24511 24758 24920 24965 24813 24756 25698 26176 25995 25941 25898 26041 25993 25903 25798 24949 24678 23939 25753 26563 27617 27662 27981 28520 28455 28374 27722 27219 27064 27018 29221 29111 29605 30010 29792 28791 29080 31224 30681 29559 30774 31440 32426 32443 32474 32849 32832 33324 33360 33404 33345 33265 33491 34350 34128 34421 34375 34413 34368 34377 34481 34410 34326 34249 33854 33828 33518 33354 33160 32562 32158 32792 32971 33186 33139 33014 32001 33998 41315 41587 41608 42329 42352 42358 42289 42174 42222 43209 43235 42933 42899 42897 42771 43297 42707 41964 41837 41671 42719 42325 43931 44262 44828 44722 44861 44756 44458 44160 43835 43804 44528 44541 44619 44566 44526 44469 44231 44603 44618 44721 44559 44398 44583 43806 44998 45430 46273 46288 46677 46769 47197 47261 47305 47304 47229 47204 47380 47753 47575 47694 47637 47656 47626 47619 47697 47629 47572 47513 47130 47136 46733 46704 46685 46215 45736 44920 44979 47942 48289 48616 48894 48979 49278 49028 49300 49223 49207 49162 49023 49349 49434 49495 49268 49266 49852 50807 51504 51132 51653 51780 51291 51782 51790 51774 52201 52252 51988 52035 51667 51532 51520 52098 52658 52410 52656 52696 52651 52716 52631 52627 52601 52686 52640 52484 52393 52227 52070 52129 53030 53037 53232 53314 52969 52736 53629 54306 54265 54043 53885 53690 53512 53233 53079 52410 55031 56088 56613 56393 56268 57852 58126 57899 59221 59534 59683 59628 60423 60495 60138 60489 60245 60063 59828 60316 61764 62090 62397 61991 62803 63232 63580 62905 63033 62907 62673 62574 62077 61662 61633 61545 61337 60573 60255 60662 60470 59855 59694 60349 60370 60421 60768 61065 60973 60920 61054 61036 60967 60974 60912 61690 62203 62048 61645 62010 62111 61846 61788 61824 61654 61534 61535 61386 61252 61115 61118 60845 60470 60556 60441 60921 60740 60878 61102 60957 60386 60613 60588 60531 60233 59963 59350 59201 59543 58688 59058 59432 59576 59768 59742 59806 59783 60207 61157 61138 61799 61485 61794 61848 62138 62167 62111 62034 61889 61691 62064 62372 62567 62645 62669 62651 62644 62593 62625 62472 62372 62320 62283 63283 64517 64677 64292 65313 65100 65372 65814 65803 66151 66152 66012 65991 65750 65686 65652 66274 66712 66498 66891 67460 67531 67427 67350 67152 67006 66809 66740 66571 66203 65736 66098 66468 66570 66883 66683 66725 66780 66826 66740 67123 67333 67178 67348 67317 67355 67370 67287 67137 67080 66957 66981 66972 67041 67069 66945 66852 66764 66493 66492 66445 66422 66178 66232 65890 65876 65437 65600 65853 65888 65918 66170 65887 65788 65813 65816 65626 83230 89378 92616 93759 94313 95192 96562 108311 108037 108632 112430 113474 113866 114536 116769 118944 118841 120258 120327 119879 119457 119101 121443 122796 123409 123034 123222 125588 126914 126992 126330 126173 126098 125851 125213 124764 124510 124315 125552 128458 128735 128783 131151 130908 129167 128990 128211 129615 130305 129958 130653 131283 131015 130574 130269 129691 129350 127710 130583 132334 132805 132880 132795 133582 134138 133962 133723 133839 133209 132971 133009 133045 132806 132732 132447 131695 131815 131657 131196 130417 130215 129969 136460 139730 140070 140605 141696 142353 142481 142266 142471 142176 141976 142006 141745 143939 145511 145475 144282 145231 145523 145253 145295 145181 144761 144521 144326 145874 146669 146490 145411 145325 145146 145042 145097 145083 144900 144841 144532 144445 143998 143914 144905 144687 144440 145494 145557 145287 144928 144909 144373 145857 145492 144144 145095 144907 145270 143370 142550 148333 147920 148002 148595 148112 146203 143758 141278 142213 143952 147984 149505 149531 148976 149238 148675 151185 151313 151764 151223 151623 152129 151623 149124 149131 148694 147377 147031 147246 147237 147219 146240 145275 144464 144259 143866 143874 143333 143268 143020 142157 140950 141180 141170 139908 138062 137462 138579 139248 137802 136950 135031 135535 135127 135435 135796 135110 135106 134680 135046 134925 134782 135201 133684 133501 133359 133142 132841 132494 133849 132712 130039 129727 129091 127754 127042 126680 126902 128259 128724 129005 128669 138213 141540 148088 149016 149278 150700 150877 151129 151717 151167 150191 148851 147267 147176 146915 146623 145901 157577 157891 157957 157697 157166 160042 163141 162783 163043 162769 161381 179567 181356 183826 186685 187152 187867 187843 183742 182683 182390 182014 181203 180492 180134 170580 170583 170525 170086 169293 168887 170992 180264 180294 180464 180073 179909 184014 185482 185153 185392 185037 184959 186377 186550 186812 186246 186020 185379 186260 188929 205631 200626 199462 195629 200442 202190 203321 203914 204239 209095 209296 210061 211253 211561 211822 213225 213511 213139 213829 213802 213605 214427 215623 216075 215634 216609 217230 217638 216948 216924 217013 216891 216459 216442 216345 216243 217483 218295 218142 219162 219146 218473 218112 218865 219241 219139 219677 219483 219369 219215 218916 218372 218072 218923 220924 222606 221380 222315 222544 222580 222593 222593 222555 222506 223553 223964 223547 224075 223876 223960 224099 223972 223889 223828 223724 223956 223819 224170 223991 223898 223804 224086 223507 224180 224250 223841 222688 221334 221428 220986 221866 222196 221867 221753 222122 222194 222146 221845 221891 220603 220515 219980 219144 218371 217935 218080 216607 215850 215762 215504 215438 215287 213295 212248 211223 211866 212057 205393 207095 207373 207906 208053 208113 208110 207910 206718 206446 208852 208678 208334 209508 210033 209822 211135 213979 215304 215728 220412 220503 220249 221842 222421 222504 223577 224370 224281 224734 224701 224538 224495 225356 226626 226697 227587 227491 226638 226322 227801 228684 228722 228844 229384 229596 229318 229410 229019 229122 229201 229121 228963 228861 228845 228693 228381 231143 232610 232698 232291 232738 232615 232652 232745 232673 232731 232673 233829 233848 233371 233606 233375 233373 233443 233390 233362 233333 233236 233527 233363 233572 233384 233316 233220 233760 232968 233292 233237 233197 232289 231016 230936 230430 231403 231439 231261 230918 230195 230309 230153 229706 229448 229121 228878 228318 227763 227935 226490 226418 225757 225560 225412 225331 223462 222555 224237 225327 226930 227656 227746 227766 227779 227435 226455 226230 229017 228809 228531 229708 230244 230025 221081 239257 241034 285217 286264 286418 290360 291065 291342 292166 291271 291719 291861 291832 295916 297403 297468 297231 296869 296507

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