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


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

BK_START 1401988587387

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

net check time: 0m0sec

place and transition orderings generation:0m0sec

init dd package: 0m0sec


before gc: list nodes free: 231745

after gc: idd nodes used:1454684, unused:14545316; list nodes free:70758443

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

590 1628 2101 3671 4646 8256 8340 9033 9246 9797 10520 10645 10687 12454 11843 13795 14196 19420 21412 21001 22258 21894 22029 24254 25112 26212 30948 29968 33860 32833 34586 36036 36772 37256 37824 56590 57815 59311 58837 58954 114435 117015 116108 114092 110955 99161 113756 116098 147980 152234 151278 149560 147291 149454 149032 147063 197737 220786 219527 228103 228845 228679 227775 224126 227478 225639 222614 292017 333537 334895 337142 340505 367173 372072 369164 362255 345312 329264 322271 321825 311148 294595 292741 290025 323924 329572 328262 335648 336563 325345 397449 398430 398806 395216 417090 417126 416633 437264 438597 437134 434951 439433 434494 449224 448825 443189 440911 441486 438407 434883 533531 534281 535667 535711 531864 531983 544649 544040 546338 549149 548422 553759 552485 551530 564002 564741 566297 564332 562959 611324 631148 639225 639800 625584 613901 598443 604748 602199 600507 606102 606192 603286 720464 719636 719751 720692 743764 744598 743727 745316 770639 771471 768128 786701 789693 790470 785611 787285 791342 747134 755950 761089 758269 756161 762662 773947 769357 819215 815587 826093 824478 824316 850245 880823 883634 877156 877499 883572 915368 912669 912187 913415 914124 909256 908109 904367 902692 897892 895637 1247554 1257408 1264793 1263736 1280917 1288515 1288724 1272406 1267910 1269706 1265328 1257571 1255601 1238778 1239616 1239139 1235223 1234692 1393256 1397911 1438952 1454223 1456406 1461350 1460999 1459452 1462124 1464818 1459449 1459347 1462027 1462667 1463046 1464124 1462599 1477933 1477681 1484865 1484186 1482945 1480944 1480175 1477069 1483721 1482965 1527769 1517879 1517267 1518732 1518461 1513993 1530114 1532050 1534363 1533315 1532489 1533751 1533469 1534556 1536185 1541493 1542044 1541558 1547257 1545367 1543242 1550905 1551245 1551694 1552272 1552870 1526733 1526397 1526630 1525174 1525289 1524518 1527847 1527661 1527872 1531451 1531584 1530827 1531367 1532007 1537325 1536202 1535857 1536748 1536332 1537579 1532213 1531310 1524566 1524067 1523012 1522730 1555114 1554606 1555822 1558016 1558047 1557835 1559005 1557797 1575283 1576359 1578709 1578829 1576788 1577533 1575955 1577446 1577977 1578450 1615408 1617841 1615766 1618556 1613184 1613715 1614831 1607650 1605202 1605202 1605514 1603543 1603517 1603379 1603564 1605528 1607610 1607435 1575022 1577044 1577215 1578871 1582275 1581339 1589244 1600257 1597750 1597349 1631495 1630446 1624182 1622261 1623392 1622086 1622970 1627873 1630005 1628313 1628913 1628183

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