Enable spot's complementation in KOFOLA

README.md

@@ -85,6 +85,7 @@ The complementation and the inclusion checking might be adjusted by the followin
 | `sh-break` | `yes`,`no`  | Enable shared breakpoint across partial algorithms; when `yes` partial algorithms that support shared breakpoints propagate a common breakpoint across partitions |
 | `tela_det_alg` | `inductive`, `dnf-tela` | Algorithm selection for complementing deterministic TELA components (default `dnf-tela`) | 
 | `sd_ind_sh_break` | `yes`, `no` | Shared breakpoint for inductive TELA procedure (assumes `tela_det_alg=inductive`) |
+| `postp_l` | `low`, `medium`, `high` | postprocessing level applied to the result of complementation (used for both - spot's and kofola's implementation)
 
 ## Testing
 

src/algorithms/complement_alg_sd_inductive.cpp

@@ -42,16 +42,45 @@ check_macrostate assign_leaf_ids(const check_macrostate& tree, unsigned& next_id
   return check_macrostate::make(tree.get_options_ptr(), node_type, assign_leaf_ids(left_ms, next_id), assign_leaf_ids(right_ms, next_id), tree.node_value().context);
 }
 
+/**
+ * @brief Internal helper for initializing `NodeContext` payloads inside a check tree.
+ *
+ * @param tree   Check tree to update in-place.
+ * @param opts   Options controlling whether shared-breakpoint contexts are used.
+ * @param is_root Whether this node is the root of the entire tree.
+ *
+ * @warning Same caveats apply as in `init_contexts_in_tree()`.
+ */
+static void init_contexts_in_tree_impl(check_macrostate& tree, options_ptr opts, bool is_root) {
+  if (tree.is_leaf()) {
+    return;
+  }
+
+  auto& base = static_cast<base_tree&>(tree);
+  init_contexts_in_tree_impl(static_cast<check_macrostate&>(base.left()), opts, false);
+  init_contexts_in_tree_impl(static_cast<check_macrostate&>(base.right()), opts, false);
+
+  // if root_shb, only root gets the shared-breakpoint context; if inf_tree_shb, every internal And-node gets a shared-breakpoint context
+  if ( (opts->use_root_shared_breakpoint && is_root) || opts->use_inf_tree_shared_breakpoint ) {
+    NodeContext ctx = NodeContext::create_subtree_sh_context(tree.type(), tree, opts->use_inf_tree_shared_breakpoint);
+    tree.node_value().set_context(ctx);
+  }
+}
+
 /**
  * @brief Initialize (or re-initialize) `NodeContext` payloads inside a check tree.
  *
- * When shared-breakpoint mode is enabled (`opts->use_shared_breakpoint == true`),
- * each internal node's `NodeContext` is recomputed from the subtree so that it
- * references the current set of `Inf` leaf IDs.
+ * Supports two mutually exclusive shared-breakpoint modes:
+ * - **Root-only mode** (`opts->use_root_shared_breakpoint == true`): computes the 
+ *   root internal node's `NodeContext` from the subtree to reference the current 
+ *   set of `Inf` leaf IDs. Non-root nodes do not receive shared-breakpoint contexts.
+ * - **Inf-tree mode** (`opts->use_inf_tree_shared_breakpoint == true`): computes 
+ *   `NodeContext` for every internal And-node in the tree, enabling per-subtree 
+ *   shared-breakpoint tracking.
  *
  * @param tree Check tree to update in-place.
- * @param opts Options controlling whether shared-breakpoint contexts are used.
- *             Must be non-null.
+ * @param opts Options controlling whether, and which shared-breakpoint strategy is used.
+ *             Must be non-null and valid (both modes cannot be enabled simultaneously).
  *
  * @warning This function traverses children by casting `base_tree::left()/right()`
  *          to `check_macrostate&`. The underlying tree stores children as
@@ -62,19 +91,7 @@ check_macrostate assign_leaf_ids(const check_macrostate& tree, unsigned& next_id
  *          traversal.
  */
 void init_contexts_in_tree(check_macrostate& tree, options_ptr opts) {
-  if (tree.is_leaf()) {
-    return;
-  }
-
-  auto& base = static_cast<base_tree&>(tree);
-  init_contexts_in_tree(static_cast<check_macrostate&>(base.left()), opts);
-  init_contexts_in_tree(static_cast<check_macrostate&>(base.right()), opts);
-
-  if (opts->use_shared_breakpoint) {
-    NodeContext ctx = NodeContext::create_subtree_sh_context(tree.type(), tree);
-    tree.node_value().set_context(ctx);
-  }
-
+  init_contexts_in_tree_impl(tree, opts, true);
 }
 
 /**
@@ -335,6 +352,14 @@ std::vector<std::pair<check_macrostate, NodeContext>> check_macrostate::get_succ
   }
 
   if (node_type == TreeType::Or) {
+    // In inf_tree_shb mode, each And-node scope is independent.  SHB context must
+    // not bleed through Or nodes: Inf leaves under Or nodes need the standard
+    // per-leaf breakpoint mechanism, and nested And nodes must see NONE as their
+    // parent context so that is_scope_root fires correctly.
+    if (this->opts_ && this->opts_->use_inf_tree_shared_breakpoint) {
+      context_sent = NodeContext{};
+    }
+
     // OR-FIN optimization: when the left subtree contains only FIN leaves (no inner Or
     // nodes), send ALL check_states to the left subtree with collect_violating=true.
     // States that fire a Fin-colored transition are collected as "violating" and are
@@ -366,12 +391,20 @@ std::vector<std::pair<check_macrostate, NodeContext>> check_macrostate::get_succ
 
         for (const auto& [right_tree, right_node_ctx] : right_succ) {
           // Propagate any further violations from right up to the parent.
-          NodeContext out_ctx{};
-          out_ctx.violating_states = right_node_ctx.violating_states;
-          out_ctx.violating_predecessors = right_node_ctx.violating_predecessors;
+          NodeContext local = actual_node_context;
+
+          NodeContext merge = left_node_ctx.union_contexts(right_node_ctx);
+          merge.violating_states = right_node_ctx.violating_states;
+          merge.violating_predecessors = right_node_ctx.violating_predecessors;
+
+          if (is_scope_root) {
+            if (!merge.is_none()) local = merge;
+            merge = NodeContext{};
+          }
+
           auto combined = check_macrostate::make(this->opts_, TreeType::Or,
-            left_restricted, right_tree, actual_node_context);
-          out.insert({combined.reduce(), out_ctx});
+            left_restricted, right_tree, local);
+          out.insert({combined.reduce(), merge});
         }
       }
       return std::vector<std::pair<check_macrostate, NodeContext>>(out.begin(), out.end());
@@ -790,7 +823,7 @@ std::vector<std::pair<check_macrostate, NodeContext>> inf_leaf::get_succ(
   std::set<unsigned> succ_break {};
 
 
-  if (opts && opts->use_shared_breakpoint && context.is_shared_breakpoint()) {
+  if (opts && opts->use_shared_breakpoint() && context.is_shared_breakpoint()) {
     if (!context.targets_leaf(this->id)) {
       return {{check_macrostate::inf(std::move(opts), std::move(succs), std::move(succ_break), this->color, this->id), NodeContext{}}};
     }
@@ -886,9 +919,11 @@ complement_sd_inductive::complement_sd_inductive(const cmpl_info& info, unsigned
   spot::acc_cond::acc_code acc = this->info_.part_to_acc_map_.at(part_index_).get_acceptance();
   this->acc_cond_ = acc.complement();
   this->opts_ = std::make_shared<sd_inductive::options>(sd_inductive::options{
-    .use_shared_breakpoint = (kofola::OPTIONS.params["sd_ind_sh_break"] == "yes"),
+    .use_root_shared_breakpoint = (kofola::OPTIONS.params["sd_ind_sh_break"] == "root"),
+    .use_inf_tree_shared_breakpoint = (kofola::OPTIONS.params["sd_ind_sh_break"] == "inf_tree"),
     .use_or_fin_opt = (kofola::OPTIONS.params["sd_ind_or_opt"] == "yes")
   });
+  assert(this->opts_->is_valid() && "options: both breakpoint types cannot be enabled simultaneously");
 }
 
 /**

src/algorithms/complement_alg_sd_inductive.hpp

@@ -25,8 +25,17 @@ namespace kofola { // {{{
 namespace sd_inductive {
 
   struct options {
-    bool use_shared_breakpoint{false};
+    bool use_root_shared_breakpoint{false};
+    bool use_inf_tree_shared_breakpoint{false};
+    bool use_shared_breakpoint() const {
+      return use_root_shared_breakpoint || use_inf_tree_shared_breakpoint;
+    }
     bool use_or_fin_opt{false};
+
+    /// Validation: both breakpoint types are mutually exclusive.
+    bool is_valid() const {
+      return !(use_root_shared_breakpoint && use_inf_tree_shared_breakpoint);
+    }
   };
 
   using options_ptr = std::shared_ptr<const options>;
@@ -58,16 +67,21 @@ namespace sd_inductive {
   class check_macrostate;
 
   /**
-   * @brief Collect IDs of `Inf` leaves under `And` nodes.
+   * @brief Collect IDs of all `Inf` leaves (or only under AND nodes in case of inf_tree_shared_breakpoint).
    *
    * Traverses the check tree @p t and appends each encountered
-   * `inf_leaf::id` to @p out. For internal nodes, only `TreeType::And`
+   * `inf_leaf::id` to @p out. 
+   * 
+   * root_shared_breakpoint: For internal nodes, all subtrees are traversed and all `Inf` leaf IDs collected.
+   * 
+   * inf_tree_shared_breakpoint:For internal nodes, only `TreeType::And`
    * subtrees are traversed; `Or` subtrees are intentionally ignored.
    *
    * @param t   Check tree (subtree root) to traverse.
    * @param out Output vector to append leaf IDs into.
+   * @param use_inf_tree_shb Whether to use the Inf tree shared breakpoint optimization, root is default.
    */
-  inline void collect_inf_leaf_ids(const check_macrostate& t, std::vector<unsigned>& out);
+  inline void collect_inf_leaf_ids(const check_macrostate& t, std::vector<unsigned>& out, bool use_inf_tree_shb = false);
 
   struct NodeContext;
   std::ostream& operator<<(std::ostream& os, const NodeContext& ctx);
@@ -174,10 +188,14 @@ namespace sd_inductive {
      * @param subtree_ Subtree to inspect for `Inf` leaf IDs.
      * @return A freshly initialized context for that subtree.
      */
-    static NodeContext create_subtree_sh_context(TreeType t, const check_macrostate& subtree_) {
+    static NodeContext create_subtree_sh_context(TreeType t, const check_macrostate& subtree_, bool inf_tree_shb) {
       NodeContext ctx;
-      collect_inf_leaf_ids(subtree_, ctx.leaf_ids_);
-      if (t == TreeType::And && ctx.leaf_ids_.size() > 0) {
+      collect_inf_leaf_ids(subtree_, ctx.leaf_ids_, inf_tree_shb);
+
+      bool not_leaf = (t == TreeType::And) || (t == TreeType::Or);
+      bool inf_tree_shb_then_and_node = (!inf_tree_shb) || (t == TreeType::And); // inf_tree_shb ==> (t == TreeType::And)
+
+      if (not_leaf && inf_tree_shb_then_and_node && ctx.leaf_ids_.size() > 0) {
         ctx.type = NodeContextType::SHARED_BREAKPOINT;
         ctx.leaf_id = ctx.leaf_ids_[ctx.leaf_index_ % ctx.leaf_ids_.size()];
       }
@@ -615,7 +633,7 @@ namespace sd_inductive {
      * @return String representation of this macrostate check tree.
      */
     std::string to_string() const {
-      return to_string_impl(static_cast<const base_tree&>(*this), opts_ && opts_->use_shared_breakpoint);
+      return to_string_impl(static_cast<const base_tree&>(*this), opts_ && opts_->use_shared_breakpoint());
     }
 
     /**
@@ -696,7 +714,7 @@ namespace sd_inductive {
     options_ptr opts_;
   };
 
-  inline void collect_inf_leaf_ids(const check_macrostate& t, std::vector<unsigned>& out) {
+  inline void collect_inf_leaf_ids(const check_macrostate& t, std::vector<unsigned>& out, bool use_inf_tree_shb) {
     using base_tree = kofola::types::binary_tree<TreeType, AndOrNode, fin_leaf, inf_leaf>;
     const base_tree& bt = static_cast<const base_tree&>(t);
     if (bt.is_leaf()) {
@@ -705,11 +723,13 @@ namespace sd_inductive {
       }
       return;
     }
-    if(bt.type() != TreeType::And) {
+
+    if(use_inf_tree_shb && (bt.type() != TreeType::And)) {
       return;
     }
-    collect_inf_leaf_ids(check_macrostate(nullptr, base_tree(bt.left())), out);
-    collect_inf_leaf_ids(check_macrostate(nullptr, base_tree(bt.right())), out);
+
+    collect_inf_leaf_ids(check_macrostate(nullptr, base_tree(bt.left())), out, use_inf_tree_shb);
+    collect_inf_leaf_ids(check_macrostate(nullptr, base_tree(bt.right())), out, use_inf_tree_shb);
   }
 
   /**

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>
@@ -59,8 +64,19 @@ spot::twa_graph_ptr kofola::apply_postprocessing(const spot::twa_graph_ptr& aut,
 		if(is_post_reduction_suitable(original_aut)) {
 			if(result->num_states() < 2000) {
 				p_post.set_type(spot::postprocessor::GeneralizedBuchi);
-			} 
-			p_post.set_level(spot::postprocessor::Low);
+			}
+
+			// Set postprocessor level based on postp_l parameter
+			auto pp_level = spot::postprocessor::Low;
+			auto level_it = kofola::OPTIONS.params.find("postp_l");
+			if (level_it != kofola::OPTIONS.params.end()) {
+				if (level_it->second == "high") {
+					pp_level = spot::postprocessor::High;
+				} else if (level_it->second == "medium") {
+					pp_level = spot::postprocessor::Medium;
+				}
+			}
+			p_post.set_level(pp_level);
 
 			result = p_post.run(result);
 		}
@@ -214,3 +230,59 @@ 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);
+
+	// Set postprocessor level based on params
+	auto level_it = kofola::OPTIONS.params.find("postp_l");
+	if (level_it != kofola::OPTIONS.params.end()) {
+		auto pp_level = spot::postprocessor::Low;
+		if (level_it->second == "high") {
+			pp_level = spot::postprocessor::High;
+		} else if (level_it->second == "medium") {
+			pp_level = spot::postprocessor::Medium;
+		}
+		p.set_level(pp_level);
+	}
+	auto det = p.run(std::const_pointer_cast<spot::twa_graph>(aut));
+	if (!det || !spot::is_universal(det))
+		return nullptr;
+
+	return spot::dualize(det);
+}

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"});
@@ -199,8 +200,8 @@ int process_args(int argc, char *argv[], kofola::options* params)
 	args::Flag debug_flag(misc_group, "debug", "output debugging information", {'d', "debug"});
 	args::ValueFlag<std::string> params_flag(misc_group, "params",
 	                                         "string with ';'-separated parameters of the form 'key=value' "
-	                                         "(or just 'key' for yes/no flags), e.g. for inclusion, "
-	                                         "'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'",
+	                                         "(or just 'key' for yes/no flags), e.g. 'postp_l=high;' for postprocessor level, "
+	                                         "or for inclusion 'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'",
 	                                         {"params"});
 
     try {
@@ -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";
 	}
@@ -337,6 +340,7 @@ int main(int argc, char *argv[])
         return EXIT_SUCCESS;
     }
 
+	// kofola's complementation
 	for (const std::string& input_filename : options.filenames) {
 		spot::parsed_aut_ptr parsed_aut = nullptr;
 		try {
@@ -358,6 +362,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") {