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


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

BK_START 1401988618510

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

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

2305 4400 5783 6797 7623 8553 10522 11626 12107 15683 15953 20281 22322 22650 23782 24190 24132 24333 24778 24936 29167 31142 32748 34686 36755 37737 38354 55917 60057 60307 60636 60535 59580 59651 80832 92974 93939 93895 123046 139267 136831 135184 134910 138381 138750 141668 142107 142012 189681 212392 213226 207496 204787 205841 205535 226179 226264 226103 230554 230603 231100 231145 324801 321381 336277 374485 371977 360986 364426 373244 373543 369101 362585 378425 376535 383863 383429 394963 394205 393869 394927 395084 393087 392767 392225 394623 395171 395310 396602 547118 558030 554007 570186 586887 628611 631793 622797 620062 618419 617369 616407 612202 611004 628711 631673 631512 631309 635746 636741 637112 637429 639105 647790 647590 646104 673592 672289 670335 682342 685711 689340 690559 692515 692523 692691 717590 724500 727427 724486 724296 721895 722200 722285 721153 721089 721063 723505 724561 724128 926921 952707 952492 943582 974097 1002302 1001938 1005287 1005305 1005681 1002126 998913 997450 1022679 1024009 1024097 1025359 1025749 1025182 1025460 1026107 1030273 1030270 1073843 1075603 1088950 1086683 1085717 1089987 1090244 1089681 1091219 1091366 1090286 1090236 1089437 1104246 1105129 1108318 1110369 1112937 1114710 1128085 1126781 1127489 1127434 1129479 1130444 1130579 1137370 1137576 1138945 1142600 1143779 1145968 1146995 1172253 1172559 1179801 1180832 1181303 1180629 1179856 1487495 1596625 1580651 1584559 1580586 1579295 1575528 1571769 1566270 1747174 1761909

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