Dear all,
there seems to be a problem with the translation LTLf -> LTL,
as supported by the "ltlfilt --from-ltlf" command from the SPOT distribution.
It seems that subformulas of the type "X p" get translated into "X (!alive | p)"
instead of "X (alive & p)", as they should be according to the LTLf semantics,
as well as the translation outlined in the Memocode '14 paper by Dutta
and Vardi.
Do you agree or am I missing something?
By the way, we are planning to use SPOT as part
of a toolchain to check the satisfiability of a flavor of LTLf-modulo-theory.
Thanks,
Marco Faella
--
Associate professor
Electrical Engineering and Information Technologies
University of Naples Federico II, Italy
http://wpage.unina.it/m.faella
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
