LTLf to NBAs: inconsistent results from code and command line
Dear Spot developers, I am Yong Li, a Phd student from Chinese Academy of Sciences. I am writing to you to ask an implementation question about the translation from LTLf to NBAs in Spot. 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: auto pf1 = spot::parse_infix_psl(argv[1]); if (pf1.format_errors(std::cerr)) { std::cerr << "error: " << argv[1] << std::endl; return -1; } // formula auto f1 = pf1.f; std::cout << f1 << std::endl; // translate to ltlf //auto ltlf = spot::from_ltlf(f1, "alive"); spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); trans.set_level(spot::postprocessor::High); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.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 post.set_pref(spot::postprocessor::High); // or ::Deterministic aut = post.run(aut); I would get a DBA with 16 states, which has much more states than the one from the command line. The full source code is attached to this email. Could you tell me how I can change the code above so to get the same DBA from the command line? Thank you very much. BTW: I would like to appreciate the Spot tool which is a tool I would install on my every Ubuntu system. Yong
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
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'; }
Hi Yong, On Mon, Jun 3, 2019 at 6:32 AM Yong Li (李勇) <liyong@ios.ac.cn> wrote:
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):
spot::translator trans; 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.
Yes, this is related to another bug I fixed two weeks ago on the development version. spot::translator has an optimization for formulas where a lot of atomic propositions are used together. When this optimization is used, a huge formulaslike yours is first rewritten as Gp0 -> Gp1, then translated to an automaton over p0, p1, and finally the occurrences of p0 and p1 in the automaton are changed back to the original Boolean formulas they represent. Doing so speeds up a lot of determinization-based algorithms that are exponential in the number of atomic propositions. The bug is that this optimization is only activated when an option_map is passed to the spot::translator object. So you should be able to fix that by just changing spot::translator trans; into spot::option_map m; spot::translator trans(&m); In the next release that will not be necessary. Of course ltl2tgba always passes an option_map to trans, because option_map is the object used to collect any option passed with the -x flag. Best regards, -- Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
Yong Li (李勇)