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.
