dot: improve option initialization
* spot/twaalgos/dot.cc: Rearrange options to speed up their initialization and avoid an "uninitialized read" error from valgrind when compiling with clang-3.9. The uninitialized read is still a bit misterious to me; valgrind was complaining about opt_shape_ who is actually initialized in the code. However looking into the assembly code generated revealed that all consecutive 0/false values were initialized together, so this patch reorganize the options to encourage that. Also the palette was copied over for each call to print_dot(), so this is now declared statically.
This commit is contained in:
parent
48655c6875
commit
70fa739fd1
1 changed files with 36 additions and 36 deletions
|
|
@ -44,40 +44,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
constexpr int MAX_BULLET = 20;
|
constexpr int MAX_BULLET = 20;
|
||||||
|
|
||||||
class dotty_output final
|
static constexpr const char palette[][8] =
|
||||||
{
|
|
||||||
std::ostream& os_;
|
|
||||||
bool opt_force_acc_trans_ = false;
|
|
||||||
bool opt_horizontal_ = true;
|
|
||||||
bool opt_name_ = false;
|
|
||||||
enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse }
|
|
||||||
opt_shape_ = ShapeAuto;
|
|
||||||
bool opt_show_acc_ = false;
|
|
||||||
bool mark_states_ = false;
|
|
||||||
bool opt_scc_ = false;
|
|
||||||
bool opt_html_labels_ = false;
|
|
||||||
bool opt_state_labels_ = false;
|
|
||||||
const_twa_graph_ptr aut_;
|
|
||||||
std::vector<std::string>* sn_ = nullptr;
|
|
||||||
std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
|
|
||||||
std::map<unsigned, unsigned>* highlight_states_ = nullptr;
|
|
||||||
std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
|
|
||||||
std::set<unsigned>* incomplete_;
|
|
||||||
std::string* name_ = nullptr;
|
|
||||||
acc_cond::mark_t inf_sets_ = 0U;
|
|
||||||
acc_cond::mark_t fin_sets_ = 0U;
|
|
||||||
bool opt_rainbow = false;
|
|
||||||
bool opt_bullet = false;
|
|
||||||
bool opt_bullet_but_buchi = false;
|
|
||||||
bool opt_all_bullets = false;
|
|
||||||
bool opt_ordered_edges_ = false;
|
|
||||||
bool opt_numbered_edges_ = false;
|
|
||||||
bool opt_want_state_names_ = true;
|
|
||||||
unsigned opt_shift_sets_ = 0;
|
|
||||||
std::string opt_font_;
|
|
||||||
std::string opt_node_color_;
|
|
||||||
|
|
||||||
const char* const palette9[9] =
|
|
||||||
{
|
{
|
||||||
"#5DA5DA", /* blue */
|
"#5DA5DA", /* blue */
|
||||||
"#F17CB0", /* pink */
|
"#F17CB0", /* pink */
|
||||||
|
|
@ -89,10 +56,43 @@ namespace spot
|
||||||
"#4D4D4D", /* gray */
|
"#4D4D4D", /* gray */
|
||||||
"#DECF3F", /* yellow */
|
"#DECF3F", /* yellow */
|
||||||
};
|
};
|
||||||
const char*const* palette = palette9;
|
constexpr int palette_mod = sizeof(palette) / sizeof(*palette);
|
||||||
int palette_mod = 9;
|
|
||||||
unsigned max_states_ = -1U;
|
class dotty_output final
|
||||||
bool max_states_given_ = false;
|
{
|
||||||
|
// Keep all 0/false-initialized values together.
|
||||||
|
std::vector<std::string>* sn_ = nullptr;
|
||||||
|
std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
|
||||||
|
std::map<unsigned, unsigned>* highlight_states_ = nullptr;
|
||||||
|
std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
|
||||||
|
std::set<unsigned>* incomplete_ = nullptr;
|
||||||
|
std::string* name_ = nullptr;
|
||||||
|
acc_cond::mark_t inf_sets_ = 0U;
|
||||||
|
acc_cond::mark_t fin_sets_ = 0U;
|
||||||
|
unsigned opt_shift_sets_ = 0;
|
||||||
|
enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse } opt_shape_ = ShapeAuto;
|
||||||
|
bool opt_force_acc_trans_ = false;
|
||||||
|
bool opt_vertical_ = false;
|
||||||
|
bool opt_name_ = false;
|
||||||
|
bool opt_show_acc_ = false;
|
||||||
|
bool mark_states_ = false;
|
||||||
|
bool opt_scc_ = false;
|
||||||
|
bool opt_html_labels_ = false;
|
||||||
|
bool opt_state_labels_ = false;
|
||||||
|
bool opt_rainbow = false;
|
||||||
|
bool opt_bullet = false;
|
||||||
|
bool opt_bullet_but_buchi = false;
|
||||||
|
bool opt_all_bullets = false;
|
||||||
|
bool opt_ordered_edges_ = false;
|
||||||
|
bool opt_numbered_edges_ = false;
|
||||||
|
bool max_states_given_ = false; // related to max_states_
|
||||||
|
|
||||||
|
const_twa_graph_ptr aut_;
|
||||||
|
std::string opt_font_;
|
||||||
|
std::string opt_node_color_;
|
||||||
|
std::ostream& os_;
|
||||||
|
bool opt_want_state_names_ = true;
|
||||||
|
unsigned max_states_ = -1U; // related to max_states_given_
|
||||||
|
|
||||||
public:
|
public:
|
||||||
|
|
||||||
|
|
@ -212,7 +212,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
case 'h':
|
case 'h':
|
||||||
opt_horizontal_ = true;
|
opt_vertical_ = false;
|
||||||
break;
|
break;
|
||||||
case 'k':
|
case 'k':
|
||||||
opt_state_labels_ = true;
|
opt_state_labels_ = true;
|
||||||
|
|
@ -238,7 +238,7 @@ namespace spot
|
||||||
opt_scc_ = true;
|
opt_scc_ = true;
|
||||||
break;
|
break;
|
||||||
case 'v':
|
case 'v':
|
||||||
opt_horizontal_ = false;
|
opt_vertical_ = true;
|
||||||
break;
|
break;
|
||||||
case 't':
|
case 't':
|
||||||
opt_force_acc_trans_ = true;
|
opt_force_acc_trans_ = true;
|
||||||
|
|
@ -368,7 +368,7 @@ namespace spot
|
||||||
if (opt_bullet && aut_->num_sets() <= MAX_BULLET)
|
if (opt_bullet && aut_->num_sets() <= MAX_BULLET)
|
||||||
opt_all_bullets = true;
|
opt_all_bullets = true;
|
||||||
os_ << "digraph G {\n";
|
os_ << "digraph G {\n";
|
||||||
if (opt_horizontal_)
|
if (!opt_vertical_)
|
||||||
os_ << " rankdir=LR\n";
|
os_ << " rankdir=LR\n";
|
||||||
if (name_ || opt_show_acc_)
|
if (name_ || opt_show_acc_)
|
||||||
{
|
{
|
||||||
|
|
@ -442,7 +442,7 @@ namespace spot
|
||||||
if (!extra.empty())
|
if (!extra.empty())
|
||||||
os_ << " " << extra << '\n';
|
os_ << " " << extra << '\n';
|
||||||
os_ << " I [label=\"\", style=invis, ";
|
os_ << " I [label=\"\", style=invis, ";
|
||||||
os_ << (opt_horizontal_ ? "width" : "height");
|
os_ << (opt_vertical_ ? "height" : "width");
|
||||||
os_ << "=0]\n I -> " << aut_->get_init_state_number() << '\n';
|
os_ << "=0]\n I -> " << aut_->get_init_state_number() << '\n';
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue