hi!
With the aid of SPOT I am developing a counter-example guided synthesizer
in python. See [1] if interested for details.
My question is:
I am trying to parse twa_run in python,
namely, parse the labels of the each step (`spot.impl.step`).
Is there a python way to walk through BDD?
(The label is a simple cube expressed in BDD, and I need to convert it into
my internal structure)
(yes, this is rather a question about python interface for buddy)
(no, that is not feature request:) if not possible, I will simply print the
label and parse the string, that is not crucial)
[1]
The idea is
- guess the model,
- then model check it and get a counter-example
- then encode the counter-example into the "guesser" (which uses an SMT
solver)
thanks,
Ayrat
I'm trying to use SPOT to build an automaton for an LTLf formula, but I
think there is a bug. I'm using this code (based on
https://spot.lrde.epita.fr/tut12.html):
#include <iostream>
#include <spot/tl/ltlf.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/translate.hh>
int main() {
spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))");
if (pf.format_errors(std::cerr))
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(pf.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
aut = post.run(aut);
print_hoa(std::cout, aut) << '\n';
return 0;
}
In LTL, this would be a contradiction, but in LTLf it is not as the next
operator cannot be true at the last timestep. There seems to be an issue
with SPOT where it simplifies the automaton as though the formula is in
LTL, yielding an incorrect automaton. Am I using this correctly? I'd be
willing to write a patch if this is indeed a bug.
Thanks,
Andrew Wells
Hi,
I have used the version 2.0 of your online tool for LTL to Buchi automata translation. At the time the tool did not return a deterministic Buchi automaton, but the new version does the transformation with ease.
I was wondering if something fundamental has changed in your code that made this possible. Do you have the Changelog from 2.0 to 2.8?
Here is the formula i used :
G(!e) & G((c&!d&Fd)->(p Ud)) & G(a&!c->(!c W(b&!c))) & GF(a)&GF(b)&GF(c)&GF(d)
RegardsHadi Zibaeenejad,PhDUniversity of Waterloo
