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


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

BK_START 1401988399490

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: 474 NrTr: 11760)

net check time: 0m0sec

place and transition orderings generation:1m22sec

init dd package: 0m0sec


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: 0m1sec

1324 2249 3646 3898 4299 4538 4827 5308 5672 6030 6634 7080 7616 8367 9038 9379 9926 10839 11247 11933 12500 13347 14034 14775 15900 16886 17386 18255 19549 20049 20951 21710 22914 23934 27351 27824 27803 27896 27782 27848 27782 27782 27782 27782 27908 27790 27817 27857 27968 28030 28192 28327 28459 28621 28782 29277 29358 29661 29680 30007 30139 30508 30650 31037 31331 31624 31948 32270 33089 33226 33759 33856 34429 34711 34997 35052 35085 35289 35296 35319 35506 35711 36103 36377 36938 37221 37463 37837 38230 38915 39367 52103 58282 70929 70941 70953 71406 71767 71997 78240 78939 78939 78939 78961 84396 88298 89841 89841 89841 89992 90025 89077 88951 94506 100367 100367 100367 100566 100514 100512 99697 107596 111579 111579 111579 111747 111703 110829 117357 121253 124953 124953 124953 125100 125052 123824 130256 133013 136884 136884 136884 136923 136959 136111 143680 146783 151788 151788 151788 151817 151840 150222 159011 162489 168923 168923 168923 168940 168975 166934 175938 179096 186024 186024 186024 186025 186036 182917 191553 194071 201034 201034 201034 201035 201058 197614 206286 208406 215462 215462 215462 215465 215469 211514 220567 222166 228905 228905 228905 228906 228027 225113 234020 235432 243030 243030 243030 243031 241952 238019 246831 254797 255044 255044 255044 255045 253767 249569 259036 267734 267734 267734 267734 267735 266239 261092 270256 278272 278272 278272 278272 278273 276572 270673 281184 287291 287291 287291 287438 287292 285346 278957 288706 293996 293996 293996 294138 293997 288514 285595 295297 300406 300406 300406 300545 300407 294078 300686 297581 304647 304647 304647 304752 304648 297414 303696 300858 307914 307914 307914 307915 307921 299344 296837 317255 317568 317608 317706 317698 317719 317584 317738 317584 317586 317588 317588 317627 317588 317610 317622 317710 317754 317878 318047 318100 318103 318520 318377 318546 318700 318898 319085 319195 319508 319619 319947 320256 320565 320433 321164 321027 321339 321642 321802 322277 322463 322998 323219 323790 323806 324395 324331 324305 324278 324239 324203 324276 324379 324746 324856 324929 325137 325368 325619 326035 326350 326683 327036 333948 333807 339657 339657 339657 339749 339863 337677 338401 340750 343781 343781 343781 343861 343959 343525 338542 341354 340155 343892 343892 343892 344040 344030 338502 341600 341131 343892 343892 343892 344067 344002 339317 343096 342417 345529 345529 345529 345724 345628 340664 344184 343504 344897 344897 344897 344923 344970 340750 338417 343421 346019 346019 346019 346027 346053 344417 338437 345039 343149 349265 349265 349265 349280 349300 341392 348530 347394 352903 352903 352903 353047 352918 344628 352343 350271 356228 356228 356228 356228 356236 351007 348515 355348 360375 360526 360526 360526 360534 358683 352645 361216 358371 365041 365041 365041 365163 365052 357209 365421 363407

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