28 Aug
2019
28 Aug
'19
5:54 a.m.
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
28 Aug
28 Aug
11:12 a.m.
On Wed, Aug 28, 2019 at 8:10 AM Andrew Wells <andrewmw94(a)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
1988
days inactive
1988
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Andrew Wells