fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
cunf: ReachabilityDeadlock on CSRepetitions/03 (P/T)
Last Updated
Apr. 26, 2013

Introduction

This page shows the outputs produced by the execution of cunf on CSRepetitions/03 (P/T). We provide:

About the Execution

Execution Summary
Memory (MB) CPU (s) End
2870.18 597.91 normal

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

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.

export BK_INPUT=CSRepetitions-PT-03
export BK_EXAMINATION=ReachabilityDeadlock
export BK_TOOL=cunf
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1713
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/CSRepetitions-PT-03
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool cunf:'
echo ' Test is CSRepetitions-PT-03, examination is ReachabilityDeadlock'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of cunf for CSRepetitions/03 (P/T)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.


execution on node 21: quadhexa-2.u-paris10.fr (runId=136933856300428_n_21)
=====================================================================
runnning cunf on CSRepetitions-PT-03 (ReachabilityDeadlock)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool cunf:
Test is CSRepetitions-PT-03, examination is ReachabilityDeadlock
=====================================================================

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

START 1371565805
FORMULA p_1_deadlock FALSE TECHNIQUES NET_UNFOLDING
CANNOT_COMPUTE
STOP 1371566448

--------------------
content from stderr:

bkh: PWD '/home/mcc/BenchKit/INPUTS/CSRepetitions-PT-03'
bkh: BK_EXAMINATION 'ReachabilityDeadlock'
bkh: iscolored FALSE
bkh: translating pnml to pep...
bkh: unfolding... cross the fingers to stay in memory!
bkh: yeah!
At size 9, 4096 histories
At size 10, 8192 histories
At size 11, 12288 histories
At size 12, 16384 histories
At size 12, 20480 histories
At size 12, 24576 histories
At size 12, 28672 histories
At size 13, 32768 histories
At size 13, 36864 histories
At size 13, 40960 histories
At size 14, 45056 histories
At size 14, 49152 histories
At size 15, 53248 histories
At size 15, 57344 histories
At size 15, 61440 histories
At size 15, 65536 histories
At size 15, 69632 histories
At size 16, 73728 histories
At size 16, 77824 histories
At size 16, 81920 histories
At size 16, 86016 histories
At size 16, 90112 histories
At size 17, 94208 histories
At size 18, 98304 histories
At size 18, 102400 histories
At size 18, 106496 histories
At size 18, 110592 histories
At size 19, 114688 histories
At size 19, 118784 histories
At size 19, 122880 histories
At size 21, 126976 histories
At size 22, 131072 histories
time 71.568
mem 99
hist 131226
events 118633
cond 99350
gen 72667
read 43886
comp 0
r(h) 2.08
s(h) 0.16
co(r) 38.97
rco(r) 0.46
mrk(h) 12.67
pre(e) 1.21
ctx(e) 0.39
pst(e) 0.84
cutoffs 31348
ewhite 91653
egray 3669
eblack 23311
net /tmp/m.ll_net
main: Formula 0
deadlock: p.id().c_str()='p_1_deadlock'
inv_dead: p.id().c_str()='p_1_deadlock'
main: Formula 1
deadlock: p.id().c_str()='p_47_deadlock'
deadlock: Running cna: 'cna-mcc u.cuf /tmp/cna.out --deadlock --reduce 4-tree stb bin sccred'
debug: 0.0: load cuf
debug: 13.8: causal
debug: 19.4: sym
debug: 20.7: asym
Traceback (most recent call last):
File "/home/mcc/BenchKit/bin//cna-mcc", line 13, in
sys.stderr ('cna: error: %s\n' % str (e))
MemoryError
deadlock: buff=''

--------------------
content from /tmp/BenchKit_head_log_file.1713: