fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
marcie: CTLCardinalityComparison on NeoElection/8 (P/T)
Last Updated
Apr. 26, 2013

Introduction

This page shows the outputs produced by the execution of marcie on NeoElection/8 (P/T). We provide:

About the Execution

Execution Summary
Memory (MB) CPU (s) End
144.54 2.00 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=NeoElection-PT-8
export BK_EXAMINATION=CTLCardinalityComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1651
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/NeoElection-PT-8
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is NeoElection-PT-8, examination is CTLCardinalityComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

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

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


execution on node 25: cluster1u27.lip6.fr (runId=136959876801568_n_25)
=====================================================================
runnning marcie on NeoElection-PT-8 (CTLCardinalityComparison)
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-8, examination is CTLCardinalityComparison
=====================================================================

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

START 1369650779

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=CTLCardinalityComparison.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 10062 NrTr: 22266)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369650786

--------------------
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_1860_cardinalitycomparison_eq_x: E F A (X ((|marking(electionInit_1)|+|marking(electionInit_2)|+|marking(electionInit_8)|+|marking(electionInit_6)|+|marking(electionInit_0)|+|marking(electionInit_3)|+|marking(electionInit_4)|+|marking(electionInit_5)|+|marking(electionInit_7)|)!=(|marking(dead_6)|+|marking(dead_8)|+|marking(dead_1)|+|marking(dead_2)|+|marking(dead_5)|+|marking(dead_4)|+|marking(dead_7)|+|marking(dead_0)|+|marking(dead_3)|)) U !((|marking(electedSecondary_7)|+|marking(electedSecondary_8)|+|marking(electedSecondary_6)|+|marking(electedSecondary_0)|+|marking(electedSecondary_5)|+|marking(electedSecondary_2)|+|marking(electedSecondary_3)|+|marking(electedSecondary_1)|+|marking(electedSecondary_4)|)!=(|marking(electionInit_1)|+|marking(electionInit_2)|+|marking(electionInit_8)|+|marking(electionInit_6)|+|marking(electionInit_0)|+|marking(electionInit_3)|+|marking(electionInit_4)|+|marking(electionInit_5)|+|marking(electionInit_7)|)))
ctl p_1861_cardinalitycomparison_full_and: E G (((|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_7_2)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_7_6)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_7_5)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_0_7)|+|marking(startNeg__broadcasting_3_8)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_8_4)|+|marking(startNeg__broadcasting_2_8)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_7_4)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_1_8)|+|marking(startNeg__broadcasting_8_7)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_8_3)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_8_8)|+|marking(startNeg__broadcasting_5_7)|+|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_7_7)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_8_2)|+|marking(startNeg__broadcasting_1_7)|+|marking(startNeg__broadcasting_7_8)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_3_7)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_8_6)|+|marking(startNeg__broadcasting_4_7)|+|marking(startNeg__broadcasting_0_8)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_7_3)|+|marking(startNeg__broadcasting_8_1)|+|marking(startNeg__broadcasting_7_1)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_2_7)|+|marking(startNeg__broadcasting_5_8)|+|marking(startNeg__broadcasting_4_8)|+|marking(startNeg__broadcasting_6_8)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_8_5)|+|marking(startNeg__broadcasting_6_3)|+|marking(startNeg__broadcasting_6_7)|)>(|marking(sendAnnPs__broadcasting_8_7)|+|marking(sendAnnPs__broadcasting_2_7)|+|marking(sendAnnPs__broadcasting_4_7)|+|marking(sendAnnPs__broadcasting_7_6)|+|marking(sendAnnPs__broadcasting_8_5)|+|marking(sendAnnPs__broadcasting_7_3)|+|marking(sendAnnPs__broadcasting_7_2)|+|marking(sendAnnPs__broadcasting_5_7)|+|marking(sendAnnPs__broadcasting_7_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_3_7)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_7_1)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_8_4)|+|marking(sendAnnPs__broadcasting_0_7)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_0_5)|+|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_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|+|marking(sendAnnPs__broadcasting_8_3)|+|marking(sendAnnPs__broadcasting_8_8)|+|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_4_8)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_8_6)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_7_5)|+|marking(sendAnnPs__broadcasting_6_7)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_1_7)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_8_2)|+|marking(sendAnnPs__broadcasting_1_8)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_7_7)|+|marking(sendAnnPs__broadcasting_6_8)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_3_8)|+|marking(sendAnnPs__broadcasting_0_8)|+|marking(sendAnnPs__broadcasting_8_1)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_2_8)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_5_8)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_7_8)|)) & ((|marking(poll__waitingMessage_7)|+|marking(poll__waitingMessage_8)|+|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_6)|+|marking(poll__waitingMessage_4)|+|marking(poll__waitingMessage_5)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)>(|marking(electionInit_1)|+|marking(electionInit_2)|+|marking(electionInit_8)|+|marking(electionInit_6)|+|marking(electionInit_0)|+|marking(electionInit_3)|+|marking(electionInit_4)|+|marking(electionInit_5)|+|marking(electionInit_7)|)))
ctl p_1862_cardinalitycomparison_full_or: E G (((|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_7_2)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_7_6)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_7_5)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_0_7)|+|marking(startNeg__broadcasting_3_8)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_8_4)|+|marking(startNeg__broadcasting_2_8)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_7_4)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_1_8)|+|marking(startNeg__broadcasting_8_7)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_8_3)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_8_8)|+|marking(startNeg__broadcasting_5_7)|+|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_7_7)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_8_2)|+|marking(startNeg__broadcasting_1_7)|+|marking(startNeg__broadcasting_7_8)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_3_7)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_8_6)|+|marking(startNeg__broadcasting_4_7)|+|marking(startNeg__broadcasting_0_8)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_7_3)|+|marking(startNeg__broadcasting_8_1)|+|marking(startNeg__broadcasting_7_1)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_2_7)|+|marking(startNeg__broadcasting_5_8)|+|marking(startNeg__broadcasting_4_8)|+|marking(startNeg__broadcasting_6_8)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_8_5)|+|marking(startNeg__broadcasting_6_3)|+|marking(startNeg__broadcasting_6_7)|)>(|marking(sendAnnPs__broadcasting_8_7)|+|marking(sendAnnPs__broadcasting_2_7)|+|marking(sendAnnPs__broadcasting_4_7)|+|marking(sendAnnPs__broadcasting_7_6)|+|marking(sendAnnPs__broadcasting_8_5)|+|marking(sendAnnPs__broadcasting_7_3)|+|marking(sendAnnPs__broadcasting_7_2)|+|marking(sendAnnPs__broadcasting_5_7)|+|marking(sendAnnPs__broadcasting_7_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_3_7)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_7_1)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_8_4)|+|marking(sendAnnPs__broadcasting_0_7)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_0_5)|+|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_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|+|marking(sendAnnPs__broadcasting_8_3)|+|marking(sendAnnPs__broadcasting_8_8)|+|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_4_8)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_8_6)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_7_5)|+|marking(sendAnnPs__broadcasting_6_7)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_1_7)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_8_2)|+|marking(sendAnnPs__broadcasting_1_8)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_7_7)|+|marking(sendAnnPs__broadcasting_6_8)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_3_8)|+|marking(sendAnnPs__broadcasting_0_8)|+|marking(sendAnnPs__broadcasting_8_1)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_2_8)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_5_8)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_7_8)|)) | ((|marking(poll__waitingMessage_7)|+|marking(poll__waitingMessage_8)|+|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_6)|+|marking(poll__waitingMessage_4)|+|marking(poll__waitingMessage_5)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)>(|marking(electionInit_1)|+|marking(electionInit_2)|+|marking(electionInit_8)|+|marking(electionInit_6)|+|marking(electionInit_0)|+|marking(electionInit_3)|+|marking(electionInit_4)|+|marking(electionInit_5)|+|marking(electionInit_7)|)))
ctl p_1863_cardinalitycomparison_full_and_notx: E G (((|marking(startNeg__broadcasting_5_4)|+|marking(startNeg__broadcasting_6_2)|+|marking(startNeg__broadcasting_2_2)|+|marking(startNeg__broadcasting_2_1)|+|marking(startNeg__broadcasting_6_1)|+|marking(startNeg__broadcasting_7_2)|+|marking(startNeg__broadcasting_4_1)|+|marking(startNeg__broadcasting_0_2)|+|marking(startNeg__broadcasting_7_6)|+|marking(startNeg__broadcasting_5_2)|+|marking(startNeg__broadcasting_2_5)|+|marking(startNeg__broadcasting_2_4)|+|marking(startNeg__broadcasting_1_3)|+|marking(startNeg__broadcasting_7_5)|+|marking(startNeg__broadcasting_1_4)|+|marking(startNeg__broadcasting_1_6)|+|marking(startNeg__broadcasting_0_7)|+|marking(startNeg__broadcasting_3_8)|+|marking(startNeg__broadcasting_5_1)|+|marking(startNeg__broadcasting_5_3)|+|marking(startNeg__broadcasting_6_5)|+|marking(startNeg__broadcasting_8_4)|+|marking(startNeg__broadcasting_2_8)|+|marking(startNeg__broadcasting_3_4)|+|marking(startNeg__broadcasting_7_4)|+|marking(startNeg__broadcasting_1_1)|+|marking(startNeg__broadcasting_2_3)|+|marking(startNeg__broadcasting_3_2)|+|marking(startNeg__broadcasting_1_2)|+|marking(startNeg__broadcasting_1_8)|+|marking(startNeg__broadcasting_8_7)|+|marking(startNeg__broadcasting_6_4)|+|marking(startNeg__broadcasting_3_1)|+|marking(startNeg__broadcasting_8_3)|+|marking(startNeg__broadcasting_4_4)|+|marking(startNeg__broadcasting_8_8)|+|marking(startNeg__broadcasting_5_7)|+|marking(startNeg__broadcasting_5_5)|+|marking(startNeg__broadcasting_1_5)|+|marking(startNeg__broadcasting_7_7)|+|marking(startNeg__broadcasting_4_2)|+|marking(startNeg__broadcasting_0_1)|+|marking(startNeg__broadcasting_4_3)|+|marking(startNeg__broadcasting_6_6)|+|marking(startNeg__broadcasting_0_4)|+|marking(startNeg__broadcasting_0_3)|+|marking(startNeg__broadcasting_8_2)|+|marking(startNeg__broadcasting_1_7)|+|marking(startNeg__broadcasting_7_8)|+|marking(startNeg__broadcasting_3_3)|+|marking(startNeg__broadcasting_0_5)|+|marking(startNeg__broadcasting_3_7)|+|marking(startNeg__broadcasting_3_5)|+|marking(startNeg__broadcasting_8_6)|+|marking(startNeg__broadcasting_4_7)|+|marking(startNeg__broadcasting_0_8)|+|marking(startNeg__broadcasting_2_6)|+|marking(startNeg__broadcasting_4_6)|+|marking(startNeg__broadcasting_7_3)|+|marking(startNeg__broadcasting_8_1)|+|marking(startNeg__broadcasting_7_1)|+|marking(startNeg__broadcasting_4_5)|+|marking(startNeg__broadcasting_0_6)|+|marking(startNeg__broadcasting_5_6)|+|marking(startNeg__broadcasting_2_7)|+|marking(startNeg__broadcasting_5_8)|+|marking(startNeg__broadcasting_4_8)|+|marking(startNeg__broadcasting_6_8)|+|marking(startNeg__broadcasting_3_6)|+|marking(startNeg__broadcasting_8_5)|+|marking(startNeg__broadcasting_6_3)|+|marking(startNeg__broadcasting_6_7)|)>(|marking(sendAnnPs__broadcasting_8_7)|+|marking(sendAnnPs__broadcasting_2_7)|+|marking(sendAnnPs__broadcasting_4_7)|+|marking(sendAnnPs__broadcasting_7_6)|+|marking(sendAnnPs__broadcasting_8_5)|+|marking(sendAnnPs__broadcasting_7_3)|+|marking(sendAnnPs__broadcasting_7_2)|+|marking(sendAnnPs__broadcasting_5_7)|+|marking(sendAnnPs__broadcasting_7_4)|+|marking(sendAnnPs__broadcasting_2_4)|+|marking(sendAnnPs__broadcasting_6_4)|+|marking(sendAnnPs__broadcasting_4_1)|+|marking(sendAnnPs__broadcasting_3_7)|+|marking(sendAnnPs__broadcasting_6_1)|+|marking(sendAnnPs__broadcasting_7_1)|+|marking(sendAnnPs__broadcasting_3_6)|+|marking(sendAnnPs__broadcasting_1_2)|+|marking(sendAnnPs__broadcasting_2_2)|+|marking(sendAnnPs__broadcasting_8_4)|+|marking(sendAnnPs__broadcasting_0_7)|+|marking(sendAnnPs__broadcasting_3_2)|+|marking(sendAnnPs__broadcasting_1_4)|+|marking(sendAnnPs__broadcasting_0_5)|+|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_6_2)|+|marking(sendAnnPs__broadcasting_2_5)|+|marking(sendAnnPs__broadcasting_8_3)|+|marking(sendAnnPs__broadcasting_8_8)|+|marking(sendAnnPs__broadcasting_2_3)|+|marking(sendAnnPs__broadcasting_6_3)|+|marking(sendAnnPs__broadcasting_4_8)|+|marking(sendAnnPs__broadcasting_5_5)|+|marking(sendAnnPs__broadcasting_8_6)|+|marking(sendAnnPs__broadcasting_1_5)|+|marking(sendAnnPs__broadcasting_7_5)|+|marking(sendAnnPs__broadcasting_6_7)|+|marking(sendAnnPs__broadcasting_0_3)|+|marking(sendAnnPs__broadcasting_3_4)|+|marking(sendAnnPs__broadcasting_4_6)|+|marking(sendAnnPs__broadcasting_4_5)|+|marking(sendAnnPs__broadcasting_0_6)|+|marking(sendAnnPs__broadcasting_4_3)|+|marking(sendAnnPs__broadcasting_1_7)|+|marking(sendAnnPs__broadcasting_2_6)|+|marking(sendAnnPs__broadcasting_1_6)|+|marking(sendAnnPs__broadcasting_8_2)|+|marking(sendAnnPs__broadcasting_1_8)|+|marking(sendAnnPs__broadcasting_3_3)|+|marking(sendAnnPs__broadcasting_0_1)|+|marking(sendAnnPs__broadcasting_5_3)|+|marking(sendAnnPs__broadcasting_3_1)|+|marking(sendAnnPs__broadcasting_7_7)|+|marking(sendAnnPs__broadcasting_6_8)|+|marking(sendAnnPs__broadcasting_1_1)|+|marking(sendAnnPs__broadcasting_3_8)|+|marking(sendAnnPs__broadcasting_0_8)|+|marking(sendAnnPs__broadcasting_8_1)|+|marking(sendAnnPs__broadcasting_5_2)|+|marking(sendAnnPs__broadcasting_2_1)|+|marking(sendAnnPs__broadcasting_2_8)|+|marking(sendAnnPs__broadcasting_3_5)|+|marking(sendAnnPs__broadcasting_5_8)|+|marking(sendAnnPs__broadcasting_4_4)|+|marking(sendAnnPs__broadcasting_6_5)|+|marking(sendAnnPs__broadcasting_4_2)|+|marking(sendAnnPs__broadcasting_5_4)|+|marking(sendAnnPs__broadcasting_7_8)|)) & ((|marking(poll__waitingMessage_7)|+|marking(poll__waitingMessage_8)|+|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_6)|+|marking(poll__waitingMessage_4)|+|marking(poll__waitingMessage_5)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)>(|marking(electionInit_1)|+|marking(electionInit_2)|+|marking(electionInit_8)|+|marking(electionInit_6)|+|marking(electionInit_0)|+|marking(electionInit_3)|+|marking(electionInit_4)|+|marking(electionInit_5)|+|marking(electionInit_7)|)))


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