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

* src/ltlvisit/reducform.hh (option): Rename as ...

(reduce_options): ... this, and use it as a bit field so
option can be combined easily.
(reduce): Adjust argument.
(reduce_form): Remove, not needed anymore.
* src/ltlvisit/reducform.cc, src/ltltest/reduc.cc,
src/tgbatest/ltl2tgba.cc: Adjust.
parent 7eb5f3d8
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/reducform.hh (option): Rename as ...
(reduce_options): ... this, and use it as a bit field so
option can be combined easily.
(reduce): Adjust argument.
(reduce_form): Remove, not needed anymore.
* src/ltlvisit/reducform.cc, src/ltltest/reduc.cc,
src/tgbatest/ltl2tgba.cc: Adjust.
* src/sanity/style.test: Catch {.*{ and }.*}. * src/sanity/style.test: Catch {.*{ and }.*}.
* src/sanity/80columns.test: Untabify files. * src/sanity/80columns.test: Untabify files.
* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines. * iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.
......
...@@ -44,29 +44,31 @@ main(int argc, char** argv) ...@@ -44,29 +44,31 @@ main(int argc, char** argv)
if (argc < 3) if (argc < 3)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::option o; int o = spot::ltl::Reduce_None;
switch (atoi(argv[1])) switch (atoi(argv[1]))
{ {
case 0: case 0:
o = spot::ltl::Base; o = spot::ltl::Reduce_Basics;
break; break;
case 1: case 1:
o = spot::ltl::Inf; o = spot::ltl::Reduce_Syntactic_Implications;
break; break;
case 2: case 2:
o = spot::ltl::EventualUniversal; o = spot::ltl::Reduce_Eventuality_And_Universality;
break; break;
case 3: case 3:
o = spot::ltl::BRI; o = spot::ltl::Reduce_All;
break; break;
case 4: case 4:
o = spot::ltl::InfBase; o = spot::ltl::Reduce_Basics | spot::ltl::Reduce_Syntactic_Implications;
break; break;
case 5: case 5:
o = spot::ltl::EventualUniversalBase; o = (spot::ltl::Reduce_Basics
| spot::ltl::Reduce_Eventuality_And_Universality);
break; break;
case 6: case 6:
o = spot::ltl::InfEventualUniversal; o = (spot::ltl::Reduce_Syntactic_Implications
| spot::ltl::Reduce_Eventuality_And_Universality);
break; break;
default: default:
return 2; return 2;
......
...@@ -36,9 +36,9 @@ namespace spot ...@@ -36,9 +36,9 @@ namespace spot
{ {
public: public:
reduce_form_visitor(option o) reduce_form_visitor(int opt)
: opt_(opt)
{ {
this->o = o;
} }
virtual ~reduce_form_visitor() virtual ~reduce_form_visitor()
...@@ -61,17 +61,7 @@ namespace spot ...@@ -61,17 +61,7 @@ namespace spot
void void
visit(constant* c) visit(constant* c)
{ {
switch (c->val()) result_ = c;
{
case constant::True:
result_ = constant::true_instance();
return;
case constant::False:
result_ = constant::false_instance();
return;
}
/* Unreachable code. */
assert(0);
} }
void void
...@@ -90,14 +80,16 @@ namespace spot ...@@ -90,14 +80,16 @@ namespace spot
return; return;
case unop::F: case unop::F:
/* If f is class of eventuality then F(f)=f. */ /* If f is a pure eventuality formula then F(f)=f. */
if (!is_eventual(result_) || o == Inf || o == InfBase) if (!(opt_ & Reduce_Eventuality_And_Universality)
|| !is_eventual(result_))
result_ = unop::instance(unop::F, result_); result_ = unop::instance(unop::F, result_);
return; return;
case unop::G: case unop::G:
/* If f is class of universality then G(f)=f. */ /* If f is a pure universality formula then G(f)=f. */
if (!is_universal(result_) || o == Inf || o == InfBase) if (!(opt_ & Reduce_Eventuality_And_Universality)
|| !is_universal(result_))
result_ = unop::instance(unop::G, result_); result_ = unop::instance(unop::G, result_);
return; return;
} }
...@@ -110,9 +102,9 @@ namespace spot ...@@ -110,9 +102,9 @@ namespace spot
{ {
formula* f2 = recurse(bo->second()); formula* f2 = recurse(bo->second());
/* If b is of class eventuality then a U b = b. /* If b is a pure eventuality formula then a U b = b.
If b is of class universality then a R b = b. */ If b is a pure universality formula a R b = b. */
if ((o != Inf) && (o != InfBase) if ((opt_ & Reduce_Eventuality_And_Universality)
&& ((is_eventual(f2) && ((bo->op()) == binop::U)) && ((is_eventual(f2) && ((bo->op()) == binop::U))
|| (is_universal(f2) && ((bo->op()) == binop::R)))) || (is_universal(f2) && ((bo->op()) == binop::R))))
{ {
...@@ -122,7 +114,7 @@ namespace spot ...@@ -122,7 +114,7 @@ namespace spot
/* case of implies */ /* case of implies */
formula* f1 = recurse(bo->first()); formula* f1 = recurse(bo->first());
if (o != EventualUniversal && o != EventualUniversalBase) if (opt_ & Reduce_Syntactic_Implications)
{ {
bool inf = inf_form(f1, f2); bool inf = inf_form(f1, f2);
bool infinv = inf_form(f2, f1); bool infinv = inf_form(f2, f1);
...@@ -206,7 +198,7 @@ namespace spot ...@@ -206,7 +198,7 @@ namespace spot
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i))); res->push_back(recurse(mo->nth(i)));
if (o != EventualUniversal && o != EventualUniversalBase) if (opt_ & Reduce_Syntactic_Implications)
{ {
switch (mo->op()) switch (mo->op())
{ {
...@@ -297,82 +289,52 @@ namespace spot ...@@ -297,82 +289,52 @@ namespace spot
formula* formula*
recurse(formula* f) recurse(formula* f)
{ {
return reduce_form(f, o); return reduce(f, opt_);
} }
protected: protected:
formula* result_; formula* result_;
option o; int opt_;
}; };
formula* formula*
reduce_form(const formula* f, option o) reduce(const formula* f, int opt)
{ {
formula* ftmp1 = NULL; formula* f1;
formula* ftmp2 = NULL; formula* f2;
reduce_form_visitor v(o);
if (o == BRI || o == InfBase || f1 = unabbreviate_logic(f);
o == EventualUniversalBase) f2 = negative_normal_form(f1);
{ destroy(f1);
ftmp1 = basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = basic_reduce_form(v.result());
destroy(ftmp1);
destroy(v.result());
return ftmp2; if (opt & Reduce_Basics)
}
else
{ {
const_cast<formula*>(f)->accept(v); f1 = basic_reduce_form(f2);
return v.result(); destroy(f2);
f2 = f1;
} }
if (opt & (Reduce_Syntactic_Implications
/* unreachable code */ | Reduce_Eventuality_And_Universality))
assert(0);
}
formula*
reduce(const formula* f, option o)
{
formula* ftmp1;
formula* ftmp2;
formula* ftmp3;
ftmp1 = unabbreviate_logic(f);
ftmp2 = negative_normal_form(ftmp1);
switch (o)
{ {
case Base: reduce_form_visitor v(opt);
ftmp3 = basic_reduce_form(ftmp2); f2->accept(v);
break; f1 = v.result();
case Inf: destroy(f2);
ftmp3 = reduce_form(ftmp2, o); f2 = f1;
break;
case InfBase: // Run basic_reduce_form again.
ftmp3 = reduce_form(ftmp2, o); //
break; // Consider `F b & g' were g is an eventual formula rewritten
case EventualUniversal: // as `g = F c' Then basic_reduce_form with rewrite it
ftmp3 = reduce_form(ftmp2, o); // as F(b & c).
break; if (opt & Reduce_Basics)
case EventualUniversalBase: {
ftmp3 = reduce_form(ftmp2, o); f1 = basic_reduce_form(f2);
break; destroy(f2);
case InfEventualUniversal: f2 = f1;
ftmp3 = reduce_form(ftmp2, o); }
break;
case BRI:
ftmp3 = reduce_form(ftmp2, o);
break;
default:
assert(0);
} }
destroy(ftmp1); return f2;
destroy(ftmp2);
return ftmp3;
} }
} }
} }
...@@ -29,13 +29,15 @@ namespace spot ...@@ -29,13 +29,15 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
enum option {Base,
Inf, enum reduce_options
InfBase, {
EventualUniversal, Reduce_None = 0,
EventualUniversalBase, Reduce_Basics = 1,
InfEventualUniversal, Reduce_Syntactic_Implications = 2,
BRI}; Reduce_Eventuality_And_Universality = 4,
Reduce_All = -1U
};
/// \brief Reduce a formula \a f using Basic rewriting, implies /// \brief Reduce a formula \a f using Basic rewriting, implies
/// relation, and class of eventuality and univerality formula. /// relation, and class of eventuality and univerality formula.
...@@ -47,15 +49,11 @@ namespace spot ...@@ -47,15 +49,11 @@ namespace spot
/// Inf for spot::ltl::reduce_inf_form, /// Inf for spot::ltl::reduce_inf_form,
/// EventualUniversal for spot::ltl::reduce_eventuality_universality_form, /// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
/// BRI for spot::ltl::reduce_form. /// BRI for spot::ltl::reduce_form.
formula* reduce(const formula* f, option opt = BRI); formula* reduce(const formula* f, int opt = Reduce_All);
/// Implement basic rewriting. /// Implement basic rewriting.
formula* basic_reduce_form(const formula* f); formula* basic_reduce_form(const formula* f);
/// Implement rewritings rules using implies relation,
/// and class of eventuality and univerality formula.
formula* reduce_form(const formula* f, option o = BRI);
/// Detect easy case of implies. /// Detect easy case of implies.
/// True if f1 < f2, false otherwise. /// True if f1 < f2, false otherwise.
bool inf_form(const formula* f1, const formula* f2); bool inf_form(const formula* f1, const formula* f2);
......
...@@ -120,10 +120,7 @@ main(int argc, char** argv) ...@@ -120,10 +120,7 @@ main(int argc, char** argv)
bool magic_many = false; bool magic_many = false;
bool expect_counter_example = false; bool expect_counter_example = false;
bool from_file = false; bool from_file = false;
bool reduc_r1 = false; int redopt = spot::ltl::Reduce_None;
bool reduc_r2 = false;
bool reduc_r3 = false;
bool reduc_r4 = false;
bool post_branching = false; bool post_branching = false;
bool fair_loop_approx = false; bool fair_loop_approx = false;
...@@ -223,6 +220,22 @@ main(int argc, char** argv) ...@@ -223,6 +220,22 @@ main(int argc, char** argv)
{ {
output = 1; output = 1;
} }
else if (!strcmp(argv[formula_index], "-r1"))
{
redopt |= spot::ltl::Reduce_Basics;
}
else if (!strcmp(argv[formula_index], "-r2"))
{
redopt |= spot::ltl::Reduce_Syntactic_Implications;
}
else if (!strcmp(argv[formula_index], "-r3"))
{
redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
}
else if (!strcmp(argv[formula_index], "-r4"))
{
redopt |= spot::ltl::Reduce_All;
}
else if (!strcmp(argv[formula_index], "-R")) else if (!strcmp(argv[formula_index], "-R"))
{ {
output = 3; output = 3;
...@@ -261,22 +274,6 @@ main(int argc, char** argv) ...@@ -261,22 +274,6 @@ main(int argc, char** argv)
fm_opt = true; fm_opt = true;
fm_symb_merge_opt = false; fm_symb_merge_opt = false;
} }
else if (!strcmp(argv[formula_index], "-r1"))
{
reduc_r1 = true;
}
else if (!strcmp(argv[formula_index], "-r2"))
{
reduc_r2 = true;
}
else if (!strcmp(argv[formula_index], "-r3"))
{
reduc_r3 = true;
}
else if (!strcmp(argv[formula_index], "-r4"))
{
reduc_r4 = true;
}
else else
{ {
break; break;
...@@ -339,29 +336,11 @@ main(int argc, char** argv) ...@@ -339,29 +336,11 @@ main(int argc, char** argv)
} }
else else
{ {
if (redopt != spot::ltl::Reduce_None)
spot::ltl::formula* ftmp = f;
if (reduc_r4)
{
f = spot::ltl::reduce(f);
}
else if (reduc_r1 | reduc_r2 | reduc_r3)
{ {
spot::ltl::option o = spot::ltl::BRI; spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
if (reduc_r1 & !reduc_r2 & !reduc_r3) spot::ltl::destroy(f);
o = spot::ltl::Base; f = t;
if (!reduc_r1 & reduc_r2 & !reduc_r3)
o = spot::ltl::EventualUniversal;
if (reduc_r1 & reduc_r2 & !reduc_r3)
o = spot::ltl::EventualUniversalBase;
if (!reduc_r1 & !reduc_r2 & reduc_r3)
o = spot::ltl::Inf;
if (reduc_r1 & !reduc_r2 & reduc_r3)
o = spot::ltl::InfBase;
if (!reduc_r1 & reduc_r2 & reduc_r3)
o = spot::ltl::InfEventualUniversal;
f = spot::ltl::reduce(f, o);
} }
if (fm_opt) if (fm_opt)
...@@ -371,11 +350,6 @@ main(int argc, char** argv) ...@@ -371,11 +350,6 @@ main(int argc, char** argv)
fair_loop_approx); fair_loop_approx);
else else
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
if (reduc_r1 || reduc_r2 || reduc_r3 || reduc_r4)
{
spot::ltl::destroy(ftmp);
}
} }
spot::tgba_tba_proxy* degeneralized = 0; spot::tgba_tba_proxy* degeneralized = 0;
......
Markdown is supported
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