25 Apr
                
                    2019
                
            
            
                25 Apr
                
                '19
                
            
            
            
        
    
                9:14 a.m.
            
        Hi Alexandre, I run the experiments and found two formulas where ltl2tgba did not finish correctly. The formulas were & | G F p0 F G p1 | G F ! p1 F G p2 & & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0 The according command-line was: ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA} Output was: ltl2tgba: direct_simulation() requires separate Inf and Fin sets Best, David