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
Hi Samuel,
Sorry for the delayed answer; had a lot on my plate this week.
Samuel Judson samuel.judson@yale.edu writes:
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):
spot::twa_graph_ptr aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); safe = f.is_syntactic_safety() || is_safety_automaton(aut);
However, for many formulas this code resolves both `safe` and `live` 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?
I think the issue is only some implicit assumptions in is_safety_automaton().
The code that is used on https://spot.lre.epita.fr/app/ (on the STUDY tab) to decide if a formula is Safety is the mp_class() function of Spot:
// returns the class of f in the hierarchy of Manna & Pnueli char mp_class(formula f) { if (f.is_syntactic_safety() && f.is_syntactic_guarantee()) return 'B'; auto dict = make_bdd_dict(); auto aut = ltl_to_tgba_fm(f, dict, true); auto min = minimize_obligation(aut, f); if (aut != min) // An obligation. { scc_info si(min); bool g = is_terminal_automaton(min, &si); bool s = is_safety_automaton(min, &si); if (g) return s ? 'B' : 'G'; else return s ? 'S' : 'O'; } // Not an obligation. Could be 'P', 'R', or 'T'. if (is_recurrence(f, aut)) return 'R'; if (is_persistence(f, aut)) return 'P'; return 'T'; }
The letters in returned by that function are references to the picture on https://spot.lre.epita.fr/hierarchy.html#orga8f7ba5 therefore f is a Safety formula is this function returns S or B.
That code does more than what you want. If we simplify it to focus only on safety, it becomes:
bool is_safety_formula(formula f) { auto dict = make_bdd_dict(); auto aut = ltl_to_tgba_fm(f, dict, true); auto min = minimize_obligation(aut, f); if (aut == min) // not an obligation. return false; return is_safety_automaton(min); }
So I think can fix your code by calling minimize_obligation() before testing is_safety_automaton().
The problem is that is_safety_automaton() was written assuming it received the output of minimize_obligaton() (a deterministic and weak automaton), but that was never documented. I would consider that a bug. The current documentation of is_safety_automaton() says that an automaton is a safety automaton if all its SCCs are accepting, but that's a necessary condition only if the automaton is also weak and deterministic. Rather than fixing the documentation, I'll see if I can generalize is_safety_automaton() so it works on any automaton.
Alexandre,
Thank you so much for responding. This is all extremely helpful, and I’ll test it out.
Samuel
On Dec 15, 2023, at 05:03, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
Hi Samuel,
Sorry for the delayed answer; had a lot on my plate this week.
Samuel Judson samuel.judson@yale.edu writes:
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):
spot::twa_graph_ptr aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); safe = f.is_syntactic_safety() || is_safety_automaton(aut);
However, for many formulas this code resolves both `safe` and `live` 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?
I think the issue is only some implicit assumptions in is_safety_automaton().
The code that is used on https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fspot.lre.e... (on the STUDY tab) to decide if a formula is Safety is the mp_class() function of Spot:
// returns the class of f in the hierarchy of Manna & Pnueli char mp_class(formula f) { if (f.is_syntactic_safety() && f.is_syntactic_guarantee()) return 'B'; auto dict = make_bdd_dict(); auto aut = ltl_to_tgba_fm(f, dict, true); auto min = minimize_obligation(aut, f); if (aut != min) // An obligation. { scc_info si(min); bool g = is_terminal_automaton(min, &si); bool s = is_safety_automaton(min, &si); if (g) return s ? 'B' : 'G'; else return s ? 'S' : 'O'; } // Not an obligation. Could be 'P', 'R', or 'T'. if (is_recurrence(f, aut)) return 'R'; if (is_persistence(f, aut)) return 'P'; return 'T'; }
The letters in returned by that function are references to the picture on https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fspot.lre.e... therefore f is a Safety formula is this function returns S or B.
That code does more than what you want. If we simplify it to focus only on safety, it becomes:
bool is_safety_formula(formula f) { auto dict = make_bdd_dict(); auto aut = ltl_to_tgba_fm(f, dict, true); auto min = minimize_obligation(aut, f); if (aut == min) // not an obligation. return false; return is_safety_automaton(min); }
So I think can fix your code by calling minimize_obligation() before testing is_safety_automaton().
The problem is that is_safety_automaton() was written assuming it received the output of minimize_obligaton() (a deterministic and weak automaton), but that was never documented. I would consider that a bug. The current documentation of is_safety_automaton() says that an automaton is a safety automaton if all its SCCs are accepting, but that's a necessary condition only if the automaton is also weak and deterministic. Rather than fixing the documentation, I'll see if I can generalize is_safety_automaton() so it works on any automaton. ______________________ Spot mailing list -- spot@lrde.epita.fr https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.lrde...
-
Alexandre Duret-Lutz -
Samuel Judson