Hello,
I'm a graduate student at National Taiwan University (Taiwan), doing automatic verification related researches.
Currently I'm working on integration of PSL translation with other types of Büchi automata and formats with
our own tool (based on Java), which the linear fragment part is implemented by Spot (and ltl2tgba).
I appreciate this fantastic tool and all of your respectable work on this.
Upon using ltl2tgba, I'd like to ask some basic question regarding F formula and SERE sequences.
Take the following formula as example:
G ( {a;b} -> F q )
where a, b, q are all atomic Boolean expressions.
ltl2tgba would give me the result like the following:
https://spot.lrde.epita.fr/spotimg/af005ecb477ea78d3b55f538089ac0fce1fa99f7…
(This is captured from online Spot converter, but is the same as one output by command-line tools.)
As we can see, there are multiple transitions marked as "a & !q",
meaning this automaton is a non-deterministic one.
Is this intended to be so?
If yes, how could I specify Spot to get a deterministic output?
If no, would this be a bug or something ambiguous?
Also, I have been curious about the algorithm that Spot parses PSL fragment.
It seems like Spot first extracts PSL symbols to LTL compatible ones and then
apply LTL translation method to automata,
Is this right? Or did I miss some parts?
I'm new to PSL translations and reading related papers now (thanks for the SPOT citation page).
Please feel free to correct me or recommend me some must-read publications.
Currently I"m working on the IEEE Standard (2010) and the book Practical Introduction to PSL.
Thank you very much.
Sincerely,
Willy Chang
Dept. of Information Management
National Taiwan University
Hello
I want to use ltl2dstar.exe for a project, but I have a problem with
v.0.5.3. when I run it with cmd it returns an error...
Exception in file common/RunProgram.win32.cpp at line 85:
CreateProcess failed...
I would be appreciate if you tell me how should I fix it.
Best,
Armin
Hi,
i would like to ask you about the most efficient way of completing an
automaton using bdd operations.
we are working with huge automata and we want to improve the automaton
creation process. For that, one of the bottlenecks is generating the
logical formulas corresponding to the automaton transitions as bdds.
For example, let us consider we have the following automaton:
State 0
|
| a & b
|
v
State 1
|
| a & c
|
v
State 2
Then, the alphabet is {a,b,c,d,e}. Thus, we need to add (!c & !d & !e) to
the first transition and (!b & !d & !e) to the second one in order to make
queries such as "F(e)".
Currently, we are implementing this manually using a loop where for each
transition we add the negation of every condition that is not present in
the transition. But it is not fast enough.
Is there any bdd operation to implement this in an efficient way?
Thanks in advance,
Sergio Hernández
Hi Spot developers,
I just extended our automata library
https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_in…
with support to write Büchi automata in the HOA format.
Now, I just wanted to check a few results without implementing
support to read HOA files.
Syntactically my files seem to be correct, (example attached, file
is read by Spot), but I also wanted to do some semantic check,
e.g., test if a certain word is accepted.
Spot provides quite a number of sophisticated operations but I did not
find something "simple" like an acceptance check.
Have I overlooked it or is it not documented?
For my purpose it is sufficient if it works on the "usual" Büchi automata.
Best,
Matthias
Hi,
Can you please explain the api for creating a bdd?
How can I create a bdd?
How do I define it?
How do I give parameter names so that I can later use it to model check a
formula?
What is the meaning of bdd_ithvar and bdd_nithvar and the int parameter
they receive?
I would be very happy if you can supply a simple example.
Thank you very much and happy new year,
Miriam
Hi all,
I am a masters student of computer science at University of Bremen,
Germany. I am working with Büchi-Automata for a study at the moment.
Therefore I want to parse an HOA file representing a Büchi-Automaton
using Python. It would be great to get an object in Python representing
the automaton. So that I can iterate over the states and their edges,
read the labels, etc.
Can this be done using Spot? If so, how? It would be nice to have a code
example.
Thank you so much for your help!
Best regards from Germany,
Marcel Walter
Dear Spot developers,
Attached is an automaton accepting an empty language. I think it is
supposed to be unambiguous. But when I ran the following command, I
got 0.
autfilt --count --is-unambiguous empty.hoa
After tracing the code, I found that the problem might be caused by
get_init_state_number (called in the product function), which creates
a new state if the input automaton has no state.
--
Ming-Hsien
