* src/ltlvisit/formlength.cc (length_form_vistor): Rename as ..
(length_visitor): ... this. (form_length): Rename as ... (length): ... this. * src/ltlvisit/reducform.hh (form_length): Rename as ... (length): ... this. * src/ltltest/reduc.cc: Adjust.
This commit is contained in:
parent
92767ce9d2
commit
e0ec45ed14
4 changed files with 19 additions and 11 deletions
|
|
@ -1,5 +1,13 @@
|
||||||
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/ltlvisit/formlength.cc (length_form_vistor): Rename as ..
|
||||||
|
(length_visitor): ... this.
|
||||||
|
(form_length): Rename as ...
|
||||||
|
(length): ... this.
|
||||||
|
* src/ltlvisit/reducform.hh (form_length): Rename as ...
|
||||||
|
(length): ... this.
|
||||||
|
* src/ltltest/reduc.cc: Adjust.
|
||||||
|
|
||||||
* src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove
|
* src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove
|
||||||
useless includes.
|
useless includes.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -103,7 +103,7 @@ main(int argc, char** argv)
|
||||||
spot::ltl::destroy(ftmp2);
|
spot::ltl::destroy(ftmp2);
|
||||||
|
|
||||||
|
|
||||||
int length_f1_before = spot::ltl::form_length(f1);
|
int length_f1_before = spot::ltl::length(f1);
|
||||||
std::string f1s_before = spot::ltl::to_string(f1);
|
std::string f1s_before = spot::ltl::to_string(f1);
|
||||||
|
|
||||||
ftmp1 = f1;
|
ftmp1 = f1;
|
||||||
|
|
@ -113,7 +113,7 @@ main(int argc, char** argv)
|
||||||
spot::ltl::destroy(ftmp1);
|
spot::ltl::destroy(ftmp1);
|
||||||
spot::ltl::destroy(ftmp2);
|
spot::ltl::destroy(ftmp2);
|
||||||
|
|
||||||
int length_f1_after = spot::ltl::form_length(f1);
|
int length_f1_after = spot::ltl::length(f1);
|
||||||
std::string f1s_after = spot::ltl::to_string(f1);
|
std::string f1s_after = spot::ltl::to_string(f1);
|
||||||
|
|
||||||
bool red = (length_f1_after < length_f1_before);
|
bool red = (length_f1_after < length_f1_before);
|
||||||
|
|
|
||||||
|
|
@ -27,17 +27,17 @@ namespace spot
|
||||||
namespace ltl
|
namespace ltl
|
||||||
{
|
{
|
||||||
|
|
||||||
class length_form_visitor : public const_visitor
|
class length_visitor : public const_visitor
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
||||||
length_form_visitor()
|
length_visitor()
|
||||||
{
|
{
|
||||||
result_ = 0;
|
result_ = 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual
|
virtual
|
||||||
~length_form_visitor()
|
~length_visitor()
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -62,13 +62,13 @@ namespace spot
|
||||||
void
|
void
|
||||||
visit(const unop* uo)
|
visit(const unop* uo)
|
||||||
{
|
{
|
||||||
result_ = 1 + form_length(uo->child());
|
result_ = 1 + length(uo->child());
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
visit(const binop* bo)
|
visit(const binop* bo)
|
||||||
{
|
{
|
||||||
result_ = 1 + form_length(bo->first()) + form_length(bo->second());
|
result_ = 1 + length(bo->first()) + length(bo->second());
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
|
|
@ -76,7 +76,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
unsigned mos = mo->size();
|
unsigned mos = mo->size();
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
for (unsigned i = 0; i < mos; ++i)
|
||||||
result_ += form_length(mo->nth(i));
|
result_ += length(mo->nth(i));
|
||||||
}
|
}
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
|
|
@ -84,9 +84,9 @@ namespace spot
|
||||||
};
|
};
|
||||||
|
|
||||||
int
|
int
|
||||||
form_length(const formula* f)
|
length(const formula* f)
|
||||||
{
|
{
|
||||||
length_form_visitor v;
|
length_visitor v;
|
||||||
const_cast<formula*>(f)->accept(v);
|
const_cast<formula*>(f)->accept(v);
|
||||||
return v.result();
|
return v.result();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -75,7 +75,7 @@ namespace spot
|
||||||
bool is_universal(const formula* f);
|
bool is_universal(const formula* f);
|
||||||
|
|
||||||
/// Length of a formula.
|
/// Length of a formula.
|
||||||
int form_length(const formula* f);
|
int length(const formula* f);
|
||||||
|
|
||||||
/// Type the first node of a formula.
|
/// Type the first node of a formula.
|
||||||
class node_type_form_visitor : public const_visitor
|
class node_type_form_visitor : public const_visitor
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue