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

Execution Outputs of marcie for NeoElection/6 (P/T)

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

execution on node 33: cluster1u35.lip6.fr (runId=136959876901594_n_33)
=====================================================================
runnning marcie on NeoElection-PT-6 (CTLMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is NeoElection-PT-6, examination is CTLMix
=====================================================================

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

START 1369655699

Marcie rev. 1103M (build: rohrch on 2013-02-17)
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 --mcc-file=CTLMix.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 4830 NrTr: 8435)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369655702

--------------------
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

mcc/mcc_parse.cc:759: Exception: parse error ctl p_1880_mix_eq_x: E F (!((|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_0_5)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_5_1)|+|marking(sendAnnPs__broadcasting_6_6)|+|marking(sendAnnPs__broadcasting_0_2)|+|marking(sendAnnPs__broadcasting_0_4)|+|marking(sendAnnPs__broadcasting_1_3)|+|marking(sendAnnPs__broadcasting_5_6)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|)=(|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_6_3)|)) xor X ((|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_6_3)|)=(|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_0_5)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_5_1)|+|marking(sendAnnPs__broadcasting_6_6)|+|marking(sendAnnPs__broadcasting_0_2)|+|marking(sendAnnPs__broadcasting_0_4)|+|marking(sendAnnPs__broadcasting_1_3)|+|marking(sendAnnPs__broadcasting_5_6)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|)))
ctl p_1881_mix_full_and: A G (((|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_6_3)|)>(|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_0_5)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_5_1)|+|marking(sendAnnPs__broadcasting_6_6)|+|marking(sendAnnPs__broadcasting_0_2)|+|marking(sendAnnPs__broadcasting_0_4)|+|marking(sendAnnPs__broadcasting_1_3)|+|marking(sendAnnPs__broadcasting_5_6)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|)) & (startNeg__send_77? | startNeg__send_160? | startNeg__send_186? | startNeg__send_19? | startNeg__send_269? | startNeg__send_112? | startNeg__send_287? | startNeg__send_238? | startNeg__send_67? | startNeg__send_224? | startNeg__send_21? | startNeg__send_11? | startNeg__send_278? | startNeg__send_61? | startNeg__send_214? | startNeg__send_35? | startNeg__send_245? | startNeg__send_58? | startNeg__send_145? | startNeg__send_220? | startNeg__send_211? | startNeg__send_227? | startNeg__send_102? | startNeg__send_153? | startNeg__send_198? | startNeg__send_97? | startNeg__send_106? | startNeg__send_16? | startNeg__send_151? | startNeg__send_13? | startNeg__send_242? | startNeg__send_116? | startNeg__send_96? | startNeg__send_53? | startNeg__send_233? | startNeg__send_22? | startNeg__send_202? | startNeg__send_219? | startNeg__send_236? | startNeg__send_101? | startNeg__send_111? | startNeg__send_49? | startNeg__send_154? | startNeg__send_284? | startNeg__send_135? | startNeg__send_105? | startNeg__send_50? | startNeg__send_169? | startNeg__send_281? | startNeg__send_270? | startNeg__send_232? | startNeg__send_70? | startNeg__send_218? | startNeg__send_234? | startNeg__send_255? | startNeg__send_57? | startNeg__send_187? | startNeg__send_103? | startNeg__send_285? | startNeg__send_45? | startNeg__send_199? | startNeg__send_74? | startNeg__send_99? | startNeg__send_177? | startNeg__send_17? | startNeg__send_51? | startNeg__send_256? | startNeg__send_273? | startNeg__send_28? | startNeg__send_193? | startNeg__send_75? | startNeg__send_147? | startNeg__send_31? | startNeg__send_229? | startNeg__send_91? | startNeg__send_137? | startNeg__send_259? | startNeg__send_268? | startNeg__send_55? | startNeg__send_213? | startNeg__send_143? | startNeg__send_8? | startNeg__send_279? | startNeg__send_117? | startNeg__send_133? | startNeg__send_88? | startNeg__send_72? | startNeg__send_264? | startNeg__send_203? | startNeg__send_274? | startNeg__send_174? | startNeg__send_196? | startNeg__send_190? | startNeg__send_134? | startNeg__send_191? | startNeg__send_98? | startNeg__send_194? | startNeg__send_261? | startNeg__send_258? | startNeg__send_46? | startNeg__send_266? | startNeg__send_59? | startNeg__send_48? | startNeg__send_68? | startNeg__send_212? | startNeg__send_71? | startNeg__send_3? | startNeg__send_217? | startNeg__send_144? | startNeg__send_185? | startNeg__send_272? | startNeg__send_85? | startNeg__send_239? | startNeg__send_142? | startNeg__send_148? | startNeg__send_254? | startNeg__send_183? | startNeg__send_155? | startNeg__send_18? | startNeg__send_237? | startNeg__send_127? | startNeg__send_275? | startNeg__send_26? | startNeg__send_87? | startNeg__send_12? | startNeg__send_170? | startNeg__send_172? | startNeg__send_182? | startNeg__send_257? | startNeg__send_171? | startNeg__send_226? | startNeg__send_241? | startNeg__send_109? | startNeg__send_215? | startNeg__send_23? | startNeg__send_231? | startNeg__send_243? | startNeg__send_1? | startNeg__send_265? | startNeg__send_192? | startNeg__send_271? | startNeg__send_161? | startNeg__send_108? | startNeg__send_150? | startNeg__send_63? | startNeg__send_90? | startNeg__send_159? | startNeg__send_197? | startNeg__send_44? | startNeg__send_110? | startNeg__send_175? | startNeg__send_188? | startNeg__send_276? | startNeg__send_73? | startNeg__send_30? | startNeg__send_225? | startNeg__send_176? | startNeg__send_262? | startNeg__send_156? | startNeg__send_152? | startNeg__send_141? | startNeg__send_263? | startNeg__send_240? | startNeg__send_60? | startNeg__send_132? | startNeg__send_114? | startNeg__send_146? | startNeg__send_2? | startNeg__send_223? | startNeg__send_139? | startNeg__send_6? | startNeg__send_92? | startNeg__send_118? | startNeg__send_131? | startNeg__send_65? | startNeg__send_7? | startNeg__send_62? | startNeg__send_104? | startNeg__send_181? | startNeg__send_140? | startNeg__send_5? | startNeg__send_32? | startNeg__send_244? | startNeg__send_130? | startNeg__send_27? | startNeg__send_95? | startNeg__send_64? | startNeg__send_221? | startNeg__send_119? | startNeg__send_14? | startNeg__send_277? | startNeg__send_24? | startNeg__send_253? | startNeg__send_228? | startNeg__send_33? | startNeg__send_93? | startNeg__send_129? | startNeg__send_43? | startNeg__send_184? | startNeg__send_10? | startNeg__send_138? | startNeg__send_235? | startNeg__send_157? | startNeg__send_76? | startNeg__send_29? | startNeg__send_158? | startNeg__send_280? | startNeg__send_86? | startNeg__send_94? | startNeg__send_69? | startNeg__send_136? | startNeg__send_200? | startNeg__send_260? | startNeg__send_216? | startNeg__send_115? | startNeg__send_47? | startNeg__send_149? | startNeg__send_100? | startNeg__send_230? | startNeg__send_25? | startNeg__send_282? | startNeg__send_179? | startNeg__send_180? | startNeg__send_201? | startNeg__send_222? | startNeg__send_54? | startNeg__send_128? | startNeg__send_52? | startNeg__send_20? | startNeg__send_189? | startNeg__send_34? | startNeg__send_15? | startNeg__send_195? | startNeg__send_267? | startNeg__send_56? | startNeg__send_4? | startNeg__send_173? | startNeg__send_89? | startNeg__send_9? | startNeg__send_283? | startNeg__send_286? | startNeg__send_107? | startNeg__send_178? | startNeg__send_66? | startNeg__send_113?))
ctl p_1882_mix_full_or: E G (((|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_6_3)|)>(|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_0_5)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_5_1)|+|marking(sendAnnPs__broadcasting_6_6)|+|marking(sendAnnPs__broadcasting_0_2)|+|marking(sendAnnPs__broadcasting_0_4)|+|marking(sendAnnPs__broadcasting_1_3)|+|marking(sendAnnPs__broadcasting_5_6)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|)) | (startNeg__send_77? | startNeg__send_160? | startNeg__send_186? | startNeg__send_19? | startNeg__send_269? | startNeg__send_112? | startNeg__send_287? | startNeg__send_238? | startNeg__send_67? | startNeg__send_224? | startNeg__send_21? | startNeg__send_11? | startNeg__send_278? | startNeg__send_61? | startNeg__send_214? | startNeg__send_35? | startNeg__send_245? | startNeg__send_58? | startNeg__send_145? | startNeg__send_220? | startNeg__send_211? | startNeg__send_227? | startNeg__send_102? | startNeg__send_153? | startNeg__send_198? | startNeg__send_97? | startNeg__send_106? | startNeg__send_16? | startNeg__send_151? | startNeg__send_13? | startNeg__send_242? | startNeg__send_116? | startNeg__send_96? | startNeg__send_53? | startNeg__send_233? | startNeg__send_22? | startNeg__send_202? | startNeg__send_219? | startNeg__send_236? | startNeg__send_101? | startNeg__send_111? | startNeg__send_49? | startNeg__send_154? | startNeg__send_284? | startNeg__send_135? | startNeg__send_105? | startNeg__send_50? | startNeg__send_169? | startNeg__send_281? | startNeg__send_270? | startNeg__send_232? | startNeg__send_70? | startNeg__send_218? | startNeg__send_234? | startNeg__send_255? | startNeg__send_57? | startNeg__send_187? | startNeg__send_103? | startNeg__send_285? | startNeg__send_45? | startNeg__send_199? | startNeg__send_74? | startNeg__send_99? | startNeg__send_177? | startNeg__send_17? | startNeg__send_51? | startNeg__send_256? | startNeg__send_273? | startNeg__send_28? | startNeg__send_193? | startNeg__send_75? | startNeg__send_147? | startNeg__send_31? | startNeg__send_229? | startNeg__send_91? | startNeg__send_137? | startNeg__send_259? | startNeg__send_268? | startNeg__send_55? | startNeg__send_213? | startNeg__send_143? | startNeg__send_8? | startNeg__send_279? | startNeg__send_117? | startNeg__send_133? | startNeg__send_88? | startNeg__send_72? | startNeg__send_264? | startNeg__send_203? | startNeg__send_274? | startNeg__send_174? | startNeg__send_196? | startNeg__send_190? | startNeg__send_134? | startNeg__send_191? | startNeg__send_98? | startNeg__send_194? | startNeg__send_261? | startNeg__send_258? | startNeg__send_46? | startNeg__send_266? | startNeg__send_59? | startNeg__send_48? | startNeg__send_68? | startNeg__send_212? | startNeg__send_71? | startNeg__send_3? | startNeg__send_217? | startNeg__send_144? | startNeg__send_185? | startNeg__send_272? | startNeg__send_85? | startNeg__send_239? | startNeg__send_142? | startNeg__send_148? | startNeg__send_254? | startNeg__send_183? | startNeg__send_155? | startNeg__send_18? | startNeg__send_237? | startNeg__send_127? | startNeg__send_275? | startNeg__send_26? | startNeg__send_87? | startNeg__send_12? | startNeg__send_170? | startNeg__send_172? | startNeg__send_182? | startNeg__send_257? | startNeg__send_171? | startNeg__send_226? | startNeg__send_241? | startNeg__send_109? | startNeg__send_215? | startNeg__send_23? | startNeg__send_231? | startNeg__send_243? | startNeg__send_1? | startNeg__send_265? | startNeg__send_192? | startNeg__send_271? | startNeg__send_161? | startNeg__send_108? | startNeg__send_150? | startNeg__send_63? | startNeg__send_90? | startNeg__send_159? | startNeg__send_197? | startNeg__send_44? | startNeg__send_110? | startNeg__send_175? | startNeg__send_188? | startNeg__send_276? | startNeg__send_73? | startNeg__send_30? | startNeg__send_225? | startNeg__send_176? | startNeg__send_262? | startNeg__send_156? | startNeg__send_152? | startNeg__send_141? | startNeg__send_263? | startNeg__send_240? | startNeg__send_60? | startNeg__send_132? | startNeg__send_114? | startNeg__send_146? | startNeg__send_2? | startNeg__send_223? | startNeg__send_139? | startNeg__send_6? | startNeg__send_92? | startNeg__send_118? | startNeg__send_131? | startNeg__send_65? | startNeg__send_7? | startNeg__send_62? | startNeg__send_104? | startNeg__send_181? | startNeg__send_140? | startNeg__send_5? | startNeg__send_32? | startNeg__send_244? | startNeg__send_130? | startNeg__send_27? | startNeg__send_95? | startNeg__send_64? | startNeg__send_221? | startNeg__send_119? | startNeg__send_14? | startNeg__send_277? | startNeg__send_24? | startNeg__send_253? | startNeg__send_228? | startNeg__send_33? | startNeg__send_93? | startNeg__send_129? | startNeg__send_43? | startNeg__send_184? | startNeg__send_10? | startNeg__send_138? | startNeg__send_235? | startNeg__send_157? | startNeg__send_76? | startNeg__send_29? | startNeg__send_158? | startNeg__send_280? | startNeg__send_86? | startNeg__send_94? | startNeg__send_69? | startNeg__send_136? | startNeg__send_200? | startNeg__send_260? | startNeg__send_216? | startNeg__send_115? | startNeg__send_47? | startNeg__send_149? | startNeg__send_100? | startNeg__send_230? | startNeg__send_25? | startNeg__send_282? | startNeg__send_179? | startNeg__send_180? | startNeg__send_201? | startNeg__send_222? | startNeg__send_54? | startNeg__send_128? | startNeg__send_52? | startNeg__send_20? | startNeg__send_189? | startNeg__send_34? | startNeg__send_15? | startNeg__send_195? | startNeg__send_267? | startNeg__send_56? | startNeg__send_4? | startNeg__send_173? | startNeg__send_89? | startNeg__send_9? | startNeg__send_283? | startNeg__send_286? | startNeg__send_107? | startNeg__send_178? | startNeg__send_66? | startNeg__send_113?))
ctl p_1883_mix_full_and_notx: E G (((|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_6_3)|)>(|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_0_5)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_5_1)|+|marking(sendAnnPs__broadcasting_6_6)|+|marking(sendAnnPs__broadcasting_0_2)|+|marking(sendAnnPs__broadcasting_0_4)|+|marking(sendAnnPs__broadcasting_1_3)|+|marking(sendAnnPs__broadcasting_5_6)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|)) & (startNeg__send_77? | startNeg__send_160? | startNeg__send_186? | startNeg__send_19? | startNeg__send_269? | startNeg__send_112? | startNeg__send_287? | startNeg__send_238? | startNeg__send_67? | startNeg__send_224? | startNeg__send_21? | startNeg__send_11? | startNeg__send_278? | startNeg__send_61? | startNeg__send_214? | startNeg__send_35? | startNeg__send_245? | startNeg__send_58? | startNeg__send_145? | startNeg__send_220? | startNeg__send_211? | startNeg__send_227? | startNeg__send_102? | startNeg__send_153? | startNeg__send_198? | startNeg__send_97? | startNeg__send_106? | startNeg__send_16? | startNeg__send_151? | startNeg__send_13? | startNeg__send_242? | startNeg__send_116? | startNeg__send_96? | startNeg__send_53? | startNeg__send_233? | startNeg__send_22? | startNeg__send_202? | startNeg__send_219? | startNeg__send_236? | startNeg__send_101? | startNeg__send_111? | startNeg__send_49? | startNeg__send_154? | startNeg__send_284? | startNeg__send_135? | startNeg__send_105? | startNeg__send_50? | startNeg__send_169? | startNeg__send_281? | startNeg__send_270? | startNeg__send_232? | startNeg__send_70? | startNeg__send_218? | startNeg__send_234? | startNeg__send_255? | startNeg__send_57? | startNeg__send_187? | startNeg__send_103? | startNeg__send_285? | startNeg__send_45? | startNeg__send_199? | startNeg__send_74? | startNeg__send_99? | startNeg__send_177? | startNeg__send_17? | startNeg__send_51? | startNeg__send_256? | startNeg__send_273? | startNeg__send_28? | startNeg__send_193? | startNeg__send_75? | startNeg__send_147? | startNeg__send_31? | startNeg__send_229? | startNeg__send_91? | startNeg__send_137? | startNeg__send_259? | startNeg__send_268? | startNeg__send_55? | startNeg__send_213? | startNeg__send_143? | startNeg__send_8? | startNeg__send_279? | startNeg__send_117? | startNeg__send_133? | startNeg__send_88? | startNeg__send_72? | startNeg__send_264? | startNeg__send_203? | startNeg__send_274? | startNeg__send_174? | startNeg__send_196? | startNeg__send_190? | startNeg__send_134? | startNeg__send_191? | startNeg__send_98? | startNeg__send_194? | startNeg__send_261? | startNeg__send_258? | startNeg__send_46? | startNeg__send_266? | startNeg__send_59? | startNeg__send_48? | startNeg__send_68? | startNeg__send_212? | startNeg__send_71? | startNeg__send_3? | startNeg__send_217? | startNeg__send_144? | startNeg__send_185? | startNeg__send_272? | startNeg__send_85? | startNeg__send_239? | startNeg__send_142? | startNeg__send_148? | startNeg__send_254? | startNeg__send_183? | startNeg__send_155? | startNeg__send_18? | startNeg__send_237? | startNeg__send_127? | startNeg__send_275? | startNeg__send_26? | startNeg__send_87? | startNeg__send_12? | startNeg__send_170? | startNeg__send_172? | startNeg__send_182? | startNeg__send_257? | startNeg__send_171? | startNeg__send_226? | startNeg__send_241? | startNeg__send_109? | startNeg__send_215? | startNeg__send_23? | startNeg__send_231? | startNeg__send_243? | startNeg__send_1? | startNeg__send_265? | startNeg__send_192? | startNeg__send_271? | startNeg__send_161? | startNeg__send_108? | startNeg__send_150? | startNeg__send_63? | startNeg__send_90? | startNeg__send_159? | startNeg__send_197? | startNeg__send_44? | startNeg__send_110? | startNeg__send_175? | startNeg__send_188? | startNeg__send_276? | startNeg__send_73? | startNeg__send_30? | startNeg__send_225? | startNeg__send_176? | startNeg__send_262? | startNeg__send_156? | startNeg__send_152? | startNeg__send_141? | startNeg__send_263? | startNeg__send_240? | startNeg__send_60? | startNeg__send_132? | startNeg__send_114? | startNeg__send_146? | startNeg__send_2? | startNeg__send_223? | startNeg__send_139? | startNeg__send_6? | startNeg__send_92? | startNeg__send_118? | startNeg__send_131? | startNeg__send_65? | startNeg__send_7? | startNeg__send_62? | startNeg__send_104? | startNeg__send_181? | startNeg__send_140? | startNeg__send_5? | startNeg__send_32? | startNeg__send_244? | startNeg__send_130? | startNeg__send_27? | startNeg__send_95? | startNeg__send_64? | startNeg__send_221? | startNeg__send_119? | startNeg__send_14? | startNeg__send_277? | startNeg__send_24? | startNeg__send_253? | startNeg__send_228? | startNeg__send_33? | startNeg__send_93? | startNeg__send_129? | startNeg__send_43? | startNeg__send_184? | startNeg__send_10? | startNeg__send_138? | startNeg__send_235? | startNeg__send_157? | startNeg__send_76? | startNeg__send_29? | startNeg__send_158? | startNeg__send_280? | startNeg__send_86? | startNeg__send_94? | startNeg__send_69? | startNeg__send_136? | startNeg__send_200? | startNeg__send_260? | startNeg__send_216? | startNeg__send_115? | startNeg__send_47? | startNeg__send_149? | startNeg__send_100? | startNeg__send_230? | startNeg__send_25? | startNeg__send_282? | startNeg__send_179? | startNeg__send_180? | startNeg__send_201? | startNeg__send_222? | startNeg__send_54? | startNeg__send_128? | startNeg__send_52? | startNeg__send_20? | startNeg__send_189? | startNeg__send_34? | startNeg__send_15? | startNeg__send_195? | startNeg__send_267? | startNeg__send_56? | startNeg__send_4? | startNeg__send_173? | startNeg__send_89? | startNeg__send_9? | startNeg__send_283? | startNeg__send_286? | startNeg__send_107? | startNeg__send_178? | startNeg__send_66? | startNeg__send_113?))


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