Commit b6cd54ab authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 39332fb1
......@@ -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
......
......@@ -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)
......
......@@ -73,6 +73,53 @@ namespace spot
return !count_nondet_states_aux<false>(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<unsigned, unsigned>;
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<unsigned, unsigned>;
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)
{
......
......@@ -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);
/// @}
}
#!/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 <<EOF
HOA: v1.1
name: "XGa R (!a & Fa)"
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic
spot.highlight.states: 1 1
spot.highlight.edges: 2 2 3 2
--BODY--
State: 0 {0}
[0] 0
State: 1
[!0] 0
[!0] 1
--END--
EOF
diff expected-nd.hoa out-nd.hoa
# While we are at it, make sure randomize preserves highlighted states
# (but not highlighted edges, at least until someone implement it).
autfilt -H1.1 --seed=3 --randomize out-nd.hoa > rand.hoa
cat >expected-rand.hoa <<EOF
HOA: v1.1
name: "XGa R (!a & Fa)"
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic
spot.highlight.states: 0 1
--BODY--
State: 0
[!0] 0
[!0] 1
State: 1 {0}
[0] 1
--END--
EOF
diff expected-rand.hoa rand.hoa
# --highlight-nondet=N is a short for
# --highlight-nondet-states=N --highlight-nondet-edges=N
autfilt -H1.1 --seed=3 --randomize --highlight-nondet=5 out-nd.hoa > rand2.hoa
cat >expected-rand2.hoa <<EOF
HOA: v1.1
name: "XGa R (!a & Fa)"
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic
spot.highlight.states: 0 5
spot.highlight.edges: 1 5 2 5
--BODY--
State: 0
[!0] 0
[!0] 1
State: 1 {0}
[0] 1
--END--
EOF
diff expected-rand2.hoa rand2.hoa
# These highlighted a bug in the bitvector routines because their
# state count is a multiple of 64.
......
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