diff --git a/ChangeLog b/ChangeLog index c13167507..2fa25bc47 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2006-02-15 Alexandre Duret-Lutz + * iface/gspn/ltlgspn.cc, src/tgbaalgos/gtec/gtec.cc, + src/tgbaalgos/gtec/gtec.hh: New option (-e6) to disable + inclusion check in the stack. + * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: Count the number of removed components. diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index eb0bb1031..0464e0309 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -73,6 +73,8 @@ syntax(char* prog) << std::endl << " -e5 use d. incl. Couvreur's emptiness-check's shy variant" << std::endl + << " -e6 like -e5, but without inclusion checks in the " + << "search stack" << std::endl #endif << " -m degeneralize and perform a magic-search" << std::endl << std::endl @@ -105,6 +107,7 @@ main(int argc, char **argv) bool proj = true; #ifdef SSP bool doublehash = true; + bool stack_inclusion = true; #endif std::string dead = "true"; @@ -155,6 +158,11 @@ main(int argc, char **argv) { check = Couvreur5; } + else if (!strcmp(argv[formula_index], "-e6")) + { + check = Couvreur5; + stack_inclusion = false; + } #endif else if (!strcmp(argv[formula_index], "-m")) { @@ -260,7 +268,7 @@ main(int argc, char **argv) ec = spot::couvreur99_check_ssp_shy_semi(prod); break; case Couvreur5: - ec = spot::couvreur99_check_ssp_shy(prod); + ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion); break; #endif default: diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 2fd4335e3..e5e6b0db5 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -973,12 +973,13 @@ namespace spot class couvreur99_check_shy_ssp : public couvreur99_check_shy { public: - couvreur99_check_shy_ssp(const tgba* a) + couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion) : couvreur99_check_shy(a, option_map(), numbered_state_heap_ssp_factory_semi::instance()), inclusion_count_heap(0), - inclusion_count_stack(0) + inclusion_count_stack(0), + stack_inclusion(stack_inclusion) { stats["inclusion count heap"] = static_cast @@ -994,6 +995,7 @@ namespace spot private: unsigned inclusion_count_heap; unsigned inclusion_count_stack; + bool stack_inclusion; protected: unsigned @@ -1064,8 +1066,9 @@ namespace spot } else { - if (spot_inclusion(old_state->left(), - new_state->left())) + if (stack_inclusion + && spot_inclusion(old_state->left(), + new_state->left())) { ++inclusion_count_stack; @@ -1197,10 +1200,10 @@ namespace spot } couvreur99_check* - couvreur99_check_ssp_shy(const tgba* ssp_automata) + couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion) { assert(dynamic_cast(ssp_automata)); - return new couvreur99_check_shy_ssp(ssp_automata); + return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion); } #if 0 diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index f32411019..f9f12fa09 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -54,7 +54,8 @@ namespace spot /// @{ couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); - couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata); + couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata, + bool stack_inclusion = true); /// @}