diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index afd4db00deba273829c203a091526b195d2290a7..2b8b0d1699494e2012399424a14f635b89f99516 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -69,6 +69,17 @@ namespace spot return !couvreur99(a)->check(); } + void + twa::set_named_prop(std::string s, std::nullptr_t) + { + auto p = named_prop_.find(s); + if (p == named_prop_.end()) + return; + p->second.second(p->second.first); + named_prop_.erase(p); + return; + } + void twa::set_named_prop(std::string s, void* val, std::function destructor) diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 91cae55e90187eedc934cc6c8c837f20d0ab39ed..0f68585b3d67b59ee9b403cbaeba66161a206520 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -22,6 +22,7 @@ #pragma once +#include #include #include #include @@ -952,7 +953,7 @@ namespace spot #ifndef SWIG /// \brief Declare a named property /// - /// Arbitrary object can be attached to automata. Those are called + /// 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. /// @@ -969,15 +970,16 @@ namespace spot /// \brief Declare a named property /// - /// Arbitrary object can be attached to automata. Those are called + /// 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 attaches the object \a val to the current automaton, /// under the name \a s. /// - /// The object will be automatically destroyed when the automaton - /// is destroyed. + /// When the automaton is destroyed, the \a destructor function will + /// be called to destroy the attached object. /// /// See https://spot.lrde.epita.fr/concepts.html#named-properties /// for a list of named properties used by Spot. @@ -987,6 +989,18 @@ namespace spot set_named_prop(s, val, [](void *p) { delete static_cast(p); }); } + /// \brief Erase 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 removes the property \a s if it exists. + /// + /// See https://spot.lrde.epita.fr/concepts.html#named-properties + /// for a list of named properties used by Spot. + void set_named_prop(std::string s, std::nullptr_t); + /// \brief Retrieve a named property /// /// Because named property can be object of any type, retrieving diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4037ba72dda93495b66a161ea22bb76877a52c55..f6c1ff9c9f29881882378f3a154cff4bdf373a36 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -45,6 +45,7 @@ namespace spot void twa_graph::merge_edges() { + set_named_prop("highlight-edges", nullptr); g_.remove_dead_edges_(); typedef graph_t::edge_storage_t tr_t; @@ -272,8 +273,7 @@ namespace spot void twa_graph::defrag_states(std::vector&& newst, unsigned used_states) { - auto* names = get_named_prop>("state-names"); - if (names) + if (auto* names = get_named_prop>("state-names")) { unsigned size = names->size(); for (unsigned s = 0; s < size; ++s) @@ -285,6 +285,18 @@ namespace spot } names->resize(used_states); } + if (auto hs = get_named_prop> + ("highlight-states")) + { + std::map hs2; + for (auto p: *hs) + { + unsigned dst = newst[p.first]; + if (dst != -1U) + hs2[dst] = p.second; + } + std::swap(*hs, hs2); + } g_.defrag_states(std::move(newst), used_states); } diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index ee5d0fe284a718b7c7b404dac6aa317c32373ee3..59188a3b694c0b8a4a8a9aa339e28c7b30045da9 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -508,9 +508,24 @@ namespace spot if (auto hedges = aut->get_named_prop >("highlight-edges")) { + // Numbering edges is a delicate process. The + // "highlight-edges" property uses edges numbers that are + // indices in the "edges" vector. However these edges + // need not be sorted. When edges are output in HOA, they + // are output with increasing source state number, and the + // edges number expected in the HOA file should use that + // order. So we need to make a first pass on the + // automaton to number all edges as they will be output. + unsigned maxedge = aut->edge_vector().size(); + std::vector renum(maxedge); + unsigned edge = 0; + for (unsigned i = 0; i < num_states; ++i) + for (auto& t: aut->out(i)) + renum[aut->get_graph().index_of_edge(t)] = ++edge; os << "spot.highlight.edges:"; for (auto& p: *hedges) - os << ' ' << p.first << ' ' << p.second; + if (p.first < maxedge) // highlighted edges could come from user + os << ' ' << renum[p.first] << ' ' << p.second; os << nl; } } diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc index 552fef6e80ea8f424bd0c60cae7c2eaace869403..b00e71bf120dcbb06b1a5cf4771768c519214b66 100644 --- a/spot/twaalgos/randomize.cc +++ b/spot/twaalgos/randomize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -50,6 +50,14 @@ namespace spot (*nn)[nums[i]] = (*sn)[i]; aut->set_named_prop("state-names", nn); } + if (auto hs = aut->get_named_prop> + ("highlight-states")) + { + std::map hs2; + for (auto p: *hs) + hs2[nums[p.first]] = p.second; + std::swap(*hs, hs2); + } } if (randomize_edges) { @@ -57,7 +65,7 @@ namespace spot auto& v = g.edge_vector(); mrandom_shuffle(v.begin() + 1, v.end()); } - + aut->set_named_prop("highlight-edges", nullptr); typedef twa_graph::graph_t::edge_storage_t tr_t; g.sort_edges_([](const tr_t& lhs, const tr_t& rhs) { return lhs.src < rhs.src; }); diff --git a/spot/twaalgos/randomize.hh b/spot/twaalgos/randomize.hh index c040a1bc2f17ec99483672da133b8cac84bc9f92..faf020c27496aa233a28258a9d47af44767ae80a 100644 --- a/spot/twaalgos/randomize.hh +++ b/spot/twaalgos/randomize.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -27,6 +27,9 @@ namespace spot /// /// Make a random permutation of the state, and of the edges /// leaving this state. + /// + /// This function preserves state names, and highlighted states, + /// but it does not preserve highlighted edges. SPOT_API void randomize(twa_graph_ptr& aut, bool randomize_states = true, diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 5cac651623c004448dfa69bbcc6d6da32600e1b4..17714d53b8547396391d3c5008b78e62be7413d5 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -980,14 +980,14 @@ acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic properties: stutter-invariant terminal -spot.highlight.edges: 1 0 2 1 3 2 4 3 +spot.highlight.edges: 3 0 1 1 4 3 2 2 spot.highlight.states: 0 0 2 3 --BODY-- +State: 1 /* Defined before State 0 on purpose */ +[2] 0 /* because it affects the edge numbering */ +[1&!2] 1 /* used in spot.highlight.edges */ State: 0 {0} [t] 0 -State: 1 -[2] 0 -[1&!2] 1 State: 2 [2] 0 [!0&1&!2] 1 diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index e48bfd9d1b0d793252a28f6a54d7dd4a9a28fac3..1b4afad69a07edbf278171094d8b631018d733ed 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -226,17 +226,34 @@ digraph G { node [shape="circle"] I [label="", style=invis, width=0] I -> 2 - 0 [label="s1"] + 0 [label="s1", style="bold", color="#F15854"] 1 [label="s2"] - 2 [label="s3"] + 2 [label="s3", style="bold", color="#4D4D4D"] } digraph G { rankdir=LR node [shape="circle"] I [label="", style=invis, width=0] I -> 0 - 0 [label="s3"] + 0 [label="s3", style="bold", color="#4D4D4D"] } +HOA: v1.1 +States: 3 +Start: 2 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +spot.highlight.edges: 3 1 2 2 1 3 +--BODY-- +State: 0 +[t] 0 +State: 1 +[t] 0 +State: 2 +[t] 1 +--END-- EOF diff stdout expected diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index ca5a7e3ecab2e4578995a72faca0f2def47527ad..5d066455ae527c04816b7e889bf6f1e2bafc5821 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -21,6 +21,7 @@ #include #include #include +#include #include static void f1() @@ -84,7 +85,7 @@ static void f1() spot::print_dot(std::cout, tg); } -// Test purge with named states. +// Test purge with named and highlighted states. static void f2() { auto d = spot::make_bdd_dict(); @@ -93,20 +94,44 @@ static void f2() auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); - (void) s1; (void) s2; - std::vector* names; - names = new std::vector({"s1", "s2", "s3"}); - - tg->set_named_prop>("state-names", names); + tg->set_named_prop("state-names", + new std::vector({"s1", "s2", "s3"})); + { + auto hs = new std::map; + hs->emplace(s1, 5); + hs->emplace(s3, 7); + tg->set_named_prop("highlight-states", hs); + } tg->set_init_state(s3); spot::print_dot(std::cout, tg); tg->purge_unreachable_states(); spot::print_dot(std::cout, tg); } +// Make sure the HOA printer adjusts the highlighted edges numbers +static void f3() +{ + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + + auto hs = new std::map; + tg->set_named_prop("highlight-edges", hs); + + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + tg->set_init_state(s3); + hs->emplace(tg->new_edge(s3, s2, bddtrue), 1); + hs->emplace(tg->new_edge(s2, s1, bddtrue), 2); + hs->emplace(tg->new_edge(s1, s1, bddtrue), 3); + + spot::print_hoa(std::cout, tg, "1.1") << '\n'; +} + int main() { f1(); f2(); + f3(); }