stats=%s unnecessary slow
This is related to #268 (closed) because it uses the same formula, but the issue discussed here is different.
With
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"))))))'
The following function prints a 3-state automaton instantaneously:
ltl2tgba --low --any "$f"
but adding --stats=%s
to just display the number of states takes a very long time (I did not wait until completion).
I suspect we compute the number of transitions even when %t
is not used.