3 Jun
2019
3 Jun
'19
6:32 a.m.
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(a)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';
}