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


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

BK_START 1401988552818

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: 67 NrTr: 76)

net check time: 0m0sec

place and transition orderings generation:0m0sec

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

1461 2579 4882 5723 7829 11174 13730 14337 16309 16456 25493 24552 26281 26966 27096 28323 28617 28438 27175 26041 31638 32069 31942 33665 44486 44475 47061 62460 62359 65832 66356 76050 121156 119882 123068 123368 122296 121906 121844 121365 118493 124336 125328 126116 128304 129147 132260 133551 170782 172671 181791 190576 191038 195187 195802 195553 195415 195265 215777 216329 225409 228144 229318 230265 228636 228367 225459 229025 226996 226251 297156 302970 302224 318414 317028 322269 319736 316146 313900 313108 329779 329971 330147 331660 332492 337744 338605 352621 353030 352967 351645 352492 371436 372921 378229 380338 380530 379846 382658 382424 380045 379689 379262 426727 450789 452027 497545 492866 490631 488771 486865 491777 532504 531995 530828 530418 529605 536884 536875 538417 536404 534861 569101 572519 574011 576723 576782 576143 577666 577405 577851 577839 577932 589576 593286 593541 592849 589877 796766 798182 795937 793585 790473 822886 823449 830843 831981 976334 972734 982859 979328 977945 975548 973039 984879 985175 987779 1038709 1040059 1044136 1043750 1044641 1043671 1041857 1040531 1042763 1038487 1037006 1033411 1021522 1016022 1013815 980794 972772 971701 965338 944760 939807 935873 935192 934503 933901 932454 931291 930903 929494 927749 988222 1004631 1034044 1032662 1030833 1032972 1029070 1056061 1050851 1029977 1031112 1183645 1223550 1230932 1229216 1228704 1230270 1230738 1231334 1230243 1230099 1228539 1227873 1219046 1216195 1234844 1235971 1241986 1241196 1241390 1240805 1235479 1235414 1237082 1235829 1235409 1228658 1224501 1222414 1222436 1222508 1222435 1221604 1220853 1218152 1216857 1563036 1562639 1558216 1576948 1673420 1718380 1724349 1757874 1760566 1761353 1758886 1756516 1747918 1740236 1783307 1783607 1787687 1788346 1798810

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