15 Dec
2023
15 Dec
'23
11:03 a.m.
Hi Samuel,
Sorry for the delayed answer; had a lot on my plate this week.
Samuel Judson <samuel.judson(a)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.