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=CTLFireability
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 CTLFireability'
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 28: cluster1u30.lip6.fr (runId=136959876701535_n_28)
=====================================================================
runnning marcie on NeoElection-PT-3 (CTLFireability)
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 CTLFireability
=====================================================================

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

START 1369630828

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 972 NrTr: 1016)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m7sec


-> reachability set: #nodes 19347 (1.9e+04) #states 974,325 (5)



starting CTL model checker
--------------------------

checking: AG [[[[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | [[["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | [["network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["masterState_3_T_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[[["network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [["masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[[[[["masterState_2_F_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]] | "masterState_0_F_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)] | "masterState_3_F_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]] | "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)]]]]] | "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)]] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)] | "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo)] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]]]]]]]]]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)]] | "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]] | "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] & ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_RP_0" \in [1, oo) | [[[["poll__handlingMessage_1" \in [1, oo) && "network_1_0_RP_0" \in [1, oo) | ["network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_RP_0" \in [1, oo) | ["network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo)]]]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_RP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_RP_0" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[[[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | [[["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | [["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | [[[["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | [[[[[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo)]] | "masterState_0_F_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)]]]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)]]]]] | "masterState_0_F_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo)]]]]]]]]]]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] & ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_RP_0" \in [1, oo) | [[[["poll__handlingMessage_1" \in [1, oo) && "network_1_0_RP_0" \in [1, oo) | ["network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_RP_0" \in [1, oo) | ["network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo)]]]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_RP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_RP_0" \in [1, oo)]]]]]]]]

-> the formula is FALSE

FORMULA p_1841_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m5sec

checking: AF [[[["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) | ["network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[[["network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | [["masterState_0_F_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | [["network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [["network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [[["network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [["network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [[[[["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | [[[["masterState_0_F_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["masterState_1_F_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[["masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]] | "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]]] | "masterState_0_F_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "masterState_3_F_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)]]]] | "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "masterState_3_T_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)]] | "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]] | "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]]]]]]]]]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]]] | "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]]] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)]]]]]]]]]] | "masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]] | "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "masterState_0_F_3" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)]]] | "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | [[[[[["network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "network_3_0_RP_0" \in [1, oo) | ["network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo) | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo)]]] | "network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]]] | "network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)] | "network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_3_3_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_1_2_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]]
normalized: ~ [EG [~ [[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | [[[[[["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | [["masterState_0_F_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["masterState_3_T_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]] | "masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]]]]]]]]]]]]]]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]]]]]]]]]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]]] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]] | "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "masterState_3_F_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)]] | "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | ["network_1_2_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_3_3_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[["network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [["network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_RP_0" \in [1, oo) | ["network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo)]]]] | "network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]]] | "network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)] | "network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1842_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[["network_1_2_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_3_3_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_0_3_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo)]]]]]]]]]]]]]]] & ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | [[[[[[[[[[[[[[["masterState_2_T_0" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | [["masterState_3_T_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[[[[[[[[[[[[["network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [["network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | [["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | "masterState_3_F_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]] | "masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)] | "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "masterState_3_F_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)]]] | "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]]] | "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)] | "masterState_2_F_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "masterState_3_T_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)]]] | "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: EG [[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | [[[[[[[[[[[[[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | [[[[[[[[[[[[[[["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | [["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | [["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo)]]] | "masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]] | "masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] & [[[[[[[[[[[[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_2_RP_0" \in [1, oo) | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_RP_0" \in [1, oo)] | "network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_3_1_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_3_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_3_3_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_1_2_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1843_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[["poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo) | ["network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_RP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_RP_0" \in [1, oo) | ["network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_RP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_RP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_RP_0" \in [1, oo) | ["network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_2_0_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | "network_3_2_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]]]]]]]]]]]]] | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | [[[["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) | [["masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | ["masterState_3_F_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[[[[[[[["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | [[[[[["network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]]]]]]] | "masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "masterState_1_F_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)] | "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo)]]]] | "masterState_0_T_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]]]]]
normalized: E [true U [[[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | [["masterState_0_T_3" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [[[["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) | [[[[[[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | "masterState_0_F_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)]]] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo)]]]] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | [[[[[[[[[[[[[[["network_3_2_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | "network_2_0_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_RP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_RP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_RP_0" \in [1, oo)] | "network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_RP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_RP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)] | "network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo)]]]

-> the formula is FALSE

FORMULA p_1844_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[~ [[["masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [["network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["masterState_1_F_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[[["network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | [[[[[[[[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | [[["masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | [[[["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | ["network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [[[["masterState_1_F_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo) | [[["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | [["network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [["network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [[[["network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | [["masterState_1_F_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [["network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo) | [["masterState_1_T_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | ["masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)]]]]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo)]]]]]]]]]]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_T_3" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)]]] | "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]] | "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)]] | "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]] | "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)]]]]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo)]]]]]]] | "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_1" \in [1, oo)] | "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "masterState_1_F_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)]]] | "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)]]]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)]] | "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]] & EG [["poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo) | [["network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[[["network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | [[[["network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | ["network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["network_3_2_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo) | "network_2_0_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_RP_0" \in [1, oo)] | "network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]]] | "network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo)]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo)]]]]]
normalized: EG [[EG [[["poll__handlingMessage_3" \in [1, oo) && "network_3_3_RP_0" \in [1, oo) | [[["poll__handlingMessage_0" \in [1, oo) && "network_0_3_RP_0" \in [1, oo) | ["network_1_3_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | ["network_1_0_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo) | [[["network_0_2_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["network_2_2_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_RP_0" \in [1, oo) | [[["network_2_0_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo) | "network_3_2_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)] | "network_2_1_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_3_0_RP_0" \in [1, oo) && "poll__handlingMessage_3" \in [1, oo)]]]] | "network_2_3_RP_0" \in [1, oo) && "poll__handlingMessage_2" \in [1, oo)] | "network_0_1_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]]]] | "network_1_1_RP_0" \in [1, oo) && "poll__handlingMessage_1" \in [1, oo)] | "network_0_0_RP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_2_RP_0" \in [1, oo)]] & ~ [["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | [["poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | [[[[[["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) && "masterState_1_T_3" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) | [[["masterState_0_F_2" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "masterState_3_T_2" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo) | [[[[[[["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo) | [[[[[["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) | ["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | [[[[["poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | ["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [["masterState_0_F_1" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) | [[["masterState_0_F_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) | ["poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo) | ["poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) | [["poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) | [["masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | [[[["poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) | [["poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) | [[[[[[[[[[["poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) | [[[[["poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) | [[[[[[[[[["poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo) | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo) && "masterState_1_F_2" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "masterState_0_F_2" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_F_0" \in [1, oo)]]] | "poll__handlingMessage_2" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo) && "masterState_2_F_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_3_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_3" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_T_0" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)]] | "masterState_0_F_1" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_F_3" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_3_AnnP_0" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo)]]]] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_1" \in [1, oo)]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_T_2" \in [1, oo)]]] | "masterState_0_T_3" \in [1, oo) && "network_0_0_AnnP_0" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)]]]] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_F_2" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_T_1" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_3_AnnP_0" \in [1, oo)]]]] | "poll__handlingMessage_2" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "masterState_0_T_1" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_0_AnnP_0" \in [1, oo) && "masterState_1_T_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_F_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)]]] | "poll__handlingMessage_0" \in [1, oo) && "network_0_2_AnnP_0" \in [1, oo) && "masterState_0_T_2" \in [1, oo)] | "masterState_0_T_3" \in [1, oo) && "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_1" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "network_2_0_AnnP_0" \in [1, oo) && "masterState_2_T_0" \in [1, oo)] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "network_2_1_AnnP_0" \in [1, oo)]]]]]]]]]] | "poll__handlingMessage_1" \in [1, oo) && "network_1_1_AnnP_0" \in [1, oo) && "masterState_1_T_2" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_0_AnnP_0" \in [1, oo) && "masterState_3_F_0" \in [1, oo)]]]] | "poll__handlingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "network_1_2_AnnP_0" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "network_3_1_AnnP_0" \in [1, oo)] | "poll__handlingMessage_0" \in [1, oo) && "network_0_1_AnnP_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_2_AnnP_0" \in [1, oo) && "masterState_3_F_1" \in [1, oo)] | "poll__handlingMessage_3" \in [1, oo) && "network_3_3_AnnP_0" \in [1, oo) && "masterState_3_T_0" \in [1, oo)]] | "poll__handlingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "network_2_2_AnnP_0" \in [1, oo)]]]]]

.
EG iterations: 1
.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1845_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[["electionInit_1" \in [1, oo) | ["electionInit_3" \in [1, oo) | "electionInit_2" \in [1, oo)]] | "electionInit_0" \in [1, oo)] & ["negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo) | ["masterState_1_F_0" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) | [[[[[["negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "masterState_1_F_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo) | [["negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_0" \in [1, oo) | [["negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo) | ["negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo) | ["stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "masterState_0_F_1" \in [1, oo) | "poll__waitingMessage_3" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "masterState_3_F_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)]]] | "stage_0_NEG" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "masterState_0_F_2" \in [1, oo)]] | "masterState_2_F_1" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo)]] | "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)] | "negotiation_1_3_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo)] | "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo)] | "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo)] | "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[[[[["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) | ["stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) | ["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | [["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) | [["masterState_0_F_2" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | [[["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_3" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) | "masterState_0_F_1" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo)] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo)] | "stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo)]] | "masterState_0_F_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo)]] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_1" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo)]]]]]] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo)] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo)] | "stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo)] & ["electionInit_0" \in [1, oo) | [["electionInit_2" \in [1, oo) | "electionInit_3" \in [1, oo)] | "electionInit_1" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_1886_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[["electionInit_1" \in [1, oo) | ["electionInit_2" \in [1, oo) | "electionInit_3" \in [1, oo)]] | "electionInit_0" \in [1, oo)] | [["negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo) | ["negotiation_2_3_DONE" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo) | ["negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo) | ["poll__waitingMessage_1" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "stage_1_NEG" \in [1, oo) | [["stage_1_NEG" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) | ["poll__waitingMessage_3" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "stage_3_NEG" \in [1, oo) | ["negotiation_1_3_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "masterState_1_F_1" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) | [["negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_2" \in [1, oo) | [["negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo) | ["masterState_3_F_3" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo) | "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_1" \in [1, oo)]] | "stage_3_NEG" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo)]] | "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_0" \in [1, oo)]]]]] | "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo)]]]]] | "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | [[[[["stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) | [[[[["masterState_0_F_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | [["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | [["masterState_0_F_1" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | "stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_3" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo)] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo)]] | "masterState_0_F_2" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo)]] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo)] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_1" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo)] | "stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo)] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo)]] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo)] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo)] | "stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "masterState_2_F_3" \in [1, oo)] | "stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo)]] | ["electionInit_0" \in [1, oo) | [["electionInit_3" \in [1, oo) | "electionInit_2" \in [1, oo)] | "electionInit_1" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_1887_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[[[[[[[[[[[[[["negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "masterState_3_F_3" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo) | "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_1" \in [1, oo)] | "stage_2_NEG" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo)] | "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)] | "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_2" \in [1, oo)] | "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "masterState_0_F_0" \in [1, oo)] | "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo)] | "masterState_1_F_1" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo)] | "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)] | "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo)] | "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "stage_0_NEG" \in [1, oo)] | "stage_1_NEG" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo)] | "negotiation_2_3_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo)] | "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "stage_2_NEG" \in [1, oo)] | "negotiation_1_3_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "stage_1_NEG" \in [1, oo)] | "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "stage_3_NEG" \in [1, oo)] & [["electionInit_1" \in [1, oo) | ["electionInit_2" \in [1, oo) | "electionInit_3" \in [1, oo)]] | "electionInit_0" \in [1, oo)]]]
normalized: E [true U [["electionInit_0" \in [1, oo) | ["electionInit_1" \in [1, oo) | ["electionInit_3" \in [1, oo) | "electionInit_2" \in [1, oo)]]] & ["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_2" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_0" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "masterState_2_F_3" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "masterState_2_F_2" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_3" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) | ["stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "masterState_0_F_3" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_2" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) | ["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_1" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | ["stage_1_NEG" \in [1, oo) && "poll__waitingMessage_1" \in [1, oo) && "negotiation_1_3_DONE" \in [1, oo) && "masterState_1_F_1" \in [1, oo) && "negotiation_1_1_DONE" \in [1, oo) && "negotiation_1_2_DONE" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_1" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) | ["masterState_0_F_0" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | ["masterState_0_F_2" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) | ["stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_0" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo) | ["stage_2_NEG" \in [1, oo) && "poll__waitingMessage_2" \in [1, oo) && "masterState_2_F_0" \in [1, oo) && "negotiation_2_1_DONE" \in [1, oo) && "negotiation_2_3_DONE" \in [1, oo) && "negotiation_2_2_DONE" \in [1, oo) | ["masterState_0_F_1" \in [1, oo) && "stage_0_NEG" \in [1, oo) && "poll__waitingMessage_0" \in [1, oo) && "negotiation_0_2_DONE" \in [1, oo) && "negotiation_0_3_DONE" \in [1, oo) && "negotiation_0_1_DONE" \in [1, oo) | "stage_3_NEG" \in [1, oo) && "poll__waitingMessage_3" \in [1, oo) && "masterState_3_F_3" \in [1, oo) && "negotiation_3_3_DONE" \in [1, oo) && "negotiation_3_1_DONE" \in [1, oo) && "negotiation_3_2_DONE" \in [1, oo)]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1888_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m23sec

STOP 1369630851

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


initing FirstDep: 0m0sec

2413 2983 4406 5170 8021 8230 9312 9485 12146 12633 13261 15641 17360 19352
iterations count:14854 (14), effective:108 (0)

initing FirstDep: 0m0sec

19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:3 (0)

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