Commit d3b5e5bd authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add option -e54 to ltlgspn-ssp

parent 8c0d1003
2008-08-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/gspn/ltlgspn.cc: New option: -e54.
* iface/gspn/ssp.hh, iface/gspn/ssp.cc: Add the
reversed_double_inclusion boolean for this.
2008-06-12 Damien Lefortier <dam@lrde.epita.fr> 2008-06-12 Damien Lefortier <dam@lrde.epita.fr>
Add ELTL visitors in eltlvisit/ and start the ELTL translation (LACIM). Add ELTL visitors in eltlvisit/ and start the ELTL translation (LACIM).
......
...@@ -73,7 +73,9 @@ syntax(char* prog) ...@@ -73,7 +73,9 @@ syntax(char* prog)
<< " -e4 use semi-d. incl. Couvreur's emptiness-check's " << " -e4 use semi-d. incl. Couvreur's emptiness-check's "
<< "shy variant" << "shy variant"
<< std::endl << std::endl
<< " -e45 mix of -e4 and -e5 " << std::endl << " -e45 mix of -e4 and -e5 (semi.d. incl. before d.incl.)"
<< std::endl
<< " -e54 mix of -e5 and -e4 (the other way around)" << std::endl
<< " -e5 use d. incl. Couvreur's emptiness-check's shy variant" << " -e5 use d. incl. Couvreur's emptiness-check's shy variant"
<< std::endl << std::endl
<< " -e6 like -e5, but without inclusion checks in the " << " -e6 like -e5, but without inclusion checks in the "
...@@ -116,6 +118,7 @@ main(int argc, char **argv) ...@@ -116,6 +118,7 @@ main(int argc, char **argv)
bool stack_inclusion = true; bool stack_inclusion = true;
bool pushfront = false; bool pushfront = false;
bool double_inclusion = false; bool double_inclusion = false;
bool reversed_double_inclusion = false;
bool no_decomp = false; bool no_decomp = false;
#endif #endif
std::string dead = "true"; std::string dead = "true";
...@@ -172,6 +175,12 @@ main(int argc, char **argv) ...@@ -172,6 +175,12 @@ main(int argc, char **argv)
check = Couvreur5; check = Couvreur5;
double_inclusion = true; double_inclusion = true;
} }
else if (!strcmp(argv[formula_index], "-e54"))
{
check = Couvreur5;
double_inclusion = true;
reversed_double_inclusion = true;
}
else if (!strcmp(argv[formula_index], "-e5")) else if (!strcmp(argv[formula_index], "-e5"))
{ {
check = Couvreur5; check = Couvreur5;
...@@ -295,6 +304,7 @@ main(int argc, char **argv) ...@@ -295,6 +304,7 @@ main(int argc, char **argv)
case Couvreur5: case Couvreur5:
ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion, ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion,
double_inclusion, double_inclusion,
reversed_double_inclusion,
no_decomp); no_decomp);
break; break;
#endif #endif
......
...@@ -994,7 +994,9 @@ namespace spot ...@@ -994,7 +994,9 @@ namespace spot
{ {
public: public:
couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion, couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion,
bool double_inclusion, bool no_decomp) bool double_inclusion,
bool reversed_double_inclusion,
bool no_decomp)
: couvreur99_check_shy(a, : couvreur99_check_shy(a,
option_map(), option_map(),
numbered_state_heap_ssp_factory_semi::instance()), numbered_state_heap_ssp_factory_semi::instance()),
...@@ -1002,6 +1004,7 @@ namespace spot ...@@ -1002,6 +1004,7 @@ namespace spot
inclusion_count_stack(0), inclusion_count_stack(0),
stack_inclusion(stack_inclusion), stack_inclusion(stack_inclusion),
double_inclusion(double_inclusion), double_inclusion(double_inclusion),
reversed_double_inclusion(reversed_double_inclusion),
no_decomp(no_decomp) no_decomp(no_decomp)
{ {
onepass_ = true; onepass_ = true;
...@@ -1022,6 +1025,7 @@ namespace spot ...@@ -1022,6 +1025,7 @@ namespace spot
unsigned inclusion_count_stack; unsigned inclusion_count_stack;
bool stack_inclusion; bool stack_inclusion;
bool double_inclusion; bool double_inclusion;
bool reversed_double_inclusion;
bool no_decomp; bool no_decomp;
protected: protected:
...@@ -1110,6 +1114,7 @@ namespace spot ...@@ -1110,6 +1114,7 @@ namespace spot
{ {
if (stack_inclusion if (stack_inclusion
&& double_inclusion && double_inclusion
&& !reversed_double_inclusion
&& spot_inclusion(new_state->left(), && spot_inclusion(new_state->left(),
old_state->left())) old_state->left()))
break; break;
...@@ -1181,6 +1186,12 @@ namespace spot ...@@ -1181,6 +1186,12 @@ namespace spot
break; break;
} }
if (stack_inclusion
&& double_inclusion
&& reversed_double_inclusion
&& spot_inclusion(new_state->left(),
old_state->left()))
break;
} }
} }
} }
...@@ -1296,11 +1307,15 @@ namespace spot ...@@ -1296,11 +1307,15 @@ namespace spot
couvreur99_check* couvreur99_check*
couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion, couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion,
bool double_inclusion, bool no_decomp) bool double_inclusion,
bool reversed_double_inclusion,
bool no_decomp)
{ {
assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata)); assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion, return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion,
double_inclusion, no_decomp); double_inclusion,
reversed_double_inclusion,
no_decomp);
} }
#if 0 #if 0
......
// Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2006, 2007, 2008 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC), // Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie. // Universit Pierre et Marie Curie.
// //
...@@ -58,6 +58,8 @@ namespace spot ...@@ -58,6 +58,8 @@ namespace spot
couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata, couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata,
bool stack_inclusion = true, bool stack_inclusion = true,
bool double_inclusion = false, bool double_inclusion = false,
bool reversed_double_inclusion
= false,
bool no_decomp = false); bool no_decomp = false);
/// @} /// @}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment