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


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

BK_START 1401988648593

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: 74 NrTr: 92)

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


before gc: list nodes free: 1972805

after gc: idd nodes used:978694, unused:15021306; list nodes free:75054332

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

1144 1780 2232 3833 4184 7848 9292 9662 13118 13122 13704 14584 18857 22638 24555 27303 30334 40806 53951 56884 58528 59385 59311 60096 58601 56968 63905 66454 68557 69523 69558 69478 69228 68918 75495 74753 103789 124811 126298 126820 126983 126476 122410 122337 118879 110411 110555 110411 110633 110833 111280 110435 110724 110837 111011 111250 111842 111937 176296 213362 217574 213614 215859 204855 190115 188775 202178 204305 224612 222913 221731 214416 212761 217557 217368 217192 216302 216381 217901 217475 222549 226861 228094 226022 223730 223996 222017 306585 331958 376199 390951 412623 415125 416568 408323 404323 375621 374390 363753 574257 675194 675890 669009 628343 627433 617722 594690 587334 569855 554745 530159 527684 525293 568025 569679 599227 601167 597585 641998 644027 638672 707218 707199 717199 718583 718897 719632 720553 722743 722218 723403 748042 751766 748671 746875 747309 747808 745321 752146 750084 751310 751443 751256 752442 753242 753127 755151 754520 720855 721275 726335 729311 733757 735392 738476 739461 749661 760242 762475 759571 763060 762132 778193 780307 780823 780268 776418 868254 876347 886643 921646 923045 931284 926517 930569 932688 884728 887119 886657 900522 893577 890321 892981 919470 926790 924254 919779 916499 918989 918879 918953 913495 913278 913533 912050 911798 939897 941483 948395 970148 971277 980107 978149 977164 976335 979931 983801 969498 967905 985801 984661 985180 985620 983772 987412 987944 989401 989856 976581 974877 973914 1101869 1100485 1093335 1103702 1126750 1130637 1129177 1134928 1150693 1150038 1140327 1137447 1140803 1131533 1130216 1129727 1210866 1252589 1265059 1264443 1265386 1262335 1269466 1269170 1272260 1274072 1279351 1280231 1280581 1282246 1298671 1302690 1302583 1332789 1337177 1335340 1357907 1361430 1357713 1356151 1355189 1370765 1385760 1385585 1665986 1745853

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