diff --git a/NEWS b/NEWS index d12c0bb91eb4324b70c07b56c23286ae0ebf31b6..793a4652165625e2bcab08c24d1af8ad13b941b2 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,23 @@ New in spot 2.3.3.dev (not yet released) - spot::dtwa_complement now simply returns the result of dualize() + - There is a new named property for automata called + "original-states" that can be used to record the origin of a state + when an automaton is transformed. It is currently defined by the + degeneralization algorithms, and by transform_accessible() and + algorithms based on it (like remove_ap::strip(), + decompose_strength(), decompose_scc()). This is realy meant as an + aid for writing algorithms that need this mapping, but it can also + be used to debug these algorithms: the "original-states" + information is displayed by the dot printer when the 'd' option is + passed. For instance in + + % ltl2tgba 'GF(a <-> Fb)' --dot=s + % ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=ds + + the second command outputs an automaton with states that show + references to the first one. + Bugs fixed: - the transformation to state-based acceptance (spot::sbacc()) was diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 78f747a82da2d71b822459fab9ffd6eb6a2afaea..933757443cb7e6d9ec3b6d640d4031588bb0b565 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -92,17 +92,22 @@ static const argp_option options[] = OPTION_ARG_OPTIONAL, "GraphViz's format. Add letters for " "(1) force numbered states, " - "(a) acceptance display, (b) acceptance sets as bullets, " + "(a) display acceptance, " + "(b) acceptance sets as bullets, " "(B) bullets except for Büchi/co-Büchi automata, " "(c) force circular nodes, " "(C) color nodes with COLOR, " + "(d) show origins when known, " "(e) force elliptic nodes, " - "(f(FONT)) use FONT, (h) horizontal layout, " + "(f(FONT)) use FONT, " + "(h) horizontal layout, " "(k) use state labels when possible, " - "(n) with name, (N) without name, " + "(n) with name, " + "(N) without name, " "(o) ordered transitions, " "(r) rainbow colors for acceptance sets, " - "(R) color acceptance sets by Inf/Fin, (s) with SCCs, " + "(R) color acceptance sets by Inf/Fin, " + "(s) with SCCs, " "(t) force transition-based acceptance, " "(v) vertical layout, " "(y) split universal edges by color, " diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 0208d724ea7780310010afe998923c81649b2b94..3df01a3d60d21abd4a501801d1592a4456d2b18e 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1118,6 +1118,7 @@ Here is a list of named properties currently used inside Spot: |---------------------+--------------------------------+---------------------------------------------------------------------------------------------------------------------------------| | ~automaton-name~ | ~std::string~ | name for the automaton, for instance to display in the HOA format | | ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton | +| ~original-states~ | ~std::vector~ | original state number before transformation (used by some algorithms like =degeneralize()=) | | ~state-names~ | ~std::vector~ | vector naming each state of the automaton, for display purpose | | ~highlight-edges~ | ~std::map~ | map of (edge number, color number) for highlighting the output | | ~highlight-states~ | ~std::map~ | map of (state number, color number) for highlighting the output | diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index bb55b1d532cba2006f4c75dc5f653d6a42331760..a7fa5a09826cc63c097bced9092896355f9ebe88 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -214,6 +214,10 @@ namespace spot // Preserve determinism, weakness, and stutter-invariance res->prop_copy(a, { false, true, true, true, true, true }); + auto orig_states = new std::vector(); + orig_states->reserve(a->num_states()); // likely more are needed. + res->set_named_prop("original-states", orig_states); + // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can // be used as a level in degen_state to indicate the next expected @@ -290,16 +294,37 @@ namespace spot s.second = 0; } - ds2num[s] = res->new_state(); - todo.emplace_back(s); - - // If use_lvl_cache is on insert initial state to level cache - // Level cache stores first encountered level for each state. - // When entering an SCC first the lvl_cache is checked. - // If such state exists level from chache is used. - // If not, a new level (starting with 0) is computed. - if (use_lvl_cache) - lvl_cache[s.first] = std::make_pair(s.second, true); + auto new_state = [&](degen_state& ds) + { + unsigned ns = res->new_state(); + ds2num[ds] = ns; + todo.emplace_back(ds); + + assert(ns == orig_states->size()); + orig_states->emplace_back(ds.first); + + // Level cache stores one encountered level for each state + // (the value of use_lvl_cache determinates which level + // should be remembered). + // When entering an SCC first the lvl_cache is checked. + // If such state exists level from chache is used. + if (use_lvl_cache) + { + unsigned lvl = ds.second; + if (lvl_cache[ds.first].second) + { + if (use_lvl_cache == 3) + lvl = std::max(lvl_cache[ds.first].first, lvl); + else if (use_lvl_cache == 2) + lvl = std::min(lvl_cache[ds.first].first, lvl); + else + lvl = lvl_cache[ds.first].first; // Do not change + } + lvl_cache[ds.first] = std::make_pair(lvl, true); + } + return ns; + }; + new_state(s); while (!todo.empty()) { @@ -502,31 +527,9 @@ namespace spot int dest; ds2num_map::const_iterator di = ds2num.find(d); if (di != ds2num.end()) - { - dest = di->second; - } + dest = di->second; else - { - dest = res->new_state(); - ds2num[d] = dest; - todo.emplace_back(d); - // Insert new state to cache - - if (use_lvl_cache) - { - auto lvl = d.second; - if (lvl_cache[d.first].second) - { - if (use_lvl_cache == 3) - lvl = std::max(lvl_cache[d.first].first, lvl); - else if (use_lvl_cache == 2) - lvl = std::min(lvl_cache[d.first].first, lvl); - else - lvl = lvl_cache[d.first].first; // Do not change - } - lvl_cache[d.first] = std::make_pair(lvl, true); - } - } + dest = new_state(d); unsigned& t = tr_cache[dest * 2 + is_acc]; diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 5160602c6083f95c726d7d7bce9eff53a2aef1ae..48579d839477a2eb3cbba7b870d6f3c5041903bb 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 2015, Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014 2015, 2017, Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -48,6 +48,14 @@ namespace spot /// /// The degeneralize_tba() variant produce a degeneralized automaton /// with transition-based acceptance. + /// + /// The mapping between each state of the resulting automaton + /// and the original state of the input automaton is stored in the + /// "original-states" named property of the produced automaton. Call + /// `aut->get_named_prop>("original-states")` + /// to retrieve it. Note that these functions may return the original + /// automaton as-is if it is already degeneralized; in this case + /// the "original-states" property is not defined. /// \@{ SPOT_API twa_graph_ptr degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true, diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index fd1d7e2634107b720d7785883dad04fec918baaa..ff557b7d447c6680d9fec98a7843efa2b6fb3c26 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -67,6 +67,7 @@ namespace spot std::map* highlight_edges_ = nullptr; std::map* highlight_states_ = nullptr; std::vector>* sprod_ = nullptr; + std::vector* orig_ = nullptr; std::set* incomplete_ = nullptr; std::string* name_ = nullptr; acc_cond::mark_t inf_sets_ = 0U; @@ -87,6 +88,7 @@ namespace spot bool opt_all_bullets = false; bool opt_ordered_edges_ = false; bool opt_numbered_edges_ = false; + bool opt_orig_show_ = false; bool max_states_given_ = false; // related to max_states_ const_twa_graph_ptr aut_; @@ -199,6 +201,9 @@ namespace spot options = end + 1; } break; + case 'd': + opt_orig_show_ = true; + break; case 'e': opt_shape_ = ShapeEllipse; break; @@ -520,6 +525,8 @@ namespace spot os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second; else os_ << s; + if (orig_ && s < orig_->size()) + os_ << " (" << (*orig_)[s] << ')'; if (acc) { os_ << "\\n"; @@ -538,6 +545,8 @@ namespace spot os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second; else os_ << s; + if (orig_ && s < orig_->size()) + os_ << " (" << (*orig_)[s] << ')'; if (acc) { os_ << "
"; @@ -557,6 +566,8 @@ namespace spot os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second; else os_ << s; + if (orig_ && s < orig_->size()) + os_ << " (" << (*orig_)[s] << ')'; if (opt_state_labels_) escape_str(os_ << "\\n", state_label(s)); os_ << '"'; @@ -687,6 +698,8 @@ namespace spot sprod_ = nullptr; } } + if (opt_orig_show_) + orig_ = aut->get_named_prop>("original-states"); if (opt_state_labels_) { // Verify that we can use state labels for this automaton. @@ -720,11 +733,12 @@ namespace spot && aut_->prop_state_acc().is_true()); if (opt_shape_ == ShapeAuto) { - if (sn_ || sprod_ || aut->num_states() > 100 || opt_state_labels_) + if (sn_ || sprod_ || aut->num_states() > 100 + || opt_state_labels_ || orig_) { opt_shape_ = ShapeEllipse; // If all state names are short, prefer circles. - if (!opt_state_labels_ && + if (!opt_state_labels_ && !orig_ && sn_ && std::all_of(sn_->begin(), sn_->end(), [](const std::string& s) { return s.size() <= 2; })) diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 52f0fdcc3fe647330068cb0837f760d8a3b5fc48..2f40368c0e19132d22b3ad06b83a71ba5a3f4970 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -25,19 +25,26 @@ namespace spot { /// \brief Clone and mask an automaton. /// - /// Copy the edges of automaton \a old, into automaton - /// \a cpy, creating new states at the same time. The argument \a - /// trans should behave as a function with the following prototype: + /// Copy the edges of automaton \a old into the empty automaton \a + /// cpy, creating new states as needed. The argument \a trans + /// should behave as a function with the following prototype: /// /// void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc, /// unsigned dst) /// - /// It can modify either the condition or the acceptance sets of - /// the edges. Set the condition to bddfalse to remove the edge - /// (this will also remove the destination state and its descendants - /// if they are not reachable by another edge). + /// + /// The \a trans function may modify either the condition or the + /// acceptance sets of the edges. Set the condition to bddfalse to + /// remove the edge (this will also remove the destination state and + /// its descendants if they are not reachable by another edge). + /// + /// The mapping between each state of the resulting automaton + /// and the original state of the input automaton is stored in the + /// "original-states" named property of the produced automaton. Call + /// `aut->get_named_prop>("original-states")` + /// to retrieve it. + /// /// \param init The optional new initial state. - template void transform_accessible(const const_twa_graph_ptr& old, twa_graph_ptr& cpy, @@ -50,6 +57,10 @@ namespace spot std::vector todo; std::vector seen(old->num_states(), -1U); + auto orig_states = new std::vector(); + orig_states->reserve(old->num_states()); // maybe less are needed. + cpy->set_named_prop("original-states", orig_states); + auto new_state = [&](unsigned old_state) -> unsigned { @@ -58,12 +69,17 @@ namespace spot { tmp = cpy->new_state(); seen[old_state] = tmp; + orig_states->emplace_back(old_state); todo.emplace_back(old_state); } return tmp; }; cpy->set_init_state(new_state(init)); + if (seen[init] != 0) + throw std::runtime_error + ("the destination automaton of transform_accessible() should be empty"); + while (!todo.empty()) { unsigned old_src = todo.back(); @@ -79,11 +95,12 @@ namespace spot trans(t.src, cond, acc, t.dst); if (cond != bddfalse) - cpy->new_edge(new_src, - new_state(t.dst), - cond, acc); + cpy->new_edge(new_src, new_state(t.dst), + cond, acc); } } + + orig_states->shrink_to_fit(); } /// \brief Copy an automaton and update each edge. @@ -133,6 +150,7 @@ namespace spot { transform_accessible(old, cpy, trans, old->get_init_state_number()); } + template void transform_copy(const const_twa_graph_ptr& old, twa_graph_ptr& cpy, diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 40cf0e6349cfe43895b712a4d701cc463a6c3ffd..e0b0739074d47bb40d06c936bc85f57fe9bbe192 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de +# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016, 2017 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -1041,3 +1041,26 @@ test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count` test 2 = `genltl --dac=1..3 | ltl2tgba --stats='%e,"%h",%s' | dstar2tgba -F-/2 --stats='%<,%>,"%h"' | autfilt --states=2..3 -F-/3 --stats='%<,"%h"' | wc -l` + +# --dot=d +ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=d | grep ' (' >out +cat >expected <out +cat >expected < 0 + 0 [label="0 (1)"] + 0 -> 0 [label="a"] +} +EOF +diff out expected