I'm trying to use SPOT to build an automaton for an LTLf formula, but I think there is a bug. I'm using this code (based on https://spot.lrde.epita.fr/tut12.html):
#include <iostream> #include <spot/tl/ltlf.hh> #include <spot/tl/parse.hh> #include <spot/twaalgos/hoa.hh> #include <spot/twaalgos/remprop.hh> #include <spot/twaalgos/translate.hh>
int main() { spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))"); if (pf.format_errors(std::cerr)) return 1;
spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));
spot::remove_ap rem; rem.add_ap("alive"); aut = rem.strip(aut);
spot::postprocessor post; post.set_type(spot::postprocessor::BA); post.set_pref(spot::postprocessor::Small); // or ::Deterministic aut = post.run(aut);
print_hoa(std::cout, aut) << '\n'; return 0; }
In LTL, this would be a contradiction, but in LTLf it is not as the next operator cannot be true at the last timestep. There seems to be an issue with SPOT where it simplifies the automaton as though the formula is in LTL, yielding an incorrect automaton. Am I using this correctly? I'd be willing to write a patch if this is indeed a bug.
Thanks, Andrew Wells
On Wed, Aug 28, 2019 at 8:10 AM Andrew Wells andrewmw94@gmail.com wrote:
I'm trying to use SPOT to build an automaton for an LTLf formula, but I think there is a bug. I'm using this code (based on https://spot.lrde.epita.fr/tut12.html):
[...]
spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))");
[...]
spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));
[...]
Hi Andrew,
Hmmm... The problem is that Spot really support only LTL over infinite words, so its LTL operators have some hard-coded simplifications when the arguments are true/false (e.g., F(0)=0, F(1)=1, G(0)=0, G(1)=1, X(0)=0, X(1)=1) or for idempotence rules (FFa = Fa, GGa=Ga, etc.) Those rules are listed as "trivial identities" in several sub-sections of https://spot.lrde.epita.fr/tl.pdf and are automatically applied every time an LTL formula is constructed. So there is actually no way to represent the formula ((a && b) U (! (X 1))) in Spot: because X(1)=1, !1=0, and (a && b) U 0 = 0, the output of the parser is already 0. The LTL simplifier and translations algorithms also rely on the fact that these trivial identities (especially X(1)=1) are automatically simplified.
When I added the from_ltlf() function to help support LTLf, I did not realize those trivial identities could cause any problem. I'm just realizing that with your email. Looking at the list of trivial identities we have, I believe X(1)=1 is the only one that makes no sense in LTLf. Do you agree? I'm not sure what is the best way to fix that. I guess we need a way to disable the X(1)=1 simplification, at least during parsing. That could be an option for the constructor of X, and for the parser. Or we could introduce support for two versions of X (weak/strong) with different trivial identities, getting us closer to the PSL standard.
In this particular case, because from_ltlf() will add some "alive" property in your formula, a simple workaround for you would be to alter the input formula to use X(alive) instead of X(1).
-
Alexandre Duret-Lutz -
Andrew Wells