7 Dec
2023
7 Dec
'23
8:17 p.m.
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
15 Dec
15 Dec
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.
3:30 p.m.
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(a)lrde.epita.fr> wrote:
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://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fspot.lre.…
(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.…
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(a)lrde.epita.fr
https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.lrd…
418
days inactive
426
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Samuel Judson