fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r24sr-ovh1-140198150801652
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-S10J40, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r24sr-ovh1-140198150801652
=====================================================================


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

BK_START 1401988442925

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: 854 NrTr: 12340)

net check time: 0m0sec

place and transition orderings generation:3m15sec

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: 0m3sec

858 2355 3150 5067 6195 6592 6801 6832 7230 7435 7669 7863 8083 8580 8797 8907 9419 9620 9745 10244 10489 10871 11078 11358 11803 12013 12318 13034 13261 13434 13976 14285 14471 15175 15550 16197 16459 16853 17547 17738 18113 19142 19142 19592 20704 20704 21429 22297 22734 23041 23979 24432 24754 25733 26112 26446 27365 27811 28157 29084 29524 29842 30784 31227 32425 32504 32961 33300 34288 34757 35110 36068 36563 36925 37923 38424 39603 39810 40423 41748 41945 42480 43755 43973 44514 45821 46019 46559 47940 48083 48673 50169 50273 50872 52509 52509 53166 54909 54909 55512 57189 57192 57812 59538 59538 60199 62036 62036 62701 64527 64527 65160 66830 67036 67744 69571 69658 70342 72133 72294 72983 74798 74972 84377 84602 85203 85186 85185 85164 85353 85164 85168 85348 85172 85172 85500 85329 85175 85392 85327 85261 85184 85317 85184 85185 85311 85185 85186 85522 85290 85189 85400 85282 85323 85203 85293 85217 85229 85309 85241 85244 85624 85298 85255 85466 85294 85486 85341 85400 85399 85462 85962 85603 85671 85734 85836 86114 86011 86155 86161 86261 86727 86516 86633 86739 86927 86931 87047 87387 87359 87496 88064 87853 88187 88142 88415 88403 88562 89205 88994 89355 89335 89647 89643 89827 90620 90334 90533 90723 91079 91086 91294 91893 91874 92093 92913 92702 93126 93168 93600 93601 93851 94821 94547 94816 95068 95548 95552 96090 96601 96594 96875 97869 97658 98128 98221 98755 98755 99052 100115 99904 100404 100523 101109 101109 101432 102663 102353 102878 103021 103655 103655 104011 105360 105028 105396 105753 106443 106445 106827 107919 107919 108460 109021 109012 109025 109115 109101 109086 109131 109206 109282 109270 109494 109483 109470 109571 109707 109851 109841 110252 110266 110311 110605 110854 111173 111250 111821 111895 111996 112411 112725 112850 113310 114009 114148 114311 115049 115204 115391 115974 116370 116993 117213 118073 118293 118535 119436 119675 119943 120688 121165 121956 122265 123302 123610 123940 125017 125344 125700 155075 155470 156041 160382 160632 160993 161147 161500 167047 202402 207298 208063 208863 209512 209564 209616 209660 209677 209681 209684 209689 209693 209696 209700 210141 211240 211243 211246 211250 211252 211664 212474 239027 240088 241319 242377 243002 243002 243002 243002 243002 243004 243006 243011 243016 243018 243023 243027 243029 243033 243002 243707 250361 250785 251184 251465 251671 251972 252221 252427 256789 264483 263912 263818 263872 263915 263967 264006 264052 264055 264060 264064 264067 264072 264076 264078 264270 264271 264274 264278 264208 263059 264726 264709 273959 274290 274682 274970 275157 275317 275542 275797 281133 288333 292673 293183 293922 294313 294344 294383 294425 294456 294461 294464 294469 294473 294476 294480

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-S10J40"
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-S10J40.tgz
mv PolyORBNT-PT-S10J40 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-S10J40, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198150801652"
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 ;