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

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

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

execution on node 30: cluster1u32.lip6.fr (runId=136959876901591_n_30)
=====================================================================
runnning marcie on NeoElection-PT-3 (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-3, examination is CTLMix
=====================================================================

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

START 1369637426

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: 972 NrTr: 1016)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369637426

--------------------
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: A F (X ((|marking(electionFailed_2)|+|marking(electionFailed_0)|+|marking(electionFailed_3)|+|marking(electionFailed_1)|)!=(|marking(crashed_3)|+|marking(crashed_2)|+|marking(crashed_1)|+|marking(crashed_0)|)) <=> !(true & (|marking(electionFailed_2)|!=|marking(electedSecondary_2)|) & (|marking(electionFailed_0)|!=|marking(electedSecondary_0)|) & (|marking(electionFailed_3)|!=|marking(electedSecondary_3)|) & (|marking(electionFailed_1)|!=|marking(electedSecondary_1)|)))
ctl p_1881_mix_full_and: A F (((|marking(electedPrimary_2)|+|marking(electedPrimary_1)|+|marking(electedPrimary_0)|+|marking(electedPrimary_3)|)<=(|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)) & ((true) & (true & (|marking(network_2_3_RI_2)|<=|marking(poll__networl_2_3_RI_2)|) & (|marking(network_1_1_RP_2)|<=|marking(poll__networl_1_1_RP_2)|) & (|marking(network_0_3_AskP_2)|<=|marking(poll__networl_0_3_AskP_2)|) & (|marking(network_1_1_AnsP_3)|<=|marking(poll__networl_1_1_AnsP_3)|) & (|marking(network_3_0_RP_1)|<=|marking(poll__networl_3_0_RP_1)|) & (|marking(network_1_3_RI_0)|<=|marking(poll__networl_1_3_RI_0)|) & (|marking(network_1_0_AskP_3)|<=|marking(poll__networl_1_0_AskP_3)|) & (|marking(network_1_1_RP_0)|<=|marking(poll__networl_1_1_RP_0)|) & (|marking(network_0_2_AnsP_3)|<=|marking(poll__networl_0_2_AnsP_3)|) & (|marking(network_2_0_AnnP_0)|<=|marking(poll__networl_2_0_AnnP_0)|) & (|marking(network_2_2_AnsP_3)|<=|marking(poll__networl_2_2_AnsP_3)|) & (|marking(network_3_1_AskP_1)|<=|marking(poll__networl_3_1_AskP_1)|) & (|marking(network_2_3_RI_3)|<=|marking(poll__networl_2_3_RI_3)|) & (|marking(network_3_0_AI_3)|<=|marking(poll__networl_3_0_AI_3)|) & (|marking(network_1_0_AI_2)|<=|marking(poll__networl_1_0_AI_2)|) & (|marking(network_0_0_RP_3)|<=|marking(poll__networl_0_0_RP_3)|) & (|marking(network_1_3_RI_2)|<=|marking(poll__networl_1_3_RI_2)|) & (|marking(network_0_2_RI_1)|<=|marking(poll__networl_0_2_RI_1)|) & (|marking(network_2_0_AnnP_3)|<=|marking(poll__networl_2_0_AnnP_3)|) & (|marking(network_0_2_RP_0)|<=|marking(poll__networl_0_2_RP_0)|) & (|marking(network_0_1_AnsP_0)|<=|marking(poll__networl_0_1_AnsP_0)|) & (|marking(network_1_0_AnsP_2)|<=|marking(poll__networl_1_0_AnsP_2)|) & (|marking(network_3_3_AnnP_2)|<=|marking(poll__networl_3_3_AnnP_2)|) & (|marking(network_1_3_AI_3)|<=|marking(poll__networl_1_3_AI_3)|) & (|marking(network_1_0_AskP_2)|<=|marking(poll__networl_1_0_AskP_2)|) & (|marking(network_1_3_RP_2)|<=|marking(poll__networl_1_3_RP_2)|) & (|marking(network_3_2_AI_3)|<=|marking(poll__networl_3_2_AI_3)|) & (|marking(network_2_0_AskP_1)|<=|marking(poll__networl_2_0_AskP_1)|) & (|marking(network_3_2_AnsP_3)|<=|marking(poll__networl_3_2_AnsP_3)|) & (|marking(network_3_0_AnnP_1)|<=|marking(poll__networl_3_0_AnnP_1)|) & (|marking(network_1_2_AnsP_0)|<=|marking(poll__networl_1_2_AnsP_0)|) & (|marking(network_3_3_AI_0)|<=|marking(poll__networl_3_3_AI_0)|) & (|marking(network_0_0_RI_2)|<=|marking(poll__networl_0_0_RI_2)|) & (|marking(network_0_3_AskP_1)|<=|marking(poll__networl_0_3_AskP_1)|) & (|marking(network_3_0_AskP_1)|<=|marking(poll__networl_3_0_AskP_1)|) & (|marking(network_2_2_RI_3)|<=|marking(poll__networl_2_2_RI_3)|) & (|marking(network_1_0_RI_2)|<=|marking(poll__networl_1_0_RI_2)|) & (|marking(network_0_1_AskP_2)|<=|marking(poll__networl_0_1_AskP_2)|) & (|marking(network_3_3_RP_2)|<=|marking(poll__networl_3_3_RP_2)|) & (|marking(network_3_3_AskP_2)|<=|marking(poll__networl_3_3_AskP_2)|) & (|marking(network_1_3_RP_1)|<=|marking(poll__networl_1_3_RP_1)|) & (|marking(network_3_0_AnnP_0)|<=|marking(poll__networl_3_0_AnnP_0)|) & (|marking(network_2_1_AnsP_0)|<=|marking(poll__networl_2_1_AnsP_0)|) & (|marking(network_3_2_AskP_2)|<=|marking(poll__networl_3_2_AskP_2)|) & (|marking(network_2_3_AI_3)|<=|marking(poll__networl_2_3_AI_3)|) & (|marking(network_0_0_AI_2)|<=|marking(poll__networl_0_0_AI_2)|) & (|marking(network_2_2_RI_0)|<=|marking(poll__networl_2_2_RI_0)|) & (|marking(network_1_3_AskP_2)|<=|marking(poll__networl_1_3_AskP_2)|) & (|marking(network_1_0_AskP_0)|<=|marking(poll__networl_1_0_AskP_0)|) & (|marking(network_1_2_AskP_3)|<=|marking(poll__networl_1_2_AskP_3)|) & (|marking(network_0_0_AnnP_1)|<=|marking(poll__networl_0_0_AnnP_1)|) & (|marking(network_1_1_AskP_0)|<=|marking(poll__networl_1_1_AskP_0)|) & (|marking(network_1_3_AnnP_2)|<=|marking(poll__networl_1_3_AnnP_2)|) & (|marking(network_3_1_AnsP_2)|<=|marking(poll__networl_3_1_AnsP_2)|) & (|marking(network_0_3_AnnP_2)|<=|marking(poll__networl_0_3_AnnP_2)|) & (|marking(network_1_2_RP_2)|<=|marking(poll__networl_1_2_RP_2)|) & (|marking(network_0_1_RI_3)|<=|marking(poll__networl_0_1_RI_3)|) & (|marking(network_1_1_RI_0)|<=|marking(poll__networl_1_1_RI_0)|) & (|marking(network_0_1_AskP_3)|<=|marking(poll__networl_0_1_AskP_3)|) & (|marking(network_2_2_AI_2)|<=|marking(poll__networl_2_2_AI_2)|) & (|marking(network_3_0_RP_2)|<=|marking(poll__networl_3_0_RP_2)|) & (|marking(network_1_1_AnsP_2)|<=|marking(poll__networl_1_1_AnsP_2)|) & (|marking(network_0_2_AI_1)|<=|marking(poll__networl_0_2_AI_1)|) & (|marking(network_3_2_RI_1)|<=|marking(poll__networl_3_2_RI_1)|) & (|marking(network_2_0_AI_0)|<=|marking(poll__networl_2_0_AI_0)|) & (|marking(network_0_2_AnsP_2)|<=|marking(poll__networl_0_2_AnsP_2)|) & (|marking(network_1_0_RP_0)|<=|marking(poll__networl_1_0_RP_0)|) & (|marking(network_2_1_AskP_1)|<=|marking(poll__networl_2_1_AskP_1)|) & (|marking(network_3_2_RP_0)|<=|marking(poll__networl_3_2_RP_0)|) & (|marking(network_2_0_RP_0)|<=|marking(poll__networl_2_0_RP_0)|) & (|marking(network_1_2_AI_2)|<=|marking(poll__networl_1_2_AI_2)|) & (|marking(network_0_2_AI_3)|<=|marking(poll__networl_0_2_AI_3)|) & (|marking(network_1_3_AnsP_2)|<=|marking(poll__networl_1_3_AnsP_2)|) & (|marking(network_1_3_AI_2)|<=|marking(poll__networl_1_3_AI_2)|) & (|marking(network_0_2_AskP_3)|<=|marking(poll__networl_0_2_AskP_3)|) & (|marking(network_1_1_AnsP_1)|<=|marking(poll__networl_1_1_AnsP_1)|) & (|marking(network_2_0_AskP_0)|<=|marking(poll__networl_2_0_AskP_0)|) & (|marking(network_1_2_RI_3)|<=|marking(poll__networl_1_2_RI_3)|) & (|marking(network_1_2_RP_0)|<=|marking(poll__networl_1_2_RP_0)|) & (|marking(network_2_1_AskP_2)|<=|marking(poll__networl_2_1_AskP_2)|) & (|marking(network_0_0_AnsP_2)|<=|marking(poll__networl_0_0_AnsP_2)|) & (|marking(network_0_2_RP_1)|<=|marking(poll__networl_0_2_RP_1)|) & (|marking(network_1_3_AI_0)|<=|marking(poll__networl_1_3_AI_0)|) & (|marking(network_1_1_AnnP_1)|<=|marking(poll__networl_1_1_AnnP_1)|) & (|marking(network_2_1_AnnP_1)|<=|marking(poll__networl_2_1_AnnP_1)|) & (|marking(network_1_2_AI_0)|<=|marking(poll__networl_1_2_AI_0)|) & (|marking(network_0_2_AnnP_1)|<=|marking(poll__networl_0_2_AnnP_1)|) & (|marking(network_1_0_AI_0)|<=|marking(poll__networl_1_0_AI_0)|) & (|marking(network_1_2_RI_1)|<=|marking(poll__networl_1_2_RI_1)|) & (|marking(network_3_1_RP_2)|<=|marking(poll__networl_3_1_RP_2)|) & (|marking(network_3_3_AskP_3)|<=|marking(poll__networl_3_3_AskP_3)|) & (|marking(network_3_2_AnnP_3)|<=|marking(poll__networl_3_2_AnnP_3)|) & (|marking(network_1_1_AnnP_0)|<=|marking(poll__networl_1_1_AnnP_0)|) & (|marking(network_2_2_AnnP_1)|<=|marking(poll__networl_2_2_AnnP_1)|) & (|marking(network_3_2_AskP_0)|<=|marking(poll__networl_3_2_AskP_0)|) & (|marking(network_1_1_AskP_1)|<=|marking(poll__networl_1_1_AskP_1)|) & (|marking(network_0_3_AnnP_3)|<=|marking(poll__networl_0_3_AnnP_3)|) & (|marking(network_0_2_AnsP_0)|<=|marking(poll__networl_0_2_AnsP_0)|) & (|marking(network_2_1_AnsP_3)|<=|marking(poll__networl_2_1_AnsP_3)|) & (|marking(network_3_3_AI_3)|<=|marking(poll__networl_3_3_AI_3)|) & (|marking(network_3_1_AnnP_2)|<=|marking(poll__networl_3_1_AnnP_2)|) & (|marking(network_2_3_AskP_1)|<=|marking(poll__networl_2_3_AskP_1)|) & (|marking(network_3_2_AnsP_1)|<=|marking(poll__networl_3_2_AnsP_1)|) & (|marking(network_2_1_RP_2)|<=|marking(poll__networl_2_1_RP_2)|) & (|marking(network_3_0_RI_3)|<=|marking(poll__networl_3_0_RI_3)|) & (|marking(network_3_3_RI_1)|<=|marking(poll__networl_3_3_RI_1)|) & (|marking(network_2_3_AskP_2)|<=|marking(poll__networl_2_3_AskP_2)|) & (|marking(network_0_1_RI_2)|<=|marking(poll__networl_0_1_RI_2)|) & (|marking(network_2_1_RP_1)|<=|marking(poll__networl_2_1_RP_1)|) & (|marking(network_2_2_AskP_3)|<=|marking(poll__networl_2_2_AskP_3)|) & (|marking(network_1_3_RI_3)|<=|marking(poll__networl_1_3_RI_3)|) & (|marking(network_3_2_AI_1)|<=|marking(poll__networl_3_2_AI_1)|) & (|marking(network_1_2_RP_3)|<=|marking(poll__networl_1_2_RP_3)|) & (|marking(network_2_2_AI_1)|<=|marking(poll__networl_2_2_AI_1)|) & (|marking(network_2_3_RI_1)|<=|marking(poll__networl_2_3_RI_1)|) & (|marking(network_0_1_AskP_1)|<=|marking(poll__networl_0_1_AskP_1)|) & (|marking(network_1_3_AskP_3)|<=|marking(poll__networl_1_3_AskP_3)|) & (|marking(network_0_3_AI_0)|<=|marking(poll__networl_0_3_AI_0)|) & (|marking(network_1_2_AnnP_0)|<=|marking(poll__networl_1_2_AnnP_0)|) & (|marking(network_0_0_AskP_1)|<=|marking(poll__networl_0_0_AskP_1)|) & (|marking(network_0_2_AnnP_2)|<=|marking(poll__networl_0_2_AnnP_2)|) & (|marking(network_1_0_RP_3)|<=|marking(poll__networl_1_0_RP_3)|) & (|marking(network_3_3_AnnP_1)|<=|marking(poll__networl_3_3_AnnP_1)|) & (|marking(network_3_0_RP_0)|<=|marking(poll__networl_3_0_RP_0)|) & (|marking(network_0_3_AskP_0)|<=|marking(poll__networl_0_3_AskP_0)|) & (|marking(network_3_2_RP_2)|<=|marking(poll__networl_3_2_RP_2)|) & (|marking(network_3_2_RP_1)|<=|marking(poll__networl_3_2_RP_1)|) & (|marking(network_1_0_AnnP_2)|<=|marking(poll__networl_1_0_AnnP_2)|) & (|marking(network_2_0_AnsP_3)|<=|marking(poll__networl_2_0_AnsP_3)|) & (|marking(network_3_1_RP_0)|<=|marking(poll__networl_3_1_RP_0)|) & (|marking(network_2_2_RP_1)|<=|marking(poll__networl_2_2_RP_1)|) & (|marking(network_0_1_AskP_0)|<=|marking(poll__networl_0_1_AskP_0)|) & (|marking(network_0_3_AnsP_1)|<=|marking(poll__networl_0_3_AnsP_1)|) & (|marking(network_3_3_AI_2)|<=|marking(poll__networl_3_3_AI_2)|) & (|marking(network_0_3_AI_3)|<=|marking(poll__networl_0_3_AI_3)|) & (|marking(network_1_3_AI_1)|<=|marking(poll__networl_1_3_AI_1)|) & (|marking(network_0_2_AskP_0)|<=|marking(poll__networl_0_2_AskP_0)|) & (|marking(network_3_3_RP_1)|<=|marking(poll__networl_3_3_RP_1)|) & (|marking(network_2_1_AnsP_1)|<=|marking(poll__networl_2_1_AnsP_1)|) & (|marking(network_3_0_AnsP_2)|<=|marking(poll__networl_3_0_AnsP_2)|) & (|marking(network_0_3_RI_0)|<=|marking(poll__networl_0_3_RI_0)|) & (|marking(network_1_2_AI_3)|<=|marking(poll__networl_1_2_AI_3)|) & (|marking(network_3_1_RI_1)|<=|marking(poll__networl_3_1_RI_1)|) & (|marking(network_3_3_AnsP_1)|<=|marking(poll__networl_3_3_AnsP_1)|) & (|marking(network_0_0_AnsP_1)|<=|marking(poll__networl_0_0_AnsP_1)|) & (|marking(network_2_1_RI_1)|<=|marking(poll__networl_2_1_RI_1)|) & (|marking(network_3_0_AskP_3)|<=|marking(poll__networl_3_0_AskP_3)|) & (|marking(network_1_2_AnsP_3)|<=|marking(poll__networl_1_2_AnsP_3)|) & (|marking(network_1_2_RP_1)|<=|marking(poll__networl_1_2_RP_1)|) & (|marking(network_3_0_AI_2)|<=|marking(poll__networl_3_0_AI_2)|) & (|marking(network_0_1_AnsP_1)|<=|marking(poll__networl_0_1_AnsP_1)|) & (|marking(network_0_2_RI_0)|<=|marking(poll__networl_0_2_RI_0)|) & (|marking(network_2_2_AnsP_1)|<=|marking(poll__networl_2_2_AnsP_1)|) & (|marking(network_3_3_AskP_0)|<=|marking(poll__networl_3_3_AskP_0)|) & (|marking(network_1_2_AnnP_3)|<=|marking(poll__networl_1_2_AnnP_3)|) & (|marking(network_1_1_AI_1)|<=|marking(poll__networl_1_1_AI_1)|) & (|marking(network_3_2_RP_3)|<=|marking(poll__networl_3_2_RP_3)|) & (|marking(network_3_0_RI_0)|<=|marking(poll__networl_3_0_RI_0)|) & (|marking(network_0_0_AI_0)|<=|marking(poll__networl_0_0_AI_0)|) & (|marking(network_3_3_RP_3)|<=|marking(poll__networl_3_3_RP_3)|) & (|marking(network_0_0_RI_3)|<=|marking(poll__networl_0_0_RI_3)|) & (|marking(network_2_2_RP_3)|<=|marking(poll__networl_2_2_RP_3)|) & (|marking(network_0_1_RP_3)|<=|marking(poll__networl_0_1_RP_3)|) & (|marking(network_1_0_AI_1)|<=|marking(poll__networl_1_0_AI_1)|) & (|marking(network_3_3_AI_1)|<=|marking(poll__networl_3_3_AI_1)|) & (|marking(network_3_3_RI_3)|<=|marking(poll__networl_3_3_RI_3)|) & (|marking(network_0_3_AnnP_1)|<=|marking(poll__networl_0_3_AnnP_1)|) & (|marking(network_3_0_AnsP_3)|<=|marking(poll__networl_3_0_AnsP_3)|) & (|marking(network_3_2_AI_0)|<=|marking(poll__networl_3_2_AI_0)|) & (|marking(network_1_1_RI_2)|<=|marking(poll__networl_1_1_RI_2)|) & (|marking(network_1_0_AnnP_3)|<=|marking(poll__networl_1_0_AnnP_3)|) & (|marking(network_3_0_RI_2)|<=|marking(poll__networl_3_0_RI_2)|) & (|marking(network_2_2_AI_3)|<=|marking(poll__networl_2_2_AI_3)|) & (|marking(network_2_3_AnnP_2)|<=|marking(poll__networl_2_3_AnnP_2)|) & (|marking(network_0_3_RI_2)|<=|marking(poll__networl_0_3_RI_2)|) & (|marking(network_3_1_AI_3)|<=|marking(poll__networl_3_1_AI_3)|) & (|marking(network_3_1_RP_1)|<=|marking(poll__networl_3_1_RP_1)|) & (|marking(network_2_0_RI_2)|<=|marking(poll__networl_2_0_RI_2)|) & (|marking(network_2_1_RI_3)|<=|marking(poll__networl_2_1_RI_3)|) & (|marking(network_2_3_AnnP_3)|<=|marking(poll__networl_2_3_AnnP_3)|) & (|marking(network_1_0_AnnP_1)|<=|marking(poll__networl_1_0_AnnP_1)|) & (|marking(network_3_2_AnsP_2)|<=|marking(poll__networl_3_2_AnsP_2)|) & (|marking(network_0_0_AskP_2)|<=|marking(poll__networl_0_0_AskP_2)|) & (|marking(network_0_0_RI_0)|<=|marking(poll__networl_0_0_RI_0)|) & (|marking(network_1_0_RI_3)|<=|marking(poll__networl_1_0_RI_3)|) & (|marking(network_1_1_RI_3)|<=|marking(poll__networl_1_1_RI_3)|) & (|marking(network_0_0_AnsP_0)|<=|marking(poll__networl_0_0_AnsP_0)|) & (|marking(network_0_1_AnsP_2)|<=|marking(poll__networl_0_1_AnsP_2)|) & (|marking(network_2_0_RI_3)|<=|marking(poll__networl_2_0_RI_3)|) & (|marking(network_3_3_RI_2)|<=|marking(poll__networl_3_3_RI_2)|) & (|marking(network_1_1_AI_3)|<=|marking(poll__networl_1_1_AI_3)|) & (|marking(network_3_3_AskP_1)|<=|marking(poll__networl_3_3_AskP_1)|) & (|marking(network_2_2_AnnP_0)|<=|marking(poll__networl_2_2_AnnP_0)|) & (|marking(network_0_1_AnnP_0)|<=|marking(poll__networl_0_1_AnnP_0)|) & (|marking(network_0_3_AnsP_0)|<=|marking(poll__networl_0_3_AnsP_0)|) & (|marking(network_3_2_AI_2)|<=|marking(poll__networl_3_2_AI_2)|) & (|marking(network_2_3_AI_0)|<=|marking(poll__networl_2_3_AI_0)|) & (|marking(network_2_0_RP_2)|<=|marking(poll__networl_2_0_RP_2)|) & (|marking(network_0_0_RI_1)|<=|marking(poll__networl_0_0_RI_1)|) & (|marking(network_3_0_AnnP_3)|<=|marking(poll__networl_3_0_AnnP_3)|) & (|marking(network_2_1_RI_0)|<=|marking(poll__networl_2_1_RI_0)|) & (|marking(network_2_3_AnsP_1)|<=|marking(poll__networl_2_3_AnsP_1)|) & (|marking(network_2_1_RI_2)|<=|marking(poll__networl_2_1_RI_2)|) & (|marking(network_0_3_RI_1)|<=|marking(poll__networl_0_3_RI_1)|) & (|marking(network_2_2_AnsP_0)|<=|marking(poll__networl_2_2_AnsP_0)|) & (|marking(network_1_1_RP_3)|<=|marking(poll__networl_1_1_RP_3)|) & (|marking(network_1_2_AI_1)|<=|marking(poll__networl_1_2_AI_1)|) & (|marking(network_2_3_RP_3)|<=|marking(poll__networl_2_3_RP_3)|) & (|marking(network_1_3_AnsP_0)|<=|marking(poll__networl_1_3_AnsP_0)|) & (|marking(network_3_1_AnsP_3)|<=|marking(poll__networl_3_1_AnsP_3)|) & (|marking(network_3_1_AI_0)|<=|marking(poll__networl_3_1_AI_0)|) & (|marking(network_3_2_AskP_1)|<=|marking(poll__networl_3_2_AskP_1)|) & (|marking(network_3_1_AnnP_3)|<=|marking(poll__networl_3_1_AnnP_3)|) & (|marking(network_1_0_AI_3)|<=|marking(poll__networl_1_0_AI_3)|) & (|marking(network_0_3_RP_1)|<=|marking(poll__networl_0_3_RP_1)|) & (|marking(network_1_3_AnsP_3)|<=|marking(poll__networl_1_3_AnsP_3)|) & (|marking(network_3_2_RI_2)|<=|marking(poll__networl_3_2_RI_2)|) & (|marking(network_0_1_AnnP_2)|<=|marking(poll__networl_0_1_AnnP_2)|) & (|marking(network_1_1_AI_2)|<=|marking(poll__networl_1_1_AI_2)|) & (|marking(network_2_2_AskP_0)|<=|marking(poll__networl_2_2_AskP_0)|) & (|marking(network_3_0_AskP_0)|<=|marking(poll__networl_3_0_AskP_0)|) & (|marking(network_2_2_AnnP_3)|<=|marking(poll__networl_2_2_AnnP_3)|) & (|marking(network_0_2_RP_3)|<=|marking(poll__networl_0_2_RP_3)|) & (|marking(network_0_2_RP_2)|<=|marking(poll__networl_0_2_RP_2)|) & (|marking(network_2_0_AI_3)|<=|marking(poll__networl_2_0_AI_3)|) & (|marking(network_3_1_RI_0)|<=|marking(poll__networl_3_1_RI_0)|) & (|marking(network_2_0_RP_1)|<=|marking(poll__networl_2_0_RP_1)|) & (|marking(network_3_0_AI_0)|<=|marking(poll__networl_3_0_AI_0)|) & (|marking(network_1_3_RI_1)|<=|marking(poll__networl_1_3_RI_1)|) & (|marking(network_0_0_RP_2)|<=|marking(poll__networl_0_0_RP_2)|) & (|marking(network_3_1_AskP_3)|<=|marking(poll__networl_3_1_AskP_3)|) & (|marking(network_1_2_AskP_2)|<=|marking(poll__networl_1_2_AskP_2)|) & (|marking(network_2_3_AI_2)|<=|marking(poll__networl_2_3_AI_2)|) & (|marking(network_3_0_RI_1)|<=|marking(poll__networl_3_0_RI_1)|) & (|marking(network_2_1_RP_3)|<=|marking(poll__networl_2_1_RP_3)|) & (|marking(network_2_1_AI_0)|<=|marking(poll__networl_2_1_AI_0)|) & (|marking(network_0_1_AI_3)|<=|marking(poll__networl_0_1_AI_3)|) & (|marking(network_1_3_AskP_1)|<=|marking(poll__networl_1_3_AskP_1)|) & (|marking(network_2_0_AnsP_0)|<=|marking(poll__networl_2_0_AnsP_0)|) & (|marking(network_1_2_AnnP_1)|<=|marking(poll__networl_1_2_AnnP_1)|) & (|marking(network_0_3_RI_3)|<=|marking(poll__networl_0_3_RI_3)|) & (|marking(network_0_1_RP_0)|<=|marking(poll__networl_0_1_RP_0)|) & (|marking(network_3_1_RI_2)|<=|marking(poll__networl_3_1_RI_2)|) & (|marking(network_0_0_AI_3)|<=|marking(poll__networl_0_0_AI_3)|) & (|marking(network_1_3_AnnP_3)|<=|marking(poll__networl_1_3_AnnP_3)|) & (|marking(network_3_3_AnsP_0)|<=|marking(poll__networl_3_3_AnsP_0)|) & (|marking(network_3_1_AnnP_1)|<=|marking(poll__networl_3_1_AnnP_1)|) & (|marking(network_2_1_AI_3)|<=|marking(poll__networl_2_1_AI_3)|) & (|marking(network_0_3_AnsP_3)|<=|marking(poll__networl_0_3_AnsP_3)|) & (|marking(network_2_1_AI_1)|<=|marking(poll__networl_2_1_AI_1)|) & (|marking(network_2_0_RI_1)|<=|marking(poll__networl_2_0_RI_1)|) & (|marking(network_2_1_AnnP_2)|<=|marking(poll__networl_2_1_AnnP_2)|) & (|marking(network_2_3_AI_1)|<=|marking(poll__networl_2_3_AI_1)|) & (|marking(network_0_1_AI_1)|<=|marking(poll__networl_0_1_AI_1)|) & (|marking(network_3_2_RI_3)|<=|marking(poll__networl_3_2_RI_3)|) & (|marking(network_3_0_AnsP_1)|<=|marking(poll__networl_3_0_AnsP_1)|) & (|marking(network_3_3_AnnP_0)|<=|marking(poll__networl_3_3_AnnP_0)|) & (|marking(network_0_1_AI_0)|<=|marking(poll__networl_0_1_AI_0)|) & (|marking(network_3_2_AnsP_0)|<=|marking(poll__networl_3_2_AnsP_0)|) & (|marking(network_0_0_RP_0)|<=|marking(poll__networl_0_0_RP_0)|) & (|marking(network_2_1_AskP_3)|<=|marking(poll__networl_2_1_AskP_3)|) & (|marking(network_3_0_AI_1)|<=|marking(poll__networl_3_0_AI_1)|) & (|marking(network_1_3_RP_3)|<=|marking(poll__networl_1_3_RP_3)|) & (|marking(network_2_3_RP_1)|<=|marking(poll__networl_2_3_RP_1)|) & (|marking(network_0_1_RI_0)|<=|marking(poll__networl_0_1_RI_0)|) & (|marking(network_3_0_RP_3)|<=|marking(poll__networl_3_0_RP_3)|) & (|marking(network_0_2_AnsP_1)|<=|marking(poll__networl_0_2_AnsP_1)|) & (|marking(network_1_2_AnsP_1)|<=|marking(poll__networl_1_2_AnsP_1)|) & (|marking(network_1_3_AnnP_1)|<=|marking(poll__networl_1_3_AnnP_1)|) & (|marking(network_2_0_AnnP_1)|<=|marking(poll__networl_2_0_AnnP_1)|) & (|marking(network_0_1_RP_2)|<=|marking(poll__networl_0_1_RP_2)|) & (|marking(network_2_0_RP_3)|<=|marking(poll__networl_2_0_RP_3)|) & (|marking(network_1_1_AnnP_2)|<=|marking(poll__networl_1_1_AnnP_2)|) & (|marking(network_2_0_AnnP_2)|<=|marking(poll__networl_2_0_AnnP_2)|) & (|marking(network_2_3_AskP_0)|<=|marking(poll__networl_2_3_AskP_0)|) & (|marking(network_1_2_AskP_0)|<=|marking(poll__networl_1_2_AskP_0)|) & (|marking(network_2_2_RI_2)|<=|marking(poll__networl_2_2_RI_2)|) & (|marking(network_0_0_AnnP_3)|<=|marking(poll__networl_0_0_AnnP_3)|) & (|marking(network_0_3_RP_0)|<=|marking(poll__networl_0_3_RP_0)|) & (|marking(network_1_0_RI_1)|<=|marking(poll__networl_1_0_RI_1)|) & (|marking(network_0_3_RP_3)|<=|marking(poll__networl_0_3_RP_3)|) & (|marking(network_1_3_AnsP_1)|<=|marking(poll__networl_1_3_AnsP_1)|) & (|marking(network_3_0_AnnP_2)|<=|marking(poll__networl_3_0_AnnP_2)|) & (|marking(network_3_2_AnnP_1)|<=|marking(poll__networl_3_2_AnnP_1)|) & (|marking(network_0_3_AskP_3)|<=|marking(poll__networl_0_3_AskP_3)|) & (|marking(network_1_2_RI_2)|<=|marking(poll__networl_1_2_RI_2)|) & (|marking(network_0_3_AI_1)|<=|marking(poll__networl_0_3_AI_1)|) & (|marking(network_1_3_RP_0)|<=|marking(poll__networl_1_3_RP_0)|) & (|marking(network_0_0_AnsP_3)|<=|marking(poll__networl_0_0_AnsP_3)|) & (|marking(network_2_1_AnnP_0)|<=|marking(poll__networl_2_1_AnnP_0)|) & (|marking(network_1_1_AskP_2)|<=|marking(poll__networl_1_1_AskP_2)|) & (|marking(network_0_3_AnsP_2)|<=|marking(poll__networl_0_3_AnsP_2)|) & (|marking(network_2_0_AskP_2)|<=|marking(poll__networl_2_0_AskP_2)|) & (|marking(network_2_1_AskP_0)|<=|marking(poll__networl_2_1_AskP_0)|) & (|marking(network_1_2_AskP_1)|<=|marking(poll__networl_1_2_AskP_1)|) & (|marking(network_2_2_AI_0)|<=|marking(poll__networl_2_2_AI_0)|) & (|marking(network_2_1_AI_2)|<=|marking(poll__networl_2_1_AI_2)|) & (|marking(network_3_3_AnsP_3)|<=|marking(poll__networl_3_3_AnsP_3)|) & (|marking(network_3_1_RP_3)|<=|marking(poll__networl_3_1_RP_3)|) & (|marking(network_3_1_AI_2)|<=|marking(poll__networl_3_1_AI_2)|) & (|marking(network_2_1_RP_0)|<=|marking(poll__networl_2_1_RP_0)|) & (|marking(network_1_0_AnsP_0)|<=|marking(poll__networl_1_0_AnsP_0)|) & (|marking(network_0_3_AI_2)|<=|marking(poll__networl_0_3_AI_2)|) & (|marking(network_2_0_AnsP_1)|<=|marking(poll__networl_2_0_AnsP_1)|) & (|marking(network_3_0_AnsP_0)|<=|marking(poll__networl_3_0_AnsP_0)|) & (|marking(network_2_0_RI_0)|<=|marking(poll__networl_2_0_RI_0)|) & (|marking(network_0_2_AskP_1)|<=|marking(poll__networl_0_2_AskP_1)|) & (|marking(network_2_2_RP_0)|<=|marking(poll__networl_2_2_RP_0)|) & (|marking(network_0_2_AnnP_3)|<=|marking(poll__networl_0_2_AnnP_3)|) & (|marking(network_0_0_AI_1)|<=|marking(poll__networl_0_0_AI_1)|) & (|marking(network_2_3_AnnP_1)|<=|marking(poll__networl_2_3_AnnP_1)|) & (|marking(network_3_1_AskP_2)|<=|marking(poll__networl_3_1_AskP_2)|) & (|marking(network_2_2_RI_1)|<=|marking(poll__networl_2_2_RI_1)|) & (|marking(network_2_2_AskP_2)|<=|marking(poll__networl_2_2_AskP_2)|) & (|marking(network_1_1_AI_0)|<=|marking(poll__networl_1_1_AI_0)|) & (|marking(network_0_1_AnnP_1)|<=|marking(poll__networl_0_1_AnnP_1)|) & (|marking(network_1_2_AnnP_2)|<=|marking(poll__networl_1_2_AnnP_2)|) & (|marking(network_3_2_AskP_3)|<=|marking(poll__networl_3_2_AskP_3)|) & (|marking(network_0_3_RP_2)|<=|marking(poll__networl_0_3_RP_2)|) & (|marking(network_1_1_RP_1)|<=|marking(poll__networl_1_1_RP_1)|) & (|marking(network_1_0_AnsP_1)|<=|marking(poll__networl_1_0_AnsP_1)|) & (|marking(network_2_3_AnsP_2)|<=|marking(poll__networl_2_3_AnsP_2)|) & (|marking(network_1_0_AnnP_0)|<=|marking(poll__networl_1_0_AnnP_0)|) & (|marking(network_0_0_AskP_0)|<=|marking(poll__networl_0_0_AskP_0)|) & (|marking(network_1_0_AskP_1)|<=|marking(poll__networl_1_0_AskP_1)|) & (|marking(network_0_1_RI_1)|<=|marking(poll__networl_0_1_RI_1)|) & (|marking(network_2_3_AnsP_0)|<=|marking(poll__networl_2_3_AnsP_0)|) & (|marking(network_2_3_AnnP_0)|<=|marking(poll__networl_2_3_AnnP_0)|) & (|marking(network_1_0_RP_1)|<=|marking(poll__networl_1_0_RP_1)|) & (|marking(network_3_3_AnnP_3)|<=|marking(poll__networl_3_3_AnnP_3)|) & (|marking(network_0_1_AnnP_3)|<=|marking(poll__networl_0_1_AnnP_3)|) & (|marking(network_2_0_AnsP_2)|<=|marking(poll__networl_2_0_AnsP_2)|) & (|marking(network_2_2_AnsP_2)|<=|marking(poll__networl_2_2_AnsP_2)|) & (|marking(network_2_1_AnnP_3)|<=|marking(poll__networl_2_1_AnnP_3)|) & (|marking(network_0_2_RI_3)|<=|marking(poll__networl_0_2_RI_3)|) & (|marking(network_3_3_RP_0)|<=|marking(poll__networl_3_3_RP_0)|) & (|marking(network_3_1_AskP_0)|<=|marking(poll__networl_3_1_AskP_0)|) & (|marking(network_0_1_RP_1)|<=|marking(poll__networl_0_1_RP_1)|) & (|marking(network_0_2_AskP_2)|<=|marking(poll__networl_0_2_AskP_2)|) & (|marking(network_1_1_AnnP_3)|<=|marking(poll__networl_1_1_AnnP_3)|) & (|marking(network_3_1_AnnP_0)|<=|marking(poll__networl_3_1_AnnP_0)|) & (|marking(network_0_1_AnsP_3)|<=|marking(poll__networl_0_1_AnsP_3)|) & (|marking(network_1_0_RP_2)|<=|marking(poll__networl_1_0_RP_2)|) & (|marking(network_3_2_AnnP_2)|<=|marking(poll__networl_3_2_AnnP_2)|) & (|marking(network_3_2_RI_0)|<=|marking(poll__networl_3_2_RI_0)|) & (|marking(network_0_0_RP_1)|<=|marking(poll__networl_0_0_RP_1)|) & (|marking(network_1_1_RI_1)|<=|marking(poll__networl_1_1_RI_1)|) & (|marking(network_3_3_AnsP_2)|<=|marking(poll__networl_3_3_AnsP_2)|) & (|marking(network_3_1_AnsP_1)|<=|marking(poll__networl_3_1_AnsP_1)|) & (|marking(network_2_2_AnnP_2)|<=|marking(poll__networl_2_2_AnnP_2)|) & (|marking(network_0_0_AskP_3)|<=|marking(poll__networl_0_0_AskP_3)|) & (|marking(network_2_3_RP_2)|<=|marking(poll__networl_2_3_RP_2)|) & (|marking(network_0_2_AI_2)|<=|marking(poll__networl_0_2_AI_2)|) & (|marking(network_2_0_AI_1)|<=|marking(poll__networl_2_0_AI_1)|) & (|marking(network_2_2_AskP_1)|<=|marking(poll__networl_2_2_AskP_1)|) & (|marking(network_1_3_AnnP_0)|<=|marking(poll__networl_1_3_AnnP_0)|) & (|marking(network_1_0_AnsP_3)|<=|marking(poll__networl_1_0_AnsP_3)|) & (|marking(network_3_0_AskP_2)|<=|marking(poll__networl_3_0_AskP_2)|) & (|marking(network_1_2_AnsP_2)|<=|marking(poll__networl_1_2_AnsP_2)|) & (|marking(network_2_0_AskP_3)|<=|marking(poll__networl_2_0_AskP_3)|) & (|marking(network_3_2_AnnP_0)|<=|marking(poll__networl_3_2_AnnP_0)|) & (|marking(network_3_1_RI_3)|<=|marking(poll__networl_3_1_RI_3)|) & (|marking(network_3_3_RI_0)|<=|marking(poll__networl_3_3_RI_0)|) & (|marking(network_0_2_RI_2)|<=|marking(poll__networl_0_2_RI_2)|) & (|marking(network_1_1_AskP_3)|<=|marking(poll__networl_1_1_AskP_3)|) & (|marking(network_3_1_AI_1)|<=|marking(poll__networl_3_1_AI_1)|) & (|marking(network_1_1_AnsP_0)|<=|marking(poll__networl_1_1_AnsP_0)|) & (|marking(network_0_2_AnnP_0)|<=|marking(poll__networl_0_2_AnnP_0)|) & (|marking(network_0_0_AnnP_0)|<=|marking(poll__networl_0_0_AnnP_0)|) & (|marking(network_3_1_AnsP_0)|<=|marking(poll__networl_3_1_AnsP_0)|) & (|marking(network_0_2_AI_0)|<=|marking(poll__networl_0_2_AI_0)|) & (|marking(network_2_3_AskP_3)|<=|marking(poll__networl_2_3_AskP_3)|) & (|marking(network_2_3_AnsP_3)|<=|marking(poll__networl_2_3_AnsP_3)|) & (|marking(network_2_3_RI_0)|<=|marking(poll__networl_2_3_RI_0)|) & (|marking(network_0_1_AI_2)|<=|marking(poll__networl_0_1_AI_2)|) & (|marking(network_0_3_AnnP_0)|<=|marking(poll__networl_0_3_AnnP_0)|) & (|marking(network_2_0_AI_2)|<=|marking(poll__networl_2_0_AI_2)|) & (|marking(network_1_2_RI_0)|<=|marking(poll__networl_1_2_RI_0)|) & (|marking(network_2_1_AnsP_2)|<=|marking(poll__networl_2_1_AnsP_2)|) & (|marking(network_2_3_RP_0)|<=|marking(poll__networl_2_3_RP_0)|) & (|marking(network_1_3_AskP_0)|<=|marking(poll__networl_1_3_AskP_0)|) & (|marking(network_0_0_AnnP_2)|<=|marking(poll__networl_0_0_AnnP_2)|) & (|marking(network_1_0_RI_0)|<=|marking(poll__networl_1_0_RI_0)|) & (|marking(network_2_2_RP_2)|<=|marking(poll__networl_2_2_RP_2)|))))
ctl p_1882_mix_full_or: A G (((|marking(electedPrimary_2)|+|marking(electedPrimary_1)|+|marking(electedPrimary_0)|+|marking(electedPrimary_3)|)<=(|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)) | ((true) & (true & (|marking(network_2_3_RI_2)|<=|marking(poll__networl_2_3_RI_2)|) & (|marking(network_1_1_RP_2)|<=|marking(poll__networl_1_1_RP_2)|) & (|marking(network_0_3_AskP_2)|<=|marking(poll__networl_0_3_AskP_2)|) & (|marking(network_1_1_AnsP_3)|<=|marking(poll__networl_1_1_AnsP_3)|) & (|marking(network_3_0_RP_1)|<=|marking(poll__networl_3_0_RP_1)|) & (|marking(network_1_3_RI_0)|<=|marking(poll__networl_1_3_RI_0)|) & (|marking(network_1_0_AskP_3)|<=|marking(poll__networl_1_0_AskP_3)|) & (|marking(network_1_1_RP_0)|<=|marking(poll__networl_1_1_RP_0)|) & (|marking(network_0_2_AnsP_3)|<=|marking(poll__networl_0_2_AnsP_3)|) & (|marking(network_2_0_AnnP_0)|<=|marking(poll__networl_2_0_AnnP_0)|) & (|marking(network_2_2_AnsP_3)|<=|marking(poll__networl_2_2_AnsP_3)|) & (|marking(network_3_1_AskP_1)|<=|marking(poll__networl_3_1_AskP_1)|) & (|marking(network_2_3_RI_3)|<=|marking(poll__networl_2_3_RI_3)|) & (|marking(network_3_0_AI_3)|<=|marking(poll__networl_3_0_AI_3)|) & (|marking(network_1_0_AI_2)|<=|marking(poll__networl_1_0_AI_2)|) & (|marking(network_0_0_RP_3)|<=|marking(poll__networl_0_0_RP_3)|) & (|marking(network_1_3_RI_2)|<=|marking(poll__networl_1_3_RI_2)|) & (|marking(network_0_2_RI_1)|<=|marking(poll__networl_0_2_RI_1)|) & (|marking(network_2_0_AnnP_3)|<=|marking(poll__networl_2_0_AnnP_3)|) & (|marking(network_0_2_RP_0)|<=|marking(poll__networl_0_2_RP_0)|) & (|marking(network_0_1_AnsP_0)|<=|marking(poll__networl_0_1_AnsP_0)|) & (|marking(network_1_0_AnsP_2)|<=|marking(poll__networl_1_0_AnsP_2)|) & (|marking(network_3_3_AnnP_2)|<=|marking(poll__networl_3_3_AnnP_2)|) & (|marking(network_1_3_AI_3)|<=|marking(poll__networl_1_3_AI_3)|) & (|marking(network_1_0_AskP_2)|<=|marking(poll__networl_1_0_AskP_2)|) & (|marking(network_1_3_RP_2)|<=|marking(poll__networl_1_3_RP_2)|) & (|marking(network_3_2_AI_3)|<=|marking(poll__networl_3_2_AI_3)|) & (|marking(network_2_0_AskP_1)|<=|marking(poll__networl_2_0_AskP_1)|) & (|marking(network_3_2_AnsP_3)|<=|marking(poll__networl_3_2_AnsP_3)|) & (|marking(network_3_0_AnnP_1)|<=|marking(poll__networl_3_0_AnnP_1)|) & (|marking(network_1_2_AnsP_0)|<=|marking(poll__networl_1_2_AnsP_0)|) & (|marking(network_3_3_AI_0)|<=|marking(poll__networl_3_3_AI_0)|) & (|marking(network_0_0_RI_2)|<=|marking(poll__networl_0_0_RI_2)|) & (|marking(network_0_3_AskP_1)|<=|marking(poll__networl_0_3_AskP_1)|) & (|marking(network_3_0_AskP_1)|<=|marking(poll__networl_3_0_AskP_1)|) & (|marking(network_2_2_RI_3)|<=|marking(poll__networl_2_2_RI_3)|) & (|marking(network_1_0_RI_2)|<=|marking(poll__networl_1_0_RI_2)|) & (|marking(network_0_1_AskP_2)|<=|marking(poll__networl_0_1_AskP_2)|) & (|marking(network_3_3_RP_2)|<=|marking(poll__networl_3_3_RP_2)|) & (|marking(network_3_3_AskP_2)|<=|marking(poll__networl_3_3_AskP_2)|) & (|marking(network_1_3_RP_1)|<=|marking(poll__networl_1_3_RP_1)|) & (|marking(network_3_0_AnnP_0)|<=|marking(poll__networl_3_0_AnnP_0)|) & (|marking(network_2_1_AnsP_0)|<=|marking(poll__networl_2_1_AnsP_0)|) & (|marking(network_3_2_AskP_2)|<=|marking(poll__networl_3_2_AskP_2)|) & (|marking(network_2_3_AI_3)|<=|marking(poll__networl_2_3_AI_3)|) & (|marking(network_0_0_AI_2)|<=|marking(poll__networl_0_0_AI_2)|) & (|marking(network_2_2_RI_0)|<=|marking(poll__networl_2_2_RI_0)|) & (|marking(network_1_3_AskP_2)|<=|marking(poll__networl_1_3_AskP_2)|) & (|marking(network_1_0_AskP_0)|<=|marking(poll__networl_1_0_AskP_0)|) & (|marking(network_1_2_AskP_3)|<=|marking(poll__networl_1_2_AskP_3)|) & (|marking(network_0_0_AnnP_1)|<=|marking(poll__networl_0_0_AnnP_1)|) & (|marking(network_1_1_AskP_0)|<=|marking(poll__networl_1_1_AskP_0)|) & (|marking(network_1_3_AnnP_2)|<=|marking(poll__networl_1_3_AnnP_2)|) & (|marking(network_3_1_AnsP_2)|<=|marking(poll__networl_3_1_AnsP_2)|) & (|marking(network_0_3_AnnP_2)|<=|marking(poll__networl_0_3_AnnP_2)|) & (|marking(network_1_2_RP_2)|<=|marking(poll__networl_1_2_RP_2)|) & (|marking(network_0_1_RI_3)|<=|marking(poll__networl_0_1_RI_3)|) & (|marking(network_1_1_RI_0)|<=|marking(poll__networl_1_1_RI_0)|) & (|marking(network_0_1_AskP_3)|<=|marking(poll__networl_0_1_AskP_3)|) & (|marking(network_2_2_AI_2)|<=|marking(poll__networl_2_2_AI_2)|) & (|marking(network_3_0_RP_2)|<=|marking(poll__networl_3_0_RP_2)|) & (|marking(network_1_1_AnsP_2)|<=|marking(poll__networl_1_1_AnsP_2)|) & (|marking(network_0_2_AI_1)|<=|marking(poll__networl_0_2_AI_1)|) & (|marking(network_3_2_RI_1)|<=|marking(poll__networl_3_2_RI_1)|) & (|marking(network_2_0_AI_0)|<=|marking(poll__networl_2_0_AI_0)|) & (|marking(network_0_2_AnsP_2)|<=|marking(poll__networl_0_2_AnsP_2)|) & (|marking(network_1_0_RP_0)|<=|marking(poll__networl_1_0_RP_0)|) & (|marking(network_2_1_AskP_1)|<=|marking(poll__networl_2_1_AskP_1)|) & (|marking(network_3_2_RP_0)|<=|marking(poll__networl_3_2_RP_0)|) & (|marking(network_2_0_RP_0)|<=|marking(poll__networl_2_0_RP_0)|) & (|marking(network_1_2_AI_2)|<=|marking(poll__networl_1_2_AI_2)|) & (|marking(network_0_2_AI_3)|<=|marking(poll__networl_0_2_AI_3)|) & (|marking(network_1_3_AnsP_2)|<=|marking(poll__networl_1_3_AnsP_2)|) & (|marking(network_1_3_AI_2)|<=|marking(poll__networl_1_3_AI_2)|) & (|marking(network_0_2_AskP_3)|<=|marking(poll__networl_0_2_AskP_3)|) & (|marking(network_1_1_AnsP_1)|<=|marking(poll__networl_1_1_AnsP_1)|) & (|marking(network_2_0_AskP_0)|<=|marking(poll__networl_2_0_AskP_0)|) & (|marking(network_1_2_RI_3)|<=|marking(poll__networl_1_2_RI_3)|) & (|marking(network_1_2_RP_0)|<=|marking(poll__networl_1_2_RP_0)|) & (|marking(network_2_1_AskP_2)|<=|marking(poll__networl_2_1_AskP_2)|) & (|marking(network_0_0_AnsP_2)|<=|marking(poll__networl_0_0_AnsP_2)|) & (|marking(network_0_2_RP_1)|<=|marking(poll__networl_0_2_RP_1)|) & (|marking(network_1_3_AI_0)|<=|marking(poll__networl_1_3_AI_0)|) & (|marking(network_1_1_AnnP_1)|<=|marking(poll__networl_1_1_AnnP_1)|) & (|marking(network_2_1_AnnP_1)|<=|marking(poll__networl_2_1_AnnP_1)|) & (|marking(network_1_2_AI_0)|<=|marking(poll__networl_1_2_AI_0)|) & (|marking(network_0_2_AnnP_1)|<=|marking(poll__networl_0_2_AnnP_1)|) & (|marking(network_1_0_AI_0)|<=|marking(poll__networl_1_0_AI_0)|) & (|marking(network_1_2_RI_1)|<=|marking(poll__networl_1_2_RI_1)|) & (|marking(network_3_1_RP_2)|<=|marking(poll__networl_3_1_RP_2)|) & (|marking(network_3_3_AskP_3)|<=|marking(poll__networl_3_3_AskP_3)|) & (|marking(network_3_2_AnnP_3)|<=|marking(poll__networl_3_2_AnnP_3)|) & (|marking(network_1_1_AnnP_0)|<=|marking(poll__networl_1_1_AnnP_0)|) & (|marking(network_2_2_AnnP_1)|<=|marking(poll__networl_2_2_AnnP_1)|) & (|marking(network_3_2_AskP_0)|<=|marking(poll__networl_3_2_AskP_0)|) & (|marking(network_1_1_AskP_1)|<=|marking(poll__networl_1_1_AskP_1)|) & (|marking(network_0_3_AnnP_3)|<=|marking(poll__networl_0_3_AnnP_3)|) & (|marking(network_0_2_AnsP_0)|<=|marking(poll__networl_0_2_AnsP_0)|) & (|marking(network_2_1_AnsP_3)|<=|marking(poll__networl_2_1_AnsP_3)|) & (|marking(network_3_3_AI_3)|<=|marking(poll__networl_3_3_AI_3)|) & (|marking(network_3_1_AnnP_2)|<=|marking(poll__networl_3_1_AnnP_2)|) & (|marking(network_2_3_AskP_1)|<=|marking(poll__networl_2_3_AskP_1)|) & (|marking(network_3_2_AnsP_1)|<=|marking(poll__networl_3_2_AnsP_1)|) & (|marking(network_2_1_RP_2)|<=|marking(poll__networl_2_1_RP_2)|) & (|marking(network_3_0_RI_3)|<=|marking(poll__networl_3_0_RI_3)|) & (|marking(network_3_3_RI_1)|<=|marking(poll__networl_3_3_RI_1)|) & (|marking(network_2_3_AskP_2)|<=|marking(poll__networl_2_3_AskP_2)|) & (|marking(network_0_1_RI_2)|<=|marking(poll__networl_0_1_RI_2)|) & (|marking(network_2_1_RP_1)|<=|marking(poll__networl_2_1_RP_1)|) & (|marking(network_2_2_AskP_3)|<=|marking(poll__networl_2_2_AskP_3)|) & (|marking(network_1_3_RI_3)|<=|marking(poll__networl_1_3_RI_3)|) & (|marking(network_3_2_AI_1)|<=|marking(poll__networl_3_2_AI_1)|) & (|marking(network_1_2_RP_3)|<=|marking(poll__networl_1_2_RP_3)|) & (|marking(network_2_2_AI_1)|<=|marking(poll__networl_2_2_AI_1)|) & (|marking(network_2_3_RI_1)|<=|marking(poll__networl_2_3_RI_1)|) & (|marking(network_0_1_AskP_1)|<=|marking(poll__networl_0_1_AskP_1)|) & (|marking(network_1_3_AskP_3)|<=|marking(poll__networl_1_3_AskP_3)|) & (|marking(network_0_3_AI_0)|<=|marking(poll__networl_0_3_AI_0)|) & (|marking(network_1_2_AnnP_0)|<=|marking(poll__networl_1_2_AnnP_0)|) & (|marking(network_0_0_AskP_1)|<=|marking(poll__networl_0_0_AskP_1)|) & (|marking(network_0_2_AnnP_2)|<=|marking(poll__networl_0_2_AnnP_2)|) & (|marking(network_1_0_RP_3)|<=|marking(poll__networl_1_0_RP_3)|) & (|marking(network_3_3_AnnP_1)|<=|marking(poll__networl_3_3_AnnP_1)|) & (|marking(network_3_0_RP_0)|<=|marking(poll__networl_3_0_RP_0)|) & (|marking(network_0_3_AskP_0)|<=|marking(poll__networl_0_3_AskP_0)|) & (|marking(network_3_2_RP_2)|<=|marking(poll__networl_3_2_RP_2)|) & (|marking(network_3_2_RP_1)|<=|marking(poll__networl_3_2_RP_1)|) & (|marking(network_1_0_AnnP_2)|<=|marking(poll__networl_1_0_AnnP_2)|) & (|marking(network_2_0_AnsP_3)|<=|marking(poll__networl_2_0_AnsP_3)|) & (|marking(network_3_1_RP_0)|<=|marking(poll__networl_3_1_RP_0)|) & (|marking(network_2_2_RP_1)|<=|marking(poll__networl_2_2_RP_1)|) & (|marking(network_0_1_AskP_0)|<=|marking(poll__networl_0_1_AskP_0)|) & (|marking(network_0_3_AnsP_1)|<=|marking(poll__networl_0_3_AnsP_1)|) & (|marking(network_3_3_AI_2)|<=|marking(poll__networl_3_3_AI_2)|) & (|marking(network_0_3_AI_3)|<=|marking(poll__networl_0_3_AI_3)|) & (|marking(network_1_3_AI_1)|<=|marking(poll__networl_1_3_AI_1)|) & (|marking(network_0_2_AskP_0)|<=|marking(poll__networl_0_2_AskP_0)|) & (|marking(network_3_3_RP_1)|<=|marking(poll__networl_3_3_RP_1)|) & (|marking(network_2_1_AnsP_1)|<=|marking(poll__networl_2_1_AnsP_1)|) & (|marking(network_3_0_AnsP_2)|<=|marking(poll__networl_3_0_AnsP_2)|) & (|marking(network_0_3_RI_0)|<=|marking(poll__networl_0_3_RI_0)|) & (|marking(network_1_2_AI_3)|<=|marking(poll__networl_1_2_AI_3)|) & (|marking(network_3_1_RI_1)|<=|marking(poll__networl_3_1_RI_1)|) & (|marking(network_3_3_AnsP_1)|<=|marking(poll__networl_3_3_AnsP_1)|) & (|marking(network_0_0_AnsP_1)|<=|marking(poll__networl_0_0_AnsP_1)|) & (|marking(network_2_1_RI_1)|<=|marking(poll__networl_2_1_RI_1)|) & (|marking(network_3_0_AskP_3)|<=|marking(poll__networl_3_0_AskP_3)|) & (|marking(network_1_2_AnsP_3)|<=|marking(poll__networl_1_2_AnsP_3)|) & (|marking(network_1_2_RP_1)|<=|marking(poll__networl_1_2_RP_1)|) & (|marking(network_3_0_AI_2)|<=|marking(poll__networl_3_0_AI_2)|) & (|marking(network_0_1_AnsP_1)|<=|marking(poll__networl_0_1_AnsP_1)|) & (|marking(network_0_2_RI_0)|<=|marking(poll__networl_0_2_RI_0)|) & (|marking(network_2_2_AnsP_1)|<=|marking(poll__networl_2_2_AnsP_1)|) & (|marking(network_3_3_AskP_0)|<=|marking(poll__networl_3_3_AskP_0)|) & (|marking(network_1_2_AnnP_3)|<=|marking(poll__networl_1_2_AnnP_3)|) & (|marking(network_1_1_AI_1)|<=|marking(poll__networl_1_1_AI_1)|) & (|marking(network_3_2_RP_3)|<=|marking(poll__networl_3_2_RP_3)|) & (|marking(network_3_0_RI_0)|<=|marking(poll__networl_3_0_RI_0)|) & (|marking(network_0_0_AI_0)|<=|marking(poll__networl_0_0_AI_0)|) & (|marking(network_3_3_RP_3)|<=|marking(poll__networl_3_3_RP_3)|) & (|marking(network_0_0_RI_3)|<=|marking(poll__networl_0_0_RI_3)|) & (|marking(network_2_2_RP_3)|<=|marking(poll__networl_2_2_RP_3)|) & (|marking(network_0_1_RP_3)|<=|marking(poll__networl_0_1_RP_3)|) & (|marking(network_1_0_AI_1)|<=|marking(poll__networl_1_0_AI_1)|) & (|marking(network_3_3_AI_1)|<=|marking(poll__networl_3_3_AI_1)|) & (|marking(network_3_3_RI_3)|<=|marking(poll__networl_3_3_RI_3)|) & (|marking(network_0_3_AnnP_1)|<=|marking(poll__networl_0_3_AnnP_1)|) & (|marking(network_3_0_AnsP_3)|<=|marking(poll__networl_3_0_AnsP_3)|) & (|marking(network_3_2_AI_0)|<=|marking(poll__networl_3_2_AI_0)|) & (|marking(network_1_1_RI_2)|<=|marking(poll__networl_1_1_RI_2)|) & (|marking(network_1_0_AnnP_3)|<=|marking(poll__networl_1_0_AnnP_3)|) & (|marking(network_3_0_RI_2)|<=|marking(poll__networl_3_0_RI_2)|) & (|marking(network_2_2_AI_3)|<=|marking(poll__networl_2_2_AI_3)|) & (|marking(network_2_3_AnnP_2)|<=|marking(poll__networl_2_3_AnnP_2)|) & (|marking(network_0_3_RI_2)|<=|marking(poll__networl_0_3_RI_2)|) & (|marking(network_3_1_AI_3)|<=|marking(poll__networl_3_1_AI_3)|) & (|marking(network_3_1_RP_1)|<=|marking(poll__networl_3_1_RP_1)|) & (|marking(network_2_0_RI_2)|<=|marking(poll__networl_2_0_RI_2)|) & (|marking(network_2_1_RI_3)|<=|marking(poll__networl_2_1_RI_3)|) & (|marking(network_2_3_AnnP_3)|<=|marking(poll__networl_2_3_AnnP_3)|) & (|marking(network_1_0_AnnP_1)|<=|marking(poll__networl_1_0_AnnP_1)|) & (|marking(network_3_2_AnsP_2)|<=|marking(poll__networl_3_2_AnsP_2)|) & (|marking(network_0_0_AskP_2)|<=|marking(poll__networl_0_0_AskP_2)|) & (|marking(network_0_0_RI_0)|<=|marking(poll__networl_0_0_RI_0)|) & (|marking(network_1_0_RI_3)|<=|marking(poll__networl_1_0_RI_3)|) & (|marking(network_1_1_RI_3)|<=|marking(poll__networl_1_1_RI_3)|) & (|marking(network_0_0_AnsP_0)|<=|marking(poll__networl_0_0_AnsP_0)|) & (|marking(network_0_1_AnsP_2)|<=|marking(poll__networl_0_1_AnsP_2)|) & (|marking(network_2_0_RI_3)|<=|marking(poll__networl_2_0_RI_3)|) & (|marking(network_3_3_RI_2)|<=|marking(poll__networl_3_3_RI_2)|) & (|marking(network_1_1_AI_3)|<=|marking(poll__networl_1_1_AI_3)|) & (|marking(network_3_3_AskP_1)|<=|marking(poll__networl_3_3_AskP_1)|) & (|marking(network_2_2_AnnP_0)|<=|marking(poll__networl_2_2_AnnP_0)|) & (|marking(network_0_1_AnnP_0)|<=|marking(poll__networl_0_1_AnnP_0)|) & (|marking(network_0_3_AnsP_0)|<=|marking(poll__networl_0_3_AnsP_0)|) & (|marking(network_3_2_AI_2)|<=|marking(poll__networl_3_2_AI_2)|) & (|marking(network_2_3_AI_0)|<=|marking(poll__networl_2_3_AI_0)|) & (|marking(network_2_0_RP_2)|<=|marking(poll__networl_2_0_RP_2)|) & (|marking(network_0_0_RI_1)|<=|marking(poll__networl_0_0_RI_1)|) & (|marking(network_3_0_AnnP_3)|<=|marking(poll__networl_3_0_AnnP_3)|) & (|marking(network_2_1_RI_0)|<=|marking(poll__networl_2_1_RI_0)|) & (|marking(network_2_3_AnsP_1)|<=|marking(poll__networl_2_3_AnsP_1)|) & (|marking(network_2_1_RI_2)|<=|marking(poll__networl_2_1_RI_2)|) & (|marking(network_0_3_RI_1)|<=|marking(poll__networl_0_3_RI_1)|) & (|marking(network_2_2_AnsP_0)|<=|marking(poll__networl_2_2_AnsP_0)|) & (|marking(network_1_1_RP_3)|<=|marking(poll__networl_1_1_RP_3)|) & (|marking(network_1_2_AI_1)|<=|marking(poll__networl_1_2_AI_1)|) & (|marking(network_2_3_RP_3)|<=|marking(poll__networl_2_3_RP_3)|) & (|marking(network_1_3_AnsP_0)|<=|marking(poll__networl_1_3_AnsP_0)|) & (|marking(network_3_1_AnsP_3)|<=|marking(poll__networl_3_1_AnsP_3)|) & (|marking(network_3_1_AI_0)|<=|marking(poll__networl_3_1_AI_0)|) & (|marking(network_3_2_AskP_1)|<=|marking(poll__networl_3_2_AskP_1)|) & (|marking(network_3_1_AnnP_3)|<=|marking(poll__networl_3_1_AnnP_3)|) & (|marking(network_1_0_AI_3)|<=|marking(poll__networl_1_0_AI_3)|) & (|marking(network_0_3_RP_1)|<=|marking(poll__networl_0_3_RP_1)|) & (|marking(network_1_3_AnsP_3)|<=|marking(poll__networl_1_3_AnsP_3)|) & (|marking(network_3_2_RI_2)|<=|marking(poll__networl_3_2_RI_2)|) & (|marking(network_0_1_AnnP_2)|<=|marking(poll__networl_0_1_AnnP_2)|) & (|marking(network_1_1_AI_2)|<=|marking(poll__networl_1_1_AI_2)|) & (|marking(network_2_2_AskP_0)|<=|marking(poll__networl_2_2_AskP_0)|) & (|marking(network_3_0_AskP_0)|<=|marking(poll__networl_3_0_AskP_0)|) & (|marking(network_2_2_AnnP_3)|<=|marking(poll__networl_2_2_AnnP_3)|) & (|marking(network_0_2_RP_3)|<=|marking(poll__networl_0_2_RP_3)|) & (|marking(network_0_2_RP_2)|<=|marking(poll__networl_0_2_RP_2)|) & (|marking(network_2_0_AI_3)|<=|marking(poll__networl_2_0_AI_3)|) & (|marking(network_3_1_RI_0)|<=|marking(poll__networl_3_1_RI_0)|) & (|marking(network_2_0_RP_1)|<=|marking(poll__networl_2_0_RP_1)|) & (|marking(network_3_0_AI_0)|<=|marking(poll__networl_3_0_AI_0)|) & (|marking(network_1_3_RI_1)|<=|marking(poll__networl_1_3_RI_1)|) & (|marking(network_0_0_RP_2)|<=|marking(poll__networl_0_0_RP_2)|) & (|marking(network_3_1_AskP_3)|<=|marking(poll__networl_3_1_AskP_3)|) & (|marking(network_1_2_AskP_2)|<=|marking(poll__networl_1_2_AskP_2)|) & (|marking(network_2_3_AI_2)|<=|marking(poll__networl_2_3_AI_2)|) & (|marking(network_3_0_RI_1)|<=|marking(poll__networl_3_0_RI_1)|) & (|marking(network_2_1_RP_3)|<=|marking(poll__networl_2_1_RP_3)|) & (|marking(network_2_1_AI_0)|<=|marking(poll__networl_2_1_AI_0)|) & (|marking(network_0_1_AI_3)|<=|marking(poll__networl_0_1_AI_3)|) & (|marking(network_1_3_AskP_1)|<=|marking(poll__networl_1_3_AskP_1)|) & (|marking(network_2_0_AnsP_0)|<=|marking(poll__networl_2_0_AnsP_0)|) & (|marking(network_1_2_AnnP_1)|<=|marking(poll__networl_1_2_AnnP_1)|) & (|marking(network_0_3_RI_3)|<=|marking(poll__networl_0_3_RI_3)|) & (|marking(network_0_1_RP_0)|<=|marking(poll__networl_0_1_RP_0)|) & (|marking(network_3_1_RI_2)|<=|marking(poll__networl_3_1_RI_2)|) & (|marking(network_0_0_AI_3)|<=|marking(poll__networl_0_0_AI_3)|) & (|marking(network_1_3_AnnP_3)|<=|marking(poll__networl_1_3_AnnP_3)|) & (|marking(network_3_3_AnsP_0)|<=|marking(poll__networl_3_3_AnsP_0)|) & (|marking(network_3_1_AnnP_1)|<=|marking(poll__networl_3_1_AnnP_1)|) & (|marking(network_2_1_AI_3)|<=|marking(poll__networl_2_1_AI_3)|) & (|marking(network_0_3_AnsP_3)|<=|marking(poll__networl_0_3_AnsP_3)|) & (|marking(network_2_1_AI_1)|<=|marking(poll__networl_2_1_AI_1)|) & (|marking(network_2_0_RI_1)|<=|marking(poll__networl_2_0_RI_1)|) & (|marking(network_2_1_AnnP_2)|<=|marking(poll__networl_2_1_AnnP_2)|) & (|marking(network_2_3_AI_1)|<=|marking(poll__networl_2_3_AI_1)|) & (|marking(network_0_1_AI_1)|<=|marking(poll__networl_0_1_AI_1)|) & (|marking(network_3_2_RI_3)|<=|marking(poll__networl_3_2_RI_3)|) & (|marking(network_3_0_AnsP_1)|<=|marking(poll__networl_3_0_AnsP_1)|) & (|marking(network_3_3_AnnP_0)|<=|marking(poll__networl_3_3_AnnP_0)|) & (|marking(network_0_1_AI_0)|<=|marking(poll__networl_0_1_AI_0)|) & (|marking(network_3_2_AnsP_0)|<=|marking(poll__networl_3_2_AnsP_0)|) & (|marking(network_0_0_RP_0)|<=|marking(poll__networl_0_0_RP_0)|) & (|marking(network_2_1_AskP_3)|<=|marking(poll__networl_2_1_AskP_3)|) & (|marking(network_3_0_AI_1)|<=|marking(poll__networl_3_0_AI_1)|) & (|marking(network_1_3_RP_3)|<=|marking(poll__networl_1_3_RP_3)|) & (|marking(network_2_3_RP_1)|<=|marking(poll__networl_2_3_RP_1)|) & (|marking(network_0_1_RI_0)|<=|marking(poll__networl_0_1_RI_0)|) & (|marking(network_3_0_RP_3)|<=|marking(poll__networl_3_0_RP_3)|) & (|marking(network_0_2_AnsP_1)|<=|marking(poll__networl_0_2_AnsP_1)|) & (|marking(network_1_2_AnsP_1)|<=|marking(poll__networl_1_2_AnsP_1)|) & (|marking(network_1_3_AnnP_1)|<=|marking(poll__networl_1_3_AnnP_1)|) & (|marking(network_2_0_AnnP_1)|<=|marking(poll__networl_2_0_AnnP_1)|) & (|marking(network_0_1_RP_2)|<=|marking(poll__networl_0_1_RP_2)|) & (|marking(network_2_0_RP_3)|<=|marking(poll__networl_2_0_RP_3)|) & (|marking(network_1_1_AnnP_2)|<=|marking(poll__networl_1_1_AnnP_2)|) & (|marking(network_2_0_AnnP_2)|<=|marking(poll__networl_2_0_AnnP_2)|) & (|marking(network_2_3_AskP_0)|<=|marking(poll__networl_2_3_AskP_0)|) & (|marking(network_1_2_AskP_0)|<=|marking(poll__networl_1_2_AskP_0)|) & (|marking(network_2_2_RI_2)|<=|marking(poll__networl_2_2_RI_2)|) & (|marking(network_0_0_AnnP_3)|<=|marking(poll__networl_0_0_AnnP_3)|) & (|marking(network_0_3_RP_0)|<=|marking(poll__networl_0_3_RP_0)|) & (|marking(network_1_0_RI_1)|<=|marking(poll__networl_1_0_RI_1)|) & (|marking(network_0_3_RP_3)|<=|marking(poll__networl_0_3_RP_3)|) & (|marking(network_1_3_AnsP_1)|<=|marking(poll__networl_1_3_AnsP_1)|) & (|marking(network_3_0_AnnP_2)|<=|marking(poll__networl_3_0_AnnP_2)|) & (|marking(network_3_2_AnnP_1)|<=|marking(poll__networl_3_2_AnnP_1)|) & (|marking(network_0_3_AskP_3)|<=|marking(poll__networl_0_3_AskP_3)|) & (|marking(network_1_2_RI_2)|<=|marking(poll__networl_1_2_RI_2)|) & (|marking(network_0_3_AI_1)|<=|marking(poll__networl_0_3_AI_1)|) & (|marking(network_1_3_RP_0)|<=|marking(poll__networl_1_3_RP_0)|) & (|marking(network_0_0_AnsP_3)|<=|marking(poll__networl_0_0_AnsP_3)|) & (|marking(network_2_1_AnnP_0)|<=|marking(poll__networl_2_1_AnnP_0)|) & (|marking(network_1_1_AskP_2)|<=|marking(poll__networl_1_1_AskP_2)|) & (|marking(network_0_3_AnsP_2)|<=|marking(poll__networl_0_3_AnsP_2)|) & (|marking(network_2_0_AskP_2)|<=|marking(poll__networl_2_0_AskP_2)|) & (|marking(network_2_1_AskP_0)|<=|marking(poll__networl_2_1_AskP_0)|) & (|marking(network_1_2_AskP_1)|<=|marking(poll__networl_1_2_AskP_1)|) & (|marking(network_2_2_AI_0)|<=|marking(poll__networl_2_2_AI_0)|) & (|marking(network_2_1_AI_2)|<=|marking(poll__networl_2_1_AI_2)|) & (|marking(network_3_3_AnsP_3)|<=|marking(poll__networl_3_3_AnsP_3)|) & (|marking(network_3_1_RP_3)|<=|marking(poll__networl_3_1_RP_3)|) & (|marking(network_3_1_AI_2)|<=|marking(poll__networl_3_1_AI_2)|) & (|marking(network_2_1_RP_0)|<=|marking(poll__networl_2_1_RP_0)|) & (|marking(network_1_0_AnsP_0)|<=|marking(poll__networl_1_0_AnsP_0)|) & (|marking(network_0_3_AI_2)|<=|marking(poll__networl_0_3_AI_2)|) & (|marking(network_2_0_AnsP_1)|<=|marking(poll__networl_2_0_AnsP_1)|) & (|marking(network_3_0_AnsP_0)|<=|marking(poll__networl_3_0_AnsP_0)|) & (|marking(network_2_0_RI_0)|<=|marking(poll__networl_2_0_RI_0)|) & (|marking(network_0_2_AskP_1)|<=|marking(poll__networl_0_2_AskP_1)|) & (|marking(network_2_2_RP_0)|<=|marking(poll__networl_2_2_RP_0)|) & (|marking(network_0_2_AnnP_3)|<=|marking(poll__networl_0_2_AnnP_3)|) & (|marking(network_0_0_AI_1)|<=|marking(poll__networl_0_0_AI_1)|) & (|marking(network_2_3_AnnP_1)|<=|marking(poll__networl_2_3_AnnP_1)|) & (|marking(network_3_1_AskP_2)|<=|marking(poll__networl_3_1_AskP_2)|) & (|marking(network_2_2_RI_1)|<=|marking(poll__networl_2_2_RI_1)|) & (|marking(network_2_2_AskP_2)|<=|marking(poll__networl_2_2_AskP_2)|) & (|marking(network_1_1_AI_0)|<=|marking(poll__networl_1_1_AI_0)|) & (|marking(network_0_1_AnnP_1)|<=|marking(poll__networl_0_1_AnnP_1)|) & (|marking(network_1_2_AnnP_2)|<=|marking(poll__networl_1_2_AnnP_2)|) & (|marking(network_3_2_AskP_3)|<=|marking(poll__networl_3_2_AskP_3)|) & (|marking(network_0_3_RP_2)|<=|marking(poll__networl_0_3_RP_2)|) & (|marking(network_1_1_RP_1)|<=|marking(poll__networl_1_1_RP_1)|) & (|marking(network_1_0_AnsP_1)|<=|marking(poll__networl_1_0_AnsP_1)|) & (|marking(network_2_3_AnsP_2)|<=|marking(poll__networl_2_3_AnsP_2)|) & (|marking(network_1_0_AnnP_0)|<=|marking(poll__networl_1_0_AnnP_0)|) & (|marking(network_0_0_AskP_0)|<=|marking(poll__networl_0_0_AskP_0)|) & (|marking(network_1_0_AskP_1)|<=|marking(poll__networl_1_0_AskP_1)|) & (|marking(network_0_1_RI_1)|<=|marking(poll__networl_0_1_RI_1)|) & (|marking(network_2_3_AnsP_0)|<=|marking(poll__networl_2_3_AnsP_0)|) & (|marking(network_2_3_AnnP_0)|<=|marking(poll__networl_2_3_AnnP_0)|) & (|marking(network_1_0_RP_1)|<=|marking(poll__networl_1_0_RP_1)|) & (|marking(network_3_3_AnnP_3)|<=|marking(poll__networl_3_3_AnnP_3)|) & (|marking(network_0_1_AnnP_3)|<=|marking(poll__networl_0_1_AnnP_3)|) & (|marking(network_2_0_AnsP_2)|<=|marking(poll__networl_2_0_AnsP_2)|) & (|marking(network_2_2_AnsP_2)|<=|marking(poll__networl_2_2_AnsP_2)|) & (|marking(network_2_1_AnnP_3)|<=|marking(poll__networl_2_1_AnnP_3)|) & (|marking(network_0_2_RI_3)|<=|marking(poll__networl_0_2_RI_3)|) & (|marking(network_3_3_RP_0)|<=|marking(poll__networl_3_3_RP_0)|) & (|marking(network_3_1_AskP_0)|<=|marking(poll__networl_3_1_AskP_0)|) & (|marking(network_0_1_RP_1)|<=|marking(poll__networl_0_1_RP_1)|) & (|marking(network_0_2_AskP_2)|<=|marking(poll__networl_0_2_AskP_2)|) & (|marking(network_1_1_AnnP_3)|<=|marking(poll__networl_1_1_AnnP_3)|) & (|marking(network_3_1_AnnP_0)|<=|marking(poll__networl_3_1_AnnP_0)|) & (|marking(network_0_1_AnsP_3)|<=|marking(poll__networl_0_1_AnsP_3)|) & (|marking(network_1_0_RP_2)|<=|marking(poll__networl_1_0_RP_2)|) & (|marking(network_3_2_AnnP_2)|<=|marking(poll__networl_3_2_AnnP_2)|) & (|marking(network_3_2_RI_0)|<=|marking(poll__networl_3_2_RI_0)|) & (|marking(network_0_0_RP_1)|<=|marking(poll__networl_0_0_RP_1)|) & (|marking(network_1_1_RI_1)|<=|marking(poll__networl_1_1_RI_1)|) & (|marking(network_3_3_AnsP_2)|<=|marking(poll__networl_3_3_AnsP_2)|) & (|marking(network_3_1_AnsP_1)|<=|marking(poll__networl_3_1_AnsP_1)|) & (|marking(network_2_2_AnnP_2)|<=|marking(poll__networl_2_2_AnnP_2)|) & (|marking(network_0_0_AskP_3)|<=|marking(poll__networl_0_0_AskP_3)|) & (|marking(network_2_3_RP_2)|<=|marking(poll__networl_2_3_RP_2)|) & (|marking(network_0_2_AI_2)|<=|marking(poll__networl_0_2_AI_2)|) & (|marking(network_2_0_AI_1)|<=|marking(poll__networl_2_0_AI_1)|) & (|marking(network_2_2_AskP_1)|<=|marking(poll__networl_2_2_AskP_1)|) & (|marking(network_1_3_AnnP_0)|<=|marking(poll__networl_1_3_AnnP_0)|) & (|marking(network_1_0_AnsP_3)|<=|marking(poll__networl_1_0_AnsP_3)|) & (|marking(network_3_0_AskP_2)|<=|marking(poll__networl_3_0_AskP_2)|) & (|marking(network_1_2_AnsP_2)|<=|marking(poll__networl_1_2_AnsP_2)|) & (|marking(network_2_0_AskP_3)|<=|marking(poll__networl_2_0_AskP_3)|) & (|marking(network_3_2_AnnP_0)|<=|marking(poll__networl_3_2_AnnP_0)|) & (|marking(network_3_1_RI_3)|<=|marking(poll__networl_3_1_RI_3)|) & (|marking(network_3_3_RI_0)|<=|marking(poll__networl_3_3_RI_0)|) & (|marking(network_0_2_RI_2)|<=|marking(poll__networl_0_2_RI_2)|) & (|marking(network_1_1_AskP_3)|<=|marking(poll__networl_1_1_AskP_3)|) & (|marking(network_3_1_AI_1)|<=|marking(poll__networl_3_1_AI_1)|) & (|marking(network_1_1_AnsP_0)|<=|marking(poll__networl_1_1_AnsP_0)|) & (|marking(network_0_2_AnnP_0)|<=|marking(poll__networl_0_2_AnnP_0)|) & (|marking(network_0_0_AnnP_0)|<=|marking(poll__networl_0_0_AnnP_0)|) & (|marking(network_3_1_AnsP_0)|<=|marking(poll__networl_3_1_AnsP_0)|) & (|marking(network_0_2_AI_0)|<=|marking(poll__networl_0_2_AI_0)|) & (|marking(network_2_3_AskP_3)|<=|marking(poll__networl_2_3_AskP_3)|) & (|marking(network_2_3_AnsP_3)|<=|marking(poll__networl_2_3_AnsP_3)|) & (|marking(network_2_3_RI_0)|<=|marking(poll__networl_2_3_RI_0)|) & (|marking(network_0_1_AI_2)|<=|marking(poll__networl_0_1_AI_2)|) & (|marking(network_0_3_AnnP_0)|<=|marking(poll__networl_0_3_AnnP_0)|) & (|marking(network_2_0_AI_2)|<=|marking(poll__networl_2_0_AI_2)|) & (|marking(network_1_2_RI_0)|<=|marking(poll__networl_1_2_RI_0)|) & (|marking(network_2_1_AnsP_2)|<=|marking(poll__networl_2_1_AnsP_2)|) & (|marking(network_2_3_RP_0)|<=|marking(poll__networl_2_3_RP_0)|) & (|marking(network_1_3_AskP_0)|<=|marking(poll__networl_1_3_AskP_0)|) & (|marking(network_0_0_AnnP_2)|<=|marking(poll__networl_0_0_AnnP_2)|) & (|marking(network_1_0_RI_0)|<=|marking(poll__networl_1_0_RI_0)|) & (|marking(network_2_2_RP_2)|<=|marking(poll__networl_2_2_RP_2)|))))
ctl p_1883_mix_full_and_notx: A F (((|marking(electedPrimary_2)|+|marking(electedPrimary_1)|+|marking(electedPrimary_0)|+|marking(electedPrimary_3)|)<=(|marking(poll__waitingMessage_2)|+|marking(poll__waitingMessage_3)|+|marking(poll__waitingMessage_1)|+|marking(poll__waitingMessage_0)|)) & ((true) & (true & (|marking(network_2_3_RI_2)|<=|marking(poll__networl_2_3_RI_2)|) & (|marking(network_1_1_RP_2)|<=|marking(poll__networl_1_1_RP_2)|) & (|marking(network_0_3_AskP_2)|<=|marking(poll__networl_0_3_AskP_2)|) & (|marking(network_1_1_AnsP_3)|<=|marking(poll__networl_1_1_AnsP_3)|) & (|marking(network_3_0_RP_1)|<=|marking(poll__networl_3_0_RP_1)|) & (|marking(network_1_3_RI_0)|<=|marking(poll__networl_1_3_RI_0)|) & (|marking(network_1_0_AskP_3)|<=|marking(poll__networl_1_0_AskP_3)|) & (|marking(network_1_1_RP_0)|<=|marking(poll__networl_1_1_RP_0)|) & (|marking(network_0_2_AnsP_3)|<=|marking(poll__networl_0_2_AnsP_3)|) & (|marking(network_2_0_AnnP_0)|<=|marking(poll__networl_2_0_AnnP_0)|) & (|marking(network_2_2_AnsP_3)|<=|marking(poll__networl_2_2_AnsP_3)|) & (|marking(network_3_1_AskP_1)|<=|marking(poll__networl_3_1_AskP_1)|) & (|marking(network_2_3_RI_3)|<=|marking(poll__networl_2_3_RI_3)|) & (|marking(network_3_0_AI_3)|<=|marking(poll__networl_3_0_AI_3)|) & (|marking(network_1_0_AI_2)|<=|marking(poll__networl_1_0_AI_2)|) & (|marking(network_0_0_RP_3)|<=|marking(poll__networl_0_0_RP_3)|) & (|marking(network_1_3_RI_2)|<=|marking(poll__networl_1_3_RI_2)|) & (|marking(network_0_2_RI_1)|<=|marking(poll__networl_0_2_RI_1)|) & (|marking(network_2_0_AnnP_3)|<=|marking(poll__networl_2_0_AnnP_3)|) & (|marking(network_0_2_RP_0)|<=|marking(poll__networl_0_2_RP_0)|) & (|marking(network_0_1_AnsP_0)|<=|marking(poll__networl_0_1_AnsP_0)|) & (|marking(network_1_0_AnsP_2)|<=|marking(poll__networl_1_0_AnsP_2)|) & (|marking(network_3_3_AnnP_2)|<=|marking(poll__networl_3_3_AnnP_2)|) & (|marking(network_1_3_AI_3)|<=|marking(poll__networl_1_3_AI_3)|) & (|marking(network_1_0_AskP_2)|<=|marking(poll__networl_1_0_AskP_2)|) & (|marking(network_1_3_RP_2)|<=|marking(poll__networl_1_3_RP_2)|) & (|marking(network_3_2_AI_3)|<=|marking(poll__networl_3_2_AI_3)|) & (|marking(network_2_0_AskP_1)|<=|marking(poll__networl_2_0_AskP_1)|) & (|marking(network_3_2_AnsP_3)|<=|marking(poll__networl_3_2_AnsP_3)|) & (|marking(network_3_0_AnnP_1)|<=|marking(poll__networl_3_0_AnnP_1)|) & (|marking(network_1_2_AnsP_0)|<=|marking(poll__networl_1_2_AnsP_0)|) & (|marking(network_3_3_AI_0)|<=|marking(poll__networl_3_3_AI_0)|) & (|marking(network_0_0_RI_2)|<=|marking(poll__networl_0_0_RI_2)|) & (|marking(network_0_3_AskP_1)|<=|marking(poll__networl_0_3_AskP_1)|) & (|marking(network_3_0_AskP_1)|<=|marking(poll__networl_3_0_AskP_1)|) & (|marking(network_2_2_RI_3)|<=|marking(poll__networl_2_2_RI_3)|) & (|marking(network_1_0_RI_2)|<=|marking(poll__networl_1_0_RI_2)|) & (|marking(network_0_1_AskP_2)|<=|marking(poll__networl_0_1_AskP_2)|) & (|marking(network_3_3_RP_2)|<=|marking(poll__networl_3_3_RP_2)|) & (|marking(network_3_3_AskP_2)|<=|marking(poll__networl_3_3_AskP_2)|) & (|marking(network_1_3_RP_1)|<=|marking(poll__networl_1_3_RP_1)|) & (|marking(network_3_0_AnnP_0)|<=|marking(poll__networl_3_0_AnnP_0)|) & (|marking(network_2_1_AnsP_0)|<=|marking(poll__networl_2_1_AnsP_0)|) & (|marking(network_3_2_AskP_2)|<=|marking(poll__networl_3_2_AskP_2)|) & (|marking(network_2_3_AI_3)|<=|marking(poll__networl_2_3_AI_3)|) & (|marking(network_0_0_AI_2)|<=|marking(poll__networl_0_0_AI_2)|) & (|marking(network_2_2_RI_0)|<=|marking(poll__networl_2_2_RI_0)|) & (|marking(network_1_3_AskP_2)|<=|marking(poll__networl_1_3_AskP_2)|) & (|marking(network_1_0_AskP_0)|<=|marking(poll__networl_1_0_AskP_0)|) & (|marking(network_1_2_AskP_3)|<=|marking(poll__networl_1_2_AskP_3)|) & (|marking(network_0_0_AnnP_1)|<=|marking(poll__networl_0_0_AnnP_1)|) & (|marking(network_1_1_AskP_0)|<=|marking(poll__networl_1_1_AskP_0)|) & (|marking(network_1_3_AnnP_2)|<=|marking(poll__networl_1_3_AnnP_2)|) & (|marking(network_3_1_AnsP_2)|<=|marking(poll__networl_3_1_AnsP_2)|) & (|marking(network_0_3_AnnP_2)|<=|marking(poll__networl_0_3_AnnP_2)|) & (|marking(network_1_2_RP_2)|<=|marking(poll__networl_1_2_RP_2)|) & (|marking(network_0_1_RI_3)|<=|marking(poll__networl_0_1_RI_3)|) & (|marking(network_1_1_RI_0)|<=|marking(poll__networl_1_1_RI_0)|) & (|marking(network_0_1_AskP_3)|<=|marking(poll__networl_0_1_AskP_3)|) & (|marking(network_2_2_AI_2)|<=|marking(poll__networl_2_2_AI_2)|) & (|marking(network_3_0_RP_2)|<=|marking(poll__networl_3_0_RP_2)|) & (|marking(network_1_1_AnsP_2)|<=|marking(poll__networl_1_1_AnsP_2)|) & (|marking(network_0_2_AI_1)|<=|marking(poll__networl_0_2_AI_1)|) & (|marking(network_3_2_RI_1)|<=|marking(poll__networl_3_2_RI_1)|) & (|marking(network_2_0_AI_0)|<=|marking(poll__networl_2_0_AI_0)|) & (|marking(network_0_2_AnsP_2)|<=|marking(poll__networl_0_2_AnsP_2)|) & (|marking(network_1_0_RP_0)|<=|marking(poll__networl_1_0_RP_0)|) & (|marking(network_2_1_AskP_1)|<=|marking(poll__networl_2_1_AskP_1)|) & (|marking(network_3_2_RP_0)|<=|marking(poll__networl_3_2_RP_0)|) & (|marking(network_2_0_RP_0)|<=|marking(poll__networl_2_0_RP_0)|) & (|marking(network_1_2_AI_2)|<=|marking(poll__networl_1_2_AI_2)|) & (|marking(network_0_2_AI_3)|<=|marking(poll__networl_0_2_AI_3)|) & (|marking(network_1_3_AnsP_2)|<=|marking(poll__networl_1_3_AnsP_2)|) & (|marking(network_1_3_AI_2)|<=|marking(poll__networl_1_3_AI_2)|) & (|marking(network_0_2_AskP_3)|<=|marking(poll__networl_0_2_AskP_3)|) & (|marking(network_1_1_AnsP_1)|<=|marking(poll__networl_1_1_AnsP_1)|) & (|marking(network_2_0_AskP_0)|<=|marking(poll__networl_2_0_AskP_0)|) & (|marking(network_1_2_RI_3)|<=|marking(poll__networl_1_2_RI_3)|) & (|marking(network_1_2_RP_0)|<=|marking(poll__networl_1_2_RP_0)|) & (|marking(network_2_1_AskP_2)|<=|marking(poll__networl_2_1_AskP_2)|) & (|marking(network_0_0_AnsP_2)|<=|marking(poll__networl_0_0_AnsP_2)|) & (|marking(network_0_2_RP_1)|<=|marking(poll__networl_0_2_RP_1)|) & (|marking(network_1_3_AI_0)|<=|marking(poll__networl_1_3_AI_0)|) & (|marking(network_1_1_AnnP_1)|<=|marking(poll__networl_1_1_AnnP_1)|) & (|marking(network_2_1_AnnP_1)|<=|marking(poll__networl_2_1_AnnP_1)|) & (|marking(network_1_2_AI_0)|<=|marking(poll__networl_1_2_AI_0)|) & (|marking(network_0_2_AnnP_1)|<=|marking(poll__networl_0_2_AnnP_1)|) & (|marking(network_1_0_AI_0)|<=|marking(poll__networl_1_0_AI_0)|) & (|marking(network_1_2_RI_1)|<=|marking(poll__networl_1_2_RI_1)|) & (|marking(network_3_1_RP_2)|<=|marking(poll__networl_3_1_RP_2)|) & (|marking(network_3_3_AskP_3)|<=|marking(poll__networl_3_3_AskP_3)|) & (|marking(network_3_2_AnnP_3)|<=|marking(poll__networl_3_2_AnnP_3)|) & (|marking(network_1_1_AnnP_0)|<=|marking(poll__networl_1_1_AnnP_0)|) & (|marking(network_2_2_AnnP_1)|<=|marking(poll__networl_2_2_AnnP_1)|) & (|marking(network_3_2_AskP_0)|<=|marking(poll__networl_3_2_AskP_0)|) & (|marking(network_1_1_AskP_1)|<=|marking(poll__networl_1_1_AskP_1)|) & (|marking(network_0_3_AnnP_3)|<=|marking(poll__networl_0_3_AnnP_3)|) & (|marking(network_0_2_AnsP_0)|<=|marking(poll__networl_0_2_AnsP_0)|) & (|marking(network_2_1_AnsP_3)|<=|marking(poll__networl_2_1_AnsP_3)|) & (|marking(network_3_3_AI_3)|<=|marking(poll__networl_3_3_AI_3)|) & (|marking(network_3_1_AnnP_2)|<=|marking(poll__networl_3_1_AnnP_2)|) & (|marking(network_2_3_AskP_1)|<=|marking(poll__networl_2_3_AskP_1)|) & (|marking(network_3_2_AnsP_1)|<=|marking(poll__networl_3_2_AnsP_1)|) & (|marking(network_2_1_RP_2)|<=|marking(poll__networl_2_1_RP_2)|) & (|marking(network_3_0_RI_3)|<=|marking(poll__networl_3_0_RI_3)|) & (|marking(network_3_3_RI_1)|<=|marking(poll__networl_3_3_RI_1)|) & (|marking(network_2_3_AskP_2)|<=|marking(poll__networl_2_3_AskP_2)|) & (|marking(network_0_1_RI_2)|<=|marking(poll__networl_0_1_RI_2)|) & (|marking(network_2_1_RP_1)|<=|marking(poll__networl_2_1_RP_1)|) & (|marking(network_2_2_AskP_3)|<=|marking(poll__networl_2_2_AskP_3)|) & (|marking(network_1_3_RI_3)|<=|marking(poll__networl_1_3_RI_3)|) & (|marking(network_3_2_AI_1)|<=|marking(poll__networl_3_2_AI_1)|) & (|marking(network_1_2_RP_3)|<=|marking(poll__networl_1_2_RP_3)|) & (|marking(network_2_2_AI_1)|<=|marking(poll__networl_2_2_AI_1)|) & (|marking(network_2_3_RI_1)|<=|marking(poll__networl_2_3_RI_1)|) & (|marking(network_0_1_AskP_1)|<=|marking(poll__networl_0_1_AskP_1)|) & (|marking(network_1_3_AskP_3)|<=|marking(poll__networl_1_3_AskP_3)|) & (|marking(network_0_3_AI_0)|<=|marking(poll__networl_0_3_AI_0)|) & (|marking(network_1_2_AnnP_0)|<=|marking(poll__networl_1_2_AnnP_0)|) & (|marking(network_0_0_AskP_1)|<=|marking(poll__networl_0_0_AskP_1)|) & (|marking(network_0_2_AnnP_2)|<=|marking(poll__networl_0_2_AnnP_2)|) & (|marking(network_1_0_RP_3)|<=|marking(poll__networl_1_0_RP_3)|) & (|marking(network_3_3_AnnP_1)|<=|marking(poll__networl_3_3_AnnP_1)|) & (|marking(network_3_0_RP_0)|<=|marking(poll__networl_3_0_RP_0)|) & (|marking(network_0_3_AskP_0)|<=|marking(poll__networl_0_3_AskP_0)|) & (|marking(network_3_2_RP_2)|<=|marking(poll__networl_3_2_RP_2)|) & (|marking(network_3_2_RP_1)|<=|marking(poll__networl_3_2_RP_1)|) & (|marking(network_1_0_AnnP_2)|<=|marking(poll__networl_1_0_AnnP_2)|) & (|marking(network_2_0_AnsP_3)|<=|marking(poll__networl_2_0_AnsP_3)|) & (|marking(network_3_1_RP_0)|<=|marking(poll__networl_3_1_RP_0)|) & (|marking(network_2_2_RP_1)|<=|marking(poll__networl_2_2_RP_1)|) & (|marking(network_0_1_AskP_0)|<=|marking(poll__networl_0_1_AskP_0)|) & (|marking(network_0_3_AnsP_1)|<=|marking(poll__networl_0_3_AnsP_1)|) & (|marking(network_3_3_AI_2)|<=|marking(poll__networl_3_3_AI_2)|) & (|marking(network_0_3_AI_3)|<=|marking(poll__networl_0_3_AI_3)|) & (|marking(network_1_3_AI_1)|<=|marking(poll__networl_1_3_AI_1)|) & (|marking(network_0_2_AskP_0)|<=|marking(poll__networl_0_2_AskP_0)|) & (|marking(network_3_3_RP_1)|<=|marking(poll__networl_3_3_RP_1)|) & (|marking(network_2_1_AnsP_1)|<=|marking(poll__networl_2_1_AnsP_1)|) & (|marking(network_3_0_AnsP_2)|<=|marking(poll__networl_3_0_AnsP_2)|) & (|marking(network_0_3_RI_0)|<=|marking(poll__networl_0_3_RI_0)|) & (|marking(network_1_2_AI_3)|<=|marking(poll__networl_1_2_AI_3)|) & (|marking(network_3_1_RI_1)|<=|marking(poll__networl_3_1_RI_1)|) & (|marking(network_3_3_AnsP_1)|<=|marking(poll__networl_3_3_AnsP_1)|) & (|marking(network_0_0_AnsP_1)|<=|marking(poll__networl_0_0_AnsP_1)|) & (|marking(network_2_1_RI_1)|<=|marking(poll__networl_2_1_RI_1)|) & (|marking(network_3_0_AskP_3)|<=|marking(poll__networl_3_0_AskP_3)|) & (|marking(network_1_2_AnsP_3)|<=|marking(poll__networl_1_2_AnsP_3)|) & (|marking(network_1_2_RP_1)|<=|marking(poll__networl_1_2_RP_1)|) & (|marking(network_3_0_AI_2)|<=|marking(poll__networl_3_0_AI_2)|) & (|marking(network_0_1_AnsP_1)|<=|marking(poll__networl_0_1_AnsP_1)|) & (|marking(network_0_2_RI_0)|<=|marking(poll__networl_0_2_RI_0)|) & (|marking(network_2_2_AnsP_1)|<=|marking(poll__networl_2_2_AnsP_1)|) & (|marking(network_3_3_AskP_0)|<=|marking(poll__networl_3_3_AskP_0)|) & (|marking(network_1_2_AnnP_3)|<=|marking(poll__networl_1_2_AnnP_3)|) & (|marking(network_1_1_AI_1)|<=|marking(poll__networl_1_1_AI_1)|) & (|marking(network_3_2_RP_3)|<=|marking(poll__networl_3_2_RP_3)|) & (|marking(network_3_0_RI_0)|<=|marking(poll__networl_3_0_RI_0)|) & (|marking(network_0_0_AI_0)|<=|marking(poll__networl_0_0_AI_0)|) & (|marking(network_3_3_RP_3)|<=|marking(poll__networl_3_3_RP_3)|) & (|marking(network_0_0_RI_3)|<=|marking(poll__networl_0_0_RI_3)|) & (|marking(network_2_2_RP_3)|<=|marking(poll__networl_2_2_RP_3)|) & (|marking(network_0_1_RP_3)|<=|marking(poll__networl_0_1_RP_3)|) & (|marking(network_1_0_AI_1)|<=|marking(poll__networl_1_0_AI_1)|) & (|marking(network_3_3_AI_1)|<=|marking(poll__networl_3_3_AI_1)|) & (|marking(network_3_3_RI_3)|<=|marking(poll__networl_3_3_RI_3)|) & (|marking(network_0_3_AnnP_1)|<=|marking(poll__networl_0_3_AnnP_1)|) & (|marking(network_3_0_AnsP_3)|<=|marking(poll__networl_3_0_AnsP_3)|) & (|marking(network_3_2_AI_0)|<=|marking(poll__networl_3_2_AI_0)|) & (|marking(network_1_1_RI_2)|<=|marking(poll__networl_1_1_RI_2)|) & (|marking(network_1_0_AnnP_3)|<=|marking(poll__networl_1_0_AnnP_3)|) & (|marking(network_3_0_RI_2)|<=|marking(poll__networl_3_0_RI_2)|) & (|marking(network_2_2_AI_3)|<=|marking(poll__networl_2_2_AI_3)|) & (|marking(network_2_3_AnnP_2)|<=|marking(poll__networl_2_3_AnnP_2)|) & (|marking(network_0_3_RI_2)|<=|marking(poll__networl_0_3_RI_2)|) & (|marking(network_3_1_AI_3)|<=|marking(poll__networl_3_1_AI_3)|) & (|marking(network_3_1_RP_1)|<=|marking(poll__networl_3_1_RP_1)|) & (|marking(network_2_0_RI_2)|<=|marking(poll__networl_2_0_RI_2)|) & (|marking(network_2_1_RI_3)|<=|marking(poll__networl_2_1_RI_3)|) & (|marking(network_2_3_AnnP_3)|<=|marking(poll__networl_2_3_AnnP_3)|) & (|marking(network_1_0_AnnP_1)|<=|marking(poll__networl_1_0_AnnP_1)|) & (|marking(network_3_2_AnsP_2)|<=|marking(poll__networl_3_2_AnsP_2)|) & (|marking(network_0_0_AskP_2)|<=|marking(poll__networl_0_0_AskP_2)|) & (|marking(network_0_0_RI_0)|<=|marking(poll__networl_0_0_RI_0)|) & (|marking(network_1_0_RI_3)|<=|marking(poll__networl_1_0_RI_3)|) & (|marking(network_1_1_RI_3)|<=|marking(poll__networl_1_1_RI_3)|) & (|marking(network_0_0_AnsP_0)|<=|marking(poll__networl_0_0_AnsP_0)|) & (|marking(network_0_1_AnsP_2)|<=|marking(poll__networl_0_1_AnsP_2)|) & (|marking(network_2_0_RI_3)|<=|marking(poll__networl_2_0_RI_3)|) & (|marking(network_3_3_RI_2)|<=|marking(poll__networl_3_3_RI_2)|) & (|marking(network_1_1_AI_3)|<=|marking(poll__networl_1_1_AI_3)|) & (|marking(network_3_3_AskP_1)|<=|marking(poll__networl_3_3_AskP_1)|) & (|marking(network_2_2_AnnP_0)|<=|marking(poll__networl_2_2_AnnP_0)|) & (|marking(network_0_1_AnnP_0)|<=|marking(poll__networl_0_1_AnnP_0)|) & (|marking(network_0_3_AnsP_0)|<=|marking(poll__networl_0_3_AnsP_0)|) & (|marking(network_3_2_AI_2)|<=|marking(poll__networl_3_2_AI_2)|) & (|marking(network_2_3_AI_0)|<=|marking(poll__networl_2_3_AI_0)|) & (|marking(network_2_0_RP_2)|<=|marking(poll__networl_2_0_RP_2)|) & (|marking(network_0_0_RI_1)|<=|marking(poll__networl_0_0_RI_1)|) & (|marking(network_3_0_AnnP_3)|<=|marking(poll__networl_3_0_AnnP_3)|) & (|marking(network_2_1_RI_0)|<=|marking(poll__networl_2_1_RI_0)|) & (|marking(network_2_3_AnsP_1)|<=|marking(poll__networl_2_3_AnsP_1)|) & (|marking(network_2_1_RI_2)|<=|marking(poll__networl_2_1_RI_2)|) & (|marking(network_0_3_RI_1)|<=|marking(poll__networl_0_3_RI_1)|) & (|marking(network_2_2_AnsP_0)|<=|marking(poll__networl_2_2_AnsP_0)|) & (|marking(network_1_1_RP_3)|<=|marking(poll__networl_1_1_RP_3)|) & (|marking(network_1_2_AI_1)|<=|marking(poll__networl_1_2_AI_1)|) & (|marking(network_2_3_RP_3)|<=|marking(poll__networl_2_3_RP_3)|) & (|marking(network_1_3_AnsP_0)|<=|marking(poll__networl_1_3_AnsP_0)|) & (|marking(network_3_1_AnsP_3)|<=|marking(poll__networl_3_1_AnsP_3)|) & (|marking(network_3_1_AI_0)|<=|marking(poll__networl_3_1_AI_0)|) & (|marking(network_3_2_AskP_1)|<=|marking(poll__networl_3_2_AskP_1)|) & (|marking(network_3_1_AnnP_3)|<=|marking(poll__networl_3_1_AnnP_3)|) & (|marking(network_1_0_AI_3)|<=|marking(poll__networl_1_0_AI_3)|) & (|marking(network_0_3_RP_1)|<=|marking(poll__networl_0_3_RP_1)|) & (|marking(network_1_3_AnsP_3)|<=|marking(poll__networl_1_3_AnsP_3)|) & (|marking(network_3_2_RI_2)|<=|marking(poll__networl_3_2_RI_2)|) & (|marking(network_0_1_AnnP_2)|<=|marking(poll__networl_0_1_AnnP_2)|) & (|marking(network_1_1_AI_2)|<=|marking(poll__networl_1_1_AI_2)|) & (|marking(network_2_2_AskP_0)|<=|marking(poll__networl_2_2_AskP_0)|) & (|marking(network_3_0_AskP_0)|<=|marking(poll__networl_3_0_AskP_0)|) & (|marking(network_2_2_AnnP_3)|<=|marking(poll__networl_2_2_AnnP_3)|) & (|marking(network_0_2_RP_3)|<=|marking(poll__networl_0_2_RP_3)|) & (|marking(network_0_2_RP_2)|<=|marking(poll__networl_0_2_RP_2)|) & (|marking(network_2_0_AI_3)|<=|marking(poll__networl_2_0_AI_3)|) & (|marking(network_3_1_RI_0)|<=|marking(poll__networl_3_1_RI_0)|) & (|marking(network_2_0_RP_1)|<=|marking(poll__networl_2_0_RP_1)|) & (|marking(network_3_0_AI_0)|<=|marking(poll__networl_3_0_AI_0)|) & (|marking(network_1_3_RI_1)|<=|marking(poll__networl_1_3_RI_1)|) & (|marking(network_0_0_RP_2)|<=|marking(poll__networl_0_0_RP_2)|) & (|marking(network_3_1_AskP_3)|<=|marking(poll__networl_3_1_AskP_3)|) & (|marking(network_1_2_AskP_2)|<=|marking(poll__networl_1_2_AskP_2)|) & (|marking(network_2_3_AI_2)|<=|marking(poll__networl_2_3_AI_2)|) & (|marking(network_3_0_RI_1)|<=|marking(poll__networl_3_0_RI_1)|) & (|marking(network_2_1_RP_3)|<=|marking(poll__networl_2_1_RP_3)|) & (|marking(network_2_1_AI_0)|<=|marking(poll__networl_2_1_AI_0)|) & (|marking(network_0_1_AI_3)|<=|marking(poll__networl_0_1_AI_3)|) & (|marking(network_1_3_AskP_1)|<=|marking(poll__networl_1_3_AskP_1)|) & (|marking(network_2_0_AnsP_0)|<=|marking(poll__networl_2_0_AnsP_0)|) & (|marking(network_1_2_AnnP_1)|<=|marking(poll__networl_1_2_AnnP_1)|) & (|marking(network_0_3_RI_3)|<=|marking(poll__networl_0_3_RI_3)|) & (|marking(network_0_1_RP_0)|<=|marking(poll__networl_0_1_RP_0)|) & (|marking(network_3_1_RI_2)|<=|marking(poll__networl_3_1_RI_2)|) & (|marking(network_0_0_AI_3)|<=|marking(poll__networl_0_0_AI_3)|) & (|marking(network_1_3_AnnP_3)|<=|marking(poll__networl_1_3_AnnP_3)|) & (|marking(network_3_3_AnsP_0)|<=|marking(poll__networl_3_3_AnsP_0)|) & (|marking(network_3_1_AnnP_1)|<=|marking(poll__networl_3_1_AnnP_1)|) & (|marking(network_2_1_AI_3)|<=|marking(poll__networl_2_1_AI_3)|) & (|marking(network_0_3_AnsP_3)|<=|marking(poll__networl_0_3_AnsP_3)|) & (|marking(network_2_1_AI_1)|<=|marking(poll__networl_2_1_AI_1)|) & (|marking(network_2_0_RI_1)|<=|marking(poll__networl_2_0_RI_1)|) & (|marking(network_2_1_AnnP_2)|<=|marking(poll__networl_2_1_AnnP_2)|) & (|marking(network_2_3_AI_1)|<=|marking(poll__networl_2_3_AI_1)|) & (|marking(network_0_1_AI_1)|<=|marking(poll__networl_0_1_AI_1)|) & (|marking(network_3_2_RI_3)|<=|marking(poll__networl_3_2_RI_3)|) & (|marking(network_3_0_AnsP_1)|<=|marking(poll__networl_3_0_AnsP_1)|) & (|marking(network_3_3_AnnP_0)|<=|marking(poll__networl_3_3_AnnP_0)|) & (|marking(network_0_1_AI_0)|<=|marking(poll__networl_0_1_AI_0)|) & (|marking(network_3_2_AnsP_0)|<=|marking(poll__networl_3_2_AnsP_0)|) & (|marking(network_0_0_RP_0)|<=|marking(poll__networl_0_0_RP_0)|) & (|marking(network_2_1_AskP_3)|<=|marking(poll__networl_2_1_AskP_3)|) & (|marking(network_3_0_AI_1)|<=|marking(poll__networl_3_0_AI_1)|) & (|marking(network_1_3_RP_3)|<=|marking(poll__networl_1_3_RP_3)|) & (|marking(network_2_3_RP_1)|<=|marking(poll__networl_2_3_RP_1)|) & (|marking(network_0_1_RI_0)|<=|marking(poll__networl_0_1_RI_0)|) & (|marking(network_3_0_RP_3)|<=|marking(poll__networl_3_0_RP_3)|) & (|marking(network_0_2_AnsP_1)|<=|marking(poll__networl_0_2_AnsP_1)|) & (|marking(network_1_2_AnsP_1)|<=|marking(poll__networl_1_2_AnsP_1)|) & (|marking(network_1_3_AnnP_1)|<=|marking(poll__networl_1_3_AnnP_1)|) & (|marking(network_2_0_AnnP_1)|<=|marking(poll__networl_2_0_AnnP_1)|) & (|marking(network_0_1_RP_2)|<=|marking(poll__networl_0_1_RP_2)|) & (|marking(network_2_0_RP_3)|<=|marking(poll__networl_2_0_RP_3)|) & (|marking(network_1_1_AnnP_2)|<=|marking(poll__networl_1_1_AnnP_2)|) & (|marking(network_2_0_AnnP_2)|<=|marking(poll__networl_2_0_AnnP_2)|) & (|marking(network_2_3_AskP_0)|<=|marking(poll__networl_2_3_AskP_0)|) & (|marking(network_1_2_AskP_0)|<=|marking(poll__networl_1_2_AskP_0)|) & (|marking(network_2_2_RI_2)|<=|marking(poll__networl_2_2_RI_2)|) & (|marking(network_0_0_AnnP_3)|<=|marking(poll__networl_0_0_AnnP_3)|) & (|marking(network_0_3_RP_0)|<=|marking(poll__networl_0_3_RP_0)|) & (|marking(network_1_0_RI_1)|<=|marking(poll__networl_1_0_RI_1)|) & (|marking(network_0_3_RP_3)|<=|marking(poll__networl_0_3_RP_3)|) & (|marking(network_1_3_AnsP_1)|<=|marking(poll__networl_1_3_AnsP_1)|) & (|marking(network_3_0_AnnP_2)|<=|marking(poll__networl_3_0_AnnP_2)|) & (|marking(network_3_2_AnnP_1)|<=|marking(poll__networl_3_2_AnnP_1)|) & (|marking(network_0_3_AskP_3)|<=|marking(poll__networl_0_3_AskP_3)|) & (|marking(network_1_2_RI_2)|<=|marking(poll__networl_1_2_RI_2)|) & (|marking(network_0_3_AI_1)|<=|marking(poll__networl_0_3_AI_1)|) & (|marking(network_1_3_RP_0)|<=|marking(poll__networl_1_3_RP_0)|) & (|marking(network_0_0_AnsP_3)|<=|marking(poll__networl_0_0_AnsP_3)|) & (|marking(network_2_1_AnnP_0)|<=|marking(poll__networl_2_1_AnnP_0)|) & (|marking(network_1_1_AskP_2)|<=|marking(poll__networl_1_1_AskP_2)|) & (|marking(network_0_3_AnsP_2)|<=|marking(poll__networl_0_3_AnsP_2)|) & (|marking(network_2_0_AskP_2)|<=|marking(poll__networl_2_0_AskP_2)|) & (|marking(network_2_1_AskP_0)|<=|marking(poll__networl_2_1_AskP_0)|) & (|marking(network_1_2_AskP_1)|<=|marking(poll__networl_1_2_AskP_1)|) & (|marking(network_2_2_AI_0)|<=|marking(poll__networl_2_2_AI_0)|) & (|marking(network_2_1_AI_2)|<=|marking(poll__networl_2_1_AI_2)|) & (|marking(network_3_3_AnsP_3)|<=|marking(poll__networl_3_3_AnsP_3)|) & (|marking(network_3_1_RP_3)|<=|marking(poll__networl_3_1_RP_3)|) & (|marking(network_3_1_AI_2)|<=|marking(poll__networl_3_1_AI_2)|) & (|marking(network_2_1_RP_0)|<=|marking(poll__networl_2_1_RP_0)|) & (|marking(network_1_0_AnsP_0)|<=|marking(poll__networl_1_0_AnsP_0)|) & (|marking(network_0_3_AI_2)|<=|marking(poll__networl_0_3_AI_2)|) & (|marking(network_2_0_AnsP_1)|<=|marking(poll__networl_2_0_AnsP_1)|) & (|marking(network_3_0_AnsP_0)|<=|marking(poll__networl_3_0_AnsP_0)|) & (|marking(network_2_0_RI_0)|<=|marking(poll__networl_2_0_RI_0)|) & (|marking(network_0_2_AskP_1)|<=|marking(poll__networl_0_2_AskP_1)|) & (|marking(network_2_2_RP_0)|<=|marking(poll__networl_2_2_RP_0)|) & (|marking(network_0_2_AnnP_3)|<=|marking(poll__networl_0_2_AnnP_3)|) & (|marking(network_0_0_AI_1)|<=|marking(poll__networl_0_0_AI_1)|) & (|marking(network_2_3_AnnP_1)|<=|marking(poll__networl_2_3_AnnP_1)|) & (|marking(network_3_1_AskP_2)|<=|marking(poll__networl_3_1_AskP_2)|) & (|marking(network_2_2_RI_1)|<=|marking(poll__networl_2_2_RI_1)|) & (|marking(network_2_2_AskP_2)|<=|marking(poll__networl_2_2_AskP_2)|) & (|marking(network_1_1_AI_0)|<=|marking(poll__networl_1_1_AI_0)|) & (|marking(network_0_1_AnnP_1)|<=|marking(poll__networl_0_1_AnnP_1)|) & (|marking(network_1_2_AnnP_2)|<=|marking(poll__networl_1_2_AnnP_2)|) & (|marking(network_3_2_AskP_3)|<=|marking(poll__networl_3_2_AskP_3)|) & (|marking(network_0_3_RP_2)|<=|marking(poll__networl_0_3_RP_2)|) & (|marking(network_1_1_RP_1)|<=|marking(poll__networl_1_1_RP_1)|) & (|marking(network_1_0_AnsP_1)|<=|marking(poll__networl_1_0_AnsP_1)|) & (|marking(network_2_3_AnsP_2)|<=|marking(poll__networl_2_3_AnsP_2)|) & (|marking(network_1_0_AnnP_0)|<=|marking(poll__networl_1_0_AnnP_0)|) & (|marking(network_0_0_AskP_0)|<=|marking(poll__networl_0_0_AskP_0)|) & (|marking(network_1_0_AskP_1)|<=|marking(poll__networl_1_0_AskP_1)|) & (|marking(network_0_1_RI_1)|<=|marking(poll__networl_0_1_RI_1)|) & (|marking(network_2_3_AnsP_0)|<=|marking(poll__networl_2_3_AnsP_0)|) & (|marking(network_2_3_AnnP_0)|<=|marking(poll__networl_2_3_AnnP_0)|) & (|marking(network_1_0_RP_1)|<=|marking(poll__networl_1_0_RP_1)|) & (|marking(network_3_3_AnnP_3)|<=|marking(poll__networl_3_3_AnnP_3)|) & (|marking(network_0_1_AnnP_3)|<=|marking(poll__networl_0_1_AnnP_3)|) & (|marking(network_2_0_AnsP_2)|<=|marking(poll__networl_2_0_AnsP_2)|) & (|marking(network_2_2_AnsP_2)|<=|marking(poll__networl_2_2_AnsP_2)|) & (|marking(network_2_1_AnnP_3)|<=|marking(poll__networl_2_1_AnnP_3)|) & (|marking(network_0_2_RI_3)|<=|marking(poll__networl_0_2_RI_3)|) & (|marking(network_3_3_RP_0)|<=|marking(poll__networl_3_3_RP_0)|) & (|marking(network_3_1_AskP_0)|<=|marking(poll__networl_3_1_AskP_0)|) & (|marking(network_0_1_RP_1)|<=|marking(poll__networl_0_1_RP_1)|) & (|marking(network_0_2_AskP_2)|<=|marking(poll__networl_0_2_AskP_2)|) & (|marking(network_1_1_AnnP_3)|<=|marking(poll__networl_1_1_AnnP_3)|) & (|marking(network_3_1_AnnP_0)|<=|marking(poll__networl_3_1_AnnP_0)|) & (|marking(network_0_1_AnsP_3)|<=|marking(poll__networl_0_1_AnsP_3)|) & (|marking(network_1_0_RP_2)|<=|marking(poll__networl_1_0_RP_2)|) & (|marking(network_3_2_AnnP_2)|<=|marking(poll__networl_3_2_AnnP_2)|) & (|marking(network_3_2_RI_0)|<=|marking(poll__networl_3_2_RI_0)|) & (|marking(network_0_0_RP_1)|<=|marking(poll__networl_0_0_RP_1)|) & (|marking(network_1_1_RI_1)|<=|marking(poll__networl_1_1_RI_1)|) & (|marking(network_3_3_AnsP_2)|<=|marking(poll__networl_3_3_AnsP_2)|) & (|marking(network_3_1_AnsP_1)|<=|marking(poll__networl_3_1_AnsP_1)|) & (|marking(network_2_2_AnnP_2)|<=|marking(poll__networl_2_2_AnnP_2)|) & (|marking(network_0_0_AskP_3)|<=|marking(poll__networl_0_0_AskP_3)|) & (|marking(network_2_3_RP_2)|<=|marking(poll__networl_2_3_RP_2)|) & (|marking(network_0_2_AI_2)|<=|marking(poll__networl_0_2_AI_2)|) & (|marking(network_2_0_AI_1)|<=|marking(poll__networl_2_0_AI_1)|) & (|marking(network_2_2_AskP_1)|<=|marking(poll__networl_2_2_AskP_1)|) & (|marking(network_1_3_AnnP_0)|<=|marking(poll__networl_1_3_AnnP_0)|) & (|marking(network_1_0_AnsP_3)|<=|marking(poll__networl_1_0_AnsP_3)|) & (|marking(network_3_0_AskP_2)|<=|marking(poll__networl_3_0_AskP_2)|) & (|marking(network_1_2_AnsP_2)|<=|marking(poll__networl_1_2_AnsP_2)|) & (|marking(network_2_0_AskP_3)|<=|marking(poll__networl_2_0_AskP_3)|) & (|marking(network_3_2_AnnP_0)|<=|marking(poll__networl_3_2_AnnP_0)|) & (|marking(network_3_1_RI_3)|<=|marking(poll__networl_3_1_RI_3)|) & (|marking(network_3_3_RI_0)|<=|marking(poll__networl_3_3_RI_0)|) & (|marking(network_0_2_RI_2)|<=|marking(poll__networl_0_2_RI_2)|) & (|marking(network_1_1_AskP_3)|<=|marking(poll__networl_1_1_AskP_3)|) & (|marking(network_3_1_AI_1)|<=|marking(poll__networl_3_1_AI_1)|) & (|marking(network_1_1_AnsP_0)|<=|marking(poll__networl_1_1_AnsP_0)|) & (|marking(network_0_2_AnnP_0)|<=|marking(poll__networl_0_2_AnnP_0)|) & (|marking(network_0_0_AnnP_0)|<=|marking(poll__networl_0_0_AnnP_0)|) & (|marking(network_3_1_AnsP_0)|<=|marking(poll__networl_3_1_AnsP_0)|) & (|marking(network_0_2_AI_0)|<=|marking(poll__networl_0_2_AI_0)|) & (|marking(network_2_3_AskP_3)|<=|marking(poll__networl_2_3_AskP_3)|) & (|marking(network_2_3_AnsP_3)|<=|marking(poll__networl_2_3_AnsP_3)|) & (|marking(network_2_3_RI_0)|<=|marking(poll__networl_2_3_RI_0)|) & (|marking(network_0_1_AI_2)|<=|marking(poll__networl_0_1_AI_2)|) & (|marking(network_0_3_AnnP_0)|<=|marking(poll__networl_0_3_AnnP_0)|) & (|marking(network_2_0_AI_2)|<=|marking(poll__networl_2_0_AI_2)|) & (|marking(network_1_2_RI_0)|<=|marking(poll__networl_1_2_RI_0)|) & (|marking(network_2_1_AnsP_2)|<=|marking(poll__networl_2_1_AnsP_2)|) & (|marking(network_2_3_RP_0)|<=|marking(poll__networl_2_3_RP_0)|) & (|marking(network_1_3_AskP_0)|<=|marking(poll__networl_1_3_AskP_0)|) & (|marking(network_0_0_AnnP_2)|<=|marking(poll__networl_0_0_AnnP_2)|) & (|marking(network_1_0_RI_0)|<=|marking(poll__networl_1_0_RI_0)|) & (|marking(network_2_2_RP_2)|<=|marking(poll__networl_2_2_RP_2)|))))


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