fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r06ks-qhx2-140066506402172
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
- - - DNF timeout

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 SurpriseEcho-PT-d02r15, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r06ks-qhx2-140066506402172
=====================================================================


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

BK_START 1400687151895

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: 2127 NrTr: 1674)

net check time: 0m0sec

place and transition orderings generation:0m6sec

init dd package: 0m5sec


before gc: list nodes free: 1178146

after gc: idd nodes used:71801, unused:15928199; list nodes free:66788774

before gc: list nodes free: 968842

after gc: idd nodes used:127890, unused:15872110; list nodes free:66546682

before gc: list nodes free: 716795

after gc: idd nodes used:301846, unused:15698154; list nodes free:65795403

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

13084 30234 32847 39241 42313 41970 43016 42658 42662 42703 43611 43743 43511 43041 43527 44372 43409 43431 44017 44187 44159 44309 45940 44559 45041 44413 44218 44712 44430 44657 45093 44696 44609 44970 44699 45784 48195 44414 45420 45050 44836 45037 44754 45343 45484 45521 46218 45879 46172 48863 46127 45623 46652 46031 46242 46269 46140 46143 48645 48696 50871 48764 48611 49335 49084 48936 48933 49068 49005 49212 49111 48918 49079 49888 49263 49271 49676 49332 51551 49254 49204 49547 49941 50123 49531 50125 49776 49666 53465 49371 51661 52148 51866 53291 63367 63855 64477 64129 64646 64663 65079 64811 69030 65158 65152 67556 65567 65558 66419 65792 66120 65568 65554 66072 65718 65765 66221 65787 68102 65762 65681 66085 65732 65959 65416 65287 65387 65470 65572 65967 65920 66284 66652 66527 66333 66422 67529 66457 66709 66481 66718 66633 66461 66879 66557 67120 66826 66871 67982 67485 66669 66819 67039 66767 66773 67417 67319 66764 66801 67412 67755 68778 67705 67134 66901 66997 66821 74402 75246 75300 118007 118194 118937 119031 119373 119464 120200 120670 120279 120236 121121 120947 120773 121197 121205 121610 121277 121534 121384 121195 121340 122239 121726 123410 125412 121432 121407 121598 121521 125020 121387 121332 122269 122011 122548 125539 122149 123024 122423 122264 122228 122825 122654 122893 124393 122405 122418 121500 121398 121435 122063 121729 121966 125195 121160 122135 121312 121252 121023 121003 120751 122194 120287 119129 122914 121178 121706 122182 121948 123051 123081 122760 122721 123609 123506 123178 127183 123593 124174 124218 123402 123689 123979 125661 123725 123595 123761 124712 124339 127381 124111 123971 123855 123778 124248 123707 123153 123356 123035 123223 123730 123766 124290 125231 124812 123969 124420 125164 128109 124453 124421 124940 124888 126544 124935 125828 125894 124513 124988 125307 128257 125813 125363 126063 124663 124579 126851 124815 125407 125210 125119 125704 125127 126649 125237 125568 129385 125108 125210 125023 124865 125035 124743 124730 126079 125110 124818 125261 125850 125049 125101 125393 126888 125736 125921 127142 124572 124887 125229 126040 125030 148894 149316 149806 149453 294711 294397 295259 296201 296010 296806 297520 297479 297516 298455 298351 297985 298222 297656 298091 298161 299714 298070 298020 298774 298486 299528 298114 298410 300852 298315 298398 299335 298608 299580 298138 298230 298775 298157 299138 298881 299399 300322 299042 299850 299282 301843 299087 299209 299426 299382 300674 299264 299296 298332 298268 298294 298863 298688 298839 300803 298972 298390 298205 299286 297882 297769 297646 298562 298321 295681 298400 298505 300209 298565 299445 299197 299716 300751 299859 299761 299903 299973 300578 300145 300056 300270 300146 301149 300499 300096 300507 300249 300903 302761 300393 301220 300725 301651 300090 299282 299743 299376 300690 300082 300297 300228 300047 301453 300421 301449 301004 300906 300765 300484 301469 301162 303340 300761 299580 301087 299235 299342 299974 299652 299946 299716 300150 300074 299026 299352 299035 299877 301989 299142 299133 300388 297532 297488 297787 298009 297799 297122 294502 303283 304755 308969 306577 306008 306055 307666 308004 307393 307122 307304 307365 308583 308070 307883 308371 310591 308246

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