From 0250a327479e91573853b599a9a181dd8441d538 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 26 Nov 2014 10:27:59 +0100
Subject: [PATCH] export a create_atomic_prop_set() function

* src/ltlvisit/apcollect.hh,
src/ltlvisit/apcollect.cc (create_atomic_prop_set): New function.
* src/bin/randltl.cc, bench/stutter/stutter_invariance_randomgraph.cc:
Use it.
---
 .../stutter/stutter_invariance_randomgraph.cc | 20 +++++--------------
 src/bin/randltl.cc                            | 10 +---------
 src/ltlvisit/apcollect.cc                     | 14 +++++++++++++
 src/ltlvisit/apcollect.hh                     |  4 ++++
 4 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc
index 4920e72ea..4b73af077 100644
--- a/bench/stutter/stutter_invariance_randomgraph.cc
+++ b/bench/stutter/stutter_invariance_randomgraph.cc
@@ -18,7 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "misc/timer.hh"
-#include "ltlast/atomic_prop.hh"
+#include "ltlvisit/apcollect.hh"
 #include "tgbaalgos/dtgbacomp.hh"
 #include "tgbaalgos/stutter_invariance.hh"
 #include "tgbaalgos/randomgraph.hh"
@@ -45,20 +45,11 @@ main()
         for (unsigned props_n = 1; props_n <= 4; ++props_n)
           {
             // random ap set
-            auto ap = new spot::ltl::atomic_prop_set();
-            spot::ltl::default_environment& e =
-              spot::ltl::default_environment::instance();
-            for (unsigned i = 1; i < props_n; ++i)
-              {
-                std::ostringstream p;
-                p << 'p' << i;
-                ap->insert(static_cast<const spot::ltl::atomic_prop*>
-                           (e.require(p.str())));
-              }
+            auto ap = spot::ltl::create_atomic_prop_set(props_n);
 
             // ap set as bdd
             bdd apdict = bddtrue;
-            for (auto& i: *ap)
+            for (auto& i: ap)
               apdict &= bdd_ithvar(dict->register_proposition(i, a));
 
             // generate n random automata
@@ -67,7 +58,7 @@ main()
             std::vector<aut_pair_t> vec;
             for (unsigned i = 0; i < n; ++i)
               {
-                a = spot::random_graph(states_n, d, ap, dict, 2, 0.1, 0.5,
+                a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5,
                                        true);
                 na = spot::dtgba_complement(a);
                 vec.push_back(aut_pair_t(a, na));
@@ -94,8 +85,7 @@ main()
                 std::cout << algo << ", " << props_n << ", " << states_n
                           << ", " << res << ", " << time << std::endl;
               }
-            spot::ltl::destroy_atomic_prop_set(*ap);
-            delete ap;
+            spot::ltl::destroy_atomic_prop_set(ap);
           }
       }
 
diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc
index 98b1f098a..9e444d597 100644
--- a/src/bin/randltl.cc
+++ b/src/bin/randltl.cc
@@ -256,15 +256,7 @@ parse_opt(int key, char* arg, struct argp_state* as)
 	  if (!*endptr && res >= 0) // arg is a number
 	    {
 	      ap_count_given = true;
-	      spot::ltl::default_environment& e =
-		spot::ltl::default_environment::instance();
-	      for (int i = 0; i < res; ++i)
-		{
-		  std::ostringstream p;
-		  p << 'p' << i;
-		  aprops.insert(static_cast<const spot::ltl::atomic_prop*>
-				(e.require(p.str())));
-		}
+	      aprops = spot::ltl::create_atomic_prop_set(res);
 	      break;
 	    }
 	}
diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc
index 16c8e4479..5daab9042 100644
--- a/src/ltlvisit/apcollect.cc
+++ b/src/ltlvisit/apcollect.cc
@@ -53,6 +53,20 @@ namespace spot
       };
     }
 
+    atomic_prop_set create_atomic_prop_set(unsigned n)
+    {
+      atomic_prop_set res;
+      auto& e = spot::ltl::default_environment::instance();
+      for (unsigned i = 0; i < n; ++i)
+	{
+	  std::ostringstream p;
+	  p << 'p' << i;
+	  res.insert(static_cast<const spot::ltl::atomic_prop*>
+		     (e.require(p.str())));
+	}
+      return res;
+    }
+
     void destroy_atomic_prop_set(atomic_prop_set& aprops)
     {
       atomic_prop_set::const_iterator i = aprops.begin();
diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh
index 8dd46cee6..3b51210a0 100644
--- a/src/ltlvisit/apcollect.hh
+++ b/src/ltlvisit/apcollect.hh
@@ -39,6 +39,10 @@ namespace spot
     typedef std::set<const atomic_prop*,
 		     formula_ptr_less_than> atomic_prop_set;
 
+    /// \brief construct an atomic_prop_set with n propositions
+    SPOT_API
+    atomic_prop_set create_atomic_prop_set(unsigned n);
+
     /// \brief Destroy all the atomic propositions in an
     /// atomic_prop_set.
     SPOT_API void