diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index 2b9453aa1..1196278a8 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -18,7 +18,7 @@ Describes the WDBA-minimization algorithm implemented in Spot. 2. Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček: Compositional Approach to Suspension and Other -Improvements to LTL Translation. Proceedings of SPIN'13. LNCS XXXX. +Improvements to LTL Translation. Proceedings of SPIN'13. LNCS 7976. Describes the compositional suspension, the simulation-based reductions, and the SCC-based simplifications. @@ -26,3 +26,4 @@ reductions, and the SCC-based simplifications. [SEE ALSO] .BR ltl2tgba (1) .BR ltl2tgta (1) +.BR dstar2tgba (1) diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc index a412ac69e..c5cbbc98e 100644 --- a/src/bin/spot-x.cc +++ b/src/bin/spot-x.cc @@ -90,6 +90,8 @@ on the Büchi automaton (i.e., after degeneralization has been performed). \ 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. \ The default is 3 in --high mode, and 0 otherwise.") }, + { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \ +Enabled by default.") }, { 0, 0, 0, 0, 0, 0 } }; diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index c033d2c8d..22b3b19b8 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -59,6 +59,7 @@ namespace spot if (dtgba_sat_minimize_ == -1 && dtgba_sat_minimize_acc_ >= 0) dtgba_sat_minimize_ = 0; state_based_ = opt->get("state-based", 0); + wdba_minimize_ = opt->get("wdba-minimize", 1); } } @@ -200,7 +201,7 @@ namespace spot // (Small,Low) is the only configuration where we do not run // WDBA-minimization. - if (pref_ != Small || level_ != Low) + if ((pref_ != Small || level_ != Low) && wdba_minimize_) { bool reject_bigger = (pref_ == Small) && (level_ == Medium); dba = minimize_obligation(a, f, 0, reject_bigger); diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 1f2b45146..915376d77 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -110,6 +110,7 @@ namespace spot int dtgba_sat_minimize_; int dtgba_sat_minimize_acc_; bool state_based_; + bool wdba_minimize_; }; /// @} }