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


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

BK_START 1400280571757

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: 1119 NrTr: 874)

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

12082 29232 31766 36294 41300 41618 42490 41691 42093 42052 43368 43331 43548 44295 48296 49121 49143 48889 49643 49738 49845 50313 50062 55029 87116 88971 90843 91764 91788 91975 91690 91997 91579 91476 94338 97334 98129 97241 97370 97383 97767 98012 98380 99270 98392 98322 98001 127658 257739 268994 270477 274091 275209 274718 275186 274963 275219 275036 274623 276194 276352 277306 277057 276728 275859 275490 275650 274590 267731 272078 280301 282632 288353 287064 290590 287584 287456 287310 287644 286437 286594 289191 291670 297529 297921 298821 296859 299044 298202 292146 296967 297591 299528 297491 299695 299105 299309 298881 295486 293054 295007 298270 379054 386911 691479 695545 693644 696521 697845 697610 697426 697594 697295 698232 698051 697057 698720 698878 699222 700175 699342 697662 698049 698292 696636 688357 696871 700448 701363 702640 702356 702891 702624 702684 702527 702084 703923 706483 707091 706956 708198 704643 705243 706678 705951 708084 704090 704191 699504 694351 712588 722892 725053 727195 729122 729766 729133 729928 729984 729786 730010 729796 729022 730766 730495 731566 731548 731647 729283 730488 730092 730483 728773 728861 723827 730343 734531 735899 738237 740290 740947 741612 742285 741255 741168 741203 741507 741016 740487 740882 739747 741374 743775 744021 749814 748477 750318 748511 751703 748402 752601 748378 749574 745983 748038 750647 750376 751366 750396 750554 750753 750639 750999 754733 751905 747964 749502 746620 749145 753252 750092 933116 935996 977561 976359

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