Introduction

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=Railroad-PT-010
export BK_EXAMINATION=ReachabilityDeadlock
export BK_TOOL=cunf
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1721
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Railroad-PT-010
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool cunf:'
echo ' Test is Railroad-PT-010, examination is ReachabilityDeadlock'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of cunf for Railroad/010 (P/T)

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

execution on node 38: cluster1u40.lip6.fr (runId=136975220401131_n_38)
=====================================================================
runnning cunf on Railroad-PT-010 (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 Railroad-PT-010, examination is ReachabilityDeadlock
=====================================================================

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

START 1371571367
FORMULA p_1_deadlock FALSE TECHNIQUES NET_UNFOLDING
FORMULA p_37_deadlock TRUE TECHNIQUES NET_UNFOLDING SAT_SMT
STOP 1371571710

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

bkh: PWD '/home/mcc/BenchKit/INPUTS/Railroad-PT-010'
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 12, 4096 histories
At size 13, 8192 histories
At size 13, 12288 histories
At size 14, 16384 histories
At size 14, 20480 histories
At size 15, 24576 histories
At size 15, 28672 histories
At size 15, 32768 histories
At size 15, 36864 histories
At size 16, 40960 histories
At size 16, 45056 histories
At size 16, 49152 histories
At size 16, 53248 histories
At size 16, 57344 histories
At size 16, 61440 histories
At size 17, 65536 histories
At size 17, 69632 histories
At size 17, 73728 histories
At size 17, 77824 histories
At size 17, 81920 histories
At size 17, 86016 histories
At size 17, 90112 histories
At size 18, 94208 histories
At size 18, 98304 histories
At size 18, 102400 histories
At size 18, 106496 histories
At size 18, 110592 histories
At size 18, 114688 histories
At size 18, 118784 histories
At size 18, 122880 histories
At size 18, 126976 histories
At size 19, 131072 histories
At size 19, 135168 histories
At size 19, 139264 histories
At size 19, 143360 histories
At size 19, 147456 histories
At size 19, 151552 histories
At size 19, 155648 histories
At size 19, 159744 histories
At size 19, 163840 histories
At size 19, 167936 histories
At size 19, 172032 histories
At size 20, 176128 histories
At size 20, 180224 histories
At size 20, 184320 histories
At size 20, 188416 histories
At size 20, 192512 histories
At size 20, 196608 histories
At size 20, 200704 histories
At size 20, 204800 histories
At size 20, 208896 histories
At size 20, 212992 histories
At size 20, 217088 histories
At size 20, 221184 histories
At size 21, 225280 histories
At size 21, 229376 histories
At size 21, 233472 histories
At size 21, 237568 histories
At size 21, 241664 histories
At size 21, 245760 histories
At size 21, 249856 histories
At size 21, 253952 histories
At size 21, 258048 histories
At size 21, 262144 histories
At size 21, 266240 histories
At size 21, 270336 histories
At size 21, 274432 histories
At size 21, 278528 histories
At size 22, 282624 histories
At size 22, 286720 histories
At size 22, 290816 histories
At size 22, 294912 histories
At size 22, 299008 histories
At size 22, 303104 histories
At size 22, 307200 histories
At size 22, 311296 histories
At size 22, 315392 histories
At size 22, 319488 histories
At size 22, 323584 histories
At size 22, 327680 histories
At size 22, 331776 histories
At size 23, 335872 histories
At size 23, 339968 histories
At size 23, 344064 histories
At size 23, 348160 histories
At size 23, 352256 histories
At size 23, 356352 histories
At size 23, 360448 histories
At size 23, 364544 histories
At size 23, 368640 histories
At size 23, 372736 histories
At size 23, 376832 histories
At size 23, 380928 histories
At size 24, 385024 histories
At size 24, 389120 histories
At size 24, 393216 histories
At size 24, 397312 histories
At size 24, 401408 histories
At size 24, 405504 histories
At size 24, 409600 histories
At size 24, 413696 histories
At size 24, 417792 histories
At size 24, 421888 histories
At size 24, 425984 histories
At size 25, 430080 histories
At size 25, 434176 histories
At size 25, 438272 histories
At size 25, 442368 histories
At size 25, 446464 histories
At size 25, 450560 histories
At size 25, 454656 histories
At size 25, 458752 histories
At size 25, 462848 histories
At size 26, 466944 histories
At size 26, 471040 histories
At size 26, 475136 histories
At size 26, 479232 histories
At size 26, 483328 histories
At size 26, 487424 histories
At size 26, 491520 histories
At size 27, 495616 histories
At size 27, 499712 histories
At size 27, 503808 histories
At size 27, 507904 histories
At size 27, 512000 histories
At size 28, 516096 histories
At size 28, 520192 histories
At size 28, 524288 histories
At size 28, 528384 histories
At size 29, 532480 histories
At size 29, 536576 histories
At size 30, 540672 histories
At size 31, 544768 histories
time 313.499
mem 390
hist 548502
events 48643
cond 97351
gen 300278
read 59000
comp 17363
r(h) 5.99
s(h) 0.42
co(r) 64.75
rco(r) 0.64
mrk(h) 21.50
pre(e) 2.05
ctx(e) 0.66
pst(e) 2.00
cutoffs 398387
ewhite 6805
egray 8754
eblack 33084
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_37_deadlock'
deadlock: Running cna: 'cna-mcc u.cuf /tmp/cna.out --deadlock --reduce 4-tree stb bin sccred'
debug: 0.0: load cuf
debug: 5.7: causal
debug: 6.5: sym
debug: 6.7: asym
debug: 8.5: dis
debug: 10.0: write cnf
debug: 10.1: solve
debug: 10.6: parse result
debug: 10.7: exit
deadlock: buff='answer : NO , the net is deadlock-free'

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