Hi all,
Do you know any tools that can convert universal co-buchi automata into
universal safety automata via bounding the number of visits to the final
states?
(I.e., go to absorbing bad state if visit a final state k times)
(Alternatively, convert NBW into nondet finite automaton: accept a word if
it visits a final state k times)
(I am just trying to avoid work that may have already be done:)
Thanks,
Ayrat
hi,
Is there a way to get more than one accepting run of the product automaton?
Ideally would be to have all simple accepting runs,
but some cheap heuristics would also do.
I wanted to implement some heuristics [1], but got stuck with the following:
how to map edges of the accepting run to the edges of the original product?
(or: states of the accepting run to states of the product?)
thanks!:)
ayrat
[1]
An heuristics:
- get an accepting run,
- forbid one edge of that run in the original product (for example, by
setting its label to bddfalse),
- ask for another accepting run on the thus modified product,
- restore that edge and change another edge,
and so on.
Hello dear spot devs,
I need to know which construction is used when I'm translating an LTL
formula into a monitor automaton. By that I mean:
/spot::formula some_ltl;
spot::translator trans;/
/trans.set_type(spot::postprocessor::Monitor)
spot::const_twa_graph_ptr aut = trans.run(some_ltl)/
I couldn't find documentation about this, besides some rather informal
description.
It would be great if you could point me to some more useful
documentation about the algorithm or even better a paper on it.
Best,
Marvin Stenger
Hi Marvin,
> Hello dear spot devs,
>
> I have a question concerning stepping through an automaton based on the boolean formula assigned to the edge between two states, using c++.
> What I want to achieve is the following:
> I'm translating an LTL formula into a deterministic monitor automaton, so I have a spot::const_twa_graph_ptr.
> Now I simply want to "run" the DFA, i.e., I have a trace and want to perform a state change based on the transition matching the current letter in my trace.
> I don't get that step just from the examples or the doxygen documentation.
maybe something like
unsigned step(const const_twa_graph_ptr& aut, unsigned src, bdd label)
{
for (auto& edge: aut->out(src))
if (bdd_implies(label, edge.cond))
return edge.dst;
throw std::runtime_error("unmatched label");
}
> Furthermore it would also be great, if you could tell me how to output the bdd on the edge in an human readable way (boolean formula), as it is done in the online tool of yours (https://spot.lrde.epita.fr/trans.html).
I believe this is shown in https://spot.lrde.epita.fr/tut21.html
--
Alexandre Duret-Lutz
On Thu, Nov 10, 2016 at 8:44 PM, ShufangZhu <saffiechu(a)gmail.com> wrote:
> 2016-11-10 13:01 GMT-06:00 Alexandre Duret-Lutz <adl(a)lrde.epita.fr>:
>> On Thu, Nov 10, 2016 at 6:33 PM, ShufangZhu <saffiechu(a)gmail.com> wrote:
>> > can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or
>> > directory
>> > libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a
>> > valid libtool archive
>>
>> Could you show the entire output you get when you type "make" ?
>
> Please see attached for the entire output.
OK, so this error is due to the fact that the source code is in a
directory called
/home/saffie/LTLf synthesis/spot-2.1.2
with "LTLf synthesis" containing a space. Directory or file names with
spaces cannot be supported in Makefiles.
Just rename that directory to LTLf_synthesis (or something else), and be
sure to run './configure && make clean' (to forget about the old path)
before rebuilding with 'make'.
--
Alexandre Duret-Lutz
Hi,
I am trying to install SPOT. But after I entered the command "make", there
is an error as following,
can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or
directory
libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a
valid libtool archive
My system is Ubuntu 14.04, 64-bit. And it's a virtual machine.
Thanks!
Best Regards,
Shufang
Dear Spot Team,
I am a postdoc at UCL working on the Cyclist theorem-proving framework,
which makes use of Spot. We have recently upgraded Cyclist to use Spot
2.1 from Spot 1.2.4, and one of our benchmark tests has thrown up a
possible bug in the Spot library.
Cyclist searches for cyclic proofs, and validates them by building two
Buchi automata out of a proof and checking language inclusion (ℒ(A) ⊆
ℒ(B)), which we do by first complementing B and then checking emptiness
of the product with A.
With version 1.2.4, we did this using with the following code:
spot::twa a = ...;
spot::twa b = ...;
spot::tgba_safra_complement complement(&b);
spot::tgba_product product(&a, &b);
spot::couvreur99_check ec(&product);
spot::emptiness_check_result * res = ec.check();
Since version 2.1 does not provide the tgba_safra_complement class, we
now use the following code:
spot::twa_graph_ptr a = ...;
spot::twa_graph_ptr b = ...;
spot::twa_graph_ptr det = tgba_determinize(b);
spot::twa_graph_ptr complement = to_generalized_buchi(dtwa_complement(det));
spot::const_twa_ptr product = std::make_shared<spot::twa_product>(proof, complement);
spot::couvreur99_check ec(product);
std::shared_ptr<spot::emptiness_check_result> res = ec.check();
Our benchmark test generates the following automata (given in dot
format) for a and b, respectively:
digraph G {
rankdir=LR
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="p_0 & !p_1 & !p_2 & !p_3\n{0}"]
1 [label="S1 t_53"]
1 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"]
2 [label="S2 t_53,t_49,t_50,t_51,t_52"]
2 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"]
2 -> 3 [label="p_0 & p_1 & !p_2 & !p_3\n{0}"]
3 [label="S3 t_53,t_52"]
3 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"]
3 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"]
4 [label="S5 t_53"]
4 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"]
5 [label="S4 t_53"]
5 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"]
}
digraph G {
rankdir=LR
I [label="", style=invis, width=0]
I -> 0
0 [label="init"]
0 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3"]
0 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"]
0 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"]
0 -> 4 [label="!p_0 & p_1 & !p_2 & !p_3"]
0 -> 5 [label="!p_0 & p_1 & !p_2 & !p_3"]
0 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3"]
0 -> 7 [label="!p_0 & p_1 & !p_2 & !p_3"]
0 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"]
0 -> 9 [label="p_0 & !p_1 & p_2 & !p_3"]
0 -> 10 [label="p_0 & !p_1 & !p_2 & !p_3"]
0 -> 0 [label="1"]
1 [label="S4,t53"]
1 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"]
2 [label="S3,t52"]
2 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"]
3 [label="S3,t53"]
3 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"]
4 [label="S2,t52"]
5 [label="S2,t51"]
5 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"]
6 [label="S2,t50"]
7 [label="S2,t49"]
7 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"]
8 [label="S2,t53"]
8 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"]
8 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"]
9 [label="S5,t53"]
9 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"]
10 [label="S1,t53"]
10 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"]
10 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"]
}
The code I gave above returns a non-null (i.e. non-empty) result,
however we expect that this should actually return an empty result.
What I have discovered is that the code above does indeed return an
empty result when the use_simulation flag to the tgba_determinize
function is set to false (the values of the other two flags do not make
a difference). Thus, it seems to me that this is a bug, no?
I am happy to provide any more information which is necessary for diagnosis.
Best wishes,
Reuben Rowe.
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
