From 55c50c65c870eea205c503c558d60d30f9350b7d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 20 Mar 2019 21:46:49 +0100
Subject: [PATCH] autfilt: add support for --highlight-accepting-run

Fixes #381.

* bin/autfilt.cc: Here.
* tests/core/highlightstate.test: Test it.
* NEWS: Mention it.
---
 NEWS                           |  7 +++++-
 bin/autfilt.cc                 | 13 ++++++++++-
 tests/core/highlightstate.test | 42 +++++++++++++++++++++++++++++++++-
 3 files changed, 59 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 5385682e0..5e197289e 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,10 @@
 New in spot 2.7.2.dev (not yet released)
 
+  Command-line tools:
+
+  - autfilt learned --highlight-accepting-run=NUM to highlight some
+    accepting run with color NUM.
+
   Library:
 
   - Add generic_accepting_run() as a variant of generic_emptiness_check() that
@@ -44,7 +49,7 @@ New in spot 2.7.2 (2019-03-17)
 
 New in spot 2.7.1 (2019-02-14)
 
-  Build
+  Build:
 
   - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr
     exceptions when Spot is compiled with the version of g++ 8.2 currently
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index 71ba08ffc..6b8f658ca 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -110,6 +110,7 @@ enum {
   OPT_HIGHLIGHT_NONDET_EDGES,
   OPT_HIGHLIGHT_NONDET_STATES,
   OPT_HIGHLIGHT_WORD,
+  OPT_HIGHLIGHT_ACCEPTING_RUN,
   OPT_HIGHLIGHT_LANGUAGES,
   OPT_INSTUT,
   OPT_INCLUDED_IN,
@@ -373,6 +374,8 @@ static const argp_option options[] =
       "(see spot-x)."
       , 0 },
     { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
+    { "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM",
+      OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0},
     { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
       OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
       0 },
@@ -628,6 +631,7 @@ static bool opt_split_edges = false;
 static const char* opt_sat_minimize = nullptr;
 static int opt_highlight_nondet_states = -1;
 static int opt_highlight_nondet_edges = -1;
+static int opt_highlight_accepting_run = -1;
 static bool opt_highlight_languages = false;
 static bool opt_dca = false;
 static bool opt_streett_like = false;
@@ -844,6 +848,10 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_HAS_UNIV_BRANCHING:
       opt_has_univ_branching = true;
       break;
+    case OPT_HIGHLIGHT_ACCEPTING_RUN:
+      opt_highlight_accepting_run =
+        arg ? to_pos_int(arg, "--highlight-accepting-run") : 1;
+      break;
     case OPT_HIGHLIGHT_NONDET:
       {
         int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1;
@@ -1528,6 +1536,9 @@ namespace
       if (opt_highlight_languages)
         spot::highlight_languages(aut);
 
+      if (opt_highlight_accepting_run >= 0)
+        aut->accepting_run()->highlight(opt_highlight_accepting_run);
+
       if (!opt->hl_words.empty())
         for (auto& word_aut: opt->hl_words)
           {
diff --git a/tests/core/highlightstate.test b/tests/core/highlightstate.test
index 001d9e2f1..a42eb3b53 100755
--- a/tests/core/highlightstate.test
+++ b/tests/core/highlightstate.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2016-2019 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -191,3 +191,43 @@ grep forcelabels output.dot && exit 1
 autfilt --dot input2.hoa > output2.dot
 grep xlabel output2.dot
 grep forcelabels output2.dot
+
+
+cat >case5.hoa <<EOF
+HOA: v1
+name: "case5"
+States: 7
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 8
+  ((Fin(0)&Inf(1))|(Fin(2)&Inf(3)))&(Fin(4)|Inf(5))&(Fin(6)|Inf(7))
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0&1] 1 {2}
+[0&1] 2 {2}
+State: 1
+[0&1] 3 {1 5}
+State: 2
+[0&1] 3 {1}
+[0&1] 4 {1}
+State: 3
+[0&1] 1 {0 2 3 5}
+[!0&!1] 5 {5 6}
+State: 4
+[0&1] 1 {0 2 3}
+[0&1] 2 {0 2 3}
+[!0&!1] 6 {4 5}
+State: 5
+[0&1] 3
+[0&1] 4
+State: 6
+[!0&1] 0 {2 3}
+[!0&1] 2 {0}
+--END--
+EOF
+autfilt --highlight-accepting-run=2 case5.hoa -H1.1 | grep highlight >out
+cat >expect.hoa <<EOF
+spot.highlight.edges: 2 2 5 2 10 2 13 2
+EOF
+diff out expect.hoa