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.
