30 May
2019
30 May
'19
2:18 a.m.
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
1 Jun
1 Jun
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
3 Jun
3 Jun
6:32 a.m.
New subject: LTLf to NBAs: new questions
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';
}
4 Jun
4 Jun
11:21 a.m.
New subject: LTLf to NBAs: new questions
Hi Yong,
On Mon, Jun 3, 2019 at 6:32 AM Yong Li (李勇) <liyong(a)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
2073
days inactive
2078
days old
3 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Yong Li (李勇)