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 LamportFastMutEx-PT-6, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r02kn-qhx2-140031222902406
=====================================================================

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

BK_START 1400338893167

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: 217 NrTr: 420)

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

489 968 1442 1542 1663 2031 2582 2968 6517 7196 9032 9586 9825 9960 9932 9882 10081 10707 10945 11063 11908 12560 12720 17902 18114 18020 18104 17816 18616 18691 18736 18719 18464 19200 19293 19250 19250 19019 39621 44214 45881 47448 47123 47189 54365 58866 59399 60408 59780 59477 61217 61692 62252 62140 62867 63244 63205 62571 62356 61939 61331 61585 61732 62371 62590 64992 66003 66765 66865 68038 68403 68515 71900 73080 78133 79030 82567 81567 82767 80378 80631 111257 116538 116784 117513 117622 117640 117682 117518 117610 117396 117481 117272 118340 118439 118418 117961 117518 115405 115243 120253 120564 120547 121336 121442 121209 121382 121289 121069 121071 121365 122040 120842 121103 119068 119180 124328 124579 124762 125494 125684 125545 125388 125376 125173 124235 123889 122433 126486 127525 127547 127437 127916 127991 127883 127979 128117 128505 128298 127334 126975 125536 130164 130781 130871 131522 131755 131540 131702 131625 131416 131292 131696 132107 131113 129477 129478 134301 135147 135537 135795 135968 135918 136096 136295 136216 136073 135059 134563 133079 133342 137758 138353 138398 138899 138967 138563 138500 138919 139158 139123 138074 137657 136226 136462 141570 141892 142569 142699 142784 142714 142494 142341 142201 142619 143053 142045 140350 140291 140491 274699 296150 295606 316546 325628 331402 333350 331488 333012 337410 341911 341276 340481 336985 338011 338896 339352 340552 341389 341875 343477 344467 344493 356180 361479 362937 366243 366271 366517 370243 370538 370362 370555 370290 370374 370497 376576 378431 380279 380711 381166 380650 381636 381910 378536 414045 436852 448273 453209 456335 452977 451678 458195 458485 458079 453913 452638 452045 451350 451271 450674 449751 449085 446999 446640 458503 462311 463724 465485 465022 468155 468355 467078 466373 466277 466441 466552 466717 466999 466950 474246 474692 474996 474996 476993 477294 476443 475695 475625 475288 476536 472537 473311 473366 473323 472873 470985 467203 462921 459840 457362 456039 452856 447517 476729 475458 507678 507748

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