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

* src/ltlvisit/dump.hh (dump): Take a formula* as argument,

Browse source 
not a formula&.  This is more homogeneous.
* src/ltlvisit/dump.cc (dump): Likewise.
* src/ltlvisit/dotty.hh (dotty): Likewise.
* src/ltlvisit/dotty.cc (dotty): Likewise.
* src/ltlvisit/tostring.hh (to_string): Likewise.
* src/ltlvisit/tostring.cc (to_string): Likewise.
* src/ltltest/readltl.cc, src/ltltest/equals.cc,
src/ltltest/tostring.cc: Adjust usage.
This commit is contained in:
Alexandre Duret-Lutz 2003-05-16 08:10:58 +00:00
parent 35f77be6c7
commit 7685d3a5b8
10 changed files with 70 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,9 +1,19 @@
2003-05-16 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-05-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlvisit/dump.hh (dump): Take a formula* as argument,
not a formula&. This is more homogeneous.
* src/ltlvisit/dump.cc (dump): Likewise.
* src/ltlvisit/dotty.hh (dotty): Likewise.
* src/ltlvisit/dotty.cc (dotty): Likewise.
* src/ltlvisit/tostring.hh (to_string): Likewise.
* src/ltlvisit/tostring.cc (to_string): Likewise.
* src/ltltest/readltl.cc, src/ltltest/equals.cc,
src/ltltest/tostring.cc: Adjust usage.
Check trivial multop equality at build time. The makes the Check trivial multop equality at build time. The makes the
equal visitor useless, since two equals formulae will now equal visitor useless, since two equals formulae will now
share the same address. share the same address.
* src/ltlast/multop.hh (add_sorted): New function. * src/ltlast/multop.hh (add_sorted): New function.
(paircmp): New comparison functor. (paircmp): New comparison functor.
(map): Use paircmp, we want to compare the vectors' contents, (map): Use paircmp, we want to compare the vectors' contents,

9
src/ltltest/equals.cc
View file

@ -38,26 +38,23 @@ main(int argc, char** argv)
#endif #endif
#ifdef LUNABBREV #ifdef LUNABBREV
tmp = f1; tmp = f1;
std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
f1 = spot::ltl::unabbreviate_logic(f1); f1 = spot::ltl::unabbreviate_logic(f1);
std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; spot::ltl::dump(f1, std::cout);
spot::ltl::dump(*f1, std::cout);
std::cout << std::endl; std::cout << std::endl;
#endif #endif
#ifdef TUNABBREV #ifdef TUNABBREV
tmp = f1; tmp = f1;
f1 = spot::ltl::unabbreviate_ltl(f1); f1 = spot::ltl::unabbreviate_ltl(f1);
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
spot::ltl::dump(*f1, std::cout); spot::ltl::dump(f1, std::cout);
std::cout << std::endl; std::cout << std::endl;
#endif #endif
#ifdef NENOFORM #ifdef NENOFORM
tmp = f1; tmp = f1;
f1 = spot::ltl::negative_normal_form(f1); f1 = spot::ltl::negative_normal_form(f1);
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
spot::ltl::dump(*f1, std::cout); spot::ltl::dump(f1, std::cout);
std::cout << std::endl; std::cout << std::endl;
#endif #endif

4
src/ltltest/readltl.cc
View file

@ -43,9 +43,9 @@ main(int argc, char** argv)
if (f) if (f)
{ {
#ifdef DOTTY #ifdef DOTTY
spot::ltl::dotty(*f, std::cout); spot::ltl::dotty(f, std::cout);
#else #else
spot::ltl::dump(*f, std::cout); spot::ltl::dump(f, std::cout);
std::cout << std::endl; std::cout << std::endl;
#endif #endif
spot::ltl::destroy(f); spot::ltl::destroy(f);

4
src/ltltest/tostring.cc
View file

@ -26,7 +26,7 @@ main(int argc, char **argv)
// The string generated from an abstract tree should be parsable // The string generated from an abstract tree should be parsable
// again. // again.
std::string f1s = spot::ltl::to_string(*f1); std::string f1s = spot::ltl::to_string(f1);
std::cout << f1s << std::endl; std::cout << f1s << std::endl;
spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1);
@ -41,7 +41,7 @@ main(int argc, char **argv)
// It should also map to the same string. // It should also map to the same string.
std::string f2s = spot::ltl::to_string(*f2); std::string f2s = spot::ltl::to_string(f2);
std::cout << f2s << std::endl; std::cout << f2s << std::endl;
if (f2s != f1s) if (f2s != f1s)

26
src/ltlvisit/dotty.cc
View file

@ -3,7 +3,7 @@
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
@ -16,12 +16,12 @@ namespace spot
{ {
} }
virtual virtual
~dotty_visitor() ~dotty_visitor()
{ {
} }
void void
visit(const spot::ltl::atomic_prop* ap) visit(const spot::ltl::atomic_prop* ap)
{ {
draw_node_(ap->name()); draw_node_(ap->name());
@ -32,20 +32,20 @@ namespace spot
{ {
draw_node_(c->val_name()); draw_node_(c->val_name());
} }
void void
visit(const spot::ltl::binop* bo) visit(const spot::ltl::binop* bo)
{ {
draw_rec_node_(bo->op_name()); draw_rec_node_(bo->op_name());
std::string label = label_; std::string label = label_;
label_ += "l"; label_ += "l";
draw_link_(label, label_); draw_link_(label, label_);
bo->first()->accept(*this); bo->first()->accept(*this);
label_ = draw_link_(label, label + "r"); label_ = draw_link_(label, label + "r");
bo->second()->accept(*this); bo->second()->accept(*this);
} }
void void
visit(const spot::ltl::unop* uo) visit(const spot::ltl::unop* uo)
{ {
@ -53,7 +53,7 @@ namespace spot
label_ = draw_link_(label_, label_ + "c"); label_ = draw_link_(label_, label_ + "c");
uo->child()->accept(*this); uo->child()->accept(*this);
} }
void void
visit(const spot::ltl::multop* mo) visit(const spot::ltl::multop* mo)
{ {
@ -79,10 +79,10 @@ namespace spot
return out; return out;
} }
void void
draw_rec_node_(const char* str) const draw_rec_node_(const char* str) const
{ {
os_ << " " << label_ << " [label=\"" << str << "\", shabe=box];" os_ << " " << label_ << " [label=\"" << str << "\", shabe=box];"
<< std::endl; << std::endl;
} }
@ -91,15 +91,15 @@ namespace spot
{ {
os_ << " " << label_ << " [label=\"" << str << "\"];" << std::endl; os_ << " " << label_ << " [label=\"" << str << "\"];" << std::endl;
} }
}; };
void void
dotty(const formula& f, std::ostream& os) dotty(const formula* f, std::ostream& os)
{ {
dotty_visitor v(os); dotty_visitor v(os);
os << "digraph G {" << std::endl; os << "digraph G {" << std::endl;
f.accept(v); f->accept(v);
os << "}" << std::endl; os << "}" << std::endl;
} }

4
src/ltlvisit/dotty.hh
View file

@ -4,7 +4,7 @@
#include <ltlast/formula.hh> #include <ltlast/formula.hh>
#include <iostream> #include <iostream>
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
@ -14,7 +14,7 @@ namespace spot
/// ///
/// \c dot is part of the GraphViz package /// \c dot is part of the GraphViz package
/// http://www.research.att.com/sw/tools/graphviz/ /// http://www.research.att.com/sw/tools/graphviz/
void dotty(const formula& f, std::ostream& os); void dotty(const formula* f, std::ostream& os);
} }
} }

22
src/ltlvisit/dump.cc
View file

@ -3,7 +3,7 @@
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
@ -15,13 +15,13 @@ namespace spot
: os_(os) : os_(os)
{ {
} }
virtual virtual
~dump_visitor() ~dump_visitor()
{ {
} }
void void
visit(const spot::ltl::atomic_prop* ap) visit(const spot::ltl::atomic_prop* ap)
{ {
os_ << "AP(" << ap->name() << ")"; os_ << "AP(" << ap->name() << ")";
@ -31,8 +31,8 @@ namespace spot
visit(const spot::ltl::constant* c) visit(const spot::ltl::constant* c)
{ {
os_ << "constant(" << c->val_name() << ")"; os_ << "constant(" << c->val_name() << ")";
} }
void void
visit(const spot::ltl::binop* bo) visit(const spot::ltl::binop* bo)
{ {
@ -42,7 +42,7 @@ namespace spot
bo->second()->accept(*this); bo->second()->accept(*this);
os_ << ")"; os_ << ")";
} }
void void
visit(const spot::ltl::unop* uo) visit(const spot::ltl::unop* uo)
{ {
@ -50,7 +50,7 @@ namespace spot
uo->child()->accept(*this); uo->child()->accept(*this);
os_ << ")"; os_ << ")";
} }
void void
visit(const spot::ltl::multop* mo) visit(const spot::ltl::multop* mo)
{ {
@ -68,11 +68,11 @@ namespace spot
std::ostream& os_; std::ostream& os_;
}; };
void void
dump(const formula& f, std::ostream& os) dump(const formula* f, std::ostream& os)
{ {
dump_visitor v(os); dump_visitor v(os);
f.accept(v); f->accept(v);
} }
} }

4
src/ltlvisit/dump.hh
View file

@ -4,7 +4,7 @@
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
#include <iostream> #include <iostream>
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
@ -13,7 +13,7 @@ namespace spot
/// \param os The stream where it should be output. /// \param os The stream where it should be output.
/// ///
/// This is useful to display a formula when debugging. /// This is useful to display a formula when debugging.
void dump(const formula& f, std::ostream& os); void dump(const formula* f, std::ostream& os);
} }
} }

42
src/ltlvisit/tostring.cc
View file

@ -5,7 +5,7 @@
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
@ -17,13 +17,13 @@ namespace spot
: os_(os) : os_(os)
{ {
} }
virtual virtual
~to_string_visitor() ~to_string_visitor()
{ {
} }
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
os_ << ap->name(); os_ << ap->name();
@ -33,14 +33,14 @@ namespace spot
visit(const constant* c) visit(const constant* c)
{ {
os_ << c->val_name(); os_ << c->val_name();
} }
void void
visit(const binop* bo) visit(const binop* bo)
{ {
os_ << "("; os_ << "(";
bo->first()->accept(*this); bo->first()->accept(*this);
switch(bo->op()) switch(bo->op())
{ {
case binop::Xor: case binop::Xor:
@ -59,14 +59,14 @@ namespace spot
os_ << " R "; os_ << " R ";
break; break;
} }
bo->second()->accept(*this); bo->second()->accept(*this);
os_ << ")"; os_ << ")";
} }
void void
visit(const unop* uo) visit(const unop* uo)
{ {
switch(uo->op()) switch(uo->op())
{ {
case unop::Not: case unop::Not:
@ -82,10 +82,10 @@ namespace spot
os_ << "G"; os_ << "G";
break; break;
} }
uo->child()->accept(*this); uo->child()->accept(*this);
} }
void void
visit(const multop* mo) visit(const multop* mo)
{ {
@ -97,12 +97,12 @@ namespace spot
{ {
case multop::Or: case multop::Or:
ch = " | "; ch = " | ";
break; break;
case multop::And: case multop::And:
ch = " & "; ch = " & ";
break; break;
} }
for (unsigned n = 1; n < max; ++n) for (unsigned n = 1; n < max; ++n)
{ {
os_ << ch; os_ << ch;
@ -113,16 +113,16 @@ namespace spot
private: private:
std::ostream& os_; std::ostream& os_;
}; };
void void
to_string(const formula& f, std::ostream& os) to_string(const formula* f, std::ostream& os)
{ {
to_string_visitor v(os); to_string_visitor v(os);
f.accept(v); f->accept(v);
} }
std::string std::string
to_string(const formula& f) to_string(const formula* f)
{ {
std::ostringstream os; std::ostringstream os;
to_string(f, os); to_string(f, os);

6
src/ltlvisit/tostring.hh
View file

@ -4,12 +4,12 @@
#include <ltlast/formula.hh> #include <ltlast/formula.hh>
#include <iostream> #include <iostream>
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
void to_string(const formula& f, std::ostream& os); void to_string(const formula* f, std::ostream& os);
std::string to_string(const formula& f); std::string to_string(const formula* f);
} }
} }