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