From 4f1535c8fe3937cffda5174ca1e5f16bd1d2967c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 30 Nov 2014 19:53:14 +0100 Subject: [PATCH] defaultenv: simplify usage * src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc (require): Return an atomic_prop*, not a formula*. * src/bin/randaut.cc, src/bin/randltl.cc, src/ltlvisit/apcollect.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Do not cast the return of require(). --- src/bin/randaut.cc | 4 +--- src/bin/randltl.cc | 6 ++---- src/ltlenv/defaultenv.cc | 3 +-- src/ltlenv/defaultenv.hh | 3 ++- src/ltlvisit/apcollect.cc | 3 +-- src/tgbatest/ltl2tgba.cc | 5 ++--- src/tgbatest/randtgba.cc | 8 +++----- 7 files changed, 12 insertions(+), 20 deletions(-) diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index a988034ce..dc189b408 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -31,7 +31,6 @@ #include "common_range.hh" #include "common_cout.hh" -#include "ltlast/atomic_prop.hh" #include "ltlenv/defaultenv.hh" #include "misc/random.hh" @@ -242,8 +241,7 @@ parse_opt(int key, char* arg, struct argp_state* as) break; } } - aprops.insert(static_cast - (spot::ltl::default_environment::instance().require(arg))); + aprops.insert(spot::ltl::default_environment::instance().require(arg)); break; default: diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index d3f387a90..0c1e0e502 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -32,7 +32,6 @@ #include "common_r.hh" #include -#include "ltlast/atomic_prop.hh" #include "ltlast/multop.hh" #include "ltlast/unop.hh" #include "ltlvisit/randomltl.hh" @@ -156,7 +155,7 @@ remove_some_props(spot::ltl::atomic_prop_set& s) while (n--) { - spot::ltl::atomic_prop_set::iterator i = s.begin(); + auto i = s.begin(); std::advance(i, spot::mrand(s.size())); s.erase(i); } @@ -260,8 +259,7 @@ parse_opt(int key, char* arg, struct argp_state* as) break; } } - aprops.insert(static_cast - (spot::ltl::default_environment::instance().require(arg))); + aprops.insert(spot::ltl::default_environment::instance().require(arg)); break; default: return ARGP_ERR_UNKNOWN; diff --git a/src/ltlenv/defaultenv.cc b/src/ltlenv/defaultenv.cc index 81c767b4d..35bacba47 100644 --- a/src/ltlenv/defaultenv.cc +++ b/src/ltlenv/defaultenv.cc @@ -20,7 +20,6 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "ltlast/atomic_prop.hh" #include "defaultenv.hh" namespace spot @@ -32,7 +31,7 @@ namespace spot { } - const formula* + const atomic_prop* default_environment::require(const std::string& s) { return atomic_prop::instance(s, *this); diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh index 06a264133..711e6db8a 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -24,6 +24,7 @@ # define SPOT_LTLENV_DEFAULTENV_HH # include "environment.hh" +# include "ltlast/atomic_prop.hh" namespace spot { @@ -41,7 +42,7 @@ namespace spot { public: virtual ~default_environment(); - virtual const formula* require(const std::string& prop_str); + virtual const atomic_prop* require(const std::string& prop_str); virtual const std::string& name() const; /// Get the sole instance of spot::ltl::default_environment. diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index 5daab9042..82bd67dea 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -61,8 +61,7 @@ namespace spot { std::ostringstream p; p << 'p' << i; - res.insert(static_cast - (e.require(p.str()))); + res.insert(e.require(p.str())); } return res; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a600c45f5..122bdfbbf 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -386,7 +386,7 @@ checked_main(int argc, char** argv) bool opt_stutterize = false; bool spin_comments = false; const char* hoa_opt = 0; - spot::ltl::environment& env(spot::ltl::default_environment::instance()); + auto& env = spot::ltl::default_environment::instance(); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba_ptr system_aut = 0; auto dict = spot::make_bdd_dict(); @@ -846,8 +846,7 @@ checked_main(int argc, char** argv) const char* tok = strtok(argv[formula_index] + 2, ", \t;"); while (tok) { - unobservables->insert - (static_cast(env.require(tok))); + unobservables->insert(env.require(tok)); tok = strtok(0, ", \t;"); } } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 38658e8b5..bfbd91765 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -40,7 +40,6 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "ltlenv/defaultenv.hh" -#include "ltlast/atomic_prop.hh" #include "tgbaalgos/dotty.hh" #include "tgbaparse/public.hh" #include "misc/random.hh" @@ -586,7 +585,7 @@ main(int argc, char** argv) spot::option_map options; - spot::ltl::environment& env(spot::ltl::default_environment::instance()); + auto& env = spot::ltl::default_environment::instance(); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; auto dict = spot::make_bdd_dict(); @@ -794,8 +793,7 @@ main(int argc, char** argv) } else { - ap->insert(static_cast - (env.require(argv[argn]))); + ap->insert(env.require(argv[argn])); } } @@ -886,7 +884,7 @@ main(int argc, char** argv) spot::ltl::atomic_prop_collect(f); for (spot::ltl::atomic_prop_set::iterator i = tmp->begin(); i != tmp->end(); ++i) - apf->insert(dynamic_cast + apf->insert(down_cast ((*i)->clone())); f->destroy(); delete tmp;