1 Jun
2019
1 Jun
'19
11:18 p.m.
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';
}
--
Alexandre Duret-Lutz