Hi,
the manual says in the section DESCRIPTION:
The list of automata to use should be supplied on standard input, or using
the -f or -F options.
However, the tool knows no -f option.
Fanda
I downloaded the spot tar package and tried to compile it using
./configure, make, sudo make install. However, make reports the error:
make: *** No targets specified and no makefile found. Stop.
and sudo make install reports:
make: *** No rule to make target 'install'. Stop.
What's happening, what can I do?
Thank you in advance,
-Pedro Marquez, Prof.
Hello,
I was trying to build Spot on a fresh ArchLinux install, when I came
across this issue:
> $ ./configure ...
> [...]
> checking for swig3.0... no
> checking for swig... no
> [...]
> $ make
> [...]
> swig -c++ -python -py3 -O -nofastproxy -MD -I../buddy/src -MF
> .deps/buddy_wrap.TPcxx ./buddy.i
> make[3]: swig: Command not found
> [...]
> make: *** [Makefile:1163: all] Error 2
If Spot requires Swig, shouldn't `configure` fail ? Or, if Swig is only
required for users who want to build the Python library, shouldn't the
latter not be included in the `all` rule ?
If that's any help, I attached my config.log.
Regards,
--
Clément 'Cigix' Gillard
"EAT SLEEP EAT REPEAT" @skrillbug_bot, 2016-06-23
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.
