fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r06ks-qhx2-140066506502211
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-1667
Executing tool marcie
Input is SurpriseEcho-PT-d03r05, examination is StateSpace
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r06ks-qhx2-140066506502211
=====================================================================


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

BK_START 1400687413356

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: 1445 NrTr: 1190)

net check time: 0m0sec

place and transition orderings generation:0m3sec

init dd package: 0m6sec


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

2795 5877 8119 15945 16834 41054 43545 46871 55685 57654 58589 76875 79971 80587 111037 120260 119099 127434 126331 137258 140203 139675 153186 154845 187650 189563 198098 192737 189767 205784 210524 213333 212642 229182 231457 244972 248411 239817 237093 243998 256505 258100 279477 275528 282772 281030 256023 254410 267144 273199 270093 270337 268967 284915 279524 276883 297099 287744 283809 289472 290803 289286 289942 303551 304333 316438 315577 297065 300161 298605 315632 314978 314088 312731 314246 329750 330409 329991 340368 341837 340447 339213 339585 346241 347389 346383 342915 343472 343106 342246 362580 354624 354723 350872 351186 352388 357504 357466 357026 363879 363109 361909 352225 357493 355717 353406 353018 350211 350915 350594 349307 353124 353954 354341 363513 360606 361451 366331 376180 372412 371710 383114 376880 376216 375494 367640 368644 365873 364729 374462 370660 371676 366971 365502 379204 370090 371141 366972 373848 366766 364792 359384 359211 359056 355846 354234 369518 370342 370619 374269 373020 373156 373290 391010 388729 388351 386700 408967 402522 394220 406642 396034 388217 394338 386832 398242 399211 402075 400236 397468 396128 395794 397054 397533 396732 396703 397214 396967 408430 410766 405407 405076 406529 416984 416860 425002 424395 412341 408179 409358 404413 402074 412192 412007 407262 423493 415608 414062 418416 412884 410986 408243 405967 754758

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="SurpriseEcho-PT-d03r05"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="marcie"
export BK_RESULT_DIR="/home/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/SurpriseEcho-PT-d03r05.tgz
mv SurpriseEcho-PT-d03r05 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1667"
echo " Executing tool marcie"
echo " Input is SurpriseEcho-PT-d03r05, examination is StateSpace"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r06ks-qhx2-140066506502211"
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 ;