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


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

BK_START 1400686078286

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: 117 NrTr: 176)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m5sec


before gc: list nodes free: 1491048

after gc: idd nodes used:138717, unused:15861283; list nodes free:74832533

before gc: list nodes free: 1191954

after gc: idd nodes used:296749, unused:15703251; list nodes free:76132879

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

945 2939 2628 4645 4981 4545 5308 4573 5207 4499 8407 8566 8324 10887 10471 6966 9218 8906 10398 10008 10780 10795 10338 9164 15122 13620 16744 15251 20173 20327 18683 17988 18790 22393 20737 18679 19599 18272 16954 14708 12194 11014 18075 18394 17496 21290 19759 29373 28706 26821 25791 26837 25728 24694 22429 24310 27182 30517 28794 27847 27297 27163 27136 25123 25539 26555 24047 24970 20785 21012 17064 15274 23519 27525 27203 23936 32920 30979 47630 47330 45093 43512 44888 43635 42830 41780 39946 39298 38951 39561 43812 48986 49333 46949 45646 45672 45576 44416 44039 43262 40696 42006 44226 42070 40033 41222 38033 34837 27221 26846 22859 41547 42712 42701 43875 53626 52975 49653 84985 82340 75915 73996 75616 74191 73021 71628 68726 67938 68619 65730 65282 65246 65968 64276 77273 82685 79383 76896 75649 75572 75571 74142 74004 73106 72934 71526 71209 67861 69989 74663 70572 69694 67479 68402 66555 57861 57061 44967 44573 38731 34706 70326 70154 73473 70179 91529 92151 95387 156248 157899 149248 141270 138522 138624 138729 134786 135052 131075 131868 129739 126467 128498 125614 124398 123068 112515 124240 124211 122433 161027 155344 150804 147272 149035 148178 147272 146434 143244 143090 144823 141972 140997 143119 140481 139861 134544 132929 139986 143668 139164 137957 137747 132837 132428 131513 111724 112796 106428 83927 82841 72158 65967 127373 127960 129213 137130 122962 174418 173997 177616 239071 299700 292090 268707 268233 266271 256813 255182 259490 250866 248663 253844 244901 243987 250078 242638 240698 241662 238113 231773 230790 222945 232901 234493 233871 233479 295050 304065 297515 280818 275437 275365 277607 274513 274257 270899 271591 270308 267714 269601 269496 264674 265988 264027 261014 258886 258882 253944 249990

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