Hi Yong, On Sat, Jun 1, 2019 at 10:59 AM Yong Li (李勇) <liyong@ios.ac.cn> wrote:
currently if I use following command line:
ltlfilt --from-ltlf -f "((G((P83) -> (X((P145)) | X(X((P145))) | X(X(X((P145)))) ))) -> ( G((P21) -> (X( (P118) | (P83)) | X(X( (P118) | (P83))) | X(X(X((P118) | (P83)))) )) & G( (P118) -> X(!(P118))) & G( (P83) -> X(!(P118) U (P145)))))" | ltl2tgba | autfilt --remove-ap=alive --small -B
I was able to get a weak DBA with only 8 states.
However, if I use following c++ code to do the same job: [...] I would get a DBA with 16 states, which has much more states than the one from the command line.
You did everything right and hit a bug in the remove_ap code. Sorry about this, but thank you for reporting it! Here is some code equivalent to the command-line, including one line to work around the bug of remove_ap until we fix it. #include <iostream> #include <spot/tl/parse.hh> #include <spot/tl/ltlf.hh> #include <spot/twaalgos/translate.hh> #include <spot/twaalgos/remprop.hh> int main(int argc, char** argv) { if (argc != 2) { std::cerr << "please input one formula string\n"; exit(2); } auto pf1 = spot::parse_infix_psl(argv[1]); if (pf1.format_errors(std::cerr)) { std::cerr << "error: " << argv[1] << '\n'; exit(2); } // formula spot::translator trans; spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f)); spot::remove_ap rem; rem.add_ap("alive"); aut = rem.strip(aut); // Workaround a bug in Spot <= 2.7.4: remove_ap should not preserve // the "non-terminal" property. In our case, the input of rem.strip is // non-terminal, but removing "alive" turns it unto a terminal automaton. aut->prop_terminal(spot::trival::maybe()); spot::postprocessor post; post.set_type(spot::postprocessor::BA); post.set_pref(spot::postprocessor::Small); post.set_level(spot::postprocessor::High); aut = post.run(aut); std::cout << "#states=" << aut->num_states() << '\n'; } -- Alexandre Duret-Lutz