Skip to content
GitLab
Closed
Issue created by Alexandre Duret-Lutz@adlOwner

Boolean rewriting as a speedup

Yann Thierry-Mieg complained about the following formula:

f='!((X((F(G((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((("Couple0.state_0>=1")&&("Couple7.state_7>=1"))||(("Couple0.state_0>=1")&&("Couple8.state_8>=1")))||(("Couple0.state_0>=1")&&("Couple9.state_9>=1")))||(("Couple0.state_0>=1")&&("Couple10.state_10>=1")))||(("Couple0.state_0>=1")&&("Couple11.state_11>=1")))||(("Couple6.state_6>=1")&&("Couple13.state_13>=1")))||(("Couple6.state_6>=1")&&("Couple14.state_14>=1")))||(("Couple6.state_6>=1")&&("Couple15.state_15>=1")))||(("Couple6.state_6>=1")&&("Couple16.state_16>=1")))||(("Couple6.state_6>=1")&&("Couple17.state_17>=1")))||(("Couple12.state_12>=1")&&("Couple19.state_19>=1")))||(("Couple12.state_12>=1")&&("Couple20.state_20>=1")))||(("Couple12.state_12>=1")&&("Couple21.state_21>=1")))||(("Couple12.state_12>=1")&&("Couple22.state_22>=1")))||(("Couple12.state_12>=1")&&("Couple23.state_23>=1")))||(("Couple18.state_18>=1")&&("Couple25.state_25>=1")))||(("Couple18.state_18>=1")&&("Couple26.state_26>=1")))||(("Couple18.state_18>=1")&&("Couple27.state_27>=1")))||(("Couple18.state_18>=1")&&("Couple28.state_28>=1")))||(("Couple18.state_18>=1")&&("Couple29.state_29>=1")))||(("Couple24.state_24>=1")&&("Couple31.state_31>=1")))||(("Couple24.state_24>=1")&&("Couple32.state_32>=1")))||(("Couple24.state_24>=1")&&("Couple33.state_33>=1")))||(("Couple24.state_24>=1")&&("Couple34.state_34>=1")))||(("Couple24.state_24>=1")&&("Couple35.state_35>=1")))||(("Couple1.state_1>=1")&&("Couple6.state_6>=1")))||(("Couple1.state_1>=1")&&("Couple8.state_8>=1")))||(("Couple1.state_1>=1")&&("Couple9.state_9>=1")))||(("Couple1.state_1>=1")&&("Couple10.state_10>=1")))||(("Couple1.state_1>=1")&&("Couple11.state_11>=1")))||(("Couple7.state_7>=1")&&("Couple12.state_12>=1")))||(("Couple7.state_7>=1")&&("Couple14.state_14>=1")))||(("Couple7.state_7>=1")&&("Couple15.state_15>=1")))||(("Couple7.state_7>=1")&&("Couple16.state_16>=1")))||(("Couple7.state_7>=1")&&("Couple17.state_17>=1")))||(("Couple13.state_13>=1")&&("Couple18.state_18>=1")))||(("Couple13.state_13>=1")&&("Couple20.state_20>=1")))||(("Couple13.state_13>=1")&&("Couple21.state_21>=1")))||(("Couple13.state_13>=1")&&("Couple22.state_22>=1")))||(("Couple13.state_13>=1")&&("Couple23.state_23>=1")))||(("Couple19.state_19>=1")&&("Couple24.state_24>=1")))||(("Couple19.state_19>=1")&&("Couple26.state_26>=1")))||(("Couple19.state_19>=1")&&("Couple27.state_27>=1")))||(("Couple19.state_19>=1")&&("Couple28.state_28>=1")))||(("Couple19.state_19>=1")&&("Couple29.state_29>=1")))||(("Couple25.state_25>=1")&&("Couple30.state_30>=1")))||(("Couple25.state_25>=1")&&("Couple32.state_32>=1")))||(("Couple25.state_25>=1")&&("Couple33.state_33>=1")))||(("Couple25.state_25>=1")&&("Couple34.state_34>=1")))||(("Couple25.state_25>=1")&&("Couple35.state_35>=1")))||(("Couple2.state_2>=1")&&("Couple6.state_6>=1")))||(("Couple2.state_2>=1")&&("Couple7.state_7>=1")))||(("Couple2.state_2>=1")&&("Couple9.state_9>=1")))||(("Couple2.state_2>=1")&&("Couple10.state_10>=1")))||(("Couple2.state_2>=1")&&("Couple11.state_11>=1")))||(("Couple8.state_8>=1")&&("Couple12.state_12>=1")))||(("Couple8.state_8>=1")&&("Couple13.state_13>=1")))||(("Couple8.state_8>=1")&&("Couple15.state_15>=1")))||(("Couple8.state_8>=1")&&("Couple16.state_16>=1")))||(("Couple8.state_8>=1")&&("Couple17.state_17>=1")))||(("Couple14.state_14>=1")&&("Couple18.state_18>=1")))||(("Couple14.state_14>=1")&&("Couple19.state_19>=1")))||(("Couple14.state_14>=1")&&("Couple21.state_21>=1")))||(("Couple14.state_14>=1")&&("Couple22.state_22>=1")))||(("Couple14.state_14>=1")&&("Couple23.state_23>=1")))||(("Couple20.state_20>=1")&&("Couple24.state_24>=1")))||(("Couple20.state_20>=1")&&("Couple25.state_25>=1")))||(("Couple20.state_20>=1")&&("Couple27.state_27>=1")))||(("Couple20.state_20>=1")&&("Couple28.state_28>=1")))||(("Couple20.state_20>=1")&&("Couple29.state_29>=1")))||(("Couple26.state_26>=1")&&("Couple30.state_30>=1")))||(("Couple26.state_26>=1")&&("Couple31.state_31>=1")))||(("Couple26.state_26>=1")&&("Couple33.state_33>=1")))||(("Couple26.state_26>=1")&&("Couple34.state_34>=1")))||(("Couple26.state_26>=1")&&("Couple35.state_35>=1")))||(("Couple3.state_3>=1")&&("Couple6.state_6>=1")))||(("Couple3.state_3>=1")&&("Couple7.state_7>=1")))||(("Couple3.state_3>=1")&&("Couple8.state_8>=1")))||(("Couple3.state_3>=1")&&("Couple10.state_10>=1")))||(("Couple3.state_3>=1")&&("Couple11.state_11>=1")))||(("Couple9.state_9>=1")&&("Couple12.state_12>=1")))||(("Couple9.state_9>=1")&&("Couple13.state_13>=1")))||(("Couple9.state_9>=1")&&("Couple14.state_14>=1")))||(("Couple9.state_9>=1")&&("Couple16.state_16>=1")))||(("Couple9.state_9>=1")&&("Couple17.state_17>=1")))||(("Couple15.state_15>=1")&&("Couple18.state_18>=1")))||(("Couple15.state_15>=1")&&("Couple19.state_19>=1")))||(("Couple15.state_15>=1")&&("Couple20.state_20>=1")))||(("Couple15.state_15>=1")&&("Couple22.state_22>=1")))||(("Couple15.state_15>=1")&&("Couple23.state_23>=1")))||(("Couple21.state_21>=1")&&("Couple24.state_24>=1")))||(("Couple21.state_21>=1")&&("Couple25.state_25>=1")))||(("Couple21.state_21>=1")&&("Couple26.state_26>=1")))||(("Couple21.state_21>=1")&&("Couple28.state_28>=1")))||(("Couple21.state_21>=1")&&("Couple29.state_29>=1")))||(("Couple27.state_27>=1")&&("Couple30.state_30>=1")))||(("Couple27.state_27>=1")&&("Couple31.state_31>=1")))||(("Couple27.state_27>=1")&&("Couple32.state_32>=1")))||(("Couple27.state_27>=1")&&("Couple34.state_34>=1")))||(("Couple27.state_27>=1")&&("Couple35.state_35>=1")))||(("Couple4.state_4>=1")&&("Couple6.state_6>=1")))||(("Couple4.state_4>=1")&&("Couple7.state_7>=1")))||(("Couple4.state_4>=1")&&("Couple8.state_8>=1")))||(("Couple4.state_4>=1")&&("Couple9.state_9>=1")))||(("Couple4.state_4>=1")&&("Couple11.state_11>=1")))||(("Couple10.state_10>=1")&&("Couple12.state_12>=1")))||(("Couple10.state_10>=1")&&("Couple13.state_13>=1")))||(("Couple10.state_10>=1")&&("Couple14.state_14>=1")))||(("Couple10.state_10>=1")&&("Couple15.state_15>=1")))||(("Couple10.state_10>=1")&&("Couple17.state_17>=1")))||(("Couple16.state_16>=1")&&("Couple18.state_18>=1")))||(("Couple16.state_16>=1")&&("Couple19.state_19>=1")))||(("Couple16.state_16>=1")&&("Couple20.state_20>=1")))||(("Couple16.state_16>=1")&&("Couple21.state_21>=1")))||(("Couple16.state_16>=1")&&("Couple23.state_23>=1")))||(("Couple22.state_22>=1")&&("Couple24.state_24>=1")))||(("Couple22.state_22>=1")&&("Couple25.state_25>=1")))||(("Couple22.state_22>=1")&&("Couple26.state_26>=1")))||(("Couple22.state_22>=1")&&("Couple27.state_27>=1")))||(("Couple22.state_22>=1")&&("Couple29.state_29>=1")))||(("Couple28.state_28>=1")&&("Couple30.state_30>=1")))||(("Couple28.state_28>=1")&&("Couple31.state_31>=1")))||(("Couple28.state_28>=1")&&("Couple32.state_32>=1")))||(("Couple28.state_28>=1")&&("Couple33.state_33>=1")))||(("Couple28.state_28>=1")&&("Couple35.state_35>=1")))||(("Couple5.state_5>=1")&&("Couple6.state_6>=1")))||(("Couple5.state_5>=1")&&("Couple7.state_7>=1")))||(("Couple5.state_5>=1")&&("Couple8.state_8>=1")))||(("Couple5.state_5>=1")&&("Couple9.state_9>=1")))||(("Couple5.state_5>=1")&&("Couple10.state_10>=1")))||(("Couple11.state_11>=1")&&("Couple12.state_12>=1")))||(("Couple11.state_11>=1")&&("Couple13.state_13>=1")))||(("Couple11.state_11>=1")&&("Couple14.state_14>=1")))||(("Couple11.state_11>=1")&&("Couple15.state_15>=1")))||(("Couple11.state_11>=1")&&("Couple16.state_16>=1")))||(("Couple17.state_17>=1")&&("Couple18.state_18>=1")))||(("Couple17.state_17>=1")&&("Couple19.state_19>=1")))||(("Couple17.state_17>=1")&&("Couple20.state_20>=1")))||(("Couple17.state_17>=1")&&("Couple21.state_21>=1")))||(("Couple17.state_17>=1")&&("Couple22.state_22>=1")))||(("Couple23.state_23>=1")&&("Couple24.state_24>=1")))||(("Couple23.state_23>=1")&&("Couple25.state_25>=1")))||(("Couple23.state_23>=1")&&("Couple26.state_26>=1")))||(("Couple23.state_23>=1")&&("Couple27.state_27>=1")))||(("Couple23.state_23>=1")&&("Couple28.state_28>=1")))||(("Couple29.state_29>=1")&&("Couple30.state_30>=1")))||(("Couple29.state_29>=1")&&("Couple31.state_31>=1")))||(("Couple29.state_29>=1")&&("Couple32.state_32>=1")))||(("Couple29.state_29>=1")&&("Couple33.state_33>=1")))||(("Couple29.state_29>=1")&&("Couple34.state_34>=1")))))U((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((("Couple0.state_0>=1")&&("Couple7.state_7>=1"))||(("Couple0.state_0>=1")&&("Couple8.state_8>=1")))||(("Couple0.state_0>=1")&&("Couple9.state_9>=1")))||(("Couple0.state_0>=1")&&("Couple10.state_10>=1")))||(("Couple0.state_0>=1")&&("Couple11.state_11>=1")))||(("Couple6.state_6>=1")&&("Couple13.state_13>=1")))||(("Couple6.state_6>=1")&&("Couple14.state_14>=1")))||(("Couple6.state_6>=1")&&("Couple15.state_15>=1")))||(("Couple6.state_6>=1")&&("Couple16.state_16>=1")))||(("Couple6.state_6>=1")&&("Couple17.state_17>=1")))||(("Couple12.state_12>=1")&&("Couple19.state_19>=1")))||(("Couple12.state_12>=1")&&("Couple20.state_20>=1")))||(("Couple12.state_12>=1")&&("Couple21.state_21>=1")))||(("Couple12.state_12>=1")&&("Couple22.state_22>=1")))||(("Couple12.state_12>=1")&&("Couple23.state_23>=1")))||(("Couple18.state_18>=1")&&("Couple25.state_25>=1")))||(("Couple18.state_18>=1")&&("Couple26.state_26>=1")))||(("Couple18.state_18>=1")&&("Couple27.state_27>=1")))||(("Couple18.state_18>=1")&&("Couple28.state_28>=1")))||(("Couple18.state_18>=1")&&("Couple29.state_29>=1")))||(("Couple24.state_24>=1")&&("Couple31.state_31>=1")))||(("Couple24.state_24>=1")&&("Couple32.state_32>=1")))||(("Couple24.state_24>=1")&&("Couple33.state_33>=1")))||(("Couple24.state_24>=1")&&("Couple34.state_34>=1")))||(("Couple24.state_24>=1")&&("Couple35.state_35>=1")))||(("Couple1.state_1>=1")&&("Couple6.state_6>=1")))||(("Couple1.state_1>=1")&&("Couple8.state_8>=1")))||(("Couple1.state_1>=1")&&("Couple9.state_9>=1")))||(("Couple1.state_1>=1")&&("Couple10.state_10>=1")))||(("Couple1.state_1>=1")&&("Couple11.state_11>=1")))||(("Couple7.state_7>=1")&&("Couple12.state_12>=1")))||(("Couple7.state_7>=1")&&("Couple14.state_14>=1")))||(("Couple7.state_7>=1")&&("Couple15.state_15>=1")))||(("Couple7.state_7>=1")&&("Couple16.state_16>=1")))||(("Couple7.state_7>=1")&&("Couple17.state_17>=1")))||(("Couple13.state_13>=1")&&("Couple18.state_18>=1")))||(("Couple13.state_13>=1")&&("Couple20.state_20>=1")))||(("Couple13.state_13>=1")&&("Couple21.state_21>=1")))||(("Couple13.state_13>=1")&&("Couple22.state_22>=1")))||(("Couple13.state_13>=1")&&("Couple23.state_23>=1")))||(("Couple19.state_19>=1")&&("Couple24.state_24>=1")))||(("Couple19.state_19>=1")&&("Couple26.state_26>=1")))||(("Couple19.state_19>=1")&&("Couple27.state_27>=1")))||(("Couple19.state_19>=1")&&("Couple28.state_28>=1")))||(("Couple19.state_19>=1")&&("Couple29.state_29>=1")))||(("Couple25.state_25>=1")&&("Couple30.state_30>=1")))||(("Couple25.state_25>=1")&&("Couple32.state_32>=1")))||(("Couple25.state_25>=1")&&("Couple33.state_33>=1")))||(("Couple25.state_25>=1")&&("Couple34.state_34>=1")))||(("Couple25.state_25>=1")&&("Couple35.state_35>=1")))||(("Couple2.state_2>=1")&&("Couple6.state_6>=1")))||(("Couple2.state_2>=1")&&("Couple7.state_7>=1")))||(("Couple2.state_2>=1")&&("Couple9.state_9>=1")))||(("Couple2.state_2>=1")&&("Couple10.state_10>=1")))||(("Couple2.state_2>=1")&&("Couple11.state_11>=1")))||(("Couple8.state_8>=1")&&("Couple12.state_12>=1")))||(("Couple8.state_8>=1")&&("Couple13.state_13>=1")))||(("Couple8.state_8>=1")&&("Couple15.state_15>=1")))||(("Couple8.state_8>=1")&&("Couple16.state_16>=1")))||(("Couple8.state_8>=1")&&("Couple17.state_17>=1")))||(("Couple14.state_14>=1")&&("Couple18.state_18>=1")))||(("Couple14.state_14>=1")&&("Couple19.state_19>=1")))||(("Couple14.state_14>=1")&&("Couple21.state_21>=1")))||(("Couple14.state_14>=1")&&("Couple22.state_22>=1")))||(("Couple14.state_14>=1")&&("Couple23.state_23>=1")))||(("Couple20.state_20>=1")&&("Couple24.state_24>=1")))||(("Couple20.state_20>=1")&&("Couple25.state_25>=1")))||(("Couple20.state_20>=1")&&("Couple27.state_27>=1")))||(("Couple20.state_20>=1")&&("Couple28.state_28>=1")))||(("Couple20.state_20>=1")&&("Couple29.state_29>=1")))||(("Couple26.state_26>=1")&&("Couple30.state_30>=1")))||(("Couple26.state_26>=1")&&("Couple31.state_31>=1")))||(("Couple26.state_26>=1")&&("Couple33.state_33>=1")))||(("Couple26.state_26>=1")&&("Couple34.state_34>=1")))||(("Couple26.state_26>=1")&&("Couple35.state_35>=1")))||(("Couple3.state_3>=1")&&("Couple6.state_6>=1")))||(("Couple3.state_3>=1")&&("Couple7.state_7>=1")))||(("Couple3.state_3>=1")&&("Couple8.state_8>=1")))||(("Couple3.state_3>=1")&&("Couple10.state_10>=1")))||(("Couple3.state_3>=1")&&("Couple11.state_11>=1")))||(("Couple9.state_9>=1")&&("Couple12.state_12>=1")))||(("Couple9.state_9>=1")&&("Couple13.state_13>=1")))||(("Couple9.state_9>=1")&&("Couple14.state_14>=1")))||(("Couple9.state_9>=1")&&("Couple16.state_16>=1")))||(("Couple9.state_9>=1")&&("Couple17.state_17>=1")))||(("Couple15.state_15>=1")&&("Couple18.state_18>=1")))||(("Couple15.state_15>=1")&&("Couple19.state_19>=1")))||(("Couple15.state_15>=1")&&("Couple20.state_20>=1")))||(("Couple15.state_15>=1")&&("Couple22.state_22>=1")))||(("Couple15.state_15>=1")&&("Couple23.state_23>=1")))||(("Couple21.state_21>=1")&&("Couple24.state_24>=1")))||(("Couple21.state_21>=1")&&("Couple25.state_25>=1")))||(("Couple21.state_21>=1")&&("Couple26.state_26>=1")))||(("Couple21.state_21>=1")&&("Couple28.state_28>=1")))||(("Couple21.state_21>=1")&&("Couple29.state_29>=1")))||(("Couple27.state_27>=1")&&("Couple30.state_30>=1")))||(("Couple27.state_27>=1")&&("Couple31.state_31>=1")))||(("Couple27.state_27>=1")&&("Couple32.state_32>=1")))||(("Couple27.state_27>=1")&&("Couple34.state_34>=1")))||(("Couple27.state_27>=1")&&("Couple35.state_35>=1")))||(("Couple4.state_4>=1")&&("Couple6.state_6>=1")))||(("Couple4.state_4>=1")&&("Couple7.state_7>=1")))||(("Couple4.state_4>=1")&&("Couple8.state_8>=1")))||(("Couple4.state_4>=1")&&("Couple9.state_9>=1")))||(("Couple4.state_4>=1")&&("Couple11.state_11>=1")))||(("Couple10.state_10>=1")&&("Couple12.state_12>=1")))||(("Couple10.state_10>=1")&&("Couple13.state_13>=1")))||(("Couple10.state_10>=1")&&("Couple14.state_14>=1")))||(("Couple10.state_10>=1")&&("Couple15.state_15>=1")))||(("Couple10.state_10>=1")&&("Couple17.state_17>=1")))||(("Couple16.state_16>=1")&&("Couple18.state_18>=1")))||(("Couple16.state_16>=1")&&("Couple19.state_19>=1")))||(("Couple16.state_16>=1")&&("Couple20.state_20>=1")))||(("Couple16.state_16>=1")&&("Couple21.state_21>=1")))||(("Couple16.state_16>=1")&&("Couple23.state_23>=1")))||(("Couple22.state_22>=1")&&("Couple24.state_24>=1")))||(("Couple22.state_22>=1")&&("Couple25.state_25>=1")))||(("Couple22.state_22>=1")&&("Couple26.state_26>=1")))||(("Couple22.state_22>=1")&&("Couple27.state_27>=1")))||(("Couple22.state_22>=1")&&("Couple29.state_29>=1")))||(("Couple28.state_28>=1")&&("Couple30.state_30>=1")))||(("Couple28.state_28>=1")&&("Couple31.state_31>=1")))||(("Couple28.state_28>=1")&&("Couple32.state_32>=1")))||(("Couple28.state_28>=1")&&("Couple33.state_33>=1")))||(("Couple28.state_28>=1")&&("Couple35.state_35>=1")))||(("Couple5.state_5>=1")&&("Couple6.state_6>=1")))||(("Couple5.state_5>=1")&&("Couple7.state_7>=1")))||(("Couple5.state_5>=1")&&("Couple8.state_8>=1")))||(("Couple5.state_5>=1")&&("Couple9.state_9>=1")))||(("Couple5.state_5>=1")&&("Couple10.state_10>=1")))||(("Couple11.state_11>=1")&&("Couple12.state_12>=1")))||(("Couple11.state_11>=1")&&("Couple13.state_13>=1")))||(("Couple11.state_11>=1")&&("Couple14.state_14>=1")))||(("Couple11.state_11>=1")&&("Couple15.state_15>=1")))||(("Couple11.state_11>=1")&&("Couple16.state_16>=1")))||(("Couple17.state_17>=1")&&("Couple18.state_18>=1")))||(("Couple17.state_17>=1")&&("Couple19.state_19>=1")))||(("Couple17.state_17>=1")&&("Couple20.state_20>=1")))||(("Couple17.state_17>=1")&&("Couple21.state_21>=1")))||(("Couple17.state_17>=1")&&("Couple22.state_22>=1")))||(("Couple23.state_23>=1")&&("Couple24.state_24>=1")))||(("Couple23.state_23>=1")&&("Couple25.state_25>=1")))||(("Couple23.state_23>=1")&&("Couple26.state_26>=1")))||(("Couple23.state_23>=1")&&("Couple27.state_27>=1")))||(("Couple23.state_23>=1")&&("Couple28.state_28>=1")))||(("Couple29.state_29>=1")&&("Couple30.state_30>=1")))||(("Couple29.state_29>=1")&&("Couple31.state_31>=1")))||(("Couple29.state_29>=1")&&("Couple32.state_32>=1")))||(("Couple29.state_29>=1")&&("Couple33.state_33>=1")))||(("Couple29.state_29>=1")&&("Couple34.state_34>=1"))))))'

It has 36 atomic propositions. Running ltl2tgba "$f" takes a long time to run out of memory: the powerset construction (used for WDBA minimization) has to allocate some arrays of 2^36 bits, and several loop in the code will iterate over all 2^36 letters.

ltl2tgba --any --low -f "$f" will return a 3-state automaton instantaneously.

Also ltlfilt -f "$f" --relabel-bool shows that the formula is equivalent to !X(FGa U a) where a is some horrible Boolean combination of atomic proposition. Surely it would be faster to translate !X(FGa U a) and only then replace a by its real value.