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_sharedspot::twa_product(proof, complement); spot::couvreur99_check ec(product); std::shared_ptrspot::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.