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


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

BK_START 1401988310671

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: 349 NrTr: 1210)

net check time: 0m0sec

place and transition orderings generation:0m1sec

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

1652 3632 4523 4912 5211 5541 5859 6122 6558 6873 7268 7717 8138 8544 8965 9380 9788 10186 10574 11044 11420 11823 12182 12847 33938 34247 34789 34831 34918 35280 35593 35664 35690 36013 36273 36558 36563 37075 37227 37290 37664 37991 38226 38231 38795 38911 39212 39216 39713 39923 40033 40327 40608 40867 47721 47639 48017 48226 48323 48702 48589 48935 49037 49079 49415 49280 49850 49653 50077 50244 50283 50712 50652 50982 51252 51255 51597 51674 52077 52058 52359 52572 52666 53009 53048 53317 53619 53622 53929 54053 54601 54751 54814 54928 55153 55347 55587 55812 56066 56286 64191 66258 69478 71944 73253 74244 73522 76600 78577 79902 80753 80555 83357 84793 86848 87950 89107 90022 91747 92783 93494 95019 95739 95603 94895 96902 97841 98873 98189 98201 99723 99051 98404 99119 170954 182712 184754 187137 189060 189776 191062 192241 193891 194223 252623 254529 258547 264627 266402 266591 266878 267523 269048 270681 272452 274996 278365 281642 300674 301468 301482 302164 307345 308691 308826 308952 309208 309524 309729 308686 308775 308109 372736 372981 375379 380029 383576 388403 391080 432594 436564 437980 438916 439906 440246 440349 440494 440375 439054 472458 475402 478827 483715 484518 484337 484259 484147 484789 485585 486588 488327 490270 492620 489503 486897 486249 485758 485653 484940 482784 482879 475192

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