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

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

BK_START 1400739481884

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: 264 NrTr: 536)

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

581 603 1169 1645 1742 1941 2137 2634 3034 3478 3660 7241 8128 8412 10490 11037 11225 11434 11414 11486 11524 11726 11927 12564 12841 13069 14266 14290 15289 15530 15509 20936 21853 21906 21895 21980 21758 21665 22500 22569 22536 22529 22331 22312 46088 51133 53052 54187 54663 54061 63666 65999 67535 68011 68070 68479 69593 69696 70266 70100 70579 71208 71347 71061 70483 70169 69393 69708 69914 70176 70736 71000 71274 71873 72135 72287 75453 76238 76926 77071 77061 78757 78818 78979 79852 85556 85569 91985 93227 92441 97453 95910 94615 94525 95306 131987 137673 138092 138703 138827 138951 138853 139054 138952 138843 138952 138854 138965 138781 139425 139806 140016 139972 139691 138660 139024 136911 136668 141527 142176 142402 143091 143196 143137 143304 143271 143187 143334 143112 142909 142909 143180 143258 143798 142741 143102 141114 140852 145777 146643 146859 146803 147273 147330 147140 147454 147887 147796 147924 147684 147575 146604 146869 144929 144613 148968 149577 150157 150051 150474 150635 150641 150370 150386 150559 150739 151276 151131 151010 150019 150289 148336 148063 153177 153738 153986 154746 154768 154719 154881 154749 154690 154622 154440 154485 154691 154761 154967 154274 152869 152417 152691 157949 158790 159076 159245 159507 159501 159541 159698 160071 159998 159812 159778 158752 158987 157033 156823 156986 161559 162423 162380 162583 162847 162876 162694 162501 162718 162893 163320 163222 162869 162116 161697 160048 160261 165577 166143 166371 166997 167056 167104 167239 167137 166944 166913 166776 166687 167101 167185 166586 166915 164853 164727 165067 326218 339406 341077 359990 379773 382913 390671 392563 390125 397437 398413 398794 395177 393103 394284 395082 395058 393561 395700 396633 396869 396716 398233 399014 399404 400777 401757 402626 401952 417414 419674 423223 426737 427636 427626 428097 431110 431694 431685 431567 432504 431716 431717 431831 431908 440310 442799 443942 445477 444787 444513 444651 447239 448386 447800 447525 485041 504421 523161 527912 533864 535538 532830 537672 538490 538262 536871 534049 532920 532693 532020 530750 530533 529918 528823 528646 528016

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