Commit 55c50c65 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: add support for --highlight-accepting-run

Fixes #381.

* bin/autfilt.cc: Here.
* tests/core/highlightstate.test: Test it.
* NEWS: Mention it.
parent 7af47c7d
Pipeline #7551 passed with stages
in 224 minutes and 59 seconds
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
......
// -*- 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)
{
......
#!/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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment