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

Better layout of the LTL formula parse tree.

Browse source 
* src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels
for binary operators.  Gather all constants and atomic
propositions in a sub-graph with "rank=sink".
This commit is contained in:
Alexandre Duret-Lutz 2011-06-06 17:04:49 +02:00
parent 625b9362c8
commit 4087d37fe5
2 changed files with 52 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-06-06 Alexandre Duret-Lutz <adl@va-et-vient.net>
Better layout of the LTL formula parse tree.
* src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels
for binary operators. Gather all constants and atomic
propositions in a sub-graph with "rank=sink".
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add more formula families to genltl. Add more formula families to genltl.

51
src/ltlvisit/dotty.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -24,6 +26,7 @@
#include "ltlast/visitor.hh" #include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include <ostream> #include <ostream>
#include <sstream>
namespace spot namespace spot
{ {
@ -36,7 +39,7 @@ namespace spot
public: public:
typedef Sgi::hash_map<const formula*, int, ptr_hash<formula> > map; typedef Sgi::hash_map<const formula*, int, ptr_hash<formula> > map;
dotty_visitor(std::ostream& os, map& m) dotty_visitor(std::ostream& os, map& m)
: os_(os), father_(-1), node_(m) : os_(os), father_(-1), node_(m), sinks_(new std::ostringstream)
{ {
} }
@ -62,8 +65,10 @@ namespace spot
{ {
if (draw_node_(bo, bo->op_name())) if (draw_node_(bo, bo->op_name()))
{ {
dir = left;
dotty_visitor v(*this); dotty_visitor v(*this);
bo->first()->accept(v); bo->first()->accept(v);
dir = right;
bo->second()->accept(*this); bo->second()->accept(*this);
} }
} }
@ -72,8 +77,11 @@ namespace spot
visit(const unop* uo) visit(const unop* uo)
{ {
if (draw_node_(uo, uo->op_name())) if (draw_node_(uo, uo->op_name()))
{
dir = none;
uo->child()->accept(*this); uo->child()->accept(*this);
} }
}
void void
visit(const automatop*) visit(const automatop*)
@ -86,6 +94,7 @@ namespace spot
{ {
if (!draw_node_(mo, mo->op_name())) if (!draw_node_(mo, mo->op_name()))
return; return;
dir = none;
unsigned max = mo->size(); unsigned max = mo->size();
for (unsigned n = 0; n < max; ++n) for (unsigned n = 0; n < max; ++n)
{ {
@ -93,13 +102,25 @@ namespace spot
mo->nth(n)->accept(v); mo->nth(n)->accept(v);
} }
} }
void finish()
{
os_ << " subgraph atoms {" << std::endl
<< " rank=sink;" << std::endl
<< sinks_->str() << " }" << std::endl;
delete sinks_;
}
enum { left, right, none } dir;
private: private:
std::ostream& os_; std::ostream& os_;
std::ostringstream* sinks_;
int father_; int father_;
map& node_; map& node_;
bool bool
draw_node_(const formula* f, const std::string& str, bool rec = false) draw_node_(const formula* f, const std::string& str, bool sink = false)
{ {
map::iterator i = node_.find(f); map::iterator i = node_.find(f);
int node; int node;
@ -116,16 +137,29 @@ namespace spot
} }
// the link // the link
if (father_ >= 0) if (father_ >= 0)
os_ << " " << father_ << " -> " << node << ";" << std::endl; {
os_ << " " << father_ << " -> " << node;
if (dir == left)
os_ << " [taillabel=\"L\"]";
else if (dir == right)
os_ << " [taillabel=\"R\"]";
os_ << ";" << std::endl;
}
father_ = node; father_ = node;
// the node // the node
if (node_exists) if (node_exists)
return false; return false;
os_ << " " << node
<< " [label=\"" << str << "\""; if (!sink)
if (rec) {
os_ << ", shape=box"; os_ << " " << node << " [label=\"" << str << "\"];";
os_ << "];" << std::endl; }
else
{
*sinks_ << " " << node
<< " [label=\"" << str << "\", shape=box];\n";
}
return true; return true;
} }
}; };
@ -138,6 +172,7 @@ namespace spot
dotty_visitor v(os, m); dotty_visitor v(os, m);
os << "digraph G {" << std::endl; os << "digraph G {" << std::endl;
f->accept(v); f->accept(v);
v.finish();
os << "}" << std::endl; os << "}" << std::endl;
return os; return os;
} }