Dear Spot developers, I am Yong Li, a Phd student from Chinese Academy of Sciences. I am writing to you to ask an implementation question about the translation from LTLf to NBAs in Spot. currently if I use following command line: ltlfilt --from-ltlf -f "((G((P83) -> (X((P145)) | X(X((P145))) | X(X(X((P145)))) ))) -> ( G((P21) -> (X( (P118) | (P83)) | X(X( (P118) | (P83))) | X(X(X((P118) | (P83)))) )) & G( (P118) -> X(!(P118))) & G( (P83) -> X(!(P118) U (P145)))))" | ltl2tgba | autfilt --remove-ap=alive --small -B I was able to get a weak DBA with only 8 states. However, if I use following c++ code to do the same job: auto pf1 = spot::parse_infix_psl(argv[1]); if (pf1.format_errors(std::cerr)) { std::cerr << "error: " << argv[1] << std::endl; return -1; } // formula auto f1 = pf1.f; std::cout << f1 << std::endl; // translate to ltlf //auto ltlf = spot::from_ltlf(f1, "alive"); spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); trans.set_level(spot::postprocessor::High); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f)); spot::remove_ap rem; rem.add_ap("alive"); aut = rem.strip(aut); spot::postprocessor post; post.set_type(spot::postprocessor::BA); post.set_pref(spot::postprocessor::Small); // or ::Deterministic post.set_pref(spot::postprocessor::High); // or ::Deterministic aut = post.run(aut); I would get a DBA with 16 states, which has much more states than the one from the command line. The full source code is attached to this email. Could you tell me how I can change the code above so to get the same DBA from the command line? Thank you very much. BTW: I would like to appreciate the Spot tool which is a tool I would install on my every Ubuntu system. Yong