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

Execution Outputs of cunf for Dekker/100 (P/T)

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

execution on node 40: cluster1u26.lip6.fr (runId=136941742201133_n_40)
=====================================================================
runnning cunf on Dekker-PT-100 (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 Dekker-PT-100, examination is ReachabilityDeadlock
=====================================================================

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

START 1371599813
FORMULA p_1_deadlock FALSE TECHNIQUES NET_UNFOLDING
FORMULA p_37_deadlock TRUE TECHNIQUES NET_UNFOLDING SAT_SMT
STOP 1371599886

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

bkh: PWD '/home/mcc/BenchKit/INPUTS/Dekker-PT-100'
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 4, 4096 histories
At size 4, 8192 histories
At size 4, 12288 histories
At size 4, 16384 histories
At size 5, 20480 histories
At size 5, 24576 histories
At size 5, 28672 histories
At size 6, 32768 histories
At size 6, 36864 histories
At size 6, 40960 histories
At size 6, 45056 histories
At size 6, 49152 histories
At size 6, 53248 histories
At size 6, 57344 histories
At size 6, 61440 histories
At size 6, 65536 histories
At size 6, 69632 histories
At size 6, 73728 histories
At size 6, 77824 histories
At size 6, 81920 histories
At size 6, 86016 histories
At size 6, 90112 histories
At size 6, 94208 histories
At size 6, 98304 histories
At size 6, 102400 histories
At size 6, 106496 histories
At size 6, 110592 histories
At size 6, 114688 histories
At size 6, 118784 histories
At size 6, 122880 histories
At size 6, 126976 histories
At size 6, 131072 histories
At size 6, 135168 histories
At size 6, 139264 histories
At size 6, 143360 histories
At size 6, 147456 histories
At size 6, 151552 histories
At size 6, 155648 histories
At size 6, 159744 histories
At size 6, 163840 histories
At size 6, 167936 histories
At size 6, 172032 histories
At size 6, 176128 histories
At size 6, 180224 histories
At size 6, 184320 histories
At size 6, 188416 histories
At size 6, 192512 histories
At size 6, 196608 histories
At size 6, 200704 histories
At size 6, 204800 histories
At size 6, 208896 histories
At size 6, 212992 histories
At size 6, 217088 histories
At size 6, 221184 histories
At size 6, 225280 histories
At size 6, 229376 histories
At size 6, 233472 histories
At size 6, 237568 histories
At size 6, 241664 histories
At size 6, 245760 histories
At size 6, 249856 histories
At size 6, 253952 histories
At size 6, 258048 histories
At size 6, 262144 histories
At size 6, 266240 histories
At size 6, 270336 histories
At size 6, 274432 histories
At size 6, 278528 histories
At size 6, 282624 histories
At size 6, 286720 histories
At size 6, 290816 histories
At size 6, 294912 histories
At size 6, 299008 histories
At size 6, 303104 histories
At size 6, 307200 histories
At size 6, 311296 histories
At size 6, 315392 histories
At size 6, 319488 histories
At size 6, 323584 histories
At size 6, 327680 histories
At size 6, 331776 histories
At size 6, 335872 histories
At size 6, 339968 histories
At size 6, 344064 histories
At size 6, 348160 histories
At size 6, 352256 histories
At size 6, 356352 histories
At size 6, 360448 histories
At size 6, 364544 histories
At size 6, 368640 histories
At size 6, 372736 histories
At size 6, 376832 histories
At size 6, 380928 histories
At size 6, 385024 histories
At size 6, 389120 histories
At size 6, 393216 histories
At size 6, 397312 histories
At size 6, 401408 histories
At size 6, 405504 histories
At size 6, 409600 histories
At size 6, 413696 histories
At size 6, 417792 histories
At size 6, 421888 histories
At size 6, 425984 histories
At size 6, 430080 histories
At size 6, 434176 histories
At size 6, 438272 histories
At size 6, 442368 histories
At size 6, 446464 histories
At size 6, 450560 histories
At size 6, 454656 histories
At size 6, 458752 histories
At size 6, 462848 histories
At size 6, 466944 histories
At size 6, 471040 histories
At size 6, 475136 histories
At size 6, 479232 histories
At size 6, 483328 histories
At size 6, 487424 histories
At size 6, 491520 histories
At size 6, 495616 histories
At size 6, 499712 histories
At size 6, 503808 histories
At size 6, 507904 histories
At size 6, 512000 histories
At size 6, 516096 histories
At size 6, 520192 histories
At size 6, 524288 histories
At size 6, 528384 histories
At size 6, 532480 histories
At size 6, 536576 histories
At size 6, 540672 histories
At size 6, 544768 histories
At size 6, 548864 histories
At size 6, 552960 histories
At size 6, 557056 histories
At size 6, 561152 histories
At size 6, 565248 histories
At size 6, 569344 histories
At size 6, 573440 histories
At size 6, 577536 histories
At size 6, 581632 histories
At size 6, 585728 histories
At size 6, 589824 histories
At size 6, 593920 histories
At size 6, 598016 histories
At size 6, 602112 histories
At size 6, 606208 histories
At size 6, 610304 histories
At size 6, 614400 histories
At size 6, 618496 histories
At size 6, 622592 histories
At size 6, 626688 histories
At size 6, 630784 histories
At size 6, 634880 histories
At size 6, 638976 histories
At size 6, 643072 histories
At size 6, 647168 histories
At size 6, 651264 histories
At size 6, 655360 histories
At size 6, 659456 histories
At size 6, 663552 histories
At size 6, 667648 histories
At size 6, 671744 histories
At size 6, 675840 histories
At size 6, 679936 histories
At size 6, 684032 histories
At size 6, 688128 histories
At size 6, 692224 histories
At size 6, 696320 histories
At size 6, 700416 histories
At size 6, 704512 histories
At size 6, 708608 histories
At size 6, 712704 histories
At size 6, 716800 histories
At size 6, 720896 histories
At size 6, 724992 histories
At size 6, 729088 histories
At size 6, 733184 histories
At size 6, 737280 histories
At size 6, 741376 histories
At size 6, 745472 histories
At size 6, 749568 histories
At size 6, 753664 histories
At size 6, 757760 histories
At size 6, 761856 histories
At size 6, 765952 histories
At size 6, 770048 histories
At size 6, 774144 histories
At size 6, 778240 histories
At size 6, 782336 histories
At size 6, 786432 histories
At size 6, 790528 histories
At size 6, 794624 histories
At size 6, 798720 histories
At size 6, 802816 histories
At size 6, 806912 histories
At size 6, 811008 histories
At size 6, 815104 histories
At size 6, 819200 histories
At size 6, 823296 histories
At size 6, 827392 histories
At size 6, 831488 histories
At size 6, 835584 histories
At size 6, 839680 histories
At size 6, 843776 histories
At size 6, 847872 histories
At size 6, 851968 histories
At size 6, 856064 histories
At size 6, 860160 histories
At size 6, 864256 histories
At size 6, 868352 histories
At size 6, 872448 histories
At size 6, 876544 histories
At size 6, 880640 histories
At size 6, 884736 histories
At size 6, 888832 histories
At size 6, 892928 histories
At size 6, 897024 histories
At size 6, 901120 histories
At size 6, 905216 histories
At size 6, 909312 histories
At size 6, 913408 histories
At size 6, 917504 histories
At size 6, 921600 histories
At size 6, 925696 histories
At size 6, 929792 histories
At size 6, 933888 histories
At size 6, 937984 histories
At size 6, 942080 histories
At size 6, 946176 histories
At size 6, 950272 histories
At size 6, 954368 histories
At size 6, 958464 histories
At size 6, 962560 histories
At size 6, 966656 histories
At size 6, 970752 histories
At size 6, 974848 histories
At size 6, 978944 histories
At size 6, 983040 histories
At size 6, 987136 histories
At size 6, 991232 histories
At size 6, 995328 histories
At size 6, 999424 histories
time 55.959
mem 1812
hist 1000200
events 10200
cond 20500
gen 20300
read 9900
comp 0
r(h) 1.98
s(h) 0.01
co(r) 686.46
rco(r) 0.66
mrk(h) 200.00
pre(e) 1.99
ctx(e) 1.94
pst(e) 1.99
cutoffs 990100
ewhite 200
egray 0
eblack 10000
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: 1.2: causal
debug: 1.3: sym
debug: 1.3: asym
debug: 4.5: dis
debug: 5.1: write cnf
debug: 6.4: solve
debug: 6.6: parse result
debug: 6.6: exit
deadlock: buff='answer : NO , the net is deadlock-free'

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