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
Hello,
I am trying to convert a LTL formula to Buchi automata in MATLAB. I want to
know if you have any script or library that can help me do this?
Thank you and best regards,
Alina Popa
--
Fourth-year Student | Automatic Control and Applied Informatics | Systems
Engineering
Faculty of Automatic Control and Computer Engineering
“Gheorghe Asachi” Technical University of Iasi, Romania
www.ac.tuiasi.ro
<http://www.ac.tuiasi.ro/> | www.tuiasi.ro <http://www.tuiasi.ro/>
Dear Spot Team,
I'm a master's student at Technical University of Munich and I'm currently writing my Master's Thesis in the research field of path planning for autonomous cars.
I came across Spot on the internet and I think it's a very nice tool that fits exactly my needs: I've got a discrete finite automaton (with certain attributes/APs per node) and I want to check, if this automaton satisfies a certain LTL specification. Especially, my intention is to find all path in my automaton, that satisfy a LTL specification. I've already installed Spot on my computer and tried to implement this with Python. Now I've got the following two questions:
1. What is the most simple and fastest way of defining a spot kripke graph, based on my own automaton (which is basically just a dictionary with nodes, that hold certain attributes and parent/child relations) ? Is there a possibility of including my nodes and transitions step by step into a spot kripke graph or do I have to convert my automaton at first into e.g. the HOA format and afterwards import this HOA-string as a kripke graph?
2. Building the product of a LTL formula (resp. the Büchi automaton) with the kripke graph leads to a object of the class twa_product. Is there a possibility of transforming this product back into a kripke structure or exporting it as a simple dictionary, so that I can make further computations on this "reduced" graph?
I hope you can help me with my questions and maybe provide some simple code examples. Thank you very much in advance!
Yours sincerely,
Patrick Halder
Hello,
I have noticed two types of errors that seem to occur when telling ltl2tgba to output unambiguous Büchi automata (UBA).
One seems to be some kind of assertion triggering and happens only in combination with the flag „—low“. That is,
on running:
ltl2tgba —low -U -B -f $FRML
the tool occasionally exits with exit code 2 and:
„ltl2tgba: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true“
This happens for example for the formula:
(G(!(G("2")))) & (("1") | (F("2")))
In some cases the UBA generated by ltl2tgba seem to be incorrect as well, and I don’t think this has to do with the „—low“
flag. An example formula is
(("2") W (G("1"))) -> (G("1"))
To reproduce these behaviors you can run ltlcross on the attached file „error“, as follows:
cat error | ltlcross —-lbt-input ‚ltl2tgba -U -B —-low -f %f >%O' 'ltl2tgba -f %f >%O'
Best regards,
Simon
