fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r10ks-qhx2-140069023802575
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 SurpriseRailroad-PT-050, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r10ks-qhx2-140069023802575
=====================================================================


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

BK_START 1400864327181

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: 518 NrTr: 2756)

net check time: 0m0sec

place and transition orderings generation:0m1sec

init dd package: 0m6sec


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

518 518 680 680 680 813 813 833 833 833 817 817 830 830 830 821 821 827 827 827 825 825 825 976 976 1034 1034 1082 1082 1184 1184 1272 1272 1272 1322 1322 1322 1463 1463 1582 1582 1582 1713 1713 1818 1818 1818 1916 1984 1984 1984 2046 2074 2074 2130 2148 2148 2301 2301 2301 2412 2412 2540 2540 2622 2622 2622 2797 2797 2922 2922 2922 3078 3078 3180 3180 3180 3337 3337 3436 3436 3549 3549 3600 3600 3774 3774 3774 3882 3882 4011 4011 4070 4070 4158 4172 4172 4303 4303 4356 4356 4517 4517 4596 4596 4596 4796 4796 4910 4910 4910 5062 5124 5124 5124 5270 5270 5270 5404 5440 5440 5440 5604 5604 5604 5755 5800 5800 5800 5981 5981 6052 6052 6186 6206 6206 6357 6390 6390 6390 6597 6597 6682 6682 6830 6852 6852 6852 7024 7066 7066 7273 7273 7346 7346 7346 7560 7560 7636 7636 7894 7894 7894 8010 8010 8278 8278 8278 8400 8400 8560 8572 8572 8817 8817 8908 8908 8908 9162 9162 9258 9258 9258 9514 9514 9608 9608 9608 9792 9792 9792 10027 10092 10092 10092 10305 10344 10344 10344 10578 10634 10634 10634 10944 10944 11072 11072 11072 11306 11306 11306 20805 20805 20805 24171 24171 24171 24327 24327 24332 24332 24332 24462 24462 24455 24455 24455 24457 24457 24465 24465 24465 24458 24458 24460 24460 24460 24467 24467 24467 24464 24464 24210 24210 24210 24212 24212 24226 24226 24226 24219 24219 24216 24216 24216 25197 25197 25197 28220 28220 30235 30235 30235 30215 30215 30206 30206 30206 30201 30201 30193 30193 30193 30184 30184 30184 30191 30191 30175 30175 30175 30175 30175 30065 30065 30065 30079 30079 30072 30072 30072 29955 29955 29955 30136 30136 32184 32184 32184 34022 34022 33998 33998 33998 33978 33978 33962 33962 33962 33950 33950 33950 33834 33834 33841 33841 33841 33819 33819 33718 33718 33718 33822 33822 33822 35553 35553 37269 37269 37269 37256 37256 37132 37132 37132 37116 37116 37103 37103 37103 37003 37003 37003

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