diff --git a/NEWS b/NEWS index 01156dcf2..68b6a1bae 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,14 @@ New in spot 2.10.3.dev (not yet released) property of Spot to the controllable-AP header for the Extended HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 + - "aliases" is a new named property that is filled by the HOA parser + using the list of aliases declared in the HOA file, and then used + by the HOA printer on a best-effort basis. Aliases can be used to + make HOA files more compact or more readable. But another + possible application is to use aliases to name letters of a 2^AP + alphabet, in applications where using atomic propositions is + inconvenient. + New in spot 2.10.3 (2022-01-15) Bugs fixed: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index a0cbf289a..d5641e42f 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1130,25 +1130,26 @@ method. Here is a list of named properties currently used inside Spot: -| key name | (pointed) value type | description | -|---------------------+--------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------| -| ~accepted-word~ | ~std::string~ | a word accepted by the automaton | -| ~automaton-name~ | ~std::string~ | name for the automaton, for instance to display in the HOA format | -| ~degen-levels~ | ~std::vector~ | level associated to each state by the degeneralization algorithm | -| ~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 | -| ~incomplete-states~ | ~std::set~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) | -| ~original-classes~ | ~std::vector~ | class number associated to each state of a construction (used by some algorithms like =tgba_deternize()=) | -| ~original-clauses~ | ~std::vector~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= | -| ~original-states~ | ~std::vector~ | original state number before transformation (used by some algorithms like =degeneralize()=) | -| ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton | -| ~rejected-word~ | ~std::string~ | a word rejected by the automaton | -| ~simulated-states~ | ~std::vector~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | -| ~state-names~ | ~std::vector~ | vector naming each state of the automaton, for display purpose | -| ~state-player~ | ~std::vector~ | the automaton represents a two-player game, and the vector gives the player (0 or 1) associated to each state | -| ~state-winner~ | ~std::vector~ | vector indicating the player (0 or 1) winning from this state | -| ~strategy~ | ~std::vector~ | vector representing the memoryless strategy of the players in a parity game. The value corrsponds to the edge number of the transition to take. | -| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) | +| key name | (pointed) value type | description | +|---------------------+-------------------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------| +| ~accepted-word~ | ~std::string~ | a word accepted by the automaton | +| ~aliases~ | ~std::vector>~ | a set of aliases to use when printing edge labels | +| ~automaton-name~ | ~std::string~ | name for the automaton, for instance to display in the HOA format | +| ~degen-levels~ | ~std::vector~ | level associated to each state by the degeneralization algorithm | +| ~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 | +| ~incomplete-states~ | ~std::set~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) | +| ~original-classes~ | ~std::vector~ | class number associated to each state of a construction (used by some algorithms like =tgba_deternize()=) | +| ~original-clauses~ | ~std::vector~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= | +| ~original-states~ | ~std::vector~ | original state number before transformation (used by some algorithms like =degeneralize()=) | +| ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton | +| ~rejected-word~ | ~std::string~ | a word rejected by the automaton | +| ~simulated-states~ | ~std::vector~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | +| ~state-names~ | ~std::vector~ | vector naming each state of the automaton, for display purpose | +| ~state-player~ | ~std::vector~ | the automaton represents a two-player game, and the vector gives the player (0 or 1) associated to each state | +| ~state-winner~ | ~std::vector~ | vector indicating the player (0 or 1) winning from this state | +| ~strategy~ | ~std::vector~ | vector representing the memoryless strategy of the players in a parity game. The value corrsponds to the edge number of the transition to take. | +| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) | Objects referenced via named properties are automatically destroyed when the automaton is destroyed, but this can be altered by passing a diff --git a/python/spot/impl.i b/python/spot/impl.i index cc0862ffe..ebdd61d1c 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -515,6 +515,7 @@ namespace std { %template(vectoracccode) vector; %template(vectorbool) vector; %template(vectorbdd) vector; + %template(aliasvector) vector>; %template(vectorstring) vector; %template(atomic_prop_set) set; %template(relabeling_map) map; diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 5328c576b..5bd55fd83 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -120,6 +120,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); std::vector>> start; // Initial states; std::unordered_map alias; + std::vector alias_order; struct prop_info { spot::location loc; @@ -823,6 +824,10 @@ header-item: "States:" INT o << "ignoring redefinition of alias @" << *$2; error(@$, o.str()); } + else + { + res.alias_order.emplace_back(*$2); + } delete $2; bdd_delref($4); } @@ -2714,6 +2719,15 @@ namespace spot r.aut_or_ks->set_named_prop("highlight-states", r.highlight_states); if (r.state_player) r.aut_or_ks->set_named_prop("state-player", r.state_player); + if (!r.alias_order.empty()) + { + auto* p = new std::vector>(); + p->reserve(r.alias_order.size()); + auto end = r.alias_order.rend(); + for (auto i = r.alias_order.rbegin(); i != end; ++i) + p->emplace_back(*r.alias.find(*i)); + r.aut_or_ks->set_named_prop("aliases", p); + } fix_acceptance(r); fix_initial_state(r); fix_properties(r); diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index d1fccadf4..a2ffbc70d 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2019, 2021 Laboratoire de Recherche et +// Copyright (C) 2011, 2014-2019, 2021, 2022 Laboratoire de Recherche et // Developpement de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -297,6 +297,8 @@ namespace spot if (auto* prop = a->get_named_prop(name)) \ set_named_prop(name, new type(*prop)); COPY_PROP(std::string, "accepted-word"); + typedef std::vector> aliasvect; + COPY_PROP(aliasvect, "aliases"); COPY_PROP(std::string, "automaton-name"); COPY_PROP(std::vector, "degen-levels"); typedef std::map hlmap; diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index eb5cd3431..1d3b9fbac 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -54,6 +54,10 @@ namespace spot bool use_implicit_labels; bool use_state_labels = true; bdd all_ap; + typedef std::vector> aliases_t; + aliases_t* aliases; + std::unordered_map aliases_map; + std::vector> alias_cubes; // Label support: the set of all conditions occurring in the // automaton. @@ -66,9 +70,41 @@ namespace spot check_det_and_comp(aut); use_implicit_labels = implicit && is_universal && is_complete; use_state_labels &= state_labels; + setup_aliases(aut); number_all_ap(aut); } + void setup_aliases(const const_twa_graph_ptr& aut) + { + aliases = aut->get_named_prop("aliases"); + bdd sup = aut->ap_vars(); + if (aliases) + { + // Remove all aliases that use variables that are not + // registered in this automaton. + auto badvar = [sup](std::pair& p) { + return bdd_exist(bdd_support(p.second), sup) != bddtrue; + }; + aliases->erase(std::remove_if(aliases->begin(), + aliases->end(), + badvar), + aliases->end()); + unsigned count = aliases->size(); + for (unsigned i = 0; i < count; ++i) + { + bdd a = (*aliases)[i].second; + aliases_map[a.id()] = i; + if (bdd_is_cube(a)) + alias_cubes.emplace_back(a, i); + bdd neg = !a; + aliases_map[neg.id()] = i; + if (bdd_is_cube(neg)) + alias_cubes.emplace_back(neg, i); + } + } + } + + std::ostream& emit_acc(std::ostream& os, acc_cond::mark_t b) { @@ -177,6 +213,168 @@ namespace spot " prop_state_acc()==true"); } + std::string encode_label(bdd label, unsigned aliases_start = 0) + { + if (aliases) + // Check if we have a perfect alias match for this label. + if (auto p = aliases_map.find(label.id()); p != aliases_map.end()) + if (unsigned pos = p->second; pos >= aliases_start) + { + auto& a = (*aliases)[pos]; + if (a.second == label) + return '@' + a.first; + else + return "!@" + a.first; + } + if (label == bddtrue) + return "t"; + if (label == bddfalse) + return "f"; + std::ostringstream s; + bool notfirstor = false; + if (aliases) + { + bdd orig_label = label; + // If we have some aliases that imply the label, we can use them + // and try to cover most of it as a sum of labels. + unsigned alias_count = aliases->size(); + for (unsigned i = aliases_start; i < alias_count; ++i) + if (auto& a = (*aliases)[i]; bdd_implies(a.second, orig_label)) + { + bdd rest = label - a.second; + if (rest != label) + { + if (notfirstor) + s << " | "; + s << '@' << a.first; + notfirstor = true; + label = rest; + if (label == bddfalse) + return s.str(); + } + } + // If the label was not completely translated as a + // disjunction of aliases, maybe we can see it as a + // conjunction? Let's try. + // We first try to remove cubes, from the labels, and then + // try to cover the rest with non-cubes. + { + std::ostringstream s2; + bdd labelconj = orig_label; // start again + bool notfirstand = false; + unsigned alias_count = aliases->size(); + // first pass using only cubes + for (auto [acube, i]: alias_cubes) + if (i >= aliases_start) + if (bdd_implies(orig_label, acube)) + if (bdd rest = bdd_exist(labelconj, bdd_support(acube)); + rest != labelconj) + { + auto& a = (*aliases)[i]; + if (notfirstand) + s2 << '&'; + if (acube != a.second) + s2 << '!'; + s2 << '@' << a.first; + notfirstand = true; + labelconj = rest; + if (labelconj == bddtrue) + return s2.str(); + } + // second pass using all non-cube aliases + for (unsigned i = aliases_start; i < alias_count; ++i) + { + auto& a = (*aliases)[i]; + bdd neg = !a.second; + if (!bdd_is_cube(a.second) + && bdd_implies(orig_label, a.second)) + { + bdd rest = labelconj | neg; + if (rest != labelconj) + { + if (notfirstand) + s2 << '&'; + s2 << '@' << a.first; + notfirstand = true; + labelconj = rest; + if (labelconj == bddtrue) + return s2.str(); + } + } + else if (!bdd_is_cube(neg) + && bdd_implies(orig_label, neg)) + { + bdd rest = labelconj | a.second; + if (rest != labelconj) + { + if (notfirstand) + s2 << '&'; + s2 << "!@" << a.first; + notfirstand = true; + labelconj = rest; + if (labelconj == bddtrue) + return s2.str(); + } + } + } + // If we did not manage to make it look like a + // conjunction of aliases, let's continue with + // our (possibly partial) disjunction. + } + } + minato_isop isop(label); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + if (notfirstor) + s << " | "; + bool notfirstand = false; + if (aliases) + { + // We know that cube did not match any aliases. But + // maybe it can be built as a conjunction of aliases? + // (or negated aliases) + bdd orig_cube = cube; + for (auto [acube, i]: alias_cubes) + if (i >= aliases_start) + if (bdd_implies(orig_cube, acube)) + if (bdd rest = bdd_exist(cube, bdd_support(acube)); + rest != cube) + { + if (notfirstand) + s << '&'; + if (acube != (*aliases)[i].second) + s << '!'; + s << '@' << (*aliases)[i].first; + notfirstand = true; + cube = rest; + if (cube == bddtrue) + return s.str(); + } + } + while (cube != bddtrue) + { + if (notfirstand) + s << '&'; + else + notfirstand = true; + bdd h = bdd_high(cube); + if (h == bddfalse) + { + s << '!' << ap[bdd_var(cube)]; + cube = bdd_low(cube); + } + else + { + s << ap[bdd_var(cube)]; + cube = h; + } + } + notfirstor = true; + } + return s.str(); + } + void number_all_ap(const const_twa_graph_ptr& aut) { // Make sure that the automaton uses only atomic propositions @@ -206,50 +404,7 @@ namespace spot return; for (auto& i: sup) - { - bdd cond = i.first; - if (cond == bddtrue) - { - i.second = "t"; - continue; - } - if (cond == bddfalse) - { - i.second = "f"; - continue; - } - std::ostringstream s; - bool notfirstor = false; - - minato_isop isop(cond); - bdd cube; - while ((cube = isop.next()) != bddfalse) - { - if (notfirstor) - s << " | "; - bool notfirstand = false; - while (cube != bddtrue) - { - if (notfirstand) - s << '&'; - else - notfirstand = true; - bdd h = bdd_high(cube); - if (h == bddfalse) - { - s << '!' << ap[bdd_var(cube)]; - cube = bdd_low(cube); - } - else - { - s << ap[bdd_var(cube)]; - cube = h; - } - } - notfirstor = true; - } - i.second = s.str(); - } + i.second = encode_label(i.first); } }; @@ -643,6 +798,14 @@ namespace spot } os << nl; } + if (md.aliases) + { + auto* aliases = md.aliases; + int cnt = aliases->size(); + for (int i = cnt - 1; i >= 0; --i) + os << "Alias: @" << (*aliases)[i].first << ' ' + << md.encode_label((*aliases)[i].second, i + 1) << nl; + } // If we want to output implicit labels, we have to // fill a vector with all destinations in order. @@ -799,4 +962,26 @@ namespace spot return os; } + std::vector>* + get_aliases(const const_twa_ptr& g) + { + return + g->get_named_prop>>("aliases"); + } + + void + set_aliases(twa_ptr& g, std::vector> aliases) + { + if (aliases.empty()) + { + g->set_named_prop("aliases", nullptr); + } + else + { + auto a = g->get_or_set_named_prop + >>("aliases"); + *a = aliases; + } + } + } diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh index 5f9258555..59effb419 100644 --- a/spot/twaalgos/hoa.hh +++ b/spot/twaalgos/hoa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,6 +22,9 @@ #include #include #include +#include +#include +#include namespace spot { @@ -41,4 +44,22 @@ namespace spot print_hoa(std::ostream& os, const const_twa_ptr& g, const char* opt = nullptr); + + /// \ingroup twa_io + /// \brief Obtain aliases used in the HOA format. + /// + /// Aliases are stored as a vector of pairs (name, bdd). + /// The bdd is expected to use only variable registered by \a g. + SPOT_API std::vector>* + get_aliases(const const_twa_ptr& g); + + /// \ingroup twa_io + /// \brief Define all aliases used in the HOA format. + /// + /// Aliases are stored as a vector of pairs (name, bdd). + /// The bdd is expected to use only variable registered by \a g. + /// + /// Pass an empty vector to remove existing aliases. + SPOT_API void + set_aliases(twa_ptr& g, std::vector> aliases); } diff --git a/tests/Makefile.am b/tests/Makefile.am index accbad825..af87ad6cb 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009-2021 Laboratoire de Recherche et Développement +## Copyright (C) 2009-2022 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -388,6 +388,7 @@ TESTS_python = \ python/_aux.ipynb \ python/accparse2.py \ python/alarm.py \ + python/aliases.py \ python/aiger.py \ python/alternating.py \ python/bdddict.py \ diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 530047a01..6501bee02 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -630,12 +630,14 @@ acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete properties: deterministic +Alias: @a 0 +Alias: @b.c 1&2 --BODY-- State: 0 -[!0&!1 | !0&!2] 0 -[0&!1 | 0&!2] 0 {0} -[!0&1&2] 0 {1} -[0&1&2] 0 {0 1} +[!@a&!@b.c] 0 +[@a&!@b.c] 0 {0} +[@b.c&!@a] 0 {1} +[@b.c&@a] 0 {0 1} --END-- HOA: v1 name: "GFa & GF(b & c)" @@ -646,12 +648,14 @@ acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete properties: deterministic +Alias: @b.c 1&2 +Alias: @a 0 --BODY-- State: 0 -[!0&!1 | !0&!2] 0 -[0&!1 | 0&!2] 0 {0} -[!0&1&2] 0 {1} -[0&1&2] 0 {0 1} +[!@a&!@b.c] 0 +[@a&!@b.c] 0 {0} +[!@a&@b.c] 0 {1} +[@a&@b.c] 0 {0 1} --END-- HOA: v1 States: 2 diff --git a/tests/python/aliases.py b/tests/python/aliases.py new file mode 100644 index 000000000..6f861a880 --- /dev/null +++ b/tests/python/aliases.py @@ -0,0 +1,152 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# Test for parts of Issue #497. + +import spot + +aut = spot.automaton(""" +HOA: v1 +States: 1 +Start: 0 +acc-name: who cares +Acceptance: 0 t +properties: very-weak +AP: 3 "x" "y" "z" +Alias: @p0 0 +Alias: @p1 1 +Alias: @a !@p0&!@p1 +Alias: @b !@p0&@p1 +Alias: @c @p0&!@p1 +--BODY-- +State: 0 +[@p0] 0 +[!@p0] 0 +[@p1] 0 +[!@p1] 0 +[@a] 0 +[!@a] 0 +[@b] 0 +[!@b] 0 +[@c] 0 +[!@c] 0 +[@a|@b] 0 +[@a|@c] 0 +[@b|@c] 0 +[@a|@b|@c] 0 +[!@a|!@b] 0 +[!@a|!@c] 0 +[!@b|!@c] 0 +[@p0&@p1] 0 +[!@a&!@b] 0 +[!@a&!@c] 0 +[!@b&!@c] 0 +[!@b&!@c&2] 0 +[@a&2] 0 +[!@a&2] 0 +--END--""") +s = aut.to_str('hoa') +aut2 = spot.automaton(s) +assert aut.equivalent_to(aut2) +s2 = aut.to_str('hoa') +assert s == s2 + +assert s == """HOA: v1 +States: 1 +Start: 0 +AP: 3 "x" "y" "z" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete very-weak +Alias: @p0 0 +Alias: @p1 1 +Alias: @a !@p1&!@p0 +Alias: @b @p1&!@p0 +Alias: @c !@p1&@p0 +--BODY-- +State: 0 +[@p0] 0 +[!@p0] 0 +[@p1] 0 +[!@p1] 0 +[@a] 0 +[!@a] 0 +[@b] 0 +[!@b] 0 +[@c] 0 +[!@c] 0 +[!@p0] 0 +[!@p1] 0 +[@c | @b] 0 +[@c | @b | @a] 0 +[t] 0 +[t] 0 +[t] 0 +[@p1&@p0] 0 +[@p0] 0 +[@p1] 0 +[!@c&!@b] 0 +[@a&2 | @p1&@p0&2] 0 +[@a&2] 0 +[@p0&2 | @p1&2] 0 +--END--""" + +# Check what happens to aliases when an AP has been removed, but +# the aliases have been preserved... +rem = spot.remove_ap() +rem.add_ap("x") +aut3 = rem.strip(aut) +spot.set_aliases(aut3, spot.get_aliases(aut)) +s2 = aut3.to_str('hoa') +# Aliases based on "x" should have disappeared. +assert(s2 == """HOA: v1 +States: 1 +Start: 0 +AP: 2 "y" "z" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete very-weak +Alias: @p1 0 +--BODY-- +State: 0 +[t] 0 +[t] 0 +[@p1] 0 +[!@p1] 0 +[!@p1] 0 +[t] 0 +[@p1] 0 +[t] 0 +[!@p1] 0 +[t] 0 +[t] 0 +[!@p1] 0 +[t] 0 +[t] 0 +[t] 0 +[t] 0 +[t] 0 +[@p1] 0 +[t] 0 +[@p1] 0 +[t] 0 +[1] 0 +[!@p1&1] 0 +[1] 0 +--END--""")