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.epita.fr%2Fapp%2F&data=05%7C02%7Csamuel.judson%40bulldogs.yale.edu%7C5c96e3c374824054c68c08dbfd5522a4%7Cdd8cbebb21394df8b4114e3e87abeb5c%7C0%7C0%7C638382314328458706%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=2GS94nZ%2F8ROVmF9U0YxMUM5J%2FKVgUvHOmud52Vucce0%3D&reserved=0 (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.epita.fr%2Fhierarchy.html%23orga8f7ba5&data=05%7C02%7Csamuel.judson%40bulldogs.yale.edu%7C5c96e3c374824054c68c08dbfd5522a4%7Cdd8cbebb21394df8b4114e3e87abeb5c%7C0%7C0%7C638382314328458706%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=plurcJx0BOM8XuXasYEtVk3RfJwfPlJFykymVhJCAQs%3D&reserved=0 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.epita.fr%2Fpostorius%2Flists%2Fspot.lrde.epita.fr%2F%2F&data=05%7C02%7Csamuel.judson%40bulldogs.yale.edu%7C5c96e3c374824054c68c08dbfd5522a4%7Cdd8cbebb21394df8b4114e3e87abeb5c%7C0%7C0%7C638382314328458706%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=e8DlvznwJJQHMoZ544fIa3szy1O6byFJNe54VVeAGrY%3D&reserved=0