From 87c2b291eddd0467b323a25e38dac6d6908d3072 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 23 Dec 2014 19:35:08 +0100
Subject: [PATCH] tgba_digraph: force selection of properties kept on copy

* src/tgba/tgba.hh: Declare a prop_set to specify the types.
* src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
* iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
---
 iface/ltsmin/ltsmin.cc          |  20 +--
 src/bin/autfilt.cc              |   9 +-
 src/bin/randaut.cc              |   4 +-
 src/graphtest/tgbagraph.test    | 226 +++++++++++++++++++++++---------
 src/tgba/tgba.hh                |  44 +++++--
 src/tgba/tgbagraph.hh           |  25 ++--
 src/tgbaalgos/are_isomorphic.cc |   4 +-
 src/tgbaalgos/closure.cc        |   8 +-
 src/tgbaalgos/complete.cc       |  12 +-
 src/tgbaalgos/degen.cc          |   2 +-
 src/tgbaalgos/dotty.cc          |   2 +-
 src/tgbaalgos/dtgbacomp.cc      |  25 ++--
 src/tgbaalgos/dupexp.cc         |  29 ++--
 src/tgbaalgos/dupexp.hh         |   8 +-
 src/tgbaalgos/sccfilter.cc      |  20 +--
 src/tgbaalgos/simulation.cc     |  11 +-
 src/tgbaalgos/stutterize.cc     |   3 +-
 src/tgbatest/checkpsl.cc        |   8 +-
 src/tgbatest/emptchk.cc         |   3 +-
 src/tgbatest/ltl2tgba.cc        |   6 +-
 wrap/python/spot.i              |   2 +-
 21 files changed, 309 insertions(+), 162 deletions(-)

diff --git a/iface/ltsmin/ltsmin.cc b/iface/ltsmin/ltsmin.cc
index 7f388b623..7b7652a60 100644
--- a/iface/ltsmin/ltsmin.cc
+++ b/iface/ltsmin/ltsmin.cc
@@ -602,7 +602,8 @@ namespace spot
     public:
 
       spins_kripke(const spins_interface* d, const bdd_dict_ptr& dict,
-		  const prop_set* ps, const ltl::formula* dead, int compress)
+		   const spot::prop_set* ps, const ltl::formula* dead,
+		   int compress)
 	: kripke(dict),
 	  d_(d),
 	  state_size_(d_->get_state_size()),
@@ -723,14 +724,13 @@ namespace spot
       compute_state_condition_aux(const int* vars) const
       {
 	bdd res = bddtrue;
-	for (prop_set::const_iterator i = ps_->begin();
-	     i != ps_->end(); ++i)
+	for (auto& i: *ps_)
 	  {
-	    int l = vars[i->var_num];
-	    int r = i->val;
+	    int l = vars[i.var_num];
+	    int r = i.val;
 
 	    bool cond = false;
-	    switch (i->op)
+	    switch (i.op)
 	      {
 	      case OP_EQ:
 		cond = (l == r);
@@ -753,9 +753,9 @@ namespace spot
 	      }
 
 	    if (cond)
-	      res &= bdd_ithvar(i->bddvar);
+	      res &= bdd_ithvar(i.bddvar);
 	    else
-	      res &= bdd_nithvar(i->bddvar);
+	      res &= bdd_nithvar(i.bddvar);
 	  }
 	return res;
       }
@@ -922,7 +922,7 @@ namespace spot
       bdd_dict_ptr dict_;
       const char** vname_;
       bool* format_filter_;
-      const prop_set* ps_;
+      const spot::prop_set* ps_;
       bdd alive_prop;
       bdd dead_prop;
       void (*compress_)(const int*, size_t, int*, size_t&);
@@ -1130,7 +1130,7 @@ namespace spot
         return 0;
       }
 
-    prop_set* ps = new prop_set;
+    spot::prop_set* ps = new spot::prop_set;
     int errors = convert_aps(to_observe, d, dict, dead, *ps);
     if (errors)
       {
diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 54577a03e..dda420834 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -574,8 +574,9 @@ namespace
       // If --stats or --name is used, duplicate the automaton so we
       // never modify the original automaton (e.g. with
       // merge_transitions()) and the statistics about it make sense.
-      auto aut = ((format == Stats) || opt_name) ?
-	spot::make_tgba_digraph(haut->aut) : haut->aut;
+      auto aut = ((format == Stats) || opt_name)
+	? spot::make_tgba_digraph(haut->aut, spot::tgba::prop_set::all())
+	: haut->aut;
 
       // Preprocessing.
 
@@ -599,7 +600,9 @@ namespace
 	matched &= aut->is_empty();
       if (opt_uniq)
         {
-          auto tmp = spot::canonicalize(make_tgba_digraph(aut));
+          auto tmp =
+	    spot::canonicalize(make_tgba_digraph(aut,
+						 spot::tgba::prop_set::all()));
           matched = opt_uniq->emplace(tmp->transition_vector().begin() + 1,
                                       tmp->transition_vector().end()).second;
         }
diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc
index a56a41009..37e79d14e 100644
--- a/src/bin/randaut.cc
+++ b/src/bin/randaut.cc
@@ -311,7 +311,9 @@ main(int argc, char** argv)
 
       if (opt_uniq)
         {
-          auto tmp = make_tgba_digraph(spot::canonicalize(aut));
+          auto tmp =
+	    spot::canonicalize(make_tgba_digraph(aut,
+						 spot::tgba::prop_set::all()));
           std::vector<tr_t> trans(tmp->transition_vector().begin() + 1,
                                   tmp->transition_vector().end());
           if (opt_uniq->emplace(trans).second)
diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test
index 9377deb40..14d60a1fb 100755
--- a/src/graphtest/tgbagraph.test
+++ b/src/graphtest/tgbagraph.test
@@ -35,84 +35,184 @@ run 0 ../tgbagraph | tee stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="p1 | p2\n{0,1}"]
-  3 -> 2 [label="!p1 | p2"]
-  3 -> 3 [label="1\n{0,1}"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="p1 | p2\n{0,1}"]
+  2 -> 1 [label="!p1 | p2"]
+  2 -> 2 [label="1\n{0,1}"]
 }
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="p1 | p2\n{0,1}"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="p1 | p2\n{0,1}"]
 }
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
 }
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="p1 | p2\n{0,1}"]
-  3 -> 2 [label="!p1 | p2"]
-  3 -> 1 [label="1\n{0,1}"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="p1 | p2\n{0,1}"]
+  2 -> 1 [label="!p1 | p2"]
+  2 -> 0 [label="1\n{0,1}"]
 }
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="1\n{0,1}"]
-  3 -> 2 [label="!p1 | p2"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="1\n{0,1}"]
+  2 -> 1 [label="!p1 | p2"]
 }
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="p1"]
-  1 -> 3 [label="p2\n{1}"]
-  2 [label="1"]
-  2 -> 3 [label="p1 & p2\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="1\n{0,1}"]
-  3 -> 2 [label="!p1 | p2"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="1\n{0,1}"]
+  2 -> 1 [label="!p1 | p2"]
+  3 [label="3"]
+  4 [label="4"]
+  5 [label="5"]
+  6 [label="6"]
+  7 [label="7"]
+  8 [label="8"]
+  9 [label="9"]
+  10 [label="10"]
+  11 [label="11"]
+  12 [label="12"]
+  13 [label="13"]
+  14 [label="14"]
+  15 [label="15"]
+  16 [label="16"]
+  17 [label="17"]
+  18 [label="18"]
+  19 [label="19"]
+  20 [label="20"]
+  21 [label="21"]
+  22 [label="22"]
+  23 [label="23"]
+  24 [label="24"]
+  25 [label="25"]
+  26 [label="26"]
+  27 [label="27"]
+  28 [label="28"]
+  29 [label="29"]
+  30 [label="30"]
+  31 [label="31"]
+  32 [label="32"]
+  33 [label="33"]
+  34 [label="34"]
+  35 [label="35"]
+  36 [label="36"]
+  37 [label="37"]
+  38 [label="38"]
+  39 [label="39"]
+  40 [label="40"]
+  41 [label="41"]
+  42 [label="42"]
+  43 [label="43"]
+  44 [label="44"]
+  45 [label="45"]
+  46 [label="46"]
+  47 [label="47"]
+  48 [label="48"]
+  49 [label="49"]
+  50 [label="50"]
+  51 [label="51"]
+  52 [label="52"]
+  53 [label="53"]
+  54 [label="54"]
+  55 [label="55"]
+  56 [label="56"]
+  57 [label="57"]
+  58 [label="58"]
+  59 [label="59"]
+  60 [label="60"]
+  61 [label="61"]
+  62 [label="62"]
+  63 [label="63"]
+  64 [label="64"]
+  65 [label="65"]
+  66 [label="66"]
+  67 [label="67"]
+  68 [label="68"]
+  69 [label="69"]
+  70 [label="70"]
+  71 [label="71"]
+  72 [label="72"]
+  73 [label="73"]
+  74 [label="74"]
+  75 [label="75"]
+  76 [label="76"]
+  77 [label="77"]
+  78 [label="78"]
+  79 [label="79"]
+  80 [label="80"]
+  81 [label="81"]
+  82 [label="82"]
+  83 [label="83"]
+  84 [label="84"]
+  85 [label="85"]
+  86 [label="86"]
+  87 [label="87"]
+  88 [label="88"]
+  89 [label="89"]
+  90 [label="90"]
+  91 [label="91"]
+  92 [label="92"]
+  93 [label="93"]
+  94 [label="94"]
+  95 [label="95"]
+  96 [label="96"]
+  97 [label="97"]
+  98 [label="98"]
+  99 [label="99"]
+  100 [label="100"]
+  101 [label="101"]
+  102 [label="102"]
 }
 EOF
 
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index 1532adea3..16dcd3769 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -29,6 +29,7 @@
 #include <memory>
 #include <unordered_map>
 #include <functional>
+#include <array>
 #include "misc/casts.hh"
 #include "misc/hash.hh"
 
@@ -734,24 +735,45 @@ namespace spot
       is.deterministic = val;
     }
 
-    // This is no default value here on purpose.  This way any time we
-    // add a new property we cannot to update every call to prop_copy().
-    void prop_copy(const const_tgba_ptr& other,
-		   bool state_based,
-		   bool single_acc,
-		   bool inherently_weak,
-		   bool deterministic)
+    struct prop_set
     {
-      if (state_based)
+      bool state_based;
+      bool single_acc;
+      bool inherently_weak;
+      bool deterministic;
+
+      static prop_set all()
+      {
+	return { true, true, true, true };
+      }
+    };
+
+    // There is no default value here on purpose.  This way any time we
+    // add a new property we have to update every call to prop_copy().
+    void prop_copy(const const_tgba_ptr& other, prop_set p)
+    {
+      if (p.state_based)
 	prop_state_based_acc(other->has_state_based_acc());
-      if (single_acc)
+      if (p.single_acc)
 	prop_single_acc_set(other->has_single_acc_set());
-      if (inherently_weak)
+      if (p.inherently_weak)
 	prop_inherently_weak(other->is_inherently_weak());
-      if (deterministic)
+      if (p.deterministic)
 	prop_deterministic(other->is_deterministic());
     }
 
+    void prop_keep(prop_set p)
+    {
+      if (!p.state_based)
+	prop_state_based_acc(false);
+      if (!p.single_acc)
+	prop_single_acc_set(false);
+      if (!p.inherently_weak)
+	prop_inherently_weak(false);
+      if (!p.deterministic)
+	prop_deterministic(false);
+    }
+
   };
 
   /// \addtogroup tgba_representation TGBA representations
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index 15288128e..4c875b385 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -186,13 +186,13 @@ namespace spot
     {
     }
 
-    explicit tgba_digraph(const const_tgba_digraph_ptr& other)
+    explicit tgba_digraph(const const_tgba_digraph_ptr& other, prop_set p)
       : tgba(other->get_dict()),
         g_(other->g_), init_number_(other->init_number_)
       {
 	copy_acceptance_conditions_of(other);
 	copy_ap_of(other);
-	prop_copy(other, true, true, true, true);
+	prop_copy(other, p);
       }
 
     virtual ~tgba_digraph()
@@ -489,23 +489,26 @@ namespace spot
     return std::make_shared<tgba_digraph>(dict);
   }
 
-  inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut)
+  inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut,
+					    tgba::prop_set p)
   {
-    return std::make_shared<tgba_digraph>(aut);
+    return std::make_shared<tgba_digraph>(aut, p);
   }
 
-  inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut)
+  inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut,
+					    tgba::prop_set p)
   {
-    return std::make_shared<tgba_digraph>(aut);
+    return std::make_shared<tgba_digraph>(aut, p);
   }
 
-  inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut)
+  inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut,
+					    tgba::prop_set p)
   {
-    auto p = std::dynamic_pointer_cast<const tgba_digraph>(aut);
-    if (p)
-      return std::make_shared<tgba_digraph>(p);
+    auto a = std::dynamic_pointer_cast<const tgba_digraph>(aut);
+    if (a)
+      return std::make_shared<tgba_digraph>(a, p);
     else
-      return tgba_dupexp_dfs(aut);
+      return tgba_dupexp_dfs(aut, p);
   }
 
 }
diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc
index 8e622c339..ec192bb2f 100644
--- a/src/tgbaalgos/are_isomorphic.cc
+++ b/src/tgbaalgos/are_isomorphic.cc
@@ -110,7 +110,7 @@ namespace spot
 {
   isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref)
   {
-    ref_ = make_tgba_digraph(ref);
+    ref_ = make_tgba_digraph(ref, {true, true, true, true});
     ref_deterministic_ = ref_->is_deterministic();
     if (!ref_deterministic_)
       {
@@ -142,7 +142,7 @@ namespace spot
           }
       }
 
-    auto tmp = make_tgba_digraph(aut);
+    auto tmp = make_tgba_digraph(aut, {true, true, true, true});
     spot::canonicalize(tmp);
     return *tmp == *ref_;
   }
diff --git a/src/tgbaalgos/closure.cc b/src/tgbaalgos/closure.cc
index 65df7e595..22d992b16 100644
--- a/src/tgbaalgos/closure.cc
+++ b/src/tgbaalgos/closure.cc
@@ -28,6 +28,12 @@ namespace spot
   tgba_digraph_ptr
   closure(tgba_digraph_ptr&& a)
   {
+    a->prop_keep({false,	// state_based
+	          true,		// single_acc
+	          false,	// inherently_weak
+	          false,	// deterministic
+	         });
+
     unsigned n = a->num_states();
     std::vector<unsigned> todo;
     std::vector<std::vector<unsigned> > dst2trans(n);
@@ -90,6 +96,6 @@ namespace spot
   tgba_digraph_ptr
   closure(const const_tgba_digraph_ptr& a)
   {
-    return closure(make_tgba_digraph(a));
+    return closure(make_tgba_digraph(a, {true, true, true, true}));
   }
 }
diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc
index c318df5b4..0d36c7d2e 100644
--- a/src/tgbaalgos/complete.cc
+++ b/src/tgbaalgos/complete.cc
@@ -104,12 +104,12 @@ namespace spot
 
   tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut)
   {
-    auto res = make_tgba_digraph(aut);
-    res->prop_copy(aut,
-		   true, 	// state based
-		   true, 	// single acc
-		   true, 	// inherently_weak
-		   true);	// deterministic
+    auto res = make_tgba_digraph(aut, {
+	                           true, // state based
+				   true, // single acc
+				   true, // inherently_weak
+				   true, // deterministic
+				 });
     tgba_complete_here(res);
     return res;
   }
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index 2b31cc45b..3a6f98ee8 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -203,7 +203,7 @@ namespace spot
       if (want_sba)
 	res->prop_state_based_acc();
       // Preserve determinism and weakness
-      res->prop_copy(a, false, false, true, true);
+      res->prop_copy(a, { false, false, true, true });
 
       // Create an order of acceptance conditions.  Each entry in this
       // vector correspond to an acceptance set.  Each index can
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index 5eea8ed21..0dfad6244 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -281,7 +281,7 @@ namespace spot
 	return os;
       }
     dotty_output d(os, options);
-    auto aut = make_tgba_digraph(g);
+    auto aut = make_tgba_digraph(g, tgba::prop_set::all());
     if (assume_sba)
       aut->prop_state_based_acc();
     d.print(aut);
diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc
index 617ba7c65..2cfbd3523 100644
--- a/src/tgbaalgos/dtgbacomp.cc
+++ b/src/tgbaalgos/dtgbacomp.cc
@@ -25,12 +25,12 @@ namespace spot
   tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut)
   {
     // Clone the original automaton.
-    auto res = make_tgba_digraph(aut);
-    res->prop_copy(aut,
-		   false, 	// state based
-		   false, 	// single acc
-		   false, 	// inherently_weak
-		   false);	// deterministic
+    auto res = make_tgba_digraph(aut,
+				 { false, // state based
+				   false, // single acc
+				   false, // inherently_weak
+				   false, // deterministic
+				  });
     // Copy the old acceptance condition before we replace it.
     acc_cond oldacc = aut->acc(); // Copy it!
 
@@ -113,13 +113,12 @@ namespace spot
   tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut)
   {
     // Clone the original automaton.
-    auto res = make_tgba_digraph(aut);
-    res->prop_copy(aut,
-		   true, 	// state based
-		   true, 	// single acc
-		   true, 	// inherently_weak
-		   true);	// deterministic
-
+    auto res = make_tgba_digraph(aut,
+				 { true, // state based
+				   true, // single acc
+				   true, // inherently weak
+				   true, // determinisitic
+				 });
     scc_info si(res);
 
     // We will modify res in place, and the resulting
diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc
index d86058993..6d17d2641 100644
--- a/src/tgbaalgos/dupexp.cc
+++ b/src/tgbaalgos/dupexp.cc
@@ -36,12 +36,12 @@ namespace spot
     class dupexp_iter: public T
     {
     public:
-      dupexp_iter(const const_tgba_ptr& a)
+      dupexp_iter(const const_tgba_ptr& a, tgba::prop_set p)
 	: T(a), out_(make_tgba_digraph(a->get_dict()))
       {
 	out_->copy_acceptance_conditions_of(a);
 	out_->copy_ap_of(a);
-	out_->prop_copy(a, true, true, true, true);
+	out_->prop_copy(a, p);
       }
 
       tgba_digraph_ptr
@@ -77,8 +77,9 @@ namespace spot
     {
     public:
       dupexp_iter_save(const const_tgba_ptr& a,
+		       tgba::prop_set p,
 		       std::vector<const state*>& relation)
-        : dupexp_iter<T>(a), relation_(relation)
+        : dupexp_iter<T>(a, p), relation_(relation)
       {
       }
 
@@ -96,37 +97,39 @@ namespace spot
   } // anonymous
 
   tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut)
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p)
   {
-    dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut);
+    dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut, p);
     di.run();
     return di.result();
   }
 
   tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut)
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p)
   {
-    dupexp_iter<tgba_reachable_iterator_depth_first> di(aut);
+    dupexp_iter<tgba_reachable_iterator_depth_first> di(aut, p);
     di.run();
     return di.result();
   }
 
   tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut, std::vector<const state*>& rel)
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p,
+		  std::vector<const state*>& rel)
   {
-    dupexp_iter_save<tgba_reachable_iterator_breadth_first> di(aut, rel);
+    dupexp_iter_save<tgba_reachable_iterator_breadth_first> di(aut, p, rel);
     di.run();
     return di.result();
   }
 
   tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut, std::vector<const state*>& rel)
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p,
+		  std::vector<const state*>& rel)
   {
-    auto aa = std::dynamic_pointer_cast<const spot::tgba_digraph>(aut);
+    auto aa = std::dynamic_pointer_cast<const tgba_digraph>(aut);
     if (aa)
       {
 	aa->get_init_state_number(); // Create an initial state if needed.
-	auto res = make_tgba_digraph(aa);
+	auto res = make_tgba_digraph(aa, p);
 	unsigned ns = aa->num_states();
 	rel.reserve(ns);
 	// The state numbers are common to both automata, but
@@ -136,7 +139,7 @@ namespace spot
 	return res;
       }
 
-    dupexp_iter_save<tgba_reachable_iterator_depth_first> di(aut, rel);
+    dupexp_iter_save<tgba_reachable_iterator_depth_first> di(aut, p, rel);
     di.run();
     return di.result();
   }
diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh
index 01fecd553..7ddbe4492 100644
--- a/src/tgbaalgos/dupexp.hh
+++ b/src/tgbaalgos/dupexp.hh
@@ -34,12 +34,12 @@ namespace spot
   /// \brief Build an explicit automaton from all states of \a aut,
   /// numbering states in bread first order as they are processed.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut);
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p);
   /// \ingroup tgba_misc
   /// \brief Build an explicit automaton from all states of \a aut,
   /// numbering states in depth first order as they are processed.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut);
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p);
 
   /// \ingroup tgba_misc
   /// \brief Build an explicit automaton from all states of \a aut,
@@ -48,7 +48,7 @@ namespace spot
   /// \a relation a map of all the new states (represented by
   /// their number) to the old states.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut,
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p,
 		  std::vector<const state*>& relation);
 
   /// \ingroup tgba_misc
@@ -58,7 +58,7 @@ namespace spot
   /// \a relation a map of all the new states (represented by
   /// their number) to the old states.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut,
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p,
 		  std::vector<const state*>& relation);
 }
 
diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc
index a3ff601db..5340bab7b 100644
--- a/src/tgbaalgos/sccfilter.cc
+++ b/src/tgbaalgos/sccfilter.cc
@@ -313,7 +313,7 @@ namespace spot
   scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si)
   {
     auto res = scc_filter_apply<state_filter<>>(aut, given_si);
-    res->prop_copy(aut, true, true, true, true);
+    res->prop_copy(aut, { true, true, true, true });
     return res;
   }
 
@@ -332,10 +332,11 @@ namespace spot
 			      <acc_filter_simplify<>>>>(aut, given_si);
     res->merge_transitions();
     res->prop_copy(aut,
-		   false,  // state-based acceptance is not preserved
-		   true,
-		   true,
-		   true);
+		   { false,  // state-based acceptance is not preserved
+		     true,
+		     true,
+		     true,
+		   });
     return res;
   }
 
@@ -363,10 +364,11 @@ namespace spot
 							  early_susp);
     res->merge_transitions();
     res->prop_copy(aut,
-		   false,  // state-based acceptance is not preserved
-		   true,
-		   true,
-		   false);	// determinism may not be preserved
+		   { false,  // state-based acceptance is not preserved
+		     true,
+		     true,
+		     false,	// determinism may not be preserved
+		   });
     return res;
   }
 
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 9dccbd66a..8c93279f3 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -252,7 +252,7 @@ namespace spot
         // the names (addresses) of the states in the automaton
         // returned by dupexp, and in automaton given in argument to
         // the constructor.
-        a_ = tgba_dupexp_dfs(t, new_original_);
+        a_ = tgba_dupexp_dfs(t, { true, true, true, true }, new_original_);
         scc_info_.reset(new scc_info(a_));
         old_a_ = a_;
 
@@ -701,10 +701,11 @@ namespace spot
 
 	delete gb;
 	res->prop_copy(original_,
-		       false, // state-based acc forced below
-		       false, // single acc is set by set_acceptance_conditions
-		       true,  // weakness preserved,
-		       false);	// determinism checked and set below
+		       { false, // state-based acc forced below
+			 false, // single acc set by set_acceptance_conditions
+		         true,  // weakness preserved,
+			 false, // determinism checked and set below
+		       });
         if (nb_minato == nb_satoneset)
 	  res->prop_deterministic();
 	if (Sba)
diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc
index f57d258e7..b4a2a1712 100644
--- a/src/tgbaalgos/stutterize.cc
+++ b/src/tgbaalgos/stutterize.cc
@@ -187,6 +187,7 @@ namespace spot
   tgba_digraph_ptr
   sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
   {
-    return sl2(make_tgba_digraph(a), atomic_propositions);
+    return sl2(make_tgba_digraph(a, tgba::prop_set::all()),
+	       atomic_propositions);
   }
 }
diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc
index 05ff2bd86..ba021635f 100644
--- a/src/tgbatest/checkpsl.cc
+++ b/src/tgbatest/checkpsl.cc
@@ -92,8 +92,12 @@ main(int argc, char** argv)
 
       if (fpos->is_ltl_formula())
 	{
-	  auto apos = scc_filter(make_tgba_digraph(ltl_to_taa(fpos, d)));
-	  auto aneg = scc_filter(make_tgba_digraph(ltl_to_taa(fneg, d)));
+	  auto apos =
+	    scc_filter(make_tgba_digraph(ltl_to_taa(fpos, d),
+					 spot::tgba::prop_set::all()));
+	  auto aneg =
+	    scc_filter(make_tgba_digraph(ltl_to_taa(fneg, d),
+					 spot::tgba::prop_set::all()));
 	  if (!spot::product(apos, aneg)->is_empty())
 	    {
 	      std::cerr << "non-empty intersection between pos and neg (TAA)\n";
diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc
index 6307bd2a8..a9d1d5eac 100644
--- a/src/tgbatest/emptchk.cc
+++ b/src/tgbatest/emptchk.cc
@@ -102,7 +102,8 @@ main(int argc, char** argv)
       {
 	auto a = spot::ltl_to_taa(f, d);
 	aut[0] = a;
-	aut[1] = spot::degeneralize_tba(spot::make_tgba_digraph(a));
+	auto all = spot::tgba::prop_set::all();
+	aut[1] = spot::degeneralize_tba(spot::make_tgba_digraph(a, all));
       }
       {
 	auto a = spot::ltl_to_tgba_fm(f, d);
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 195a4aefa..ae2c25160 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -328,7 +328,7 @@ spot::tgba_digraph_ptr ensure_digraph(const spot::tgba_ptr& a)
   auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
   if (aa)
     return aa;
-  return spot::make_tgba_digraph(a);
+  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
 }
 
 int
@@ -1436,10 +1436,10 @@ checked_main(int argc, char** argv)
 	case NoneDup:
 	  break;
 	case BFS:
-	  a = tgba_dupexp_bfs(a);
+	  a = tgba_dupexp_bfs(a, spot::tgba::prop_set::all());
 	  break;
 	case DFS:
-	  a = tgba_dupexp_dfs(a);
+	  a = tgba_dupexp_dfs(a, spot::tgba::prop_set::all());
 	  break;
 	}
 
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 4e0b19c33..3613cdd61 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -368,7 +368,7 @@ ensure_digraph(const spot::tgba_ptr& a)
   auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
   if (aa)
     return aa;
-  return spot::make_tgba_digraph(a);
+  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
 }
 
 std::ostream&