[Spot] Checking Safety and Liveness

Hello, Using the Spot C++ API I am having a strange issue testing whether a formula is safety or liveness. Specifically, many of the formulas I am testing are coming back as both safety and liveness, despite being non-trivial. My code snippet for the testing is (with some extraneous steps omitted): int simplification_level = 3; spot::tl_simplifier_options tlopt(simplification_level); spot::tl_simplifier simpl(tlopt); spot::parsed_formula pf = spot::parse_infix_psl(ltl); spot::formula f = simpl.simplify(pf.f); spot::twa_graph_ptr aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); safe = f.is_syntactic_safety() || is_safety_automaton(aut); live = is_liveness_automaton(aut); <<< Here `safe` and `live` are both booleans. It is based on similar code within `/bin/ltlfilt.cc <http://ltlfilt.cc/>` in the Spot codebase. However, for many formulas this code resolves both `safe` and `live` to true. As a concrete example, when I test ``` G((!"(P_0 == 'p1')" & !"(P_0 == 'p2')" & !"(P_0 == 'p3')") | F"(P_0 == 'CS')") ``` (after simplification, and derived from the BEEM benchmarks) both resolve to true. Am I using the testing API incorrectly? Is this a bug in Spot? Or is the formula malformed in some way that isn’t obvious to me? Thanks in advance for any help you can give. Samuel Judson