From 250e121a60cf50f50c287b7d72dbf033f1ff9631 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 25 Sep 2018 13:41:28 +0200
Subject: [PATCH] print_dot: add xlabel to colored states if too many colors in
 use
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Based on a report from Andreas Tollkötter.

* spot/twaalgos/dot.cc (highlight_states_show_num_): New option,
turned on implicitly when more than 8 colors are used.
* tests/core/highlightstate.test: Test it.
* NEWS: Mention it.
* THANKS: Add Andreas.
---
 NEWS                           |  6 +++
 THANKS                         |  1 +
 spot/twaalgos/dot.cc           | 16 +++++++
 tests/core/highlightstate.test | 80 +++++++++++++++++++++++++++++++++-
 4 files changed, 102 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index b663881a7..9701c15ed 100644
--- a/NEWS
+++ b/NEWS
@@ -54,6 +54,12 @@ New in spot 2.6.1.dev (not yet released)
     with arbitrary acceptance condition into a parity automaton,
     based on a last-appearance record (LAR) construction.
 
+  - 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 f80091b54..badbaa1d1 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -74,6 +74,7 @@ namespace spot
       std::vector<std::string>* sn_ = nullptr;
       std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
       std::map<unsigned, unsigned>* highlight_states_ = nullptr;
+      bool highlight_states_show_num_ = false;
       std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
       std::vector<unsigned>* orig_ = nullptr;
       std::set<unsigned>* incomplete_ = nullptr;
@@ -553,6 +554,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_;
@@ -703,6 +706,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_)
@@ -847,6 +852,17 @@ namespace spot
           aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-edges");
         highlight_states_ =
           aut->get_named_prop<std::map<unsigned, unsigned>>("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<std::set<unsigned>>("incomplete-states");
         graph_name_ = aut_->get_named_prop<std::string>("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 <<EOF
+HOA: v1
+name: "Fb & GF((a & Xb) | (!a & X!b))"
+States: 5
+Start: 0
+AP: 2 "b" "a"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+spot.highlight.states: 0 0 1 1 2 0 3 1 4 1
+--BODY--
+State: 0
+[!0&!1] 0
+[0] 1
+[!0&1] 2
+State: 1
+[!1] 3
+[1] 4
+State: 2
+[!0&!1] 0 {0}
+[!0&1] 2 {0}
+[0&!1] 3
+[0&1] 4
+State: 3
+[!0] 1 {1}
+[0&!1] 3
+[0&1] 4
+State: 4
+[0] 1 {1}
+[!0&!1] 3
+[!0&1] 4
+--END--
+EOF
+
+cat >input2.hoa <<EOF
+HOA: v1
+name: "Fb & GF((a & Xb) | (!a & X!b))"
+States: 5
+Start: 0
+AP: 2 "b" "a"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+spot.highlight.states: 0 0 1 8 2 0 3 8 4 8 /* 8 instead of 1 */
+--BODY--
+State: 0
+[!0&!1] 0
+[0] 1
+[!0&1] 2
+State: 1
+[!1] 3
+[1] 4
+State: 2
+[!0&!1] 0 {0}
+[!0&1] 2 {0}
+[0&!1] 3
+[0&1] 4
+State: 3
+[!0] 1 {1}
+[0&!1] 3
+[0&1] 4
+State: 4
+[0] 1 {1}
+[!0&!1] 3
+[!0&1] 4
+--END--
+EOF
+
+autfilt --dot input.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