diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc index ff3dc4e5e..550fac400 100644 --- a/src/bin/spot-x.cc +++ b/src/bin/spot-x.cc @@ -65,17 +65,17 @@ accepting sets. Set to 0 to disable this SCC-pruning and acceptance \ simpification pass.") }, { DOC("degen-reset", "If non-zero (the default), the \ degeneralization algorithm will reset its level any time it exits \ -a non-accepting SCC.") }, - { DOC("degen-lcache", "If non-zero (the default), whenever the \ +an SCC.") }, + { DOC("degen-lcache", "If non-zero (the default is 1), whenever the \ degeneralization algorithm enters an SCC on a state that has already \ been associated to a level elsewhere, it should reuse that level. \ Different values can be used to select which level to reuse: 1 always \ -uses the first level seen, 2 uses the minimum level seen so far, and \ +uses the first level created, 2 uses the minimum level seen so far, and \ 3 uses the maximum level seen so far. The \"lcache\" stands for \ \"level cache\".") }, { DOC("degen-order", "If non-zero, the degeneralization algorithm \ -will compute one degeneralization order for each SCC it processes. \ -This is currently disabled by default.") }, +will compute an independent degeneralization order for each SCC it \ +processes. This is currently disabled by default.") }, { DOC("degen-lskip", "If non-zero (the default), the degeneralization \ algorithm will skip as much levels as possible for each transition. This \ is enabled by default as it very often reduce the number of resulting \ @@ -84,11 +84,13 @@ automaton tends to have smaller cycles around the accepting states. \ Disabling skipping will produce automata with large cycles, and often \ with more states.") }, { DOC("degen-lowinit", "Whenever the degeneralization algorihm enters \ -a new SCC (or starts from the initial states), it starts on a level that \ +a new SCC (or starts from the initial state), it starts on some level L that \ is compatible with all outgoing transitions. If degen-lowinit is zero \ (the default) and the corresponding state (in the generalized automaton) \ -has an accepting self-loop, then the level is set to the accepting \ -level, as it might favor finding accepting cycles earlier.") }, +has an accepting self-loop, then level L is replaced by the accepting \ +level, as it might favor finding accepting cycles earlier. If \ +degen-lowinit is non-zero, then level L is always used without looking \ +for the presence of an accepting self-loop.") }, { DOC("simul", "Set to 0 to disable simulation-based reductions. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ diff --git a/src/twaalgos/degen.cc b/src/twaalgos/degen.cc index 329610e62..2a3f65a57 100644 --- a/src/twaalgos/degen.cc +++ b/src/twaalgos/degen.cc @@ -426,7 +426,7 @@ namespace spot acc = otheracc; // If use_z_lvl is on, start with level zero 0 when - // swhitching SCCs + // switching SCCs unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0; // If using custom acc orders, get next level diff --git a/src/twaalgos/degen.hh b/src/twaalgos/degen.hh index 772b6c386..ff4014581 100644 --- a/src/twaalgos/degen.hh +++ b/src/twaalgos/degen.hh @@ -31,7 +31,7 @@ namespace spot /// at most (N+1) times the number of states of the original automaton. /// /// When \a use_z_lvl is set, the level of the degeneralized - /// automaton is reset everytime an accepting SCC is exited. If \a + /// automaton is reset everytime an SCC is exited. If \a /// use_cust_acc_orders is set, the degeneralization will compute a /// custom acceptance order for each SCC (this option is disabled by /// default because our benchmarks show that it usually does more