MCC'2021- Execution of r035-tajo-162038167600003\nExecution of r035-tajo-162038167600003\n3215.684 461655.00 477890.00 130.50 TTFTFFTFTFTTFFTF normal\nFormatting '/mnt/tpsp/fkordon/mcc2021-input.r035-tajo-162038167600003.qcow2', fmt=qcow2 size=4294967296 backing_file='/mnt/tpsp/fkordon/mcc2021-input.qcow2' encryption=off cluster_size=65536 lazy_refcounts=off\nRun identifier is r035-tajo-162038167600003\n[2021-05-13 08:08:56] [INFO ] Load time of PNML (colored model parsed with PNMLFW) : 583 ms\n[2021-05-13 08:08:56] [INFO ] Imported 15 HL places and 11 HL transitions for a total of 48 PT places and 5438.0 transition bindings in 25 ms.\n[2021-05-13 08:08:56] [INFO ] Unfolded HLPN to a Petri net with 48 places and 288 transitions in 16 ms.\nIncomplete random walk after 100000 steps, including 1110 resets, run finished after 1818 ms. (steps per millisecond=55 ) properties seen :[0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 1, 0, 1, 1, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0]\n[2021-05-13 08:08:58] [INFO ] Flow matrix only has 90 transitions (discarded 198 similar events)\n[2021-05-13 08:08:58] [INFO ] Computed 7 place invariants in 16 ms\n[2021-05-13 08:08:58] [INFO ] [Real]Absence check using 7 positive place invariants in 22 ms returned unsat\n[2021-05-13 08:08:58] [INFO ] [Real]Absence check using 7 positive place invariants in 9 ms returned unsat\n[2021-05-13 08:08:58] [INFO ] [Real]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:08:58] [INFO ] [Real]Absence check using state equation in 47 ms returned sat\n[2021-05-13 08:08:58] [INFO ] [Nat]Absence check using 7 positive place invariants in 19 ms returned sat\n[2021-05-13 08:08:58] [INFO ] [Nat]Absence check using state equation in 48 ms returned sat\n[2021-05-13 08:08:58] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 24 ms.\n[2021-05-13 08:08:59] [INFO ] Added : 77 causal constraints over 16 iterations in 365 ms. Result :sat\n[2021-05-13 08:08:59] [INFO ] Deduced a trap composed of 5 places in 91 ms\n[2021-05-13 08:08:59] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 133 ms\n[2021-05-13 08:08:59] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned sat\n[2021-05-13 08:08:59] [INFO ] [Real]Absence check using state equation in 21 ms returned sat\n[2021-05-13 08:08:59] [INFO ] [Nat]Absence check using state equation in 26 ms returned sat\n[2021-05-13 08:08:59] [INFO ] [Nat]Added 22 Read/Feed constraints in 8 ms returned sat\n[2021-05-13 08:08:59] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 13 ms.\n[2021-05-13 08:09:00] [INFO ] Added : 84 causal constraints over 18 iterations in 461 ms. Result :sat\n[2021-05-13 08:09:00] [INFO ] [Real]Absence check using state equation in 41 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Absence check using 7 positive place invariants in 7 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Absence check using state equation in 34 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Added 22 Read/Feed constraints in 12 ms returned sat\n[2021-05-13 08:09:00] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 23 ms.\n[2021-05-13 08:09:00] [INFO ] Added : 76 causal constraints over 16 iterations in 370 ms. Result :sat\n[2021-05-13 08:09:00] [INFO ] [Real]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Real]Absence check using state equation in 34 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Absence check using 7 positive place invariants in 9 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Absence check using state equation in 41 ms returned sat\n[2021-05-13 08:09:00] [INFO ] [Nat]Added 22 Read/Feed constraints in 7 ms returned sat\n[2021-05-13 08:09:00] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 22 ms.\n[2021-05-13 08:09:01] [INFO ] Added : 74 causal constraints over 16 iterations in 279 ms. Result :sat\n[2021-05-13 08:09:01] [INFO ] Deduced a trap composed of 5 places in 75 ms\n[2021-05-13 08:09:01] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 98 ms\n[2021-05-13 08:09:01] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Real]Adding state equation constraints to refine reachable states.\n[2021-05-13 08:09:01] [INFO ] [Real]Absence check using state equation in 30 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Real]Added 22 Read/Feed constraints in 5 ms returned sat\n[2021-05-13 08:09:01] [INFO ] Solution in real domain found non-integer solution.\n[2021-05-13 08:09:01] [INFO ] [Nat]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Nat]Adding state equation constraints to refine reachable states.\n[2021-05-13 08:09:01] [INFO ] [Nat]Absence check using state equation in 26 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Nat]Added 22 Read/Feed constraints in 6 ms returned sat\n[2021-05-13 08:09:01] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 17 ms.\n[2021-05-13 08:09:01] [INFO ] Added : 74 causal constraints over 20 iterations in 384 ms. Result :sat\n[2021-05-13 08:09:01] [INFO ] Deduced a trap composed of 16 places in 64 ms\n[2021-05-13 08:09:01] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned unsat\n[2021-05-13 08:09:01] [INFO ] [Real]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Real]Absence check using state equation in 36 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Real]Added 22 Read/Feed constraints in 6 ms returned sat\n[2021-05-13 08:09:01] [INFO ] [Nat]Absence check using 7 positive place invariants in 12 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Nat]Absence check using state equation in 41 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Nat]Added 22 Read/Feed constraints in 7 ms returned sat\n[2021-05-13 08:09:02] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 14 ms.\n[2021-05-13 08:09:02] [INFO ] Added : 78 causal constraints over 17 iterations in 349 ms. Result :sat\n[2021-05-13 08:09:02] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned unsat\n[2021-05-13 08:09:02] [INFO ] [Real]Absence check using 7 positive place invariants in 13 ms returned unsat\n[2021-05-13 08:09:02] [INFO ] [Real]Absence check using 7 positive place invariants in 6 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Real]Absence check using state equation in 39 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Nat]Absence check using 7 positive place invariants in 7 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Nat]Absence check using state equation in 27 ms returned sat\n[2021-05-13 08:09:02] [INFO ] [Nat]Added 22 Read/Feed constraints in 5 ms returned sat\n[2021-05-13 08:09:02] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 12 ms.\n[2021-05-13 08:09:02] [INFO ] Added : 73 causal constraints over 15 iterations in 324 ms. Result :sat\n[2021-05-13 08:09:03] [INFO ] Deduced a trap composed of 5 places in 44 ms\n[2021-05-13 08:09:03] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 67 ms\n[2021-05-13 08:09:03] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned unsat\n[2021-05-13 08:09:03] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Real]Absence check using state equation in 29 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Absence check using 7 positive place invariants in 8 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Absence check using state equation in 33 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Added 22 Read/Feed constraints in 6 ms returned sat\n[2021-05-13 08:09:03] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 11 ms.\n[2021-05-13 08:09:03] [INFO ] Added : 79 causal constraints over 16 iterations in 317 ms. Result :sat\n[2021-05-13 08:09:03] [INFO ] Deduced a trap composed of 5 places in 78 ms\n[2021-05-13 08:09:03] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 101 ms\n[2021-05-13 08:09:03] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned unsat\n[2021-05-13 08:09:03] [INFO ] [Real]Absence check using state equation in 25 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Absence check using state equation in 37 ms returned sat\n[2021-05-13 08:09:03] [INFO ] [Nat]Added 22 Read/Feed constraints in 7 ms returned sat\n[2021-05-13 08:09:03] [INFO ] Deduced a trap composed of 15 places in 29 ms\n[2021-05-13 08:09:03] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 36 ms\n[2021-05-13 08:09:03] [INFO ] Added : 73 causal constraints over 15 iterations in 256 ms. Result :sat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned unsat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned unsat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using 7 positive place invariants in 4 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using state equation in 29 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Real]Added 22 Read/Feed constraints in 4 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Nat]Absence check using 7 positive place invariants in 5 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Nat]Absence check using state equation in 26 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Nat]Added 22 Read/Feed constraints in 5 ms returned sat\n[2021-05-13 08:09:04] [INFO ] Deduced a trap composed of 5 places in 33 ms\n[2021-05-13 08:09:04] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 40 ms\n[2021-05-13 08:09:04] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 10 ms.\n[2021-05-13 08:09:04] [INFO ] Added : 84 causal constraints over 17 iterations in 282 ms. Result :sat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Real]Absence check using state equation in 23 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Real]Added 22 Read/Feed constraints in 3 ms returned sat\n[2021-05-13 08:09:04] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 14 ms.\n[2021-05-13 08:09:04] [INFO ] [Nat]Absence check using state equation in 29 ms returned sat\n[2021-05-13 08:09:04] [INFO ] [Nat]Added 22 Read/Feed constraints in 6 ms returned sat\n[2021-05-13 08:09:04] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 11 ms.\n[2021-05-13 08:09:05] [INFO ] Added : 77 causal constraints over 18 iterations in 314 ms. Result :sat\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned unsat\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using 7 positive place invariants in 2 ms returned unsat\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using 7 positive place invariants in 3 ms returned sat\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using state equation in 22 ms returned sat\n[2021-05-13 08:09:05] [INFO ] [Nat]Absence check using 7 positive place invariants in 6 ms returned sat\n[2021-05-13 08:09:05] [INFO ] [Nat]Absence check using state equation in 30 ms returned sat\n[2021-05-13 08:09:05] [INFO ] [Nat]Added 22 Read/Feed constraints in 7 ms returned sat\n[2021-05-13 08:09:05] [INFO ] Computed and/alt/rep : 285/3719/87 causal constraints in 11 ms.\n[2021-05-13 08:09:05] [INFO ] Added : 74 causal constraints over 16 iterations in 256 ms. Result :sat\n[2021-05-13 08:09:05] [INFO ] Deduced a trap composed of 5 places in 52 ms\n[2021-05-13 08:09:05] [INFO ] Trap strengthening (SAT) tested/added 2/1 trap constraints in 96 ms\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using 7 positive place invariants in 15 ms returned unsat\n[2021-05-13 08:09:05] [INFO ] [Real]Absence check using 7 positive place invariants in 5 ms returned unsat\n[2021-05-13 08:09:05] [INFO ] Initial state reduction rules for CTL removed 3 formulas.\n[2021-05-13 08:09:05] [INFO ] Flatten gal took : 68 ms\n[2021-05-13 08:09:05] [INFO ] Flatten gal took : 29 ms\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-15 FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-13 FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-11 TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE\n[2021-05-13 08:09:05] [INFO ] Applying decomposition\n[2021-05-13 08:09:05] [INFO ] Flatten gal took : 28 ms\nConverted graph to binary with : CommandLine [args=[/home/mcc/BenchKit/itstools/plugins/fr.lip6.move.gal.louvain.binaries_1.0.0.202005100927/bin/convert-linux64, -i, /tmp/graph12781006523358732152.txt, -o, /tmp/graph12781006523358732152.bin, -w, /tmp/graph12781006523358732152.weights], workingDir=null]\nBuilt communities with : CommandLine [args=[/home/mcc/BenchKit/itstools/plugins/fr.lip6.move.gal.louvain.binaries_1.0.0.202005100927/bin/louvain-linux64, /tmp/graph12781006523358732152.bin, -l, -1, -v, -w, /tmp/graph12781006523358732152.weights, -q, 0, -e, 0.001], workingDir=null]\n[2021-05-13 08:09:06] [INFO ] Decomposing Gal with order\n[2021-05-13 08:09:06] [INFO ] Rewriting arrays to variables to allow decomposition.\n[2021-05-13 08:09:06] [INFO ] Removed a total of 1201 redundant transitions.\n[2021-05-13 08:09:06] [INFO ] Flatten gal took : 161 ms\n[2021-05-13 08:09:06] [INFO ] Fuse similar labels procedure discarded/fused a total of 133 labels/synchronizations in 14 ms.\n[2021-05-13 08:09:06] [INFO ] Time to serialize gal into /home/mcc/execution/CTLCardinality.pnml.gal : 6 ms\n[2021-05-13 08:09:06] [INFO ] Time to serialize properties into /home/mcc/execution/CTLCardinality.ctl : 6 ms\noriginal formula: AF(EX((((((((((((((((((gu1.SORTI_A_0+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)>=27) + EG((gi2.gu3.SORTI_B_0<=((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0))))))\n=> equivalent forward existential formula: [FwdG(Init,!(EX((((((((((((((((((gu1.SORTI_A_0+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)>=27) + EG((gi2.gu3.SORTI_B_0<=((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)))))))] = FALSE\nReverse transition relation is NOT exact ! Due to transitions gu1.liberation_A, enregistrement_AcA10, basculements0, basculements1, liberation_B, enregistrement_BcB6, altern_cpts0cpt10, altern_cpts1cpt10, timeout_As0cA0cB9cpt3, timeout_As0cA0cB9cpt10, timeout_Bs1cA5cB0cpt3, timeout_Bs1cA5cB0cpt10, Intersection with reachable at each step enabled. (destroyed/reverse/intersect/total) :0/4/12/16\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-00 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: (((AG(((((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.CAPACITE_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)<=gu1.ROUTE_B_0)) + !(EG(TRUE))) + !(EX(EG(E((((((((((((((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gu1.ROUTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)>=14) U ((((gu1.SUR_PONT_A_0+gu1.SORTI_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=8)))))) + EG(TRUE))\n=> equivalent forward existential formula: [FwdG(EY(((Init * !(EG(TRUE))) * !((!(E(TRUE U !(((((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.CAPACITE_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)<=gu1.ROUTE_B_0)))) + !(EG(TRUE)))))),E((((((((((((((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gu1.ROUTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)>=14) U ((((gu1.SUR_PONT_A_0+gu1.SORTI_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=8)))] = FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-01 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: AX(!(EG(AX((((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)<=5)))))\n=> equivalent forward existential formula: [FwdG(EY(Init),!(EX(!((((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)<=5)))))] = FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-02 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: AG(EF(((((gi2.gu4.ATTENTE_A_0+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_B_0)>=5)||((((((((((((((((((((((((((((((((((((((((gu1.ROUTE_B_0+gu1.CAPACITE_0)+gu1.SORTI_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)>=27))))\n=> equivalent forward existential formula: [(FwdU(Init,TRUE) * !(E(TRUE U ((((gi2.gu4.ATTENTE_A_0+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_B_0)>=5)||((((((((((((((((((((((((((((((((((((((((gu1.ROUTE_B_0+gu1.CAPACITE_0)+gu1.SORTI_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)>=27)))))] = FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-03 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: (EG(E(((EF((((((((((((((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu3.SORTI_B_0)+gi2.gu4.ATTENTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)>=20)) * AX(((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SORTI_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)<=17))) * AF(((gu1.SORTI_A_0+gu1.CAPACITE_0)>=1))) U ((EG((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gu1.SUR_PONT_A_0)+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.CAPACITE_0)<=(((((((((((((gu1.CAPACITE_0+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SUR_PONT_A_0)+gu1.ROUTE_B_0))) * EG(((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)<=((((((((((((((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)))) * (((((((((((((((((((((((((gu1.SORTI_A_0+gu1.SUR_PONT_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.SUR_PONT_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10))))) * AF(AG((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)>20))))\n=> equivalent forward existential formula: ([(Init * !(EG(E(((E(TRUE U (((((((((((((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu3.SORTI_B_0)+gi2.gu4.ATTENTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)>=20)) * !(EX(!(((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SORTI_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)<=17))))) * !(EG(!(((gu1.SORTI_A_0+gu1.CAPACITE_0)>=1))))) U ((EG((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gu1.SUR_PONT_A_0)+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.CAPACITE_0)<=(((((((((((((gu1.CAPACITE_0+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SUR_PONT_A_0)+gu1.ROUTE_B_0))) * EG(((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)<=((((((((((((((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)))) * (((((((((((((((((((((((((gu1.SORTI_A_0+gu1.SUR_PONT_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.SUR_PONT_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)))))))] = FALSE * [FwdG(Init,!(!(E(TRUE U !((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)>20))))))] = FALSE)\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-04 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: A(E((((((((((((((((((((((((((((((((((gu1.SORTI_A_0+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CAPACITE_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_B_0)<=12) + E(E((((((((((((((((((((gu1.CAPACITE_0+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.ROUTE_B_0)+gi0.gu0.SUR_PONT_B_0)<=((((((((((((((((((((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gu1.ROUTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.ROUTE_A_0)+gi0.gu0.SUR_PONT_B_0)) U ((((((((((((((((((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu3.SORTI_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)<=((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0))) U (((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.SORTI_B_0)<=((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)))) U EX(TRUE)) U ((((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)<=6))\n=> equivalent forward existential formula: [((Init * !(EG(!(((((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)<=6))))) * !(E(!(((((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)<=6)) U (!(E((((((((((((((((((((((((((((((((((gu1.SORTI_A_0+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CAPACITE_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_B_0)<=12) + E(E((((((((((((((((((((gu1.CAPACITE_0+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.ROUTE_B_0)+gi0.gu0.SUR_PONT_B_0)<=((((((((((((((((((((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)+gu1.ROUTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.ROUTE_A_0)+gi0.gu0.SUR_PONT_B_0)) U ((((((((((((((((((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu3.SORTI_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)<=((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0))) U (((((((((((((((((((((gi2.gu4.ATTENTE_B_0+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.SORTI_B_0)<=((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)))) U EX(TRUE))) * !(((((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)<=6))))))] != FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-05 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: (!(AX(FALSE)) * EF(EG(TRUE)))\n=> equivalent forward existential formula: [FwdG(FwdU((Init * !(!(EX(!(FALSE))))),TRUE),TRUE)] != FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-06 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: AF((((((((((((((((((((((((((((((((((((((((gu1.CAPACITE_0+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)<=((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)) + ((EF((((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.ROUTE_A_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.SUR_PONT_A_0)<=(((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu3.SORTI_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.ROUTE_A_0))) * EF((((((((((((((((((((((((((((((gu1.SORTI_A_0+gu1.CAPACITE_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_B_0)<=(((gu1.ROUTE_B_0+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)))) * (((((((((((((((((((((((((((((gu1.SUR_PONT_A_0+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.SORTI_B_0)+gu1.ROUTE_B_0)<12))))\n=> equivalent forward existential formula: [FwdG(Init,!((((((((((((((((((((((((((((((((((((((((gu1.CAPACITE_0+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)<=((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.ROUTE_B_0)) + ((E(TRUE U (((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.ROUTE_A_0)+gu1.ROUTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.SUR_PONT_A_0)<=(((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu3.SORTI_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.ROUTE_A_0))) * E(TRUE U (((((((((((((((((((((((((((((gu1.SORTI_A_0+gu1.CAPACITE_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_B_0)<=(((gu1.ROUTE_B_0+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)))) * (((((((((((((((((((((((((((((gu1.SUR_PONT_A_0+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu3.SORTI_B_0)+gu1.ROUTE_B_0)<12)))))] = FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-07 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: A((!(EX(AX(FALSE))) * AF(AG((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SORTI_A_0)+gu1.CAPACITE_0)+gu1.SUR_PONT_A_0)<=(((((gu1.CAPACITE_0+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_B_0)+gi2.gu4.ATTENTE_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0))))) U !(A(((EX(((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)<=16)) * (((((((gu1.SUR_PONT_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)<=((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0))) + EF((((((((((((((((((((gu1.SUR_PONT_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=7)||((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)>=29)))) U (((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + AG((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1))))))))\n=> equivalent forward existential formula: [((Init * !(EG(!(!(!((E(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))) U (!(((EX(((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)<=16)) * (((((((gu1.SUR_PONT_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)<=((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0))) + E(TRUE U (((((((((((((((((((gu1.SUR_PONT_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=7)||((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)>=29))))) * !((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))))) + EG(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))))))))))) * !(E(!(!(!((E(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))) U (!(((EX(((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)<=16)) * (((((((gu1.SUR_PONT_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)<=((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0))) + E(TRUE U (((((((((((((((((((gu1.SUR_PONT_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=7)||((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)>=29))))) * !((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))))) + EG(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1))))))))))))) U (!((!(EX(!(EX(!(FALSE))))) * !(EG(!(!(E(TRUE U !((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SORTI_A_0)+gu1.CAPACITE_0)+gu1.SUR_PONT_A_0)<=(((((gu1.CAPACITE_0+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_B_0)+gi2.gu4.ATTENTE_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0)))))))))) * !(!(!((E(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))) U (!(((EX(((((((gi2.gu4.ATTENTE_B_0+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)<=16)) * (((((((gu1.SUR_PONT_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)<=((((((((((((((((((((((((((((((gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_A_0)+gu1.SORTI_A_0)+gu1.ROUTE_B_0))) + E(TRUE U (((((((((((((((((((gu1.SUR_PONT_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=7)||((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)>=29))))) * !((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))))) + EG(!((((EG(((((((gi0.gu0.SUR_PONT_B_0+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SORTI_A_0)<=1)) * ((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)>1)) * ((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)>(((((((((((((((((((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0))) + !(E(TRUE U !((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gu1.SORTI_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_A_0)>=1)&&((((((((((((((((((gu1.ROUTE_A_0+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)<=(((((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu4.ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)))))))))))))))))] != FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-08 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: (!(AF(E((!(AG((((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.SORTI_A_0)+gu1.ROUTE_A_0)+gu1.ROUTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gu1.CAPACITE_0)))) + (((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)<=(((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10))) U ((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.SUR_PONT_B_0)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=(((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gu1.SUR_PONT_A_0)+gu1.CAPACITE_0)+gu1.SORTI_A_0)) + (EF((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=9)) * EX((((((((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.ROUTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)<=(((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)))))))) + (!(AG((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)>=15))) * !(EF((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_B_0)+gu1.SUR_PONT_A_0)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SORTI_A_0)<=((((((((((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10))&&((gu1.SORTI_A_0+gu1.SUR_PONT_A_0)<=(((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_B_0)))))))\n=> equivalent forward existential formula: ([((Init * !(!(!(EG(!(E((!(!(E(TRUE U !((((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.SORTI_A_0)+gu1.ROUTE_A_0)+gu1.ROUTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gu1.CAPACITE_0)))))) + (((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)<=(((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10))) U ((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.SUR_PONT_B_0)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=(((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gu1.SUR_PONT_A_0)+gu1.CAPACITE_0)+gu1.SORTI_A_0)) + (E(TRUE U (((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=9)) * EX((((((((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.ROUTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)<=(((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)))))))))))) * !(E(TRUE U !((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)>=15)))))] = FALSE * [(FwdU((Init * !(!(!(EG(!(E((!(!(E(TRUE U !((((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gu1.SORTI_A_0)+gu1.ROUTE_A_0)+gu1.ROUTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.SUR_PONT_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(((((((((((((((((gi2.gu4.ATTENTE_B_0+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi2.gu4.ATTENTE_A_0)+gu1.CAPACITE_0)))))) + (((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)<=(((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10))) U ((((((((((((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.SUR_PONT_B_0)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=(((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.ATTENTE_A_0)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gi2.gu3.SORTI_B_0)+gu1.SUR_PONT_A_0)+gu1.CAPACITE_0)+gu1.SORTI_A_0)) + (E(TRUE U (((gi0.gu0.SUR_PONT_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=9)) * EX((((((((((((((((((((((((((((((((gi2.gu3.SORTI_B_0+gu1.ROUTE_A_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.ATTENTE_B_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)<=(((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_B_0)+gi2.gu3.SORTI_B_0)))))))))))),TRUE) * (((((((((((((((((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_B_0)+gu1.SUR_PONT_A_0)+gu1.CAPACITE_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SORTI_A_0)<=((((((((((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10))&&((gu1.SORTI_A_0+gu1.SUR_PONT_A_0)<=(((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.CAPACITE_0)+gi2.gu4.ATTENTE_B_0))))] = FALSE)\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-09 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-10 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: AX(E(((AG(((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)<=(gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1))) * ((((((((((((((((((((((((((((((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu3.SORTI_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)<=(((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1))) * EF((((((((((((((((((((gu1.ROUTE_A_0+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_A_0)<=((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_B_0)))) U (AG((((((((((((((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)<=((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0))||((gi2.gu3.SORTI_B_0+gu1.ROUTE_B_0)<=6))) * EG(AF((((gu1.ROUTE_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_B_0)))))))\n=> equivalent forward existential formula: [(EY(Init) * !(E(((!(E(TRUE U !(((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)<=(gi0.gu2.CONTROLEUR_0+gi0.gu2.CONTROLEUR_1))))) * ((((((((((((((((((((((((((((((((((((((((((gu1.SORTI_A_0+gu1.CHOIX_0)+gu1.CHOIX_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu3.SORTI_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_A_0)<=(((((((((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu3.SORTI_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gu1.ROUTE_B_0)+gi0.gu0.SUR_PONT_B_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1))) * E(TRUE U (((((((((((((((((((gu1.ROUTE_A_0+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CAPACITE_0)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_A_0)<=((gu1.SUR_PONT_A_0+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_B_0)))) U (!(E(TRUE U !((((((((((((((((((((((((((((((((((((((((((gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)+gu1.SUR_PONT_A_0)+gi2.gu3.COMPTEUR_0)+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu0.SUR_PONT_B_0)+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)<=((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gu1.CAPACITE_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.SORTI_A_0)+gu1.ROUTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gi2.gu4.ATTENTE_B_0)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0))||((gi2.gu3.SORTI_B_0+gu1.ROUTE_B_0)<=6))))) * EG(!(EG(!((((gu1.ROUTE_B_0+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=((((((((((((((gi2.gu3.COMPTEUR_0+gi2.gu3.COMPTEUR_1)+gi2.gu3.COMPTEUR_2)+gi2.gu3.COMPTEUR_3)+gi2.gu3.COMPTEUR_4)+gi2.gu3.COMPTEUR_5)+gi2.gu3.COMPTEUR_6)+gi2.gu3.COMPTEUR_7)+gi2.gu3.COMPTEUR_8)+gi2.gu3.COMPTEUR_9)+gi2.gu3.COMPTEUR_10)+gu1.SORTI_A_0)+gi2.gu4.ATTENTE_A_0)+gu1.SUR_PONT_A_0)+gi2.gu4.ATTENTE_B_0))))))))))] = FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-12 FALSE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\noriginal formula: !(AF((AG((!(AF(((((((((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.CAPACITE_0)<=((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)))) + (EG((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)<=((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gu1.CAPACITE_0))) * EX(((((((((((((gi0.gu0.SUR_PONT_B_0+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=((((((((((((((gu1.SUR_PONT_A_0+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)))))) + EX(A(((((((((gu1.SORTI_A_0+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.CAPACITE_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=1) U (((((((((((((((gi2.gu4.ATTENTE_A_0+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1)))))))\n=> equivalent forward existential formula: [FwdG(Init,!((!(E(TRUE U !((!(!(EG(!(((((((((((gi0.gu0.SUR_PONT_B_0+gi2.gu4.ATTENTE_B_0)+gu1.ROUTE_A_0)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gu1.SORTI_A_0)+gu1.CAPACITE_0)<=((((((((((((((((((((((((((((((gi0.gu0.NB_ATTENTE_A_0+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.SORTI_A_0)+gi0.gu0.SUR_PONT_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_A_0)+gu1.NB_ATTENTE_B_0)+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu3.SORTI_B_0)))))) + (EG((((((gu1.CHOIX_0+gu1.CHOIX_1)+gi2.gu4.ATTENTE_A_0)+gu1.ROUTE_A_0)+gu1.SUR_PONT_A_0)<=((((((((((((((((((((((((((((((gu1.NB_ATTENTE_B_0+gu1.NB_ATTENTE_B_1)+gu1.NB_ATTENTE_B_2)+gu1.NB_ATTENTE_B_3)+gu1.NB_ATTENTE_B_4)+gu1.NB_ATTENTE_B_5)+gu1.NB_ATTENTE_B_6)+gu1.NB_ATTENTE_B_7)+gu1.NB_ATTENTE_B_8)+gu1.NB_ATTENTE_B_9)+gu1.NB_ATTENTE_B_10)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gu1.CHOIX_0)+gu1.CHOIX_1)+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.ATTENTE_B_0)+gu1.CAPACITE_0))) * EX(((((((((((((gi0.gu0.SUR_PONT_B_0+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=((((((((((((((gu1.SUR_PONT_A_0+gu1.ROUTE_A_0)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)))))))) + EX(!((E(!((((((((((((((((gi2.gu4.ATTENTE_A_0+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1))) U (!(((((((((gu1.SORTI_A_0+gu1.ROUTE_A_0)+gi2.gu4.ATTENTE_B_0)+gu1.CAPACITE_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi2.gu4.VIDANGE_0)+gi2.gu4.VIDANGE_1)<=1)) * !((((((((((((((((gi2.gu4.ATTENTE_A_0+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1))))) + EG(!((((((((((((((((gi2.gu4.ATTENTE_A_0+gu1.ROUTE_B_0)+gi0.gu2.CONTROLEUR_0)+gi0.gu2.CONTROLEUR_1)+gi0.gu0.NB_ATTENTE_A_0)+gi0.gu0.NB_ATTENTE_A_1)+gi0.gu0.NB_ATTENTE_A_2)+gi0.gu0.NB_ATTENTE_A_3)+gi0.gu0.NB_ATTENTE_A_4)+gi0.gu0.NB_ATTENTE_A_5)+gi0.gu0.NB_ATTENTE_A_6)+gi0.gu0.NB_ATTENTE_A_7)+gi0.gu0.NB_ATTENTE_A_8)+gi0.gu0.NB_ATTENTE_A_9)+gi0.gu0.NB_ATTENTE_A_10)<=(gi2.gu4.VIDANGE_0+gi2.gu4.VIDANGE_1))))))))))] != FALSE\nFORMULA BridgeAndVehicles-COL-V10P10N10-CTLCardinality-14 TRUE TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN\necho " Run identifier is r035-tajo-162038167600003"