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


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

BK_START 1400808413484

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: 1330 NrTr: 2030)

net check time: 0m0sec

place and transition orderings generation:0m4sec

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

1330 1654 2156 2919 5608 5608 9960 12053 16238 16514 16515 17595 17595 17595 18595 18595 18595 19598 19598 19655 20515 20515 21414 21414 21435 21435 22669 24299 24299 24299 24575 24575 25328 25328 25328 25328 25328 25328 25328 25328 25328 25328 25328 25190 24359 38610 38624 39078 39050 39300 41174 41186 41198 42504 42504 42504 42504 43809 43809 43809 45041 45066 45041 46271 46281 46271 47940 48175 48967 54611 54611 54651 54651 54679 54651 54651 54741 54741 54765 54766 55608 55608 55608 55654 55654 55654 55671 55671 55671 55672 54859 56125 62680 62668 62754 62916 62916 62736 62968 62968 62779 62993 62988 62985 62985 62801 62768 63398 66448 63700 89446 89446 89818 89818 91325 91325 91325 91325 92629 92629 92629 92629 93932 93932 93932 95168 95213 95168 96373 96373 96373 96509 98207 99366 99540 102318 102318 104978 112572 112572 115147 115147 115323 117141 117141 117141 119531 119531 119531 122884 122884 124094 129622 130897 130750

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