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

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

BK_START 1400739371806

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: 174 NrTr: 318)

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

412 1067 1225 1366 1821 2426 4646 5950 7598 8032 8305 8368 8291 8497 9043 9293 10147 10793 10885 13672 13596 13654 13422 14108 14071 13901 16378 16466 16472 16230 17088 16948 16820 34351 38133 39789 41091 40883 41052 47397 51378 52255 52116 51798 51600 53283 53835 54057 54102 54757 54941 54915 54333 53862 53495 53777 55923 56685 57277 58191 58639 58893 63025 68025 68442 70819 69881 72000 73160 70407 89447 89701 90354 90441 90301 90424 90344 90442 90582 91086 91132 90715 89879 88496 92319 92964 93128 93701 93761 93679 93649 93492 93501 94137 93926 93152 92073 95930 96461 96499 97145 97258 96907 97070 96910 97226 96684 95424 95509 111933 112676 113013 113282 113238 113431 113452 113312 112494 110933 111250 115403 115922 116215 116369 116033 116300 116606 116483 115746 114070 114552 118745 119546 119596 119698 119589 119367 119197 119574 119039 117717 117684 229013 242021 243484 262574 269941 276780 275120 276403 277595 278218 285443 285439 284787 280841 282931 283562 284840 285881 294367 299638 302143 303698 303970 306745 307145 307264 307362 307122 310283 314070 314485 316021 316475 316487 316702 316688 342303 361199 371000 376098 374620 373555 372099 378022 377686 374963 372497 372078 371278 370927 368600 375792 380810 383034 383737 383441 385840 386352 385430 384555 384805 385075 385027 389877 392050 391610 393386 393524 392796 392460 392072 393350 389974 390426 390612 390466 387956 385258 379966 379113 374724 370234 394111 418901 429497 427458 448020 450254 459387 464537 471921 461822 477139 469945 469432 461430 470698 471107 476766 482224 463608 571423 575105 577494 577212 579630 580143 579924 579653 579551 579071 577842 577374 577302 577371 577362 578003 577882 580366 580720 585428 583696 581045 580270 582207 614194 622643 628766 628603 628512

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