Enable spot's complementation in KOFOLA

src/complement/complement_tela.cpp

@@ -25,6 +25,11 @@
 #include <spot/twaalgos/complete.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/complement.hh>
+#include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/alternation.hh>
+#include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/cleanacc.hh>
 
 // standard library
 #include <queue>
@@ -214,3 +219,52 @@ bool kofola::is_post_reduction_suitable(const spot::twa_graph_ptr& aut) {
 	}
 	return true;
 }
+
+spot::twa_graph_ptr kofola::spot_complement(const spot::twa_graph_ptr& aut)
+{
+	spot::twa_graph_ptr result = spot::complement(aut);
+
+	if (!aut->is_existential() || is_universal(aut))
+	{
+		spot::twa_graph_ptr res = spot::dualize(aut);
+		// There are cases with "t" acceptance that get converted to
+		// Büchi during completion, then dualized to co-Büchi, but the
+		// acceptance is still not used.  Try to clean it up in this
+		// case.
+		if (aut->num_sets() == 0 ||
+			// Also dualize removes sink states, but doesn't simplify
+			// the acceptance condition.
+			res->num_states() < aut->num_states())
+		spot::cleanup_acceptance_here(res);
+
+		return result;
+	}
+	if (spot::is_very_weak_automaton(aut))
+		// Removing alternation may need more acceptance sets than Spot
+		// supports.  When this happens res==nullptr and we fall back to
+		// determinization-based complementation.
+		if (spot::twa_graph_ptr res = spot::remove_alternation(spot::dualize(aut), false,
+															nullptr, false)) {
+																return result;
+															}
+	// Determinize
+	spot::option_map m;
+
+	// In addition to the above options, the simulation-based
+	// optimization of the determinization is already restricted by
+	// the default values of simul-max and simul-trans-pruning.
+	// (See spot-x(7) for details.)
+	spot::postprocessor p(&m);
+	p.set_type(spot::postprocessor::Generic);
+	p.set_pref(spot::postprocessor::Deterministic);
+	p.set_level(spot::postprocessor::Low);
+
+	auto det = p.run(std::const_pointer_cast<spot::twa_graph>(aut));
+	if (!det || !spot::is_universal(det))
+		return nullptr;
+
+	// Apply postprocessor to the dualized result if postp_l is specified
+	spot::twa_graph_ptr dualized = spot::dualize(det);
+
+	return dualized;
+}

src/complement/complement_tela.hpp

@@ -36,6 +36,9 @@ spot::twa_graph_ptr complement_deterministic(const spot::twa_graph_ptr& aut);
 /// applies postprocessing to an automaton based on configuration parameters
 spot::twa_graph_ptr apply_postprocessing(const spot::twa_graph_ptr& aut, const spot::twa_graph_ptr& original_aut);
 
+/// complements using Spot's built-in complement algorithm (essentially copy-paste from spot)
+spot::twa_graph_ptr spot_complement(const spot::twa_graph_ptr& aut);
+
 /// complements a TELA using the synchronous algorithm (cf. paper)
 spot::twa_graph_ptr complement_sync(const spot::twa_graph_ptr& aut);
 

src/main.cpp

@@ -185,6 +185,7 @@ int process_args(int argc, char *argv[], kofola::options* params)
 	// command
 	args::Group operation_group(parser, "Operation:", args::Group::Validators::AtMostOne);
 	args::Flag complement_flag(operation_group, "complement", "complement the inputs (default)", {"complement"});
+	args::Flag spot_complement_flag(operation_group, "spot_complement", "complement the inputs using Spot", {"spot_complement"});
 	args::Flag det_flag(operation_group, "det", "determinize the inputs", {"det"});
 	args::Flag type_flag(operation_group, "type", "print out types of the inputs", {"type"});
 	args::Flag scc_types_flag(operation_group, "scc-types", "print out types of SCCs in the inputs", {"scc-types"});
@@ -249,6 +250,8 @@ int process_args(int argc, char *argv[], kofola::options* params)
         params->operation = "inclusion";
 	} else if (to_elev_flag) {
 		params->operation = "elevatorization";
+	} else if (spot_complement_flag) {
+		params->operation = "spot_complement";
     } else { // default
 		params->operation = "complement";
 	}
@@ -358,6 +361,13 @@ int main(int argc, char *argv[])
 
 					spot::print_hoa(std::cout, result);
 					std::cout << "\n";
+				} else if(options.operation == "spot_complement") {
+					spot::twa_graph_ptr result = kofola::spot_complement(aut);
+
+					if (result) {
+						spot::print_hoa(std::cout, result);
+						std::cout << "\n";
+					}
 				} else if (options.operation == "type") {
 					assert(false);
 				} else if (options.operation == "determinize") {