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


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

BK_START 1401983902585

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: 16994

after gc: idd nodes used:14717, unused:15985283; list nodes free:134055963

before gc: list nodes free: 22625

after gc: idd nodes used:36083, unused:15963917; list nodes free:132386967

before gc: list nodes free: 37003

after gc: idd nodes used:48368, unused:15951632; list nodes free:120322685

before gc: list nodes free: 20033

after gc: idd nodes used:54703, unused:15945297; list nodes free:109349703

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 10267 10517 10767 11017 11267 11517 11767 12017 12267 12517 12767 13017 13267 13517 13767 14017 14267 14517limit of 2048MB is reached
14767 15017 15267 15517 15767 16017 16267 16517 16767 17017 17267 17517 17767 18017 18267 18517 18767 19017 19267 19517 19767 20017 30240 30457 30675 30890 31117 31325 31548 31760 31980 32195 32415 32630 32850 33065 33285 33500 33720 33935 34155 34370 34590 34805 35025 35240 35457 35675 35890limit of 2048MB is reached
36117 36325 36548 36760 36980 37195 37415 37630 37850 38065 38285 38500 38720 38935 39155 39370 39590 39805 40025 40240 40457 40675 40890 41117 41325 41548 41760 41980 42195 42415 42630 42850 43065 43285 43500 43720 43935 44155 44370 44590 44805 45025 45240 45457 45675 45890 46117 46325 46548 46760 46980 47195 47415 47630 47850 48065 48285limit of 2048MB is reached
48500 48720 48935 49155 49370 49590 49805 50025 50240 50457 50675 50890 51117 51325 51548 51760 51980 52195 52415 52630 52850 53065 53285 53500 53720 53935 54155 54370 54590limit of 2048MB is reached
54805 55025 55240 55457 55675 55890 56117 56325 56548 56760 56980 57195 57415 57630

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