diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 0f68585b3..2a7d707e9 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -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 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(p); + else return nullptr; - return static_cast(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 + T* get_or_set_named_prop(std::string s) + { + if (void* p = get_named_prop_(s)) + return static_cast(p); + + auto tmp = new T; + set_named_prop(s, tmp); + return tmp; + } + #endif /// \brief Destroy all named properties. diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index daf604b67..d0d05de23 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -648,7 +648,8 @@ namespace spot if (!a) throw std::runtime_error("highlight() only work for twa_graph"); - auto h = new std::map; // highlighted edges + auto h = a->get_or_set_named_prop> + ("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 diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 0b5fb62fe..a0eb644ea 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -79,18 +79,24 @@ namespace spot if (aut->prop_deterministic()) return; unsigned ns = aut->num_states(); - auto* highlight = new std::map; + auto* highlight = aut->get_or_set_named_prop> + ("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; + auto* highlight = aut->get_or_set_named_prop> + ("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 diff --git a/tests/core/det.test b/tests/core/det.test index c44725d81..c98c4d296 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -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 < output +cat >expected <