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