From a1b3b065fa7fe4b3821ccc0c16ee8bb1b413e7f2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 30 Apr 2016 23:54:31 +0200 Subject: [PATCH] print_hoa: output all registered APs Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap() so that the methods where this behavior is expected can be fixed. And fix ltsmin::kripke() which did not register APs. Part of #170. * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs. Throw an exception when printing automata using unregistered APs. * spot/ltsmin/ltsmin.cc: Call register_ap(). * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc, spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap): New methods. * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc, spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them. * tests/core/maskacc.test, tests/core/maskkeep.test, tests/core/strength.test: Adjust expected results. * NEWS: Mention those changes. --- NEWS | 15 +++++++++++++++ spot/ltsmin/ltsmin.cc | 9 +++++++-- spot/tl/exclusive.cc | 5 +++-- spot/twa/twa.cc | 11 +++++++++++ spot/twa/twa.hh | 4 ++++ spot/twa/twagraph.cc | 22 ++++++++++++++++++++++ spot/twa/twagraph.hh | 6 ++++++ spot/twaalgos/hoa.cc | 16 +++++++++++++--- spot/twaalgos/postproc.cc | 3 +++ spot/twaalgos/relabel.cc | 6 +++--- spot/twaalgos/remprop.cc | 8 ++++---- tests/core/maskacc.test | 6 +++--- tests/core/maskkeep.test | 4 ++-- tests/core/strength.test | 30 +++++++++++++++--------------- 14 files changed, 111 insertions(+), 34 deletions(-) diff --git a/NEWS b/NEWS index 865aa8c6a..4ba38c360 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.0.0a (not yet released) + Library: + + * twa::unregister_ap() and twa_graph::remove_unused_ap() are new + methods introduced to fix some of the bugs below. + Documentation: * Add missing documentation for the option string passed to @@ -19,10 +24,20 @@ New in spot 2.0.0a (not yet released) been performed. * The automaton parser did not fully register atomic propositions for automata read from never claim or as LBTT. + * spot::ltsmin::kripke() had the same issue. * The sub_stats_reachable() function used to count the number of transitions based on the number of atomic propositions actually *used* by the automaton instead of using the number of AP declared. + * print_hoa() will now output all the atomic propositions that have + been registered, not only those that are used in the automaton. + (Note that it will also throw an exception if the automaton uses + an unregistered AP; this is how some of the above bugs were + found.) + * The for Small or Deterministic preference, the postprocessor + will now unregister atomic propositions that are no longer + used in labels. Simplification of exclusive properties + and remove_ap::strip() will do similarly. New in spot 2.0 (2016-04-11) diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 4f9f2fe7f..86f6f14f2 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1103,8 +1103,13 @@ namespace spot dict->unregister_all_my_variables(iface.get()); throw; } - - return std::make_shared(iface, dict, ps, dead, compress); + auto res = std::make_shared(iface, dict, ps, dead, compress); + // All atomic propositions have been registered to the bdd_dict + // for iface, but we also need to add them to the automaton so + // twa::ap() works. + for (auto ap: *to_observe) + res->register_ap(ap); + return res; } ltsmin_model::~ltsmin_model() diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index abeed73a3..cb32b86f6 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -193,6 +193,7 @@ namespace spot res |= cube; cond = res; }); + res->remove_unused_ap(); } else { diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index b3fc0216f..afd4db00d 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -92,6 +92,17 @@ namespace spot return i->second.first; } + void + twa::unregister_ap(int b) + { + auto d = get_dict(); + assert(d->bdd_map[b].type == bdd_dict::var); + auto pos = std::find(aps_.begin(), aps_.end(), d->bdd_map[b].f); + assert(pos != aps_.end()); + aps_.erase(pos); + d->unregister_variable(b, this); + bddaps_ = bdd_exist(bddaps_, bdd_ithvar(b)); + } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index c213b9266..3664d1ff9 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -738,6 +738,10 @@ namespace spot } ///@} + /// \brief Unregister an atomic proposition. + /// + /// \param num the BDD variable number returned by register_ap(). + void unregister_ap(int num); /// \brief Register all atomic propositions that have /// already be register by the bdd_dict for this automaton. diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4a1d864ba..85481d4e6 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -287,4 +287,26 @@ namespace spot } g_.defrag_states(std::move(newst), used_states); } + + void twa_graph::remove_unused_ap() + { + if (ap().empty()) + return; + std::set conds; + bdd all = ap_vars(); + for (auto& e: g_.edges()) + { + all = bdd_exist(all, bdd_support(e.cond)); + if (all == bddtrue) // All letters are used. + return; + } + auto d = get_dict(); + while (all != bddtrue) + { + unregister_ap(bdd_var(all)); + all = bdd_high(all); + } + } + + } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index d6daf240e..bf093e168 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -441,6 +441,12 @@ namespace spot /// Remove all unreachable states. void purge_unreachable_states(); + /// \brief Remove unused atomic proposition + /// + /// Remove, from the list of atomic propositions registered by the + /// automaton, those that are not actually used by its labels. + void remove_unused_ap(); + acc_cond::mark_t state_acc_sets(unsigned s) const { assert((bool)prop_state_acc() || num_sets() == 0); diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 74a8bb128..821f1e9cc 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -67,7 +67,7 @@ namespace spot check_det_and_comp(aut); use_implicit_labels = implicit && is_deterministic && is_complete; use_state_labels &= state_labels; - number_all_ap(); + number_all_ap(aut); } std::ostream& @@ -164,12 +164,22 @@ namespace spot assert(state_acc || aut->prop_state_acc() != true); } - void number_all_ap() + void number_all_ap(const const_twa_graph_ptr& aut) { + // Make sure that the automaton uses only atomic propositions + // that have been registered via twa::register_ap() or some + // variant. If that is not the case, it is a bug that should + // be fixed in the function creating the automaton. Since + // that function could be written by the user, throw an + // exception rather than using an assert(). bdd all = bddtrue; for (auto& i: sup) all &= bdd_support(i.first); - all_ap = all; + all_ap = aut->ap_vars(); + if (bdd_exist(all, all_ap) != bddtrue) + throw std::runtime_error("print_hoa(): automaton uses " + "unregistered atomic propositions"); + all = all_ap; while (all != bddtrue) { diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 210b7af51..6c05a795e 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -223,6 +223,7 @@ namespace spot if (m->num_states() < a->num_states()) a = m; } + a->remove_unused_ap(); if (COMP_) a = complete(a); return a; @@ -478,6 +479,8 @@ namespace spot sim = dba ? dba : sim; + sim->remove_unused_ap(); + if (COMP_) sim = complete(sim); if (SBACC_) diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index f72fb0030..0c8fb29fe 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -38,6 +38,6 @@ namespace spot for (auto& t: aut->edges()) t.cond = bdd_replace(t.cond, pairs); for (auto v: vars) - d->unregister_variable(v, aut); + aut->unregister_ap(v); } } diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 0a0fa0821..f1d5ca53f 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -139,7 +139,7 @@ namespace spot if (v >= 0) { exist &= bdd_ithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } for (auto ap: props_pos) @@ -148,7 +148,7 @@ namespace spot if (v >= 0) { restrict &= bdd_ithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } for (auto ap: props_neg) @@ -157,7 +157,7 @@ namespace spot if (v >= 0) { restrict &= bdd_nithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } diff --git a/tests/core/maskacc.test b/tests/core/maskacc.test index f5211ca08..c5eda7fb8 100755 --- a/tests/core/maskacc.test +++ b/tests/core/maskacc.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# 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. # @@ -95,7 +95,7 @@ cat >expect3 <expect1 <