fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150801587
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-1668
Executing tool marcie
Input is PolyORBNT-PT-S05J40, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198150801587
=====================================================================


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

BK_START 1401988344306

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: 629 NrTr: 1590)

net check time: 0m0sec

place and transition orderings generation:0m4sec

init dd package: 0m0sec


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

1180 2512 4306 5278 6837 7585 8929 9234 9757 9072 9364 9874 9196 9482 9974 9385 9571 10048 9630 9746 10137 10022 10446 10474 10737 11062 11090 11306 11537 11579 11727 12108 12144 12338 12713 12741 12980 13523 13626 13895 14107 14454 14815 15073 15523 15977 16269 16776 17193 17442 17863 17969 18540 18957 19096 19555 20082 20242 20720 21340 21419 21978 22578 22663 23244 23846 23939 24578 25274 25373 25983 26578 26604 27226 27950 27980 28651 28957 29492 30181 30454 30923 31650 32063 32738 33084 33812 34337 34701 35209 35923 36302 36829 37641 37796 38590 39377 39539 40437 41397 41564 42387 43184 43199 44132 44464 45052 46014 46437 47206 47714 48650 49441 49973 50879 51628 52175 52779 53785 54356 55027 56116 56714 57394 58499 58721 59749 60809 61038 63138 63925 64318 64203 64163 64215 64487 64511 64300 64452 64297 64297 64297 64340 64299 64303 64322 64365 64501 64448 64531 64581 64683 64879 64856 64923 65063 65298 65569 65476 65572 65768 66060 66087 66205 66445 66779 66826 67096 67245 67538 68013 67998 68168 68510 68947 69045 69416 69610 70006 70499 70625 70842 83146 83000 82682 82428 82262 82129 82035 81971 81104 79810 79109 78797 78769 82113 82761 83140 83103 83167 83444 83485 83509 83295 83445 83291 83291 83291 83335 83345 83293 83335 83419 83512 83681 83922 83801 83874 84025 84256 84435 84463 84561 84767 84992 85294 85353 85480 85739 86012 86361 86445 86606 86925 87257 87668 87782 87965 88340 88727 89187 89327 89753 89974 90420 90939 91107 103711 103447 103140 102922 102767 102673 102557 102486 101117 100044 99419 99122 99061 99099 99971 99959 99961 99982 99635 99411 99384 99376 99367 99359 99330 99354 99384 99419 99462 99510 99566 99903 99969 99945 100038 100139 100247 100359 100477 100603 100736 100879 100944 101100 101263 101431 101608 101789 101978 102176 102380 102592 102809 125916 125956 125974 134762 134965 134997 134000 135214 135242 135275 134039 135332 135365 135395 134139 135444 135482 135511 134205 135112 135153 135065 133748 151636 151676 151694 174083 173899 173932 181428 194914 195267 195091 199181 212480 211889 211693 214446 228244 227642 227301 229905 243958 243907 243726 248741 263390 262788 262526 265162 279703 279615 279585 282720 298249 298009 297671 301507 316064 315359 315116 331782 331354 331290 332355 346607 345991 345583 347529 361160 360454 359961 362745 375960 375591 374310 374319 389382 388633 387946 387881 402829 402714 401339 401087 415639 414846 414204 413284 427585 426752 426216 424786 440158 438506 437991

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="PolyORBNT-PT-S05J40"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="marcie"
export BK_RESULT_DIR="/srv/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/PolyORBNT-PT-S05J40.tgz
mv PolyORBNT-PT-S05J40 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool marcie"
echo " Input is PolyORBNT-PT-S05J40, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198150801587"
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 ;