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

Execution Outputs of marcie for SimpleLoadBal/05 (P/T)

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

execution on node 31: cluster1u33.lip6.fr (runId=136983930101196_n_31)
=====================================================================
runnning marcie on SimpleLoadBal-PT-05 (ReachabilityMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is SimpleLoadBal-PT-05, examination is ReachabilityMix
=====================================================================

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

START 1369873005

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 59 NrTr: 180)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m0sec


-> reachability set: #nodes 8102 (8.1e+03) #states 116,176 (5)



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

checking: AG [[["lb_load_1_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_2_1" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | [[["lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_5" \in [1, oo) | [[[["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_1_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_2_5" \in [1, oo) | ["lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [["lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_2_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | [["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]]]]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]]]]]]] | "lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo)]]]]]] | "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_2_3" \in [1, oo)]]] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)]] | "lb_load_1_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_load_1_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_2_2" \in [1, oo)]]]] | "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)]]]] | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]]] | "lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]]] & [server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]]]]
normalized: ~ [E [true U ~ [[[server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]] & [[["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | [[["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [["lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_2_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | [["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]]]]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]]]]]]] | "lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo)]]]]]] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)]] | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo)]]]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]]] | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo)]]]] | "lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_37_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | [["lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [[["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [[["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | [[["lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo) | [["lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo) | ["lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo) | "lb_load_2_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo)]] | "lb_load_2_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo)]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo)]]]]]]]]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]]]]]] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)]]] | "lb_load_2_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo)]]]]]]]]]]]]]]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)]]] | [[true & server_waiting_1=server_processed_1] & server_waiting_2=server_processed_2]]]
normalized: ~ [E [true U ~ [[[server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]] | [[["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | [[[["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | [[[[[[[[[[[[[[["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [[["lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [[[[[[[["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | [[[[[[[[["lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | [["lb_load_2_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | "lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo)]] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo)]]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)]]] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo)]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo)]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo)]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_38_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[[["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo) | ["lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo) | [[[["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo) | [[["lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo) | [[["lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_3" \in [1, oo) | [[["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | [[[[["lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo) | ["lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | [[["lb_load_1_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_2_0" \in [1, oo) | "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo)]]]] | "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)]]]]]]]]]]]]]]]]]] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo)]] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)]]] | "lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo)]] | "lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]] | "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]] | "lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo)] | "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)]] & [[true & server_waiting_1=server_processed_1] & server_waiting_2=server_processed_2]]]
normalized: ~ [E [true U ~ [[[server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]] & ~ [["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | [[[["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | [[["lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | [[["lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [[[[[[[[[[[[[[[[[["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | [[[["lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) | "lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo)]]] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo)]]]]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]]] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo)]] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo)]]] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)]]]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_5" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo)]]]]]]]]]

-> the formula is FALSE

FORMULA p_39_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[server_waiting_2=server_processed_2 & [true & server_waiting_1=server_processed_1]] | ~ [[[[[[[["lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo) | [["lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo) | ["lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo) | [[[[[["lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo) | ["lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo) | [["lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [[["lb_load_1_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_2_0" \in [1, oo) | ["lb_load_1_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo) | ["lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [["lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo) | ["lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo) | [[[[["lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | [["lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [[["lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo) | ["lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_2_1" \in [1, oo) | ["lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo) | ["lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo) | [[[["lb_load_2_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | "lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo)]]]]] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo)]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo)]]] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_load_1_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)]]] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)]]]]]]] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)]]] | "lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)]]] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)]] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[~ [["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [[["lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) | [[["lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) | [[["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [[[[[[["lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | [[["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | [[["lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) | [["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | [[[[["lb_load_2_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) | "lb_load_2_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo)]]]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo)]] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)]]]]] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo)]] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo)] | "lb_load_2_0" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo)]]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo)] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo)]] | "lb_load_2_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo)] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo)]]]]]] | "lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo)] | "lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo)]] | "lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo)]]]]]]]] | [server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]]]]]]

-> the formula is FALSE

FORMULA p_40_mix_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[true & server_waiting_1=server_processed_1] & server_waiting_2=server_processed_2]] & ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo) | "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_0" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) && "lb_load_2_2" \in [1, oo)] | "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) && "lb_load_2_5" \in [1, oo)] | "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_4" \in [1, oo)] | "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) && "lb_load_2_3" \in [1, oo)] | "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) && "lb_load_2_1" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[~ [["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_5" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_4" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_2" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_1" \in [1, oo) | ["lb_load_2_1" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_4" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_4" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_2" \in [1, oo) && "lb_load_1_2" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_3" \in [1, oo) && "lb_load_1_0" \in [1, oo) | ["lb_load_2_3" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_3" \in [1, oo) | ["lb_load_2_0" \in [1, oo) && "lb_routing_1_5" \in [1, oo) && "lb_load_1_0" \in [1, oo) | "lb_load_2_4" \in [1, oo) && "lb_routing_1_1" \in [1, oo) && "lb_load_1_4" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [[server_waiting_2=server_processed_2 & [server_waiting_1=server_processed_1 & true]]]]]]]

-> the formula is FALSE

FORMULA p_41_mix_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & [[true & server_notification_ack_2>server_idle_2] & server_notification_ack_1>server_idle_1]] & [[[[[[[[["server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo)]]]]]]]]] & [[server_notification_ack_1>server_idle_1 & [server_notification_ack_2>server_idle_2 & true]] & true]]]]]

-> the formula is FALSE

FORMULA p_42_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & [[true & server_notification_ack_2>server_idle_2] & server_notification_ack_1>server_idle_1]] | [[[[[[[[["server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo)]]]]]]]]] | [[server_notification_ack_1>server_idle_1 & [server_notification_ack_2>server_idle_2 & true]] & true]]]]]

-> the formula is FALSE

FORMULA p_43_mix_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & [[true & server_notification_ack_2>server_idle_2] & server_notification_ack_1>server_idle_1]] & [[[[[[[[["server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo)] | "server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo)] | "server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["server_idle_2" \in [1, oo) && "server_request_3_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_4_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_4_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_2_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_3_1" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_5_1" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_1_2" \in [1, oo) | ["server_idle_2" \in [1, oo) && "server_request_5_2" \in [1, oo) | ["server_idle_1" \in [1, oo) && "server_request_1_1" \in [1, oo) | "server_idle_1" \in [1, oo) && "server_request_2_1" \in [1, oo)]]]]]]]]] & [[server_notification_ack_1>server_idle_1 & [server_notification_ack_2>server_idle_2 & true]] & true]]]]]

-> the formula is FALSE

FORMULA p_44_mix_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m4sec

STOP 1369873009

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

1273 1923 2067 2183 3251 3407 3562 3668 4010 4144 4123 5463 5624 5744 5946 6016 6156 6373 6548 6676 6704 8111 7881 7661 7746 7740 7678 7799 7789 7814 8046 8101
iterations count:32689 (181), effective:1905 (10)

initing FirstDep: 0m0sec


iterations count:180 (1), effective:0 (0)
8219 8073
iterations count:2553 (14), effective:35 (0)

iterations count:180 (1), effective:0 (0)
6883 7906 7881
iterations count:3197 (17), effective:136 (0)
6883 7906 7881
iterations count:3197 (17), effective:136 (0)

iterations count:180 (1), effective:0 (0)
9625 8913 8508 8166
iterations count:4221 (23), effective:167 (0)

iterations count:180 (1), effective:0 (0)

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