Commit 6793d6de authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

highlight: do not reset existing highlights

* spot/twa/twa.hh (twa::get_or_set_named_prop): New method.
* spot/twaalgos/emptiness.cc, spot/twaalgos/isdet.cc: Use it to not
overwrite existing highlights.
* tests/core/det.test: Add test case.
parent 57f47c16
......@@ -957,8 +957,9 @@ namespace spot
/// named properties. They are used for instance to name all the
/// state of an automaton.
///
/// This function attaches the object \a val to the current automaton,
/// under the name \a s.
/// This function attaches the object \a val to the current
/// automaton, under the name \a s and destroy any previous
/// property with the same name.
///
/// When the automaton is destroyed, the \a destructor function will
/// be called to destroy the attached object.
......@@ -974,12 +975,12 @@ namespace spot
/// named properties. They are used for instance to name all the
/// state of an automaton.
///
/// This function attaches the object \a val to the current
/// automaton, under the name \a s and destroy any previous
/// property with the same name.
///
/// This function attaches the object \a val to the current automaton,
/// under the name \a s.
///
/// When the automaton is destroyed, the \a destructor function will
/// be called to destroy the attached object.
/// When the automaton is destroyed, the attached object will be
/// destroyed with \c delete.
///
/// See https://spot.lrde.epita.fr/concepts.html#named-properties
/// for a list of named properties used by Spot.
......@@ -1019,11 +1020,35 @@ namespace spot
template<typename T>
T* get_named_prop(std::string s) const
{
void* p = get_named_prop_(s);
if (!p)
if (void* p = get_named_prop_(s))
return static_cast<T*>(p);
else
return nullptr;
return static_cast<T*>(p);
}
/// \brief Create or retrieve a named property
///
/// Arbitrary objects can be attached to automata. Those are called
/// named properties. They are used for instance to name all the
/// state of an automaton.
///
/// This function create a property object of a given type, and
/// attached it to \a name if not such property exist, or it
/// returns
///
/// See https://spot.lrde.epita.fr/concepts.html#named-properties
/// for a list of named properties used by Spot.
template<typename T>
T* get_or_set_named_prop(std::string s)
{
if (void* p = get_named_prop_(s))
return static_cast<T*>(p);
auto tmp = new T;
set_named_prop(s, tmp);
return tmp;
}
#endif
/// \brief Destroy all named properties.
......
......@@ -648,7 +648,8 @@ namespace spot
if (!a)
throw std::runtime_error("highlight() only work for twa_graph");
auto h = new std::map<unsigned, unsigned>; // highlighted edges
auto h = a->get_or_set_named_prop<std::map<unsigned, unsigned>>
("highlight-edges");
unsigned src = a->get_init_state_number();
auto l = prefix.empty() ? &cycle : &prefix;
......@@ -683,7 +684,6 @@ namespace spot
}
src = dst;
}
a->set_named_prop("highlight-edges", h);
}
twa_graph_ptr
......
......@@ -79,18 +79,24 @@ namespace spot
if (aut->prop_deterministic())
return;
unsigned ns = aut->num_states();
auto* highlight = new std::map<unsigned, unsigned>;
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
("highlight-states");
bool deterministic = true;
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);
{
(*highlight)[src] = color;
deterministic = false;
}
else
available -= t.cond;
{
available -= t.cond;
}
}
aut->prop_deterministic(highlight->empty());
aut->set_named_prop("highlight-states", highlight);
aut->prop_deterministic(deterministic);
}
void
......@@ -99,7 +105,9 @@ namespace spot
if (aut->prop_deterministic())
return;
unsigned ns = aut->num_states();
auto* highlight = new std::map<unsigned, unsigned>;
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
("highlight-edges");
bool deterministic = true;
for (unsigned src = 0; src < ns; ++src)
{
// Make a first pass to gather non-deterministic labels
......@@ -107,17 +115,21 @@ namespace spot
bdd extra = bddfalse;
for (auto& t: aut->out(src))
if (!bdd_implies(t.cond, available))
extra |= (t.cond - available);
{
extra |= (t.cond - available);
deterministic = false;
}
else
available -= t.cond;
{
available -= t.cond;
}
// Second pass to gather the relevant edges.
if (extra != bddfalse)
if (!deterministic)
for (auto& t: aut->out(src))
if ((t.cond & extra) != bddfalse)
highlight->emplace(aut->get_graph().index_of_edge(t), color);
(*highlight)[aut->get_graph().index_of_edge(t)] = color;
}
aut->prop_deterministic(highlight->empty());
aut->set_named_prop("highlight-edges", highlight);
aut->prop_deterministic(deterministic);
}
bool
......
......@@ -235,4 +235,43 @@ ltl2tgba -f 'Ga & FGb' -f 'Ga | FGb' > out.hoa
test "`autfilt --nondet-states=1 --stats=%M out.hoa`" = "Ga & FGb"
test "`autfilt --nondet-states=2 --stats=%M out.hoa`" = "Ga | FGb"
true
cat >input <<EOF
HOA: v1.1
name: "FGa"
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
spot.highlight.edges: 1 3 2 3
spot.highlight.states: 0 2
--BODY--
State: 0 {0}
[0] 0
State: 1
[0] 0
[t] 1
--END--
EOF
autfilt -H1.1 --highlight-nondet=5 input > output
cat >expected <<EOF
HOA: v1.1
name: "FGa"
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: 0 2 1 5
spot.highlight.edges: 1 3 2 5 3 5
--BODY--
State: 0 {0}
[0] 0
State: 1
[0] 0
[t] 1
--END--
EOF
diff output expected
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