From b6cd54ab16139bd0c6dc48c6c4e6d34daae818f7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Jul 2016 13:12:58 +0200 Subject: [PATCH] autfilt: add highlighting options for nondeterminism Fixes #123. * bin/autfilt.cc: Add options --highlight-nondet-states=NUM, --highlight-nondet-edges=NUM, and --highlight-nondet=NUM. * spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh (highlight_nondet_states, highlight_nondet_edges): New functions. * tests/core/det.test: Add test cases. * NEWS: Mention them. --- NEWS | 13 ++++++-- bin/autfilt.cc | 32 ++++++++++++++++++ spot/twaalgos/isdet.cc | 47 ++++++++++++++++++++++++++ spot/twaalgos/isdet.hh | 24 ++++++++++++-- tests/core/det.test | 75 +++++++++++++++++++++++++++++++++++++++++- 5 files changed, 186 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 2f0b897bd..024d9fd29 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,11 @@ New in spot 2.0.3a (not yet released) These differ from --ap=RANGE that only consider *declared* atomic propositions, regardless of whether they are actually used. + * autfilt has two new options to highlight non-determinism: + --highlight-nondet-states=NUM and --highlight-nondet-states=NUM + where NUM is a color number. Additionally --highlight-nondet=NUM + is a shorthand for using the two. + * ltlcross and ltldo have a new syntax to specify that an input formula should be written in some given syntax after rewriting some operators away. For instance the defaults arguments passed @@ -61,9 +66,13 @@ New in spot 2.0.3a (not yet released) was secretly able of reading that since 1.99.8, but that is now documented at https://spot.lrde.epita.fr/hoa.html#extensions + * highlight_nondet_states() and highlight_nondet_edges() are + new functions that define the above two named properties. + * is_deterministic(), is_terminal(), is_weak(), and - is_inherently_weak(), count_nondet_states() will update the - corresponding properties of the automaton as a side-effect of + is_inherently_weak(), count_nondet_states(), + highlight_nondet_edges(), highlight_nondet_states() will update + the corresponding properties of the automaton as a side-effect of their check. * language_containment_checker now has default values for all diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 404206e68..d48f48c9a 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -88,6 +88,9 @@ enum { OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, OPT_GENERIC, + OPT_HIGHLIGHT_NONDET, + OPT_HIGHLIGHT_NONDET_EDGES, + OPT_HIGHLIGHT_NONDET_STATES, OPT_INSTUT, OPT_INCLUDED_IN, OPT_INHERENTLY_WEAK_SCCS, @@ -201,6 +204,16 @@ static const argp_option options[] = { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL, "minimize the automaton using a SAT solver (only works for deterministic" " automata)", 0 }, + { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM", + OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM", + 0}, + { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM", + OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM", + 0}, + { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM", + OPTION_ARG_OPTIONAL, + "highlight nondeterministic states and edges with color NUM", 0}, + /**************************************************/ { nullptr, 0, nullptr, 0, "Filtering options:", 6 }, { "ap", OPT_AP_N, "RANGE", 0, @@ -382,6 +395,8 @@ static bool opt_rem_unreach = false; static bool opt_rem_unused_ap = false; static bool opt_sep_sets = false; static const char* opt_sat_minimize = nullptr; +static int opt_highlight_nondet_states = -1; +static int opt_highlight_nondet_edges = -1; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut) @@ -485,6 +500,18 @@ parse_opt(int key, char* arg, struct argp_state*) opt->equivalent_neg = spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos)); break; + case OPT_HIGHLIGHT_NONDET: + { + int v = arg ? to_pos_int(arg) : 1; + opt_highlight_nondet_edges = opt_highlight_nondet_states = v; + break; + } + case OPT_HIGHLIGHT_NONDET_STATES: + opt_highlight_nondet_states = arg ? to_pos_int(arg) : 1; + break; + case OPT_HIGHLIGHT_NONDET_EDGES: + opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1; + break; case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) opt_instut = 1; @@ -929,6 +956,11 @@ namespace if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); + if (opt_highlight_nondet_states >= 0) + spot::highlight_nondet_states(aut, opt_highlight_nondet_states); + if (opt_highlight_nondet_edges >= 0) + spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges); + const double conversion_time = sw.stop(); if (opt->uniq) diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 72897cff0..0b5fb62fe 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -73,6 +73,53 @@ namespace spot return !count_nondet_states_aux(aut); } + void + highlight_nondet_states(twa_graph_ptr& aut, unsigned color) + { + if (aut->prop_deterministic()) + return; + unsigned ns = aut->num_states(); + auto* highlight = new std::map; + for (unsigned src = 0; src < ns; ++src) + { + bdd available = bddtrue; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + highlight->emplace(src, color); + else + available -= t.cond; + } + aut->prop_deterministic(highlight->empty()); + aut->set_named_prop("highlight-states", highlight); + } + + void + highlight_nondet_edges(twa_graph_ptr& aut, unsigned color) + { + if (aut->prop_deterministic()) + return; + unsigned ns = aut->num_states(); + auto* highlight = new std::map; + for (unsigned src = 0; src < ns; ++src) + { + // Make a first pass to gather non-deterministic labels + bdd available = bddtrue; + bdd extra = bddfalse; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + extra |= (t.cond - available); + else + available -= t.cond; + // Second pass to gather the relevant edges. + if (extra != bddfalse) + for (auto& t: aut->out(src)) + if ((t.cond & extra) != bddfalse) + highlight->emplace(aut->get_graph().index_of_edge(t), color); + } + aut->prop_deterministic(highlight->empty()); + aut->set_named_prop("highlight-edges", highlight); + } + bool is_complete(const const_twa_graph_ptr& aut) { diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index a15792ccd..3478fba8f 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -46,12 +46,32 @@ namespace spot SPOT_API bool is_deterministic(const const_twa_graph_ptr& aut); + /// \brief Highlight nondeterministic states + /// + /// A state is nondeterministic if it has two outgoing edges whose + /// labels are not incompatibles. + /// + /// \param aut the automaton to process + /// \param color the color to give to nondeterministic states. + SPOT_API void + highlight_nondet_states(twa_graph_ptr& aut, unsigned color); + + /// \brief Highlight nondeterministic edges + /// + /// An edge is nondeterministic if there exist another edge leaving + /// the same source state, with a compatible label (i.e., the + /// conjunction of the two labels is not false). + /// + /// \param aut the automaton to process + /// \param color the color to give to nondeterministic edges. + SPOT_API void + highlight_nondet_edges(twa_graph_ptr& aut, unsigned color); + /// @} + /// \brief Return true iff \a aut is complete. /// /// An automaton is complete if its translation relation is total, /// i.e., each state as a successor for any possible configuration. SPOT_API bool is_complete(const const_twa_graph_ptr& aut); - - /// @} } diff --git a/tests/core/det.test b/tests/core/det.test index ba4af3f17..58a25d887 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -141,6 +141,79 @@ diff out.tgba ex.tgba run 0 ltl2tgba -H '(0 R Xa) R (a xor Fa)' > out.hoa grep deterministic out.hoa && exit 1 +# We can highlight nondeterminism +autfilt -H1.1 --highlight-nondet-states=1 \ + --highlight-nondet-edges=2 out.hoa >out-nd.hoa +cat >expected-nd.hoa < rand.hoa +cat >expected-rand.hoa < rand2.hoa +cat >expected-rand2.hoa <