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

@@ -19,6 +19,9 @@ New in spot 2.0a (not yet released)
     is still the default, but we plan to default to version 1.1 in the
     future.
 
+  * 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
@@ -38,10 +41,20 @@ New in spot 2.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)
 

spot/ltsmin/ltsmin.cc

@@ -1103,8 +1103,13 @@ namespace spot
         dict->unregister_all_my_variables(iface.get());
         throw;
       }
-
-    return std::make_shared<spins_kripke>(iface, dict, ps, dead, compress);
+    auto res = std::make_shared<spins_kripke>(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()

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
       {

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));
+  }
 
 
 

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.

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<bdd> 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);
+      }
+  }
+
+
 }

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);

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)
           {

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_)

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);
   }
 }

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);
           }
       }
 

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 <<EOF
 HOA: v1
 States: 1
 Start: 0
-AP: 0
+AP: 2 "a" "b"
 acc-name: all
 Acceptance: 0 t
 properties: trans-labels explicit-labels state-acc deterministic

tests/core/maskkeep.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -50,7 +50,7 @@ cat >expect1 <<EOF
 HOA: v1
 States: 1
 Start: 0
-AP: 0
+AP: 2 "a" "b"
 acc-name: generalized-Buchi 2
 Acceptance: 2 Inf(0)&Inf(1)
 properties: trans-labels explicit-labels state-acc deterministic

tests/core/strength.test

@@ -293,26 +293,26 @@ State: 1 {0}
 HOA: v1
 States: 4
 Start: 0
-AP: 2 "a" "c"
+AP: 3 "b" "a" "c"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
 properties: deterministic terminal
 --BODY--
 State: 0
-[!0&!1] 0
-[0&!1] 1
-[1] 2
+[!1&!2] 0
+[1&!2] 1
+[2] 2
 State: 1
-[!0&!1] 0
-[0&!1] 1
-[!0&1] 2
-[0&1] 3
+[!1&!2] 0
+[1&!2] 1
+[!1&2] 2
+[1&2] 3
 State: 2 {0}
 [t] 2
 State: 3
-[!0] 2
-[0] 3
+[!1] 2
+[1] 3
 --END--
 /******************************/
 HOA: v1
@@ -349,17 +349,17 @@ State: 2
 HOA: v1
 States: 2
 Start: 0
-AP: 2 "a" "c"
+AP: 3 "b" "a" "c"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc deterministic
 --BODY--
 State: 0
-[!0&!1] 0 {0}
-[0&!1] 1
+[!1&!2] 0 {0}
+[1&!2] 1
 State: 1
-[!0&!1] 0 {0}
-[0&!1] 1
+[!1&!2] 0 {0}
+[1&!2] 1
 --END--
 /******************************/
 HOA: v1
@@ -655,26 +655,26 @@ State: 1 {0}
 HOA: v1.1
 States: 4
 Start: 0
-AP: 2 "a" "c"
+AP: 3 "b" "a" "c"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
 properties: deterministic stutter-invariant terminal
 --BODY--
 State: 0
-[!0&!1] 0
-[0&!1] 1
-[1] 2
+[!1&!2] 0
+[1&!2] 1
+[2] 2
 State: 1
-[!0&!1] 0
-[0&!1] 1
-[!0&1] 2
-[0&1] 3
+[!1&!2] 0
+[1&!2] 1
+[!1&2] 2
+[1&2] 3
 State: 2 {0}
 [t] 2
 State: 3
-[!0] 2
-[0] 3
+[!1] 2
+[1] 3
 --END--
 HOA: v1.1
 States: 1
@@ -710,18 +710,18 @@ State: 2
 HOA: v1.1
 States: 2
 Start: 0
-AP: 2 "a" "c"
+AP: 3 "b" "a" "c"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc !complete
 properties: deterministic stutter-invariant !inherently-weak
 --BODY--
 State: 0
-[!0&!1] 0 {0}
-[0&!1] 1
+[!1&!2] 0 {0}
+[1&!2] 1
 State: 1
-[!0&!1] 0 {0}
-[0&!1] 1
+[!1&!2] 0 {0}
+[1&!2] 1
 --END--
 HOA: v1.1
 States: 2