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