Mitigation for possible bug in Spot library - union_find termination …

…benchmark was not proving because the Spot library was not recognising the discovered proof as valid, which it is. Apparently, a true value of the use_simulation flag for the tgba_determinize function triggers the bug for this example. Setting it to false does not appear to invalidate any of the standard entailment or termination benchmarks.

src/generic/checkproof.ml

@@ -5,6 +5,8 @@ open Lib
 open Parsers
 open Soundcheck
 
+let () = do_debug := true
+
 let usage = "usage: " ^ Sys.argv.(0) ^ " [abstract proof]"
 
 let parse_proof st = 

src/generic/proofnode.ml

@@ -92,8 +92,8 @@ struct
           Seq.pp n.seq n.descr
           (Blist.pp pp_commasp 
             (fun fmt (i,pres,prog) -> 
-              Format.fprintf fmt "%i" i)) p
-              (* Format.fprintf fmt "@[%i <%a/%a>@]" i Tagpairs.pp pres Tagpairs.pp prog)) p *)
+              (* Format.fprintf fmt "%i" i)) p *)
+              Format.fprintf fmt "@[%i <%a/%a>@]" i Tagpairs.pp (Tagpairs.diff pres prog) Tagpairs.pp prog)) p
 
   let justify = Latex.text "\n\\justifies\n\\thickness=0.1em\n"
   let using = Latex.text "\\using"

src/soundness/soundness.c

@@ -109,12 +109,21 @@ extern "C" value check_soundness() {
 	CAMLparam0();
 	CAMLlocal1(v_res);
 
+	// spot::print_dot(std::cerr, proof);
 	spot::const_twa_ptr ta = std::make_shared<TraceAutomaton>(*proof);
+	// spot::print_dot(std::cerr, ta);
 	spot::twa_graph_ptr graph = copy(ta, spot::twa::prop_set::all());
-	spot::twa_graph_ptr det = to_generalized_buchi(dtwa_complement(tgba_determinize(graph, false, true, true, spot::check_stutter_invariance(graph).is_true())));
-	//spot::print_dot(std::cerr, ta);
-
-	spot::const_twa_ptr product = std::make_shared<spot::twa_product>(proof, det);
+	spot::twa_graph_ptr det = 
+		tgba_determinize(
+			graph, false, true, false, 
+			spot::check_stutter_invariance(graph).is_true()
+		);
+	spot::twa_graph_ptr complement = to_generalized_buchi(dtwa_complement(det));
+	// std::cerr << "check_stutter_invariance(graph) = " << spot::check_stutter_invariance(graph).is_true() << std::endl;
+	// spot::print_dot(std::cerr, det);
+	// spot::print_dot(std::cerr, complement);
+
+	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();