Hi Alexandre, I have another question about Spot (v 2.7.4). I am using following code to translate an LTLf formula to an NBA (full code is attached): auto pf1 = spot::parse_infix_psl(argv[1]); if (pf1.format_errors(std::cerr)) { std::cerr << "error: " << argv[1] << std::endl; 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(pf1.f)); cout << "done translating " << endl; print_hoa(std::cout, aut) << '\n'; When I input the following formula, the program seems to get stuck: (G((LiVar732) & (power) & (pumppower))) -> (G(!((LiVar808) & (mechanicalpedalposL) & (mechanicalpedalposR) & (!(((mechanicalpedalposL) & ((LiVar610) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar568))) & (!(((mechanicalpedalposL) & ((LiVar608) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar567))) & (!(((mechanicalpedalposR) & ((LiVar606) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar566))) & (!(((mechanicalpedalposR) & ((LiVar604) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar565))) & (!(((mechanicalpedalposL) & ((LiVar602) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar564))) & (!(((mechanicalpedalposL) & ((LiVar600) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar563))) & (!(((mechanicalpedalposR) & ((LiVar598) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar562))) & (!(((mechanicalpedalposR) & ((LiVar596) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar561)))))) However, Spot in command line (ltlfilt --from-ltlf -f formula | ltl2tgba) is able to translate this ltlf formula to an NBA in less than a second. I think there is also some bug in somewhere else other than remove_ap. Regards, Yong On 2019/6/1 下午4:18, Alexandre Duret-Lutz wrote:
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'; }