diff --git a/NEWS b/NEWS index 4cd48b3e0..dd92da130 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,14 @@ New in spot 2.6.1.dev (not yet released) code for the online translator. Its replacement has its own repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/ + Library: + + - When states are highlighted with more than 8 colors, print_dot() + will add some extra markers to help distinguishing the colors. + This helps with the fact that colors 8-15 are lighter versions of + colors 0-7, and that higher color numbers cycle into this 16-color + palette. + New in spot 2.6.1 (2018-08-04) Command-line tools: diff --git a/THANKS b/THANKS index 3e1e9ab7c..9ffee837f 100644 --- a/THANKS +++ b/THANKS @@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or suggestions. Akim Demaille +Andreas Tollkötter Anton Pirogov Ayrat Khalimov Caroline Lemieux diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 86465dc18..5cbbd4e0d 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -73,6 +73,7 @@ namespace spot std::vector* sn_ = nullptr; std::map* highlight_edges_ = nullptr; std::map* highlight_states_ = nullptr; + bool highlight_states_show_num_ = false; std::vector>* sprod_ = nullptr; std::vector* orig_ = nullptr; std::set* incomplete_ = nullptr; @@ -552,6 +553,8 @@ namespace spot } if (!opt_vertical_) os_ << " rankdir=LR\n"; + if (highlight_states_show_num_) + os_ << " forcelabels=true\n"; if (name_ || opt_show_acc_) { os_ << " " << label_pre_; @@ -702,6 +705,8 @@ namespace spot os_ << ",filled"; os_ << "\", color=\"" << palette[iter->second % palette_mod] << '"'; + if (highlight_states_show_num_) + os_ << ", xlabel=\"[" << iter->second << "]\""; } } if (!inline_state_names_ && (sn_ || sprod_ || opt_state_labels_) @@ -846,6 +851,17 @@ namespace spot aut->get_named_prop>("highlight-edges"); highlight_states_ = aut->get_named_prop>("highlight-states"); + if (highlight_states_) + { + // If we use more than palette_mod/2 colors, we will use + // some extra markers to distinguish colors. + auto e = highlight_states_->end(); + highlight_states_show_num_ = + std::find_if(highlight_states_->begin(), e, + [](auto p){ + return p.second >= palette_mod / 2; + }) != e; + } incomplete_ = aut->get_named_prop>("incomplete-states"); graph_name_ = aut_->get_named_prop("automaton-name"); diff --git a/tests/core/highlightstate.test b/tests/core/highlightstate.test index 618a22b50..001d9e2f1 100755 --- a/tests/core/highlightstate.test +++ b/tests/core/highlightstate.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -113,3 +113,81 @@ EOF autfilt aut.hoa --highlight-languages -H1.1 | grep spot.highlight.states >res diff expected res + + +cat >input.hoa <input2.hoa < output.dot +grep xlabel output.dot && exit 1 +grep forcelabels output.dot && exit 1 +autfilt --dot input2.hoa > output2.dot +grep xlabel output2.dot +grep forcelabels output2.dot