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` 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