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


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

BK_START 1401988378491

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: 1189 NrTr: 2350)

net check time: 0m0sec

place and transition orderings generation:0m10sec

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

1193 2197 3128 4894 4898 8302 14834 16508 16847 17671 18010 17589 18203 18203 18057 18396 17965 18557 18140 18385 18724 18550 18889 18446 19007 19007 18801 19140 18706 19250 18806 18998 19337 18924 19448 19034 19207 19546 19275 19614 19195 19686 19248 19391 19730 19291 20300 20309 20681 20886 20907 21599 21627 22002 22197 22231 23046 23089 23530 23780 23830 24479 24479 24992 25178 25247 25702 25883 26453 26656 26804 27339 27519 27672 28437 28598 29172 29408 29578 30431 30606 31126 31393 31574 32344 32344 33131 33310 33505 34058 34228 35040 35250 35460 36057 36220 36436 37248 37248 38070 38268 38502 39142 39452 40309 40508 40756 41378 41582 41837 42677 42939 43549 43758 44026 44662 44805 45724 45911 46190 46840 47008 47297 48301 48596 49250 49433 49733 50577 50577 51598 51885 52201 52888 53047 54082 54398 54729 55457 55619 55958 56926 57271 58002 58254 58606 59530 59530 60624 60768 61133 61911 62222 62593 63629 64008 64770 64920 65306 66447 66841 67613 67798 68197 69027 69352 70552 70810 71225 72061 72353 73602 73908 74335 75182 75476 76745 77000 77441 78290 78445 78894 79896 79896 81165 81378 81840 82701 82861 83332 84352 84828 85694 85968 86450 87330 87564 88895 89051 89548 90393 90636 91141 92365 92875 93805 94090 94609 95786 96311 97180 97403 97934 160996 161518 161538 161554 161576 161731 161734 161738 161741 161744 161747 161750 161752 161755 161758 161760 161763 161766 161768 161770 161773 161775 161777 161780 161782 161784 161786 161789 161791 161793 161795 161801 161810 161821 161828 161835 161841 161847 161854 161867 161950 161958 161989 162410 162416 162422 162429 162435 162442 162446 162449 162884 178511 180179 180183 208357 260982 262439 262439 262855 263194 263040 263379 262970 263570 263139 263729 263312 263549 263888 263712 264051 263710 264169 263751

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