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


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

BK_START 1401983916413

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: 14 NrTr: 16)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


before gc: list nodes free: 40994

after gc: idd nodes used:11575, unused:15988425; list nodes free:134090527

before gc: list nodes free: 59075

after gc: idd nodes used:16368, unused:15983632; list nodes free:134037800

before gc: list nodes free: 69986

after gc: idd nodes used:20045, unused:15979955; list nodes free:133997353

before gc: list nodes free: 89567

after gc: idd nodes used:23144, unused:15976856; list nodes free:133963264

before gc: list nodes free: 86798

after gc: idd nodes used:25874, unused:15974126; list nodes free:133933234

before gc: list nodes free: 76322

after gc: idd nodes used:28342, unused:15971658; list nodes free:133906086

before gc: list nodes free: 94084

after gc: idd nodes used:30611, unused:15969389; list nodes free:133881127

before gc: list nodes free: 75371

after gc: idd nodes used:32723, unused:15967277; list nodes free:133857895

before gc: list nodes free: 104549

after gc: idd nodes used:34706, unused:15965294; list nodes free:133836082

before gc: list nodes free: 133586

after gc: idd nodes used:36581, unused:15963419; list nodes free:133815457

before gc: list nodes free: 151083

after gc: idd nodes used:38364, unused:15961636; list nodes free:133795844

before gc: list nodes free: 111936

after gc: idd nodes used:40068, unused:15959932; list nodes free:133777100

before gc: list nodes free: 130610

after gc: idd nodes used:41702, unused:15958298; list nodes free:133759126

before gc: list nodes free: 143846

after gc: idd nodes used:43274, unused:15956726; list nodes free:133741834

before gc: list nodes free: 115376

after gc: idd nodes used:44791, unused:15955209; list nodes free:133725147

before gc: list nodes free: 125461

after gc: idd nodes used:46258, unused:15953742; list nodes free:133709010

before gc: list nodes free: 99316

after gc: idd nodes used:47680, unused:15952320; list nodes free:133693368

before gc: list nodes free: 163192

after gc: idd nodes used:49060, unused:15950940; list nodes free:133678188

before gc: list nodes free: 172006

after gc: idd nodes used:50402, unused:15949598; list nodes free:133663426

before gc: list nodes free: 176906

after gc: idd nodes used:51709, unused:15948291; list nodes free:133649049

before gc: list nodes free: 138703

after gc: idd nodes used:52984, unused:15947016; list nodes free:133635024

before gc: list nodes free: 128698

after gc: idd nodes used:54229, unused:15945771; list nodes free:133621329

before gc: list nodes free: 121301

after gc: idd nodes used:55446, unused:15944554; list nodes free:133607942

before gc: list nodes free: 205376

after gc: idd nodes used:56636, unused:15943364; list nodes free:133594852

before gc: list nodes free: 135662

after gc: idd nodes used:57802, unused:15942198; list nodes free:133582026

before gc: list nodes free: 234116

after gc: idd nodes used:58944, unused:15941056; list nodes free:133569464

before gc: list nodes free: 136838

after gc: idd nodes used:60065, unused:15939935; list nodes free:133557133

before gc: list nodes free: 181037

after gc: idd nodes used:61165, unused:15938835; list nodes free:133545033

before gc: list nodes free: 239557

after gc: idd nodes used:62245, unused:15937755; list nodes free:133533153

before gc: list nodes free: 174631

after gc: idd nodes used:63307, unused:15936693; list nodes free:133521471

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

514 1014 1514 2014 2514 3014 3514 4014 4514 5014 5514 6014 6514 7014 7514 8014 8514 9014 9514 10014 10514 11014 11514limit of 2048MB is reached
12014 12514 13014 13514 14014 14514 15014 15514 16014limit of 2048MB is reached
16514 17014 17514 18014 18514 19014 19514 20014limit of 2048MB is reached
20514 21014 21514 22014 22514 23014limit of 2048MB is reached
23514 24014 24514 25014 25514limit of 2048MB is reached
26014 26514 27014 27514 28014limit of 2048MB is reached
28514 29014 29514 30014 30514limit of 2048MB is reached
31014 31514 32014 32514limit of 2048MB is reached
33014 33514 34014 34514limit of 2048MB is reached
35014 35514 36014 36514limit of 2048MB is reached
37014 37514 38014limit of 2048MB is reached
38514 39014 39514 40014limit of 2048MB is reached
40514 41014 41514limit of 2048MB is reached
42014 42514 43014limit of 2048MB is reached
43514 44014 44514limit of 2048MB is reached
45014 45514 46014limit of 2048MB is reached
46514 47014 47514limit of 2048MB is reached
48014 48514 49014limit of 2048MB is reached
49514 50014limit of 2048MB is reached
50514 51014 51514limit of 2048MB is reached
52014 52514limit of 2048MB is reached
53014 53514 54014limit of 2048MB is reached
54514 55014limit of 2048MB is reached
55514 56014 56514limit of 2048MB is reached
57014 57514limit of 2048MB is reached
58014 58514limit of 2048MB is reached
59014 59514 60014limit of 2048MB is reached
60514 61014limit of 2048MB is reached
61514 62014limit of 2048MB is reached
62514 63014limit of 2048MB is reached
63514 64014limit of 2048MB is reached

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="CircadianClock-PT-100000"
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/CircadianClock-PT-100000.tgz
mv CircadianClock-PT-100000 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 CircadianClock-PT-100000, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r24sr-ovh1-140198149600170"
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 ;