alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* iface/gspn/ltlgspn.cc, src/tgbaalgos/gtec/gtec.cc,

Browse source 
src/tgbaalgos/gtec/gtec.hh: New option (-e6) to disable
inclusion check in the stack.
This commit is contained in:
Alexandre Duret-Lutz 2006-02-15 15:35:38 +00:00
parent bb47e31b1e
commit afd4ea0eb4
4 changed files with 24 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2006-02-15 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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.

10
iface/gspn/ltlgspn.cc
View file

@ -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:

15
iface/gspn/ssp.cc
View file

@ -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<spot::unsigned_statistics::unsigned_fun>
@ -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<const tgba_gspn_ssp*>(ssp_automata));
return new couvreur99_check_shy_ssp(ssp_automata);
return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion);
}
#if 0

3
iface/gspn/ssp.hh
View file

@ -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);
/// @}