From bf62d439c95e74e4338ef2225ec12f1f6cda7dfb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 May 2012 23:38:55 +0200 Subject: [PATCH] Use 'const formula*' instead of 'formula*' everywhere. The distinction makes no sense since Spot 0.5, where we switched from mutable furmulae to immutable formulae. The difference between const_visitor and visitor made no sense either. They have been merged into one: visitor. * iface/dve2/dve2check.cc, iface/gspn/ltlgspn.cc, src/eltlparse/eltlparse.yy, src/eltlparse/public.hh, src/evtgbatest/ltl2evtgba.cc, src/kripkeparse/kripkeparse.yy, src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh, src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/formula_tree.cc, src/ltlast/formula_tree.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.cc, src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/ltlfile.cc, src/ltlparse/ltlfile.hh, src/ltlparse/ltlparse.yy, src/ltlparse/public.hh, src/ltltest/consterm.cc, src/ltltest/equals.cc, src/ltltest/genltl.cc, src/ltltest/kind.cc, src/ltltest/length.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltltest/tostring.cc, src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh, src/ltlvisit/contain.cc, src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc, src/ltlvisit/length.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.cc, src/ltlvisit/mark.hh, src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh, src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc, src/ltlvisit/snf.hh, src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh, src/neverparse/neverclaimparse.yy, src/sabatest/sabacomplementtgba.cc, src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc: Massive adjustment! * src/tgbatest/reductgba.cc: Delete. --- NEWS | 21 +- iface/dve2/dve2check.cc | 8 +- iface/gspn/ltlgspn.cc | 13 +- src/eltlparse/eltlparse.yy | 12 +- src/eltlparse/public.hh | 23 +- src/evtgbatest/ltl2evtgba.cc | 11 +- src/kripkeparse/kripkeparse.yy | 9 +- src/ltlast/atomic_prop.cc | 32 +- src/ltlast/atomic_prop.hh | 8 +- src/ltlast/automatop.cc | 34 +- src/ltlast/automatop.hh | 18 +- src/ltlast/binop.cc | 48 +- src/ltlast/binop.hh | 70 ++- src/ltlast/bunop.cc | 60 ++- src/ltlast/bunop.hh | 59 ++- src/ltlast/constant.cc | 17 +- src/ltlast/constant.hh | 9 +- src/ltlast/formula.cc | 12 +- src/ltlast/formula.hh | 14 +- src/ltlast/formula_tree.cc | 7 +- src/ltlast/formula_tree.hh | 5 +- src/ltlast/multop.cc | 132 +++--- src/ltlast/multop.hh | 62 ++- src/ltlast/predecl.hh | 5 +- src/ltlast/refformula.cc | 11 +- src/ltlast/refformula.hh | 17 +- src/ltlast/unop.cc | 57 +-- src/ltlast/unop.hh | 57 ++- src/ltlast/visitor.hh | 33 +- src/ltlenv/declenv.cc | 4 +- src/ltlenv/declenv.hh | 9 +- src/ltlenv/defaultenv.cc | 7 +- src/ltlenv/defaultenv.hh | 7 +- src/ltlenv/environment.hh | 4 +- src/ltlparse/ltlfile.cc | 6 +- src/ltlparse/ltlfile.hh | 4 +- src/ltlparse/ltlparse.yy | 12 +- src/ltlparse/public.hh | 17 +- src/ltltest/consterm.cc | 7 +- src/ltltest/equals.cc | 21 +- src/ltltest/genltl.cc | 141 +++--- src/ltltest/kind.cc | 5 +- src/ltltest/length.cc | 3 +- src/ltltest/randltl.cc | 6 +- src/ltltest/readltl.cc | 11 +- src/ltltest/reduc.cc | 10 +- src/ltltest/syntimpl.cc | 15 +- src/ltltest/tostring.cc | 11 +- src/ltlvisit/apcollect.cc | 9 +- src/ltlvisit/apcollect.hh | 8 +- src/ltlvisit/clone.cc | 27 +- src/ltlvisit/clone.hh | 31 +- src/ltlvisit/contain.cc | 12 +- src/ltlvisit/contain.hh | 13 +- src/ltlvisit/dotty.cc | 2 +- src/ltlvisit/length.cc | 12 +- src/ltlvisit/lunabbrev.cc | 36 +- src/ltlvisit/lunabbrev.hh | 11 +- src/ltlvisit/mark.cc | 68 +-- src/ltlvisit/mark.hh | 8 +- src/ltlvisit/nenoform.cc | 9 +- src/ltlvisit/nenoform.hh | 9 +- src/ltlvisit/postfix.cc | 33 +- src/ltlvisit/postfix.hh | 32 +- src/ltlvisit/randomltl.cc | 33 +- src/ltlvisit/randomltl.hh | 11 +- src/ltlvisit/reduce.cc | 8 +- src/ltlvisit/reduce.hh | 11 +- src/ltlvisit/simpfg.cc | 19 +- src/ltlvisit/simpfg.hh | 13 +- src/ltlvisit/simplify.cc | 686 +++++++++++++++-------------- src/ltlvisit/simplify.hh | 5 +- src/ltlvisit/snf.cc | 28 +- src/ltlvisit/snf.hh | 4 +- src/ltlvisit/tostring.cc | 32 +- src/ltlvisit/tunabbrev.cc | 12 +- src/ltlvisit/tunabbrev.hh | 11 +- src/ltlvisit/wmunabbrev.cc | 12 +- src/ltlvisit/wmunabbrev.hh | 2 +- src/neverparse/neverclaimparse.yy | 9 +- src/sabatest/sabacomplementtgba.cc | 6 +- src/tgba/bdddict.cc | 9 +- src/tgba/formula2bdd.cc | 6 +- src/tgba/taatgba.cc | 10 +- src/tgba/taatgba.hh | 7 +- src/tgbaalgos/eltl2tgba_lacim.cc | 8 +- src/tgbaalgos/ltl2taa.cc | 9 +- src/tgbaalgos/ltl2tgba_fm.cc | 128 +++--- src/tgbaalgos/ltl2tgba_lacim.cc | 2 +- src/tgbaalgos/minimize.cc | 3 +- src/tgbaalgos/randomgraph.cc | 11 +- src/tgbaparse/tgbaparse.yy | 28 +- src/tgbatest/complementation.cc | 14 +- src/tgbatest/ltl2tgba.cc | 6 +- src/tgbatest/ltlprod.cc | 13 +- src/tgbatest/mixprod.cc | 11 +- src/tgbatest/randtgba.cc | 23 +- src/tgbatest/reductgba.cc | 179 -------- 98 files changed, 1318 insertions(+), 1535 deletions(-) delete mode 100644 src/tgbatest/reductgba.cc diff --git a/NEWS b/NEWS index 0018b9125..36e7f55bf 100644 --- a/NEWS +++ b/NEWS @@ -6,10 +6,6 @@ New in spot 0.8.3a: Expressions (SERE), and a couple of operators to bridge SERE and LTL. See doc/tl/tl.pdf for the list of operators and their semantics. - - The constructors for temporal formulae will perform some trivial - simplifications based on associativity, commutativity, - idempotence, and neutral elements. See doc/tl/tl.pdf for the - list of such simplifications. - Formula rewritings have been completely revamped, and augmented with rules for PSL operators (and some new LTL rules as well). See doc/tl/tl.pdf for the list of the rewritings implemented. @@ -51,13 +47,24 @@ New in spot 0.8.3a: * Interface changes: - Operators ->, <->, U, W, R, and M are now parsed as right-associative to better match the PSL standard. + - The constructors for temporal formulae will perform some trivial + simplifications based on associativity, commutativity, + idempotence, and neutral elements. See doc/tl/tl.pdf for the + list of such simplifications. + - Formula instances now have many methods to inspect their + properties (membership to syntactic classes, absence of X + operator, etc...) in constant time. + - LTL/PSL formulae are now handled everywhere as 'const formula*' + and not just 'formula*'. This reflects the true nature of these + (immutable) formula objects, and cleanups a lot of code. + Unfortunately, it is a backward incompatible change: you may have + to add 'const' to a couple of lines in your code, and change + 'ltl::const_vistitor' into 'ltl::visitor' if you have written a + custom visitor. - The new entry point for LTL/PSL simplifications is the function ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. The ltl_simplifier class implements a cache. Functions such as reduce() or reduce_tau03() are deprecated. - - Formula instances now have many methods to inspect their - properties (membership to syntactic classes, absence of X - operator, etc...) in constant time. - The old game-theory-based implementations for direct and delayed simulation reductions have been removed. The old direct simulation would only work on degeneralized automata, and yet diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index f775b7b11..64aadec6b 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -177,8 +177,8 @@ main(int argc, char **argv) spot::tgba* product = 0; spot::emptiness_check_instantiator* echeck_inst = 0; int exit_code = 0; - spot::ltl::formula* f = 0; - spot::ltl::formula* deadf = 0; + const spot::ltl::formula* f = 0; + const spot::ltl::formula* deadf = 0; if (dead == 0 || !strcasecmp(dead, "true")) { @@ -222,7 +222,7 @@ main(int argc, char **argv) { spot::ltl::ltl_simplifier_options opt(true, true, true, true, true); spot::ltl::ltl_simplifier simp(opt); - spot::ltl::formula* r = simp.simplify(f); + const spot::ltl::formula* r = simp.simplify(f); f->destroy(); f = r; } diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 63de32c59..d36b97f6d 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -1,6 +1,9 @@ -// Copyright (C) 2003, 2004, 2006, 2007, 2008, 2009 Laboratoire -// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis -// Coopératifs (SRC), Université Pierre et Marie Curie. +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE) +// Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -229,8 +232,8 @@ main(int argc, char **argv) } spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[formula_index + 1], - pel, env); + const spot::ltl::formula* f = + spot::ltl::parse(argv[formula_index + 1], pel, env); if (spot::ltl::format_parse_errors(std::cerr, argv[formula_index + 1], pel)) diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index a02276c49..d28f09bf5 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -64,7 +64,7 @@ namespace spot %parse-param {spot::eltl::aliasmap& amap} %parse-param {spot::eltl::parse_error_list_t &pe} %parse-param {spot::ltl::environment &parse_environment} -%parse-param {spot::ltl::formula* &result} +%parse-param {const spot::ltl::formula* &result} %lex-param {spot::eltl::parse_error_list_t &pe} %expect 0 %pure-parser @@ -74,7 +74,7 @@ namespace spot std::string* sval; spot::ltl::nfa* nval; spot::ltl::automatop::vec* aval; - spot::ltl::formula* fval; + const spot::ltl::formula* fval; /// To handle aliases. spot::ltl::formula_tree::node* pval; @@ -520,7 +520,7 @@ namespace spot { namespace eltl { - formula* + const formula* parse_file(const std::string& name, parse_error_list& error_list, environment& env, @@ -533,7 +533,7 @@ namespace spot spair("-", std::string("Cannot open file ") + name))); return 0; } - formula* result = 0; + const formula* result = 0; nfamap nmap; aliasmap amap; parse_error_list_t pe; @@ -546,14 +546,14 @@ namespace spot return result; } - formula* + const formula* parse_string(const std::string& eltl_string, parse_error_list& error_list, environment& env, bool debug) { flex_scan_string(eltl_string.c_str()); - formula* result = 0; + const formula* result = 0; nfamap nmap; aliasmap amap; parse_error_list_t pe; diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh index c96bfb71e..bd2ae874d 100644 --- a/src/eltlparse/public.hh +++ b/src/eltlparse/public.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -64,10 +65,11 @@ namespace spot /// 0 if the file could not be opened. /// /// \warning This function is not reentrant. - formula* parse_file(const std::string& filename, - parse_error_list& error_list, - environment& env = default_environment::instance(), - bool debug = false); + const formula* parse_file(const std::string& filename, + parse_error_list& error_list, + environment& env = + default_environment::instance(), + bool debug = false); /// \brief Build a formula from an ELTL string. /// \param eltl_string The string to parse. @@ -79,10 +81,11 @@ namespace spot /// 0 if the input was unparsable. /// /// \warning This function is not reentrant. - formula* parse_string(const std::string& eltl_string, - parse_error_list& error_list, - environment& env = default_environment::instance(), - bool debug = false); + const formula* parse_string(const std::string& eltl_string, + parse_error_list& error_list, + environment& env = + default_environment::instance(), + bool debug = false); /// \brief Format diagnostics produced by spot::eltl::parse. /// \param os Where diagnostics should be output. diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc index ff526f216..9391d7257 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -84,7 +85,7 @@ main(int argc, char** argv) while (tok) { unobservables->insert - (static_cast(env.require(tok))); + (static_cast(env.require(tok))); tok = strtok(0, ", \t;"); } } @@ -100,7 +101,7 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); - spot::ltl::formula* f = 0; + const spot::ltl::formula* f = 0; { spot::ltl::parse_error_list pel; diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy index 4b4c0fad3..f6fb5b4d0 100644 --- a/src/kripkeparse/kripkeparse.yy +++ b/src/kripkeparse/kripkeparse.yy @@ -1,4 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -48,7 +49,7 @@ typedef std::map formula_cache; { int token; std::string* str; - spot::ltl::formula* f; + const spot::ltl::formula* f; std::list* list; } @@ -113,7 +114,7 @@ strident "," condition "," follow_list ";" if (i == fcache.end()) { parse_error_list pel; - formula* f = spot::ltl::parse(*$3, pel, parse_environment); + const formula* f = spot::ltl::parse(*$3, pel, parse_environment); for (parse_error_list::iterator i = pel.begin(); i != pel.end(); ++i) { @@ -158,7 +159,7 @@ string: STRING { $$ = $1; error_list.push_back(spot::kripke_parse_error(@1, - "unterminated string")); + "unterminated string")); } ; diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 823a74c8e..13ee24a60 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -71,13 +72,7 @@ namespace spot } void - atomic_prop::accept(visitor& v) - { - v.visit(this); - } - - void - atomic_prop::accept(const_visitor& v) const + atomic_prop::accept(visitor& v) const { v.visit(this); } @@ -96,18 +91,19 @@ namespace spot atomic_prop::map atomic_prop::instances; - atomic_prop* + const atomic_prop* atomic_prop::instance(const std::string& name, environment& env) { pair p(name, &env); + // FIXME: Use lower_bound, or a hash_map. map::iterator i = instances.find(p); + const atomic_prop* ap; if (i != instances.end()) - { - return static_cast(i->second->clone()); - } - atomic_prop* ap = new atomic_prop(name, env); - instances[p] = ap; - return static_cast(ap->clone()); + ap = i->second; + else + ap = instances[p] = new atomic_prop(name, env); + ap->clone(); + return ap; } unsigned diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 79105f769..963359be1 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -45,10 +45,10 @@ namespace spot public: /// Build an atomic proposition with name \a name in /// environment \a env. - static atomic_prop* instance(const std::string& name, environment& env); + static const atomic_prop* + instance(const std::string& name, environment& env); - virtual void accept(visitor& visitor); - virtual void accept(const_visitor& visitor) const; + virtual void accept(visitor& visitor) const; /// Get the name of the atomic proposition. const std::string& name() const; @@ -68,7 +68,7 @@ namespace spot virtual ~atomic_prop(); typedef std::pair pair; - typedef std::map map; + typedef std::map map; static map instances; private: diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index fe7551eeb..8f9959bf9 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -84,36 +85,34 @@ namespace spot } void - automatop::accept(visitor& v) - { - v.visit(this); - } - - void - automatop::accept(const_visitor& v) const + automatop::accept(visitor& v) const { v.visit(this); } automatop::map automatop::instances; - automatop* + const automatop* automatop::instance(const nfa::ptr nfa, vec* v, bool negated) { assert(nfa != 0); triplet p(std::make_pair(nfa, negated), v); map::iterator i = instances.find(p); + const automatop* res; if (i != instances.end()) { // The instance already exists. for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) (*vi)->destroy(); delete v; - return static_cast(i->second->clone()); + res = i->second; } - automatop* res = new automatop(nfa, v, negated); - instances[p] = res; - return static_cast(res->clone()); + else + { + res = instances[p] = new automatop(nfa, v, negated); + } + res->clone(); + return res; } unsigned @@ -128,12 +127,6 @@ namespace spot return (*children_)[n]; } - formula* - automatop::nth(unsigned n) - { - return (*children_)[n]; - } - const spot::ltl::nfa::ptr automatop::get_nfa() const { @@ -165,6 +158,5 @@ namespace spot } return os; } - } } diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index c1f67160a..1ee820818 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE) +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -40,7 +41,7 @@ namespace spot { public: /// List of formulae. - typedef std::vector vec; + typedef std::vector vec; /// \brief Build a spot::ltl::automatop with many children. /// @@ -48,11 +49,10 @@ namespace spot /// the caller should allocate it with \c new, but not use it /// (especially not destroy it) after it has been passed to /// spot::ltl::automatop. - static automatop* + static const automatop* instance(const nfa::ptr nfa, vec* v, bool negated); - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Get the number of argument. unsigned size() const; @@ -60,10 +60,6 @@ namespace spot /// /// Starting with \a n = 0. const formula* nth(unsigned n) const; - /// \brief Get the nth argument. - /// - /// Starting with \a n = 0. - formula* nth(unsigned n); /// Get the NFA of this operator. const spot::ltl::nfa::ptr get_nfa() const; @@ -96,7 +92,7 @@ namespace spot return *p1.second < *p2.second; } }; - typedef std::map map; + typedef std::map map; static map instances; automatop(const nfa::ptr, vec* v, bool negated); diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index e69c47f68..23bd43e2e 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -34,7 +35,7 @@ namespace spot { namespace ltl { - binop::binop(type op, formula* first, formula* second) + binop::binop(type op, const formula* first, const formula* second) : ref_formula(BinOp), op_(op), first_(first), second_(second) { // Beware: (f U g) is a pure eventuality if both operands @@ -270,13 +271,7 @@ namespace spot } void - binop::accept(visitor& v) - { - v.visit(this); - } - - void - binop::accept(const_visitor& v) const + binop::accept(visitor& v) const { v.visit(this); } @@ -287,24 +282,12 @@ namespace spot return first_; } - formula* - binop::first() - { - return first_; - } - const formula* binop::second() const { return second_; } - formula* - binop::second() - { - return second_; - } - binop::type binop::op() const { @@ -344,8 +327,8 @@ namespace spot binop::map binop::instances; - formula* - binop::instance(type op, formula* first, formula* second) + const formula* + binop::instance(type op, const formula* first, const formula* second) { // Sort the operands of commutative operators, so that for // example the formula instance for 'a xor b' is the same as @@ -544,17 +527,22 @@ namespace spot pairf pf(first, second); pair p(op, pf); + // FIXME: Use lower_bound or hash_map. map::iterator i = instances.find(p); + const binop* res; if (i != instances.end()) { // This instance already exists. first->destroy(); second->destroy(); - return static_cast(i->second->clone()); + res = i->second; } - binop* ap = new binop(op, first, second); - instances[p] = ap; - return static_cast(ap->clone()); + else + { + res = instances[p] = new binop(op, first, second); + } + res->clone(); + return res; } unsigned diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index b71c3c321..d9af12d80 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -106,19 +106,16 @@ namespace spot /// - [*0] []-> Exp = 1 /// - Exp []-> 1 = 1 /// - boolExp <>-> Exp = !boolExp | Exp - static formula* instance(type op, formula* first, formula* second); + static const formula* instance(type op, + const formula* first, + const formula* second); - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Get the first operand. const formula* first() const; - /// Get the first operand. - formula* first(); /// Get the second operand. const formula* second() const; - /// Get the second operand. - formula* second(); /// Get the type of this operator. type op() const; @@ -135,18 +132,18 @@ namespace spot static std::ostream& dump_instances(std::ostream& os); protected: - typedef std::pair pairf; + typedef std::pair pairf; typedef std::pair pair; - typedef std::map map; + typedef std::map map; static map instances; - binop(type op, formula* first, formula* second); + binop(type op, const formula* first, const formula* second); virtual ~binop(); private: type op_; - formula* first_; - formula* second_; + const formula* first_; + const formula* second_; }; /// \brief Cast \a f into a binop @@ -154,12 +151,12 @@ namespace spot /// Cast \a f into a binop iff it is a binop instance. Return 0 /// otherwise. This is faster than \c dynamic_cast. inline - binop* - is_binop(formula* f) + const binop* + is_binop(const formula* f) { if (f->kind() != formula::BinOp) return 0; - return static_cast(f); + return static_cast(f); } /// \brief Cast \a f into a binop if it has type \a op. @@ -167,15 +164,13 @@ namespace spot /// Cast \a f into a binop iff it is a unop instance with operator \a op. /// Returns 0 otherwise. inline - binop* - is_binop(formula* f, binop::type op) + const binop* + is_binop(const formula* f, binop::type op) { - if (f->kind() != formula::BinOp) - return 0; - binop* bo = static_cast(f); - if (bo->op() != op) - return 0; - return bo; + if (const binop* bo = is_binop(f)) + if (bo->op() == op) + return bo; + return 0; } /// \brief Cast \a f into a binop if it has type \a op1 or \a op2. @@ -183,15 +178,12 @@ namespace spot /// Cast \a f into a binop iff it is a unop instance with operator \a op1 or /// \a op2. Returns 0 otherwise. inline - binop* - is_binop(formula* f, binop::type op1, binop::type op2) + const binop* + is_binop(const formula* f, binop::type op1, binop::type op2) { - if (f->kind() != formula::BinOp) - return 0; - binop* bo = static_cast(f); - binop::type op = bo->op(); - if (op == op1 || op == op2) - return bo; + if (const binop* bo = is_binop(f)) + if (bo->op() == op1 || bo->op() == op2) + return bo; return 0; } @@ -199,8 +191,8 @@ namespace spot /// /// Return 0 otherwise. inline - binop* - is_U(formula* f) + const binop* + is_U(const formula* f) { return is_binop(f, binop::U); } @@ -209,8 +201,8 @@ namespace spot /// /// Return 0 otherwise. inline - binop* - is_M(formula* f) + const binop* + is_M(const formula* f) { return is_binop(f, binop::M); } @@ -219,8 +211,8 @@ namespace spot /// /// Return 0 otherwise. inline - binop* - is_R(formula* f) + const binop* + is_R(const formula* f) { return is_binop(f, binop::R); } @@ -229,8 +221,8 @@ namespace spot /// /// Return 0 otherwise. inline - binop* - is_W(formula* f) + const binop* + is_W(const formula* f) { return is_binop(f, binop::W); } diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 9b2950db8..58689aadb 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -33,9 +33,9 @@ namespace spot { // Can't build it on startup, because it uses // constant::true_instance that may not have been built yet... - formula* bunop::one_star_ = 0; + const formula* bunop::one_star_ = 0; - bunop::bunop(type op, formula* child, unsigned min, unsigned max) + bunop::bunop(type op, const formula* child, unsigned min, unsigned max) : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max) { props = child->get_props(); @@ -95,13 +95,7 @@ namespace spot } void - bunop::accept(visitor& v) - { - v.visit(this); - } - - void - bunop::accept(const_visitor& v) const + bunop::accept(visitor& v) const { v.visit(this); } @@ -112,12 +106,6 @@ namespace spot return child_; } - formula* - bunop::child() - { - return child_; - } - unsigned bunop::min() const { @@ -187,8 +175,9 @@ namespace spot bunop::map bunop::instances; - formula* - bunop::instance(type op, formula* child, unsigned min, unsigned max) + const formula* + bunop::instance(type op, const formula* child, + unsigned min, unsigned max) { assert(min <= max); @@ -225,9 +214,8 @@ namespace spot // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] // if i*(min+1)<=j(min)+1. - if (child->kind() == BUnOp) + if (const bunop* s = is_bunop(child)) { - bunop* s = static_cast(child); unsigned i = s->min(); unsigned j = s->max(); @@ -242,7 +230,7 @@ namespace spot // (Because i<=j, this entails that the other intervals also // overlap). - formula* exp = s->child(); + const formula* exp = s->child(); if (j == unbounded) { min *= i; @@ -283,25 +271,26 @@ namespace spot child->destroy(); return i->second->clone(); } - bunop* ap = new bunop(op, child, min, max); - instances[p] = ap; - return static_cast(ap->clone()); + const bunop* res = instances[p] = new bunop(op, child, min, max); + res->clone(); + return res; } - formula* - bunop::sugar_goto(formula* b, unsigned min, unsigned max) + const formula* + bunop::sugar_goto(const formula* b, unsigned min, unsigned max) { assert(b->is_boolean()); // b[->min..max] is implemented as ((!b)[*];b)[*min..max] - formula* s = bunop::instance(bunop::Star, - unop::instance(unop::Not, b->clone())); + const formula* s = + bunop::instance(bunop::Star, + unop::instance(unop::Not, b->clone())); return bunop::instance(bunop::Star, multop::instance(multop::Concat, s, b), min, max); } - formula* - bunop::sugar_equal(formula* b, unsigned min, unsigned max) + const formula* + bunop::sugar_equal(const formula* b, unsigned min, unsigned max) { assert(b->is_boolean()); // b[=0..] = 1[*] @@ -312,12 +301,13 @@ namespace spot } // b[=min..max] is implemented as ((!b)[*];b)[*min..max];(!b)[*] - formula* s = bunop::instance(bunop::Star, - unop::instance(unop::Not, b->clone())); - formula* t = bunop::instance(bunop::Star, - multop::instance(multop::Concat, - s->clone(), b), - min, max); + const formula* s = + bunop::instance(bunop::Star, + unop::instance(unop::Not, b->clone())); + const formula* t = + bunop::instance(bunop::Star, + multop::instance(multop::Concat, + s->clone(), b), min, max); return multop::instance(multop::Concat, t, s); } diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index e6c6d1620..e31e843ef 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -57,10 +57,10 @@ namespace spot /// These rewriting rules imply that it is not possible to build /// an LTL formula object that is SYNTACTICALLY equal to one of /// these left expressions. - static formula* instance(type op, - formula* child, - unsigned min = 0, - unsigned max = unbounded); + static const formula* instance(type op, + const formula* child, + unsigned min = 0, + unsigned max = unbounded); /// \brief Implement b[->i..j] using the Kleen star. /// @@ -71,9 +71,9 @@ namespace spot /// [->1..]. /// /// \pre \a child must be a Boolean formula. - static formula* sugar_goto(formula* child, - unsigned min = 1, - unsigned max = unbounded); + static const formula* sugar_goto(const formula* child, + unsigned min = 1, + unsigned max = unbounded); /// \brief Implement b[=i..j] using the Kleen star. /// @@ -81,17 +81,14 @@ namespace spot /// ((!b)[*];b)[*i..j];(!b)[*]. /// /// \pre \a child must be a Boolean formula. - static formula* sugar_equal(formula* child, - unsigned min = 0, - unsigned max = unbounded); + static const formula* sugar_equal(const formula* child, + unsigned min = 0, + unsigned max = unbounded); - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Get the sole operand of this operator. const formula* child() const; - /// Get the sole operand of this operator. - formula* child(); /// Minimum number of repetition. unsigned min() const; @@ -122,7 +119,7 @@ namespace spot /// A global instance is returned, and it should not be /// destroyed. Remember to clone it if you use it to build a /// formula. - static formula* one_star() + static const formula* one_star() { if (!one_star_) one_star_ = instance(Star, constant::true_instance()); @@ -131,20 +128,20 @@ namespace spot protected: typedef std::pair pairu; - typedef std::pair pairo; + typedef std::pair pairo; typedef std::pair pair; - typedef std::map map; + typedef std::map map; static map instances; - bunop(type op, formula* child, unsigned min, unsigned max); + bunop(type op, const formula* child, unsigned min, unsigned max); virtual ~bunop(); private: type op_; - formula* child_; + const formula* child_; unsigned min_; unsigned max_; - static formula* one_star_; + static const formula* one_star_; }; /// \brief Cast \a f into a bunop. @@ -152,12 +149,12 @@ namespace spot /// Cast \a f into a bunop iff it is a bunop instance. Return 0 /// otherwise. This is faster than \c dynamic_cast. inline - bunop* + const bunop* is_bunop(const formula* f) { if (f->kind() != formula::BUnOp) return 0; - return static_cast(const_cast(f)); + return static_cast(f); } /// \brief Cast \a f into a bunop if it has type \a op. @@ -165,22 +162,20 @@ namespace spot /// Cast \a f into a bunop iff it is a bunop instance with operator \a op. /// Returns 0 otherwise. inline - bunop* + const bunop* is_bunop(const formula* f, bunop::type op) { - if (f->kind() != formula::BUnOp) - return 0; - bunop* bo = static_cast(const_cast(f)); - if (bo->op() != op) - return 0; - return bo; + if (const bunop* bo = is_bunop(f)) + if (bo->op() == op) + return bo; + return 0; } /// \brief Cast \a f into a bunop if it is a Star. /// /// Return 0 otherwise. inline - bunop* + const bunop* is_Star(const formula* f) { return is_bunop(f, bunop::Star); @@ -190,10 +185,10 @@ namespace spot /// /// Return 0 otherwise. inline - bunop* + const bunop* is_KleenStar(const formula* f) { - if (bunop* b = is_Star(f)) + if (const bunop* b = is_Star(f)) if (b->min() == 0 && b->max() == bunop::unbounded) return b; return 0; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 8ce6a9307..4e316c313 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D�veloppement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), -// Universit� Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -106,13 +107,7 @@ namespace spot } void - constant::accept(visitor& v) - { - v.visit(this); - } - - void - constant::accept(const_visitor& v) const + constant::accept(visitor& v) const { v.visit(this); } diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 058777d01..62ad013b5 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -37,8 +37,7 @@ namespace spot { public: enum type { False, True, EmptyWord }; - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Return the value of the constant. type val() const; @@ -74,12 +73,12 @@ namespace spot /// Cast \a f into a constant iff it is a constant instance. /// Return 0 otherwise. This is faster than \c dynamic_cast. inline - constant* - is_constant(formula* f) + const constant* + is_constant(const formula* f) { if (f->kind() != formula::Constant) return 0; - return static_cast(f); + return static_cast(f); } } } diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 586a9cc16..94086c51f 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -32,11 +32,11 @@ namespace spot { size_t formula::max_count = 0; - formula* + const formula* formula::clone() const { - const_cast(this)->ref_(); - return const_cast(this); + this->ref_(); + return this; } formula::~formula() @@ -46,18 +46,18 @@ namespace spot void formula::destroy() const { - if (const_cast(this)->unref_()) + if (this->unref_()) delete this; } void - formula::ref_() + formula::ref_() const { // Not reference counted by default. } bool - formula::unref_() + formula::unref_() const { // Not reference counted by default. return false; diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 85ed57905..85f44e199 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -82,6 +82,7 @@ namespace spot BUnOp, AutomatOp }; + protected: formula(opkind k) : count_(max_count++), kind_(k) { // If the counter of formulae ever loops, we want to skip the @@ -92,16 +93,15 @@ namespace spot max_count = 3; } - /// Entry point for vspot::ltl::visitor instances. - virtual void accept(visitor& v) = 0; - /// Entry point for vspot::ltl::const_visitor instances. - virtual void accept(const_visitor& v) const = 0; + public: + /// Entry point for spot::ltl::visitor instances. + virtual void accept(visitor& v) const = 0; /// \brief clone this node /// /// This increments the reference counter of this node (if one is /// used). - formula* clone() const; + const formula* clone() const; /// \brief release this node /// /// This decrements the reference counter of this node (if one is @@ -293,10 +293,10 @@ namespace spot virtual ~formula(); /// \brief increment reference counter if any - virtual void ref_(); + virtual void ref_() const; /// \brief decrement reference counter if any, return true when /// the instance must be deleted (usually when the counter hits 0). - virtual bool unref_(); + virtual bool unref_() const; /// \brief The hash key of this formula. size_t count_; diff --git a/src/ltlast/formula_tree.cc b/src/ltlast/formula_tree.cc index ddda01692..cfdcfe528 100644 --- a/src/ltlast/formula_tree.cc +++ b/src/ltlast/formula_tree.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,8 +29,8 @@ namespace spot { namespace formula_tree { - formula* - instanciate(const node_ptr np, const std::vector& v) + const formula* + instanciate(const node_ptr np, const std::vector& v) { if (node_atomic* n = dynamic_cast(np.get())) return n->i == True ? constant::true_instance() : diff --git a/src/ltlast/formula_tree.hh b/src/ltlast/formula_tree.hh index c26002843..e2ff61a2b 100644 --- a/src/ltlast/formula_tree.hh +++ b/src/ltlast/formula_tree.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -76,7 +76,8 @@ namespace spot /// Instanciate the formula corresponding to the node with /// atomic propositions taken from \a v. - formula* instanciate(const node_ptr np, const std::vector& v); + const formula* instanciate(const node_ptr np, + const std::vector& v); /// Get the arity. size_t arity(const node_ptr np); diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 00b785dd3..52495d559 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -119,13 +119,7 @@ namespace spot } void - multop::accept(visitor& v) - { - v.visit(this); - } - - void - multop::accept(const_visitor& v) const + multop::accept(visitor& v) const { v.visit(this); } @@ -142,18 +136,12 @@ namespace spot return (*children_)[n]; } - formula* - multop::nth(unsigned n) - { - return (*children_)[n]; - } - - formula* + const formula* multop::all_but(unsigned n) const { unsigned s = size(); vec* v = new vec; - v->reserve(s-1); + v->reserve(s - 1); for (unsigned pos = 0; pos < n; ++pos) v->push_back(nth(pos)->clone()); for (unsigned pos = n + 1; pos < s; ++pos) @@ -192,35 +180,37 @@ namespace spot return 0; } - - void - gather_bool(multop::vec* v, multop::type op) + namespace { - // Gather all boolean terms. - multop::vec* b = new multop::vec; - multop::vec::iterator i = v->begin(); - while (i != v->end()) - { - if ((*i)->is_boolean()) - { - b->push_back(*i); - i = v->erase(i); - } - else - { - ++i; - } - } - // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) - // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) - // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2)) - if (!b->empty()) - v->push_back(multop::instance(op, b)); - else - delete b; + static void + gather_bool(multop::vec* v, multop::type op) + { + // Gather all boolean terms. + multop::vec* b = new multop::vec; + multop::vec::iterator i = v->begin(); + while (i != v->end()) + { + if ((*i)->is_boolean()) + { + b->push_back(*i); + i = v->erase(i); + } + else + { + ++i; + } + } + // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2)) + if (!b->empty()) + v->push_back(multop::instance(op, b)); + else + delete b; + } } multop::map multop::instances; @@ -230,7 +220,7 @@ namespace spot // operator). For instance if `+' designates the OR operator and // `0' is false (the neutral element for `+') , then `f+f+0' is // equivalent to `f'. - formula* + const formula* multop::instance(type op, vec* v) { // Inline children of same kind. @@ -252,9 +242,8 @@ namespace spot i = v->erase(i); continue; } - if ((*i)->kind() == MultOp) + if (const multop* p = is_multop(*i)) { - multop* p = static_cast(*i); if (p->op() == op) { unsigned ps = p->size(); @@ -286,11 +275,11 @@ namespace spot unsigned orig_size = v->size(); - formula* neutral; - formula* neutral2; - formula* abs; - formula* abs2; - formula* weak_abs; + const formula* neutral; + const formula* neutral2; + const formula* abs; + const formula* abs2; + const formula* weak_abs; switch (op) { case And: @@ -343,7 +332,7 @@ namespace spot // If FExps2... and FExps3 all accept [*0]. { vec::iterator i = v->begin(); - formula* os = bunop::one_star(); + const formula* os = bunop::one_star(); while (i != v->end()) { while (i != v->end() && !(*i)->accepts_eword()) @@ -433,7 +422,7 @@ namespace spot // std::unique(), because we must destroy() any formula we drop. // Also ignore neutral elements and handle absorbent elements. { - formula* last = 0; + const formula* last = 0; vec::iterator i = v->begin(); bool weak_abs_seen = false; while (i != v->end()) @@ -512,11 +501,11 @@ namespace spot while (i != v->end()) { vec::iterator fpos = i; - formula* f; + const formula* f; unsigned min; unsigned max; bool changed = false; - if (bunop* is = is_Star(*i)) + if (const bunop* is = is_Star(*i)) { f = is->child(); min = is->min(); @@ -531,10 +520,10 @@ namespace spot ++i; while (i != v->end()) { - formula* f2; + const formula* f2; unsigned min2; unsigned max2; - if (bunop* is = is_Star(*i)) + if (const bunop* is = is_Star(*i)) { f2 = is->child(); if (f2 != f) @@ -563,8 +552,8 @@ namespace spot } if (changed) { - formula* newfs = bunop::instance(bunop::Star, f->clone(), - min, max); + const formula* newfs = + bunop::instance(bunop::Star, f->clone(), min, max); (*fpos)->destroy(); *fpos = newfs; } @@ -586,7 +575,7 @@ namespace spot // arguments of a Fusion operator to // a list with a single formula that // accepts [*0]. - formula* res = (*v)[0]; + const formula* res = (*v)[0]; if (op != Fusion || orig_size == 1 || !res->accepts_eword()) { @@ -600,6 +589,8 @@ namespace spot // The hash key. pair p(op, v); + const multop* res; + // FIXME: Use lower_bound or hash_map. map::iterator i = instances.find(p); if (i != instances.end()) { @@ -607,19 +598,20 @@ namespace spot for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) (*vi)->destroy(); delete v; - return static_cast(i->second->clone()); + res = i->second; } - - // This is the first instance of this formula. - - // Record the instance in the map, - multop* ap = new multop(op, v); - instances[p] = ap; - return ap->clone(); + else + { + // This is the first instance of this formula. + // Record the instance in the map, + res = instances[p] = new multop(op, v); + } + res->clone(); + return res; } - formula* - multop::instance(type op, formula* first, formula* second) + const formula* + multop::instance(type op, const formula* first, const formula* second) { vec* v = new vec; v->push_back(first); diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 26ac02426..268de7a23 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -44,7 +44,7 @@ namespace spot enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; /// List of formulae. - typedef std::vector vec; + typedef std::vector vec; /// \brief Build a spot::ltl::multop with two children. /// @@ -57,7 +57,8 @@ namespace spot /// This functions can perform slight optimizations and /// may not return an ltl::multop object. See the other /// instance function for the list of rewritings. - static formula* instance(type op, formula* first, formula* second); + static const formula* + instance(type op, const formula* first, const formula* second); /// \brief Build a spot::ltl::multop with many children. /// @@ -120,10 +121,9 @@ namespace spot /// - Fusion(Exp) = Exp /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = /// Fusion(Exps1...,And(BoolExp1...BoolExpN),Exps2,Exps3...) - static formula* instance(type op, vec* v); + static const formula* instance(type op, vec* v); - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Get the number of children. unsigned size() const; @@ -131,17 +131,13 @@ namespace spot /// /// Starting with \a n = 0. const formula* nth(unsigned n) const; - /// \brief Get the nth child. - /// - /// Starting with \a n = 0. - formula* nth(unsigned n); /// \brief construct a formula without the nth child. /// /// If the formula \c f is a|b|c|d and d /// is child number 2, then calling f->all_but(2) will /// return a new formula a|b|d. - formula* all_but(unsigned n) const; + const formula* all_but(unsigned n) const; /// Get the type of this operator. type op() const; @@ -170,7 +166,7 @@ namespace spot return *p1.second < *p2.second; } }; - typedef std::map map; + typedef std::map map; static map instances; multop(type op, vec* v); @@ -187,12 +183,12 @@ namespace spot /// Cast \a f into a multop iff it is a multop instance. Return 0 /// otherwise. This is faster than \c dynamic_cast. inline - multop* - is_multop(formula* f) + const multop* + is_multop(const formula* f) { if (f->kind() != formula::MultOp) return 0; - return static_cast(f); + return static_cast(f); } /// \brief Cast \a f into a multop if it has type \a op. @@ -200,15 +196,13 @@ namespace spot /// Cast \a f into a multop iff it is a multop instance with operator \a op. /// Returns 0 otherwise. inline - multop* + const multop* is_multop(const formula* f, multop::type op) { - if (f->kind() != formula::MultOp) - return 0; - multop* mo = static_cast(const_cast(f)); - if (mo->op() != op) - return 0; - return mo; + if (const multop* mo = is_multop(f)) + if (mo->op() == op) + return mo; + return 0; } /// \brief Cast \a f into a multop if it has type \a op1 or \a op2. @@ -216,22 +210,20 @@ namespace spot /// Cast \a f into a multop iff it is a multop instance with /// operator \a op1 or \a op2. Returns 0 otherwise. inline - multop* + const multop* is_multop(const formula* f, multop::type op1, multop::type op2) { - if (f->kind() != formula::MultOp) - return 0; - multop* mo = static_cast(const_cast(f)); - if (mo->op() != op1 && mo->op() != op2) - return 0; - return mo; + if (const multop* mo = is_multop(f)) + if (mo->op() == op1 || mo->op() == op2) + return mo; + return 0; } /// \brief Cast \a f into a multop if it is an And. /// /// Return 0 otherwise. inline - multop* + const multop* is_And(const formula* f) { return is_multop(f, multop::And); @@ -241,7 +233,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_AndRat(const formula* f) { return is_multop(f, multop::AndRat); @@ -251,7 +243,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_AndNLM(const formula* f) { return is_multop(f, multop::AndNLM); @@ -261,7 +253,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_Or(const formula* f) { return is_multop(f, multop::Or); @@ -271,7 +263,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_OrRat(const formula* f) { return is_multop(f, multop::OrRat); @@ -281,7 +273,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_Concat(const formula* f) { return is_multop(f, multop::Concat); @@ -291,7 +283,7 @@ namespace spot /// /// Return 0 otherwise. inline - multop* + const multop* is_Fusion(const formula* f) { return is_multop(f, multop::Fusion); diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh index fccd25361..d722897ce 100644 --- a/src/ltlast/predecl.hh +++ b/src/ltlast/predecl.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -36,7 +36,6 @@ namespace spot namespace ltl { struct visitor; - struct const_visitor; class atomic_prop; class automatop; diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc index d6b3ef7c1..9a4dec1d9 100644 --- a/src/ltlast/refformula.cc +++ b/src/ltlast/refformula.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2010 Laboratoire de Recherche de Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement de // l'EPITA (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -38,20 +39,20 @@ namespace spot } void - ref_formula::ref_() + ref_formula::ref_() const { ++ref_counter_; } bool - ref_formula::unref_() + ref_formula::unref_() const { assert(ref_counter_ > 0); return !--ref_counter_; } unsigned - ref_formula::ref_count_() + ref_formula::ref_count_() const { return ref_counter_; } diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index 2a1566bfe..2db5d46c8 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2010 Laboratoire de Recherche de Developpement de -// l'EPITA (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement +// de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -40,12 +41,12 @@ namespace spot protected: virtual ~ref_formula(); ref_formula(opkind k); - void ref_(); - bool unref_(); + void ref_() const; + bool unref_() const; /// Number of references to this formula. - unsigned ref_count_(); + unsigned ref_count_() const; private: - unsigned ref_counter_; + mutable unsigned ref_counter_; }; } diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 05e3b1c58..ef07b72c6 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -32,7 +33,7 @@ namespace spot { namespace ltl { - unop::unop(type op, formula* child) + unop::unop(type op, const formula* child) : ref_formula(UnOp), op_(op), child_(child) { props = child->get_props(); @@ -161,13 +162,7 @@ namespace spot } void - unop::accept(visitor& v) - { - v.visit(this); - } - - void - unop::accept(const_visitor& v) const + unop::accept(visitor& v) const { v.visit(this); } @@ -178,12 +173,6 @@ namespace spot return child_; } - formula* - unop::child() - { - return child_; - } - unop::type unop::op() const { @@ -217,8 +206,8 @@ namespace spot unop::map unop::instances; - formula* - unop::instance(type op, formula* child) + const formula* + unop::instance(type op, const formula* child) { // Some trivial simplifications. @@ -227,10 +216,9 @@ namespace spot case F: case G: { - if (child->kind() == UnOp) + if (const unop* u = is_unop(child)) { // F and G are idempotent. - unop* u = static_cast(child); if (u->op() == op) return u; } @@ -258,29 +246,28 @@ namespace spot return bunop::instance(bunop::Star, constant::true_instance(), 1); - if (child->kind() == UnOp) + if (const unop* u = is_unop(child)) { - unop* u = static_cast(child); // "Not" is an involution. if (u->op() == op) { - formula* c = u->child()->clone(); + const formula* c = u->child()->clone(); u->destroy(); return c; } // !Closure(Exp) = NegClosure(Exp) if (u->op() == Closure) { - formula* c = unop::instance(NegClosure, - u->child()->clone()); + const formula* c = unop::instance(NegClosure, + u->child()->clone()); u->destroy(); return c; } // !NegClosure(Exp) = Closure(Exp) if (u->op() == NegClosure) { - formula* c = unop::instance(Closure, - u->child()->clone()); + const formula* c = unop::instance(Closure, + u->child()->clone()); u->destroy(); return c; } @@ -323,17 +310,21 @@ namespace spot break; } + const unop* res; pair p(op, child); map::iterator i = instances.find(p); if (i != instances.end()) { // This instance already exists. child->destroy(); - return static_cast(i->second->clone()); + res = i->second; } - unop* ap = new unop(op, child); - instances[p] = ap; - return static_cast(ap->clone()); + else + { + res = instances[p] = new unop(op, child); + } + res->clone(); + return res; } unsigned diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index e2d753380..e1534005b 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -87,15 +87,12 @@ namespace spot /// grammar. Spot cannot read it either. However some /// BDD-based algorithm may need to negate any constant, so we /// handle this one as well. - static formula* instance(type op, formula* child); + static const formula* instance(type op, const formula* child); - virtual void accept(visitor& v); - virtual void accept(const_visitor& v) const; + virtual void accept(visitor& v) const; /// Get the sole operand of this operator. const formula* child() const; - /// Get the sole operand of this operator. - formula* child(); /// Get the type of this operator. type op() const; @@ -112,16 +109,16 @@ namespace spot static std::ostream& dump_instances(std::ostream& os); protected: - typedef std::pair pair; - typedef std::map map; + typedef std::pair pair; + typedef std::map map; static map instances; - unop(type op, formula* child); + unop(type op, const formula* child); virtual ~unop(); private: type op_; - formula* child_; + const formula* child_; }; @@ -130,12 +127,12 @@ namespace spot /// Cast \a f into a unop iff it is a unop instance. Return 0 /// otherwise. This is faster than \c dynamic_cast. inline - unop* + const unop* is_unop(const formula* f) { if (f->kind() != formula::UnOp) return 0; - return static_cast(const_cast(f)); + return static_cast(f); } /// \brief Cast \a f into a unop if it has type \a op. @@ -143,22 +140,20 @@ namespace spot /// Cast \a f into a unop iff it is a unop instance with operator \a op. /// Returns 0 otherwise. inline - unop* + const unop* is_unop(const formula* f, unop::type op) { - if (f->kind() != formula::UnOp) - return 0; - unop* uo = static_cast(const_cast(f)); - if (uo->op() != op) - return 0; - return uo; + if (const unop* uo = is_unop(f)) + if (uo->op() == op) + return uo; + return 0; } /// \brief Cast \a f into a unop if it is a Not. /// /// Return 0 otherwise. inline - unop* + const unop* is_Not(const formula* f) { return is_unop(f, unop::Not); @@ -168,7 +163,7 @@ namespace spot /// /// Return 0 otherwise. inline - unop* + const unop* is_X(const formula* f) { return is_unop(f, unop::X); @@ -178,7 +173,7 @@ namespace spot /// /// Return 0 otherwise. inline - unop* + const unop* is_F(const formula* f) { return is_unop(f, unop::F); @@ -188,7 +183,7 @@ namespace spot /// /// Return 0 otherwise. inline - unop* + const unop* is_G(const formula* f) { return is_unop(f, unop::G); @@ -198,26 +193,24 @@ namespace spot /// /// Return 0 otherwise. inline - unop* + const unop* is_GF(const formula* f) { - unop* op = is_G(f); - if (!op) - return 0; - return is_F(op->child()); + if (const unop* op = is_G(f)) + return is_F(op->child()); + return 0; } /// \brief Cast \a f into a unop if has the form FG(...). /// /// Return 0 otherwise. inline - unop* + const unop* is_FG(const formula* f) { - unop* op = is_F(f); - if (!op) - return 0; - return is_G(op->child()); + if (const unop* op = is_F(f)) + return is_G(op->child()); + return 0; } } } diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index 66fcc89b3..4dd2b46dc 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -32,38 +32,15 @@ namespace spot { namespace ltl { - /// \brief Formula visitor that can modify the formula. + /// \brief Formula visitor /// \ingroup ltl_essential /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't + /// Implementing visitors is the prefered way + /// to traverse a formula, since it does not /// involve any cast. - /// - /// If you do not need to modify the visited formula, inherit from - /// spot::ltl:const_visitor instead. struct visitor { virtual ~visitor() {} - virtual void visit(atomic_prop* node) = 0; - virtual void visit(constant* node) = 0; - virtual void visit(binop* node) = 0; - virtual void visit(unop* node) = 0; - virtual void visit(multop* node) = 0; - virtual void visit(automatop* node) = 0; - virtual void visit(bunop* node) = 0; - }; - - /// \brief Formula visitor that cannot modify the formula. - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you want to modify the visited formula, inherit from - /// spot::ltl:visitor instead. - struct const_visitor - { - virtual ~const_visitor() {} virtual void visit(const atomic_prop* node) = 0; virtual void visit(const constant* node) = 0; virtual void visit(const binop* node) = 0; @@ -72,8 +49,6 @@ namespace spot virtual void visit(const automatop* node) = 0; virtual void visit(const bunop* node) = 0; }; - - } } diff --git a/src/ltlenv/declenv.cc b/src/ltlenv/declenv.cc index b5eb04c81..b10eb8cd3 100644 --- a/src/ltlenv/declenv.cc +++ b/src/ltlenv/declenv.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -47,7 +47,7 @@ namespace spot return true; } - ltl::formula* + const formula* declarative_environment::require(const std::string& prop_str) { prop_map::iterator i = props_.find(prop_str); diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh index c40aacaae..cebcea0df 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -49,12 +50,12 @@ namespace spot /// proposition was already declared. bool declare(const std::string& prop_str); - virtual ltl::formula* require(const std::string& prop_str); + virtual const formula* require(const std::string& prop_str); /// Get the name of the environment. virtual const std::string& name(); - typedef std::map prop_map; + typedef std::map prop_map; /// Get the map of atomic proposition known to this environment. const prop_map& get_prop_map() const; diff --git a/src/ltlenv/defaultenv.cc b/src/ltlenv/defaultenv.cc index a51e036b0..8cadd2401 100644 --- a/src/ltlenv/defaultenv.cc +++ b/src/ltlenv/defaultenv.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -31,7 +34,7 @@ namespace spot { } - formula* + const formula* 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 abd046270..51d70e612 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -40,7 +43,7 @@ namespace spot { public: virtual ~default_environment(); - virtual formula* require(const std::string& prop_str); + virtual const formula* require(const std::string& prop_str); virtual const std::string& name(); /// Get the sole instance of spot::ltl::default_environment. diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 51d24d041..02439ee93 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -53,7 +53,7 @@ namespace spot /// /// \return 0 iff \a prop_str is not part of the environment, /// or the associated spot::ltl::formula otherwise. - virtual formula* require(const std::string& prop_str) = 0; + virtual const formula* require(const std::string& prop_str) = 0; /// Get the name of the environment. virtual const std::string& name() = 0; diff --git a/src/ltlparse/ltlfile.cc b/src/ltlparse/ltlfile.cc index 20b944b4a..80ada6cc8 100644 --- a/src/ltlparse/ltlfile.cc +++ b/src/ltlparse/ltlfile.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,7 +46,7 @@ namespace spot } } - formula* ltl_file::next() + const formula* ltl_file::next() { if (!in.good()) return 0; @@ -60,7 +60,7 @@ namespace spot while (input == ""); spot::ltl::parse_error_list pel; - formula* f = parse(input, pel); + const formula* f = parse(input, pel); int ret = spot::ltl::format_parse_errors(std::cerr, input, pel); if (ret) exit(ret); diff --git a/src/ltlparse/ltlfile.hh b/src/ltlparse/ltlfile.hh index f143ef667..c20defd1f 100644 --- a/src/ltlparse/ltlfile.hh +++ b/src/ltlparse/ltlfile.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -37,7 +37,7 @@ namespace spot ltl_file(const std::string& filename); ltl_file(const char* filename); /// Return the next parsed LTL formula, and 0 at end of file. - formula* next(); + const formula* next(); private: std::ifstream in; }; diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 066acc716..fedff4f46 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -41,11 +41,11 @@ %parse-param {spot::ltl::parse_error_list &error_list} %parse-param {spot::ltl::environment &parse_environment} -%parse-param {spot::ltl::formula* &result} +%parse-param {const spot::ltl::formula* &result} %union { std::string* str; - spot::ltl::formula* ltl; + const spot::ltl::formula* ltl; unsigned num; minmax_t minmax; } @@ -671,13 +671,13 @@ namespace spot { namespace ltl { - formula* + const formula* parse(const std::string& ltl_string, parse_error_list& error_list, environment& env, bool debug) { - formula* result = 0; + const formula* result = 0; flex_set_buffer(ltl_string.c_str(), ltlyy::parser::token::START_LTL); ltlyy::parser parser(error_list, env, result); @@ -686,13 +686,13 @@ namespace spot return result; } - formula* + const formula* parse_sere(const std::string& sere_string, parse_error_list& error_list, environment& env, bool debug) { - formula* result = 0; + const formula* result = 0; flex_set_buffer(sere_string.c_str(), ltlyy::parser::token::START_SERE); ltlyy::parser parser(error_list, env, result); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 6b0d0f33d..d6f315e9d 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -67,10 +67,10 @@ namespace spot /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. - formula* parse(const std::string& ltl_string, - parse_error_list& error_list, - environment& env = default_environment::instance(), - bool debug = false); + const formula* parse(const std::string& ltl_string, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); /// \brief Build a formula from a string representing a SERE. /// \param sere_string The string to parse. @@ -87,10 +87,11 @@ namespace spot /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. - formula* parse_sere(const std::string& sere_string, - parse_error_list& error_list, - environment& env = default_environment::instance(), - bool debug = false); + const formula* parse_sere(const std::string& sere_string, + parse_error_list& error_list, + environment& env = + default_environment::instance(), + bool debug = false); /// \brief Format diagnostics produced by spot::ltl::parse /// or spot::ltl::ratexp diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc index 896b6e67d..15fa1c9ea 100644 --- a/src/ltltest/consterm.cc +++ b/src/ltltest/consterm.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Dévelopement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -38,7 +39,7 @@ main(int argc, char **argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1); + const spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index ba210e78d..89a74f541 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -57,13 +58,13 @@ main(int argc, char** argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); if (check_first && spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; spot::ltl::parse_error_list p2; - spot::ltl::formula* f2 = spot::ltl::parse(argv[2], p2); + const spot::ltl::formula* f2 = spot::ltl::parse(argv[2], p2); if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; @@ -72,7 +73,7 @@ main(int argc, char** argv) { #if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM) - spot::ltl::formula* tmp; + const spot::ltl::formula* tmp; #endif #ifdef LUNABBREV tmp = f1; @@ -99,7 +100,7 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier_options opt(true, true, true, false, false); spot::ltl::ltl_simplifier simp(opt); { - spot::ltl::formula* tmp; + const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); tmp->destroy(); @@ -111,7 +112,7 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier_options opt(false, false, false, true, false); spot::ltl::ltl_simplifier simp(opt); { - spot::ltl::formula* tmp; + const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); tmp->destroy(); @@ -123,7 +124,7 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier_options opt(false, false, false, true, true); spot::ltl::ltl_simplifier simp(opt); { - spot::ltl::formula* tmp; + const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); tmp->destroy(); diff --git a/src/ltltest/genltl.cc b/src/ltltest/genltl.cc index 1e2240e3f..9fad610f7 100644 --- a/src/ltltest/genltl.cc +++ b/src/ltltest/genltl.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -155,18 +156,18 @@ to_int(const char* s) // F(p_1 & F(p_2 & F(p_3 & ... F(p_n)))) -formula* E_n(std::string name, int n) +const formula* E_n(std::string name, int n) { if (n <= 0) return constant::true_instance(); - formula* result = 0; + const formula* result = 0; for (; n > 0; --n) { std::ostringstream p; p << name << n; - formula* f = env.require(p.str()); + const formula* f = env.require(p.str()); if (result) result = And_(f, result); else @@ -177,13 +178,13 @@ formula* E_n(std::string name, int n) } // p & X(p & X(p & ... X(p))) -formula* phi_n(std::string name, int n) +const formula* phi_n(std::string name, int n) { if (n <= 0) return constant::true_instance(); - formula* result = 0; - formula* p = env.require(name); + const formula* result = 0; + const formula* p = env.require(name); for (; n > 0; --n) { if (result) @@ -194,19 +195,19 @@ formula* phi_n(std::string name, int n) return result; } -formula* N_n(std::string name, int n) +const formula* N_n(std::string name, int n) { return unop::instance(unop::F, phi_n(name, n)); } // p & X(p) & XX(p) & XXX(p) & ... X^n(p) -formula* phi_prime_n(std::string name, int n) +const formula* phi_prime_n(std::string name, int n) { if (n <= 0) return constant::true_instance(); - formula* result = 0; - formula* p = env.require(name); + const formula* result = 0; + const formula* p = env.require(name); for (; n > 0; --n) { if (result) @@ -222,7 +223,7 @@ formula* phi_prime_n(std::string name, int n) return result; } -formula* N_prime_n(std::string name, int n) +const formula* N_prime_n(std::string name, int n) { return F_(phi_prime_n(name, n)); } @@ -230,12 +231,12 @@ formula* N_prime_n(std::string name, int n) // GF(p_1) & GF(p_2) & ... & GF(p_n) if conj == true // GF(p_1) | GF(p_2) | ... | GF(p_n) if conj == false -formula* GF_n(std::string name, int n, bool conj = true) +const formula* GF_n(std::string name, int n, bool conj = true) { if (n <= 0) return conj ? constant::true_instance() : constant::false_instance(); - formula* result = 0; + const formula* result = 0; multop::type op = conj ? multop::And : multop::Or; @@ -243,7 +244,7 @@ formula* GF_n(std::string name, int n, bool conj = true) { std::ostringstream p; p << name << i; - formula* f = G_(F_(env.require(p.str()))); + const formula* f = G_(F_(env.require(p.str()))); if (result) result = multop::instance(op, f, result); @@ -255,12 +256,12 @@ formula* GF_n(std::string name, int n, bool conj = true) // FG(p_1) | FG(p_2) | ... | FG(p_n) if conj == false // FG(p_1) & FG(p_2) & ... & FG(p_n) if conj == true -formula* FG_n(std::string name, int n, bool conj = false) +const formula* FG_n(std::string name, int n, bool conj = false) { if (n <= 0) return conj ? constant::true_instance() : constant::false_instance(); - formula* result = 0; + const formula* result = 0; multop::type op = conj ? multop::And : multop::Or; @@ -268,7 +269,7 @@ formula* FG_n(std::string name, int n, bool conj = false) { std::ostringstream p; p << name << i; - formula* f = F_(G_(env.require(p.str()))); + const formula* f = F_(G_(env.require(p.str()))); if (result) result = multop::instance(op, f, result); @@ -280,8 +281,9 @@ formula* FG_n(std::string name, int n, bool conj = false) // (((p1 OP p2) OP p3)...OP pn) if right_assoc == false // (p1 OP (p2 OP (p3 OP (... pn) if right_assoc == true -formula* bin_n(std::string name, int n, - binop::type op, bool right_assoc = false) +const formula* +bin_n(std::string name, int n, + binop::type op, bool right_assoc = false) { if (n <= 0) { @@ -289,13 +291,13 @@ formula* bin_n(std::string name, int n, exit(1); } - formula* result = 0; + const formula* result = 0; for (int i = 1; i <= n; ++i) { std::ostringstream p; p << name << (right_assoc ? (n + 1 - i) : i); - formula* f = env.require(p.str()); + const formula* f = env.require(p.str()); if (!result) result = f; else if (right_assoc) @@ -307,12 +309,12 @@ formula* bin_n(std::string name, int n, } // (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))" -formula* R_n(std::string name, int n) +const formula* R_n(std::string name, int n) { if (n <= 0) return constant::true_instance(); - formula* pi; + const formula* pi; { std::ostringstream p; @@ -320,18 +322,18 @@ formula* R_n(std::string name, int n) pi = env.require(p.str()); } - formula* result = 0; + const formula* result = 0; for (int i = 1; i <= n; ++i) { - formula* gf = G_(F_(pi)); + const formula* gf = G_(F_(pi)); std::ostringstream p; p << name << i + 1; pi = env.require(p.str()); - formula* fg = G_(F_(pi->clone())); + const formula* fg = G_(F_(pi->clone())); - formula* f = Or_(gf, fg); + const formula* f = Or_(gf, fg); if (result) result = And_(f, result); @@ -343,12 +345,12 @@ formula* R_n(std::string name, int n) } // (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))" -formula* Q_n(std::string name, int n) +const formula* Q_n(std::string name, int n) { if (n <= 0) return constant::true_instance(); - formula* pi; + const formula* pi; { std::ostringstream p; @@ -356,17 +358,17 @@ formula* Q_n(std::string name, int n) pi = env.require(p.str()); } - formula* result = 0; + const formula* result = 0; for (int i = 1; i <= n; ++i) { - formula* f = F_(pi); + const formula* f = F_(pi); std::ostringstream p; p << name << i + 1; pi = env.require(p.str()); - formula* g = G_(pi->clone()); + const formula* g = G_(pi->clone()); f = Or_(f, g); @@ -381,13 +383,13 @@ formula* Q_n(std::string name, int n) // OP(p1) | OP(p2) | ... | OP(Pn) if conj == false // OP(p1) & OP(p2) & ... & OP(Pn) if conj == true -formula* combunop_n(std::string name, int n, - unop::type op, bool conj = false) +const formula* combunop_n(std::string name, int n, + unop::type op, bool conj = false) { if (n <= 0) return conj ? constant::true_instance() : constant::false_instance(); - formula* result = 0; + const formula* result = 0; multop::type cop = conj ? multop::And : multop::Or; @@ -395,7 +397,7 @@ formula* combunop_n(std::string name, int n, { std::ostringstream p; p << name << i; - formula* f = unop::instance(op, env.require(p.str())); + const formula* f = unop::instance(op, env.require(p.str())); if (result) result = multop::instance(cop, f, result); @@ -406,20 +408,21 @@ formula* combunop_n(std::string name, int n, } // !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r))) -// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav] -formula* fair_response(std::string p, std::string q, std::string r, int n) +// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav] +const formula* +fair_response(std::string p, std::string q, std::string r, int n) { - formula* fair = GF_n(p, n); - formula* resp = G_(Implies_(env.require(q), F_(env.require(r)))); + const formula* fair = GF_n(p, n); + const formula* resp = G_(Implies_(env.require(q), F_(env.require(r)))); return Not_(Implies_(fair, resp)); } // Builds X(X(...X(p))) with n occurrences of X. -formula* X_n(formula* p, int n) +const formula* X_n(const formula* p, int n) { assert(n >= 0); - formula* res = p; + const formula* res = p; while (n--) res = X_(res); return res; @@ -427,13 +430,13 @@ formula* X_n(formula* p, int n) // Based on LTLcounter.pl from Kristin Rozier. // http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/ - -formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) +const formula* +ltl_counter(std::string bit, std::string marker, int n, bool linear) { - formula* b = env.require(bit); - formula* neg_b = Not_(b); - formula* m = env.require(marker); - formula* neg_m = Not_(m); // to destroy + const formula* b = env.require(bit); + const formula* neg_b = Not_(b); + const formula* m = env.require(marker); + const formula* neg_m = Not_(m); // to destroy multop::vec* res = new multop::vec(4); @@ -453,7 +456,7 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) else { // G(m -> X(!m & X(!m X(m)))) [if n = 3] - formula* p = m->clone(); + const formula* p = m->clone(); for (int i = n - 1; i > 0; --i) p = And_(neg_m->clone(), X_(p)); (*res)[0] = And_(m->clone(), @@ -472,7 +475,7 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) else { // !b & X(!b & X(!b)) [if n = 3] - formula* p = neg_b->clone(); + const formula* p = neg_b->clone(); for (int i = n - 1; i > 0; --i) p = And_(neg_b->clone(), X_(p)); (*res)[1] = p; @@ -482,8 +485,8 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) // If the least significant bit is 0, it will be 1 at the next time, // and other bits stay the same. - formula* Xnm1_b = X_n(b->clone(), n - 1); - formula* Xn_b = X_(Xnm1_b); // to destroy + const formula* Xnm1_b = X_n(b->clone(), n - 1); + const formula* Xn_b = X_(Xnm1_b); // to destroy (*res)[2] = G_(Implies_(And_(m->clone(), neg_b->clone()), AndX_(Xnm1_b->clone(), U_(And_(Not_(m->clone()), @@ -493,8 +496,8 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) // From the least significant bit to the first 0, all the bits // are flipped on the next value. Remaining bits are identical. - formula* Xnm1_negb = X_n(neg_b, n - 1); - formula* Xn_negb = X_(Xnm1_negb); // to destroy + const formula* Xnm1_negb = X_n(neg_b, n - 1); + const formula* Xn_negb = X_(Xnm1_negb); // to destroy (*res)[3] = G_(Implies_(And_(m->clone(), b->clone()), AndX_(Xnm1_negb->clone(), @@ -515,15 +518,15 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) return multop::instance(multop::And, res); } -formula* ltl_counter_carry(std::string bit, std::string marker, - std::string carry, int n, bool linear) +const formula* ltl_counter_carry(std::string bit, std::string marker, + std::string carry, int n, bool linear) { - formula* b = env.require(bit); - formula* neg_b = Not_(b); - formula* m = env.require(marker); - formula* neg_m = Not_(m); // to destroy - formula* c = env.require(carry); - formula* neg_c = Not_(c); // to destroy + const formula* b = env.require(bit); + const formula* neg_b = Not_(b); + const formula* m = env.require(marker); + const formula* neg_m = Not_(m); // to destroy + const formula* c = env.require(carry); + const formula* neg_c = Not_(c); // to destroy multop::vec* res = new multop::vec(6); @@ -543,7 +546,7 @@ formula* ltl_counter_carry(std::string bit, std::string marker, else { // G(m -> X(!m & X(!m X(m)))) [if n = 3] - formula* p = m->clone(); + const formula* p = m->clone(); for (int i = n - 1; i > 0; --i) p = And_(neg_m->clone(), X_(p)); (*res)[0] = And_(m->clone(), @@ -562,14 +565,14 @@ formula* ltl_counter_carry(std::string bit, std::string marker, else { // !b & X(!b & X(!b)) [if n = 3] - formula* p = neg_b->clone(); + const formula* p = neg_b->clone(); for (int i = n - 1; i > 0; --i) p = And_(neg_b->clone(), X_(p)); (*res)[1] = p; } - formula* Xn_b = X_n(b->clone(), n); // to destroy - formula* Xn_negb = X_n(neg_b, n); // to destroy + const formula* Xn_b = X_n(b->clone(), n); // to destroy + const formula* Xn_negb = X_n(neg_b, n); // to destroy // If m is 1 and b is 0 then c is 0 and n steps later b is 1. (*res)[2] = G_(Implies_(And_(m->clone(), neg_b->clone()), @@ -642,7 +645,7 @@ main(int argc, char** argv) int f = to_int(argv[1]); int n = to_int(argv[2]); - formula* res = 0; + const formula* res = 0; switch (f) { diff --git a/src/ltltest/kind.cc b/src/ltltest/kind.cc index 434765624..cb14ecb93 100644 --- a/src/ltltest/kind.cc +++ b/src/ltltest/kind.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developement de +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,7 +39,7 @@ main(int argc, char **argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; diff --git a/src/ltltest/length.cc b/src/ltltest/length.cc index 27ec134b5..aeb080ae5 100644 --- a/src/ltltest/length.cc +++ b/src/ltltest/length.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2012 Laboratoire de Recherche et Developement de // l'Epita (LRDE). // @@ -47,7 +48,7 @@ main(int argc, char **argv) } spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 0321194db..2461532fc 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -185,7 +185,7 @@ main(int argc, char** argv) } else { - ap->insert(static_cast + ap->insert(static_cast (env.require(argv[argn]))); } } @@ -310,14 +310,14 @@ main(int argc, char** argv) while (max_tries_u--) { spot::srand(opt_s++); - spot::ltl::formula* f = 0; + const spot::ltl::formula* f = 0; int max_tries_r = 1000; while (max_tries_r--) { f = rf->generate(opt_f); if (opt_r) { - spot::ltl::formula* g = simp.simplify(f); + const spot::ltl::formula* g = simp.simplify(f); f->destroy(); if (spot::ltl::length(g) < opt_r) { diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index 2a868476b..a4c07a4e1 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -76,8 +77,8 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], - pel, env, debug); + const spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], + pel, env, debug); exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 16120c121..c454a374b 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -144,8 +144,8 @@ main(int argc, char** argv) o.reduce_size_strictly = true; spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o); - spot::ltl::formula* f1 = 0; - spot::ltl::formula* f2 = 0; + const spot::ltl::formula* f1 = 0; + const spot::ltl::formula* f2 = 0; std::ifstream* fin = 0; @@ -201,7 +201,7 @@ main(int argc, char** argv) } { - spot::ltl::formula* ftmp1; + const spot::ltl::formula* ftmp1; ftmp1 = f1; f1 = simp_size->negative_normal_form(f1, false); @@ -211,7 +211,7 @@ main(int argc, char** argv) std::string f1s_before = spot::ltl::to_string(f1); std::string f1l; - spot::ltl::formula* input_f = f1; + const spot::ltl::formula* input_f = f1; f1 = simp_size->simplify(input_f); if (!simp_size->are_equivalent(input_f, f1)) { @@ -222,7 +222,7 @@ main(int argc, char** argv) } else { - spot::ltl::formula* maybe_larger = simp->simplify(input_f); + const spot::ltl::formula* maybe_larger = simp->simplify(input_f); f1l = spot::ltl::to_string(maybe_larger); if (!simp->are_equivalent(input_f, maybe_larger)) { diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index e851ca08c..cebcca1d0 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -49,19 +50,19 @@ main(int argc, char** argv) int opt = atoi(argv[1]); spot::ltl::parse_error_list p1; - spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1); + const spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) return 2; spot::ltl::parse_error_list p2; - spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2); + const spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2); if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2)) return 2; - spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1); - spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2); + const spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1); + const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2); std::string f1s = spot::ltl::to_string(f1); std::string f2s = spot::ltl::to_string(f2); diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 6edd4ff63..f04306a6f 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -42,7 +43,7 @@ main(int argc, char **argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; @@ -53,7 +54,7 @@ main(int argc, char **argv) std::string f1s = spot::ltl::to_string(f1); std::cout << f1s << std::endl; - spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); + const spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); if (spot::ltl::format_parse_errors(std::cerr, f1s, p1)) return 2; diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index 65a886882..1c4636f71 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -40,7 +43,7 @@ namespace spot { } - virtual void doit(spot::ltl::atomic_prop* ap) + virtual void doit(const spot::ltl::atomic_prop* ap) { sap->insert(ap); } @@ -56,7 +59,7 @@ namespace spot if (!s) s = new atomic_prop_set; atomic_prop_collector v(s); - const_cast(f)->accept(v); + f->accept(v); return s; } diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 069afa0e9..3cf12f337 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -33,7 +36,8 @@ namespace spot /// @{ /// Set of atomic propositions. - typedef std::set atomic_prop_set; + typedef std::set atomic_prop_set; /// \brief Return the set of atomic propositions occurring in a formula. /// diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 94b3164af..c2baf29cc 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -36,46 +36,46 @@ namespace spot { } - formula* + const formula* clone_visitor::result() const { return result_; } void - clone_visitor::visit(atomic_prop* ap) + clone_visitor::visit(const atomic_prop* ap) { result_ = ap->clone(); } void - clone_visitor::visit(constant* c) + clone_visitor::visit(const constant* c) { result_ = c->clone(); } void - clone_visitor::visit(bunop* bo) + clone_visitor::visit(const bunop* bo) { result_ = bunop::instance(bo->op(), recurse(bo->child()), bo->min(), bo->max()); } void - clone_visitor::visit(unop* uo) + clone_visitor::visit(const unop* uo) { result_ = unop::instance(uo->op(), recurse(uo->child())); } void - clone_visitor::visit(binop* bo) + clone_visitor::visit(const binop* bo) { result_ = binop::instance(bo->op(), recurse(bo->first()), recurse(bo->second())); } void - clone_visitor::visit(automatop* ao) + clone_visitor::visit(const automatop* ao) { automatop::vec* res = new automatop::vec; for (unsigned i = 0; i < ao->size(); ++i) @@ -84,7 +84,7 @@ namespace spot } void - clone_visitor::visit(multop* mo) + clone_visitor::visit(const multop* mo) { multop::vec* res = new multop::vec; unsigned mos = mo->size(); @@ -93,17 +93,16 @@ namespace spot result_ = multop::instance(mo->op(), res); } - formula* - clone_visitor::recurse(formula* f) + const formula* + clone_visitor::recurse(const formula* f) { return f->clone(); } - formula* + const formula* clone(const formula* f) { - formula* res = const_cast(f)->clone(); - return res; + return f->clone(); } } } diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 6b4430ecb..08126277d 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -44,32 +45,32 @@ namespace spot clone_visitor(); virtual ~clone_visitor(); - formula* result() const; + const formula* result() const; - void visit(atomic_prop* ap); - void visit(unop* uo); - void visit(binop* bo); - void visit(automatop* mo); - void visit(multop* mo); - void visit(constant* c); - void visit(bunop* c); + void visit(const atomic_prop* ap); + void visit(const unop* uo); + void visit(const binop* bo); + void visit(const automatop* mo); + void visit(const multop* mo); + void visit(const constant* c); + void visit(const bunop* c); - virtual formula* recurse(formula* f); + virtual const formula* recurse(const formula* f); protected: - formula* result_; + const formula* result_; }; #if __GNUC__ /// \brief Clone a formula. /// \ingroup ltl_essential /// \deprecated Use f->clone() instead. - formula* clone(const formula* f) __attribute__ ((deprecated)); + const formula* clone(const formula* f) __attribute__ ((deprecated)); #else /// \brief Clone a formula. /// \ingroup ltl_essential /// \deprecated Use f->clone() instead. - formula* clone(const formula* f); + const formula* clone(const formula* f); #endif } } diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index cd05ed706..aa12fc8b2 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -87,7 +88,8 @@ namespace spot // Check whether L(l) is a subset of L(g). bool - language_containment_checker::contained(const formula* l, const formula* g) + language_containment_checker::contained(const formula* l, + const formula* g) { if (l == g) return true; @@ -153,7 +155,7 @@ namespace spot } - formula* + const formula* reduce_tau03(const formula* f, bool stronger) { if (!f->is_psl_formula()) diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index 11ad987b3..78833e131 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -88,10 +88,10 @@ namespace spot /// title = {On Translating Linear Temporal Logic into Alternating and /// Nondeterministic Automata}, /// institution = {Helsinki University of Technology, Laboratory for - /// Theoretical Computer Science}, + /// Theoretical Computer Science}, /// address = {Espoo, Finland}, /// month = dec, - /// number = {A83}, + /// number = {A83}, /// pages = {132}, /// type = {Research Report}, /// year = {2003}, @@ -106,10 +106,11 @@ namespace spot /// /// \deprecated Use spot::ltl::ltl_simplifier instead. #if __GNUC__ - formula* reduce_tau03(const formula* f, - bool stronger = true) __attribute__ ((deprecated)); + const formula* reduce_tau03(const formula* f, + bool stronger = true) + __attribute__ ((deprecated)); #else - formula* reduce_tau03(const formula* f, bool stronger = true); + const formula* reduce_tau03(const formula* f, bool stronger = true); #endif } } diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index d32de555e..9c0edbd23 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -35,7 +35,7 @@ namespace spot { namespace { - class dotty_visitor: public const_visitor + class dotty_visitor: public visitor { public: typedef Sgi::hash_map > map; diff --git a/src/ltlvisit/length.cc b/src/ltlvisit/length.cc index 6d83f7a3d..476bf6d13 100644 --- a/src/ltlvisit/length.cc +++ b/src/ltlvisit/length.cc @@ -47,7 +47,7 @@ namespace spot } virtual void - visit(multop* mo) + visit(const multop* mo) { unsigned s = mo->size(); for (unsigned i = 0; i < s; ++i) @@ -58,7 +58,7 @@ namespace spot } virtual void - doit_default(formula*) + doit_default(const formula*) { ++result_; } @@ -71,7 +71,7 @@ namespace spot { virtual void - visit(unop* uo) + visit(const unop* uo) { ++result_; // Boolean formula have length one. @@ -80,7 +80,7 @@ namespace spot } virtual void - visit(multop* mo) + visit(const multop* mo) { // Boolean formula have length one. if (mo->is_boolean()) @@ -104,7 +104,7 @@ namespace spot length(const formula* f) { length_visitor v; - const_cast(f)->accept(v); + f->accept(v); return v.result(); } @@ -112,7 +112,7 @@ namespace spot length_boolone(const formula* f) { length_boolone_visitor v; - const_cast(f)->accept(v); + f->accept(v); return v.result(); } diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 7bc002b90..4756f37b0 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -39,10 +40,10 @@ namespace spot } void - unabbreviate_logic_visitor::visit(binop* bo) + unabbreviate_logic_visitor::visit(const binop* bo) { - formula* f1 = recurse(bo->first()); - formula* f2 = recurse(bo->second()); + const formula* f1 = recurse(bo->first()); + const formula* f2 = recurse(bo->second()); binop::type op = bo->op(); switch (op) @@ -50,11 +51,12 @@ namespace spot /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: { - formula* a = multop::instance(multop::And, f1->clone(), - unop::instance(unop::Not, - f2->clone())); - formula* b = multop::instance(multop::And, f2, - unop::instance(unop::Not, f1)); + const formula* a = + multop::instance(multop::And, f1->clone(), + unop::instance(unop::Not, f2->clone())); + const formula* b = + multop::instance(multop::And, f2, + unop::instance(unop::Not, f1)); result_ = multop::instance(multop::Or, a, b); return; } @@ -66,8 +68,8 @@ namespace spot /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ case binop::Equiv: { - formula* f1c = f1->clone(); - formula* f2c = f2->clone(); + const formula* f1c = f1->clone(); + const formula* f2c = f2->clone(); result_ = multop::instance(multop::Or, @@ -97,19 +99,19 @@ namespace spot assert(0); } - formula* - unabbreviate_logic_visitor::recurse(formula* f) + const formula* + unabbreviate_logic_visitor::recurse(const formula* f) { return unabbreviate_logic(f); } - formula* + const formula* unabbreviate_logic(const formula* f) { if (f->is_sugar_free_boolean()) return f->clone(); unabbreviate_logic_visitor v; - const_cast(f)->accept(v); + f->accept(v); return v.result(); } } diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 3d192863f..e5fc001e2 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -48,9 +51,9 @@ namespace spot virtual ~unabbreviate_logic_visitor(); using super::visit; - void visit(binop* bo); + void visit(const binop* bo); - virtual formula* recurse(formula* f); + virtual const formula* recurse(const formula* f); }; /// \brief Clone and rewrite a formula to remove most of the abbreviated @@ -60,7 +63,7 @@ namespace spot /// This will rewrite binary operators such as binop::Implies, /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, /// and multop::And. - formula* unabbreviate_logic(const formula* f); + const formula* unabbreviate_logic(const formula* f); } } diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 1f5479a95..eebce4ba7 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -33,7 +33,7 @@ namespace spot { class simplify_mark_visitor : public visitor { - formula* result_; + const formula* result_; mark_tools* tools_; public: @@ -46,44 +46,44 @@ namespace spot { } - formula* + const formula* result() { return result_; } void - visit(atomic_prop* ao) + visit(const atomic_prop* ao) { result_ = ao->clone(); } void - visit(constant* c) + visit(const constant* c) { result_ = c->clone(); } void - visit(bunop* bo) + visit(const bunop* bo) { result_ = bo->clone(); } void - visit(unop* uo) + visit(const unop* uo) { result_ = uo->clone(); } void - visit(automatop* ao) + visit(const automatop* ao) { result_ = ao->clone(); } void - visit(multop* mo) + visit(const multop* mo) { unsigned mos = mo->size(); multop::vec* res = new multop::vec; @@ -101,12 +101,13 @@ namespace spot break; case multop::And: { - typedef std::set > pset; + typedef std::set > pset; pset Epairs, EMpairs; for (unsigned i = 0; i < mos; ++i) { - formula* f = mo->nth(i); + const formula* f = mo->nth(i); if (f->kind() != formula::BinOp) { @@ -114,7 +115,7 @@ namespace spot } else { - binop* bo = static_cast(f); + const binop* bo = static_cast(f); switch (bo->op()) { case binop::Xor: @@ -157,13 +158,13 @@ namespace spot } void - visit(binop* bo) + visit(const binop* bo) { result_ = bo->clone(); } - formula* - recurse(formula* f) + const formula* + recurse(const formula* f) { return tools_->simplify_mark(f); } @@ -172,7 +173,7 @@ namespace spot class mark_visitor : public visitor { - formula* result_; + const formula* result_; mark_tools* tools_; public: @@ -184,44 +185,44 @@ namespace spot { } - formula* + const formula* result() { return result_; } void - visit(atomic_prop* ap) + visit(const atomic_prop* ap) { result_ = ap->clone(); } void - visit(constant* c) + visit(const constant* c) { result_ = c->clone(); } void - visit(bunop* bo) + visit(const bunop* bo) { result_ = bo->clone(); } void - visit(unop* uo) + visit(const unop* uo) { result_ = uo->clone(); } void - visit(automatop* ao) + visit(const automatop* ao) { result_ = ao->clone(); } void - visit(multop* mo) + visit(const multop* mo) { multop::vec* res = new multop::vec; unsigned mos = mo->size(); @@ -231,7 +232,7 @@ namespace spot } void - visit(binop* bo) + visit(const binop* bo) { switch (bo->op()) { @@ -249,8 +250,8 @@ namespace spot case binop::EConcatMarked: case binop::EConcat: { - formula* f1 = bo->first()->clone(); - formula* f2 = recurse(bo->second()); + const formula* f1 = bo->first()->clone(); + const formula* f2 = recurse(bo->second()); result_ = binop::instance(binop::EConcatMarked, f1, f2); return; } @@ -259,8 +260,8 @@ namespace spot assert(0); } - formula* - recurse(formula* f) + const formula* + recurse(const formula* f) { return tools_->mark_concat_ops(f); } @@ -301,21 +302,21 @@ namespace spot } } - formula* + const formula* mark_tools::mark_concat_ops(const formula* f) { f2f_map::iterator i = markops_.find(f); if (i != markops_.end()) return i->second->clone(); - const_cast(f)->accept(*markvisitor_); + f->accept(*markvisitor_); - formula* r = down_cast(markvisitor_)->result(); + const formula* r = down_cast(markvisitor_)->result(); markops_[f->clone()] = r->clone(); return r; } - formula* + const formula* mark_tools::simplify_mark(const formula* f) { if (!f->is_marked()) @@ -325,9 +326,10 @@ namespace spot if (i != simpmark_.end()) return i->second->clone(); - const_cast(f)->accept(*simpvisitor_); + f->accept(*simpvisitor_); - formula* r = down_cast(simpvisitor_)->result(); + const formula* r = + down_cast(simpvisitor_)->result(); simpmark_[f->clone()] = r->clone(); return r; } diff --git a/src/ltlvisit/mark.hh b/src/ltlvisit/mark.hh index fa5e6c9e1..143a269ff 100644 --- a/src/ltlvisit/mark.hh +++ b/src/ltlvisit/mark.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -36,9 +36,9 @@ namespace spot /// \ingroup ltl_rewriting /// /// \param f The formula to rewrite. - formula* mark_concat_ops(const formula* f); + const formula* mark_concat_ops(const formula* f); - formula* simplify_mark(const formula* f); + const formula* simplify_mark(const formula* f); mark_tools(); ~mark_tools(); diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 9ab588de9..65120485a 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -27,7 +28,7 @@ namespace spot { namespace ltl { - formula* + const formula* negative_normal_form(const formula* f, bool negated) { if (!negated && f->is_in_nenoform()) diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index f26c25153..bba5998f6 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -45,8 +46,8 @@ namespace spot /// or spot::ltl::unabbreviate_ltl first. (Calling these functions /// after spot::ltl::negative_normal_form would likely produce a /// formula which is not in negative normal form.) - - formula* negative_normal_form(const formula* f, bool negated = false); + const formula* + negative_normal_form(const formula* f, bool negated = false); } } diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index f10c32225..91507d307 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -37,20 +38,20 @@ namespace spot } void - postfix_visitor::visit(atomic_prop* ap) + postfix_visitor::visit(const atomic_prop* ap) { doit(ap); } void - postfix_visitor::visit(unop* uo) + postfix_visitor::visit(const unop* uo) { uo->child()->accept(*this); doit(uo); } void - postfix_visitor::visit(binop* bo) + postfix_visitor::visit(const binop* bo) { bo->first()->accept(*this); bo->second()->accept(*this); @@ -58,7 +59,7 @@ namespace spot } void - postfix_visitor::visit(automatop* ao) + postfix_visitor::visit(const automatop* ao) { unsigned s = ao->size(); for (unsigned i = 0; i < s; ++i) @@ -67,7 +68,7 @@ namespace spot } void - postfix_visitor::visit(multop* mo) + postfix_visitor::visit(const multop* mo) { unsigned s = mo->size(); for (unsigned i = 0; i < s; ++i) @@ -76,62 +77,62 @@ namespace spot } void - postfix_visitor::visit(bunop* so) + postfix_visitor::visit(const bunop* so) { so->child()->accept(*this); doit(so); } void - postfix_visitor::visit(constant* c) + postfix_visitor::visit(const constant* c) { doit(c); } void - postfix_visitor::doit(atomic_prop* ap) + postfix_visitor::doit(const atomic_prop* ap) { doit_default(ap); } void - postfix_visitor::doit(unop* uo) + postfix_visitor::doit(const unop* uo) { doit_default(uo); } void - postfix_visitor::doit(binop* bo) + postfix_visitor::doit(const binop* bo) { doit_default(bo); } void - postfix_visitor::doit(multop* mo) + postfix_visitor::doit(const multop* mo) { doit_default(mo); } void - postfix_visitor::doit(automatop* ao) + postfix_visitor::doit(const automatop* ao) { doit_default(ao); } void - postfix_visitor::doit(bunop* so) + postfix_visitor::doit(const bunop* so) { doit_default(so); } void - postfix_visitor::doit(constant* c) + postfix_visitor::doit(const constant* c) { doit_default(c); } void - postfix_visitor::doit_default(formula* f) + postfix_visitor::doit_default(const formula* f) { (void)f; // Dummy implementation that does nothing. diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index b360c1a2c..642a61f5e 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -43,22 +43,22 @@ namespace spot postfix_visitor(); virtual ~postfix_visitor(); - void visit(atomic_prop* ap); - void visit(unop* uo); - void visit(binop* bo); - void visit(multop* mo); - void visit(automatop* c); - void visit(constant* c); - void visit(bunop* c); + void visit(const atomic_prop* ap); + void visit(const unop* uo); + void visit(const binop* bo); + void visit(const multop* mo); + void visit(const automatop* c); + void visit(const constant* c); + void visit(const bunop* c); - virtual void doit(atomic_prop* ap); - virtual void doit(unop* uo); - virtual void doit(binop* bo); - virtual void doit(multop* mo); - virtual void doit(automatop* mo); - virtual void doit(constant* c); - virtual void doit(bunop* c); - virtual void doit_default(formula* f); + virtual void doit(const atomic_prop* ap); + virtual void doit(const unop* uo); + virtual void doit(const binop* bo); + virtual void doit(const multop* mo); + virtual void doit(const automatop* mo); + virtual void doit(const constant* c); + virtual void doit(const bunop* c); + virtual void doit_default(const formula* f); }; } } diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 37e20514c..367d62d8d 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,7 +1,8 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -35,7 +36,7 @@ namespace spot { namespace { - static formula* + static const formula* ap_builder(const random_formula* rl, int n) { assert(n == 1); @@ -45,7 +46,7 @@ namespace spot return (*i)->clone(); } - static formula* + static const formula* true_builder(const random_formula*, int n) { assert(n == 1); @@ -53,7 +54,7 @@ namespace spot return constant::true_instance(); } - static formula* + static const formula* boolform_builder(const random_formula* rl, int n) { assert(n >= 1); @@ -61,7 +62,7 @@ namespace spot return rs->rb.generate(n); } - static formula* + static const formula* false_builder(const random_formula*, int n) { assert(n == 1); @@ -69,7 +70,7 @@ namespace spot return constant::false_instance(); } - static formula* + static const formula* eword_builder(const random_formula*, int n) { assert(n == 1); @@ -78,14 +79,14 @@ namespace spot } template - static formula* + static const formula* unop_builder(const random_formula* rl, int n) { assert(n >= 2); return unop::instance(Op, rl->generate(n - 1)); } - static formula* + static const formula* closure_builder(const random_formula* rl, int n) { assert(n >= 2); @@ -94,7 +95,7 @@ namespace spot } template - static formula* + static const formula* binop_builder(const random_formula* rl, int n) { assert(n >= 3); @@ -104,7 +105,7 @@ namespace spot } template - static formula* + static const formula* binop_SERELTL_builder(const random_formula* rl, int n) { assert(n >= 3); @@ -115,7 +116,7 @@ namespace spot } template - static formula* + static const formula* bunop_unbounded_builder(const random_formula* rl, int n) { assert(n >= 2); @@ -123,7 +124,7 @@ namespace spot } template - static formula* + static const formula* bunop_bounded_builder(const random_formula* rl, int n) { assert(n >= 2); @@ -133,7 +134,7 @@ namespace spot } template - static formula* + static const formula* bunop_bool_bounded_builder(const random_formula* rl, int n) { assert(n >= 2); @@ -145,7 +146,7 @@ namespace spot template - static formula* + static const formula* multop_builder(const random_formula* rl, int n) { assert(n >= 3); @@ -197,7 +198,7 @@ namespace spot assert(total_2_and_more_ != 0.0); } - formula* + const formula* random_formula::generate(int n) const { assert(n > 0); diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index f153b3e4d..f1fb21036 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -61,7 +62,7 @@ namespace spot /// n, because some simple simplifications are performed by the /// AST. (For instance the formula a | a is /// automatically reduced to a by spot::ltl::multop.) - formula* generate(int n) const; + const formula* generate(int n) const; /// \brief Print the priorities of each operator, constants, /// and atomic propositions. @@ -84,7 +85,7 @@ namespace spot const char* name; int min_n; double proba; - typedef formula* (*builder)(const random_formula* rl, int n); + typedef const formula* (*builder)(const random_formula* rl, int n); builder build; void setup(const char* name, int min_n, builder build); }; diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 488bc1e26..d081e033c 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -30,7 +30,7 @@ namespace spot { namespace ltl { - formula* + const formula* reduce(const formula* f, int opt) { ltl_simplifier_options o; @@ -40,7 +40,7 @@ namespace spot o.containment_checks = opt & Reduce_Containment_Checks; o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger; ltl_simplifier simplifier(o); - return const_cast(simplifier.simplify(f)); + return simplifier.simplify(f); } bool diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index 628603be9..3c8cd29a6 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -70,10 +71,10 @@ namespace spot /// /// \deprecated Use spot::ltl::ltl_simplifier instead. #if __GNUC__ - formula* + const formula* reduce(const formula* f, int opt = Reduce_All) __attribute__ ((deprecated)); #else - formula* reduce(const formula* f, int opt = Reduce_All); + const formula* reduce(const formula* f, int opt = Reduce_All); #endif /// @} diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index 498bae629..e9c594c6b 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -40,10 +41,10 @@ namespace spot } void - simplify_f_g_visitor::visit(binop* bo) + simplify_f_g_visitor::visit(const binop* bo) { - formula* f1 = recurse(bo->first()); - formula* f2 = recurse(bo->second()); + const formula* f1 = recurse(bo->first()); + const formula* f2 = recurse(bo->second()); binop::type op = bo->op(); switch (op) @@ -89,19 +90,19 @@ namespace spot assert(0); } - formula* - simplify_f_g_visitor::recurse(formula* f) + const formula* + simplify_f_g_visitor::recurse(const formula* f) { return simplify_f_g(f); } - formula* + const formula* simplify_f_g(const formula* f) { if (f->is_boolean()) return f->clone(); simplify_f_g_visitor v; - const_cast(f)->accept(v); + f->accept(v); return v.result(); } } diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh index 02ce24e10..8d226e3f7 100644 --- a/src/ltlvisit/simpfg.hh +++ b/src/ltlvisit/simpfg.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -49,9 +50,9 @@ namespace spot virtual ~simplify_f_g_visitor(); using super::visit; - void visit(binop* bo); + void visit(const binop* bo); - virtual formula* recurse(formula* f); + virtual const formula* recurse(const formula* f); }; /// \brief Replace true U f and false R g by @@ -65,7 +66,7 @@ namespace spot /// - a W false = G a /// /// \ingroup ltl_rewriting - formula* simplify_f_g(const formula* f); + const formula* simplify_f_g(const formula* f); } } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 2ea90679c..46aeb7d62 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -380,15 +380,15 @@ namespace spot { } - formula* result() const + const formula* result() const { return result_; } void - visit(atomic_prop* ap) + visit(const atomic_prop* ap) { - formula* f = ap->clone(); + const formula* f = ap->clone(); if (negated_) result_ = unop::instance(unop::Not, f); else @@ -396,7 +396,7 @@ namespace spot } void - visit(constant* c) + visit(const constant* c) { // Negation of constants is taken care of in the constructor // of unop::Not, so these cases should be caught by @@ -407,9 +407,9 @@ namespace spot } void - visit(unop* uo) + visit(const unop* uo) { - formula* f = uo->child(); + const formula* f = uo->child(); switch (uo->op()) { case unop::Not: @@ -453,7 +453,7 @@ namespace spot } void - visit(bunop* bo) + visit(const bunop* bo) { // !(a*) should never occur. assert(!negated_); @@ -461,7 +461,9 @@ namespace spot bo->min(), bo->max()); } - formula* equiv_or_xor(bool equiv, formula* f1, formula* f2) + const formula* equiv_or_xor(bool equiv, + const formula* f1, + const formula* f2) { // Rewrite a<=>b as (a&b)|(!a&!b) if (equiv) @@ -486,10 +488,10 @@ namespace spot } void - visit(binop* bo) + visit(const binop* bo) { - formula* f1 = bo->first(); - formula* f2 = bo->second(); + const formula* f1 = bo->first(); + const formula* f2 = bo->second(); switch (bo->op()) { case binop::Xor: @@ -556,7 +558,7 @@ namespace spot } void - visit(automatop* ao) + visit(const automatop* ao) { bool negated = negated_; negated_ = false; @@ -568,7 +570,7 @@ namespace spot } void - visit(multop* mo) + visit(const multop* mo) { multop::type op = mo->op(); /* !(a & b & c) == !a | !b | !c */ @@ -615,21 +617,20 @@ namespace spot } } - formula* - recurse_(formula* f, bool negated) + const formula* + recurse_(const formula* f, bool negated) { - return - const_cast(nenoform_recursively(f, negated, cache_)); + return nenoform_recursively(f, negated, cache_); } - formula* - recurse(formula* f) + const formula* + recurse(const formula* f) { return recurse_(f, negated_); } protected: - formula* result_; + const formula* result_; bool negated_; ltl_simplifier_cache* cache_; }; @@ -640,14 +641,10 @@ namespace spot bool negated, ltl_simplifier_cache* c) { - if (f->kind() == formula::UnOp) + if (const unop* uo = is_Not(f)) { - const unop* uo = static_cast(f); - if (uo->op() == unop::Not) - { - negated = !negated; - f = uo->child(); - } + negated = !negated; + f = uo->child(); } const formula* key = f; @@ -665,7 +662,7 @@ namespace spot else { negative_normal_form_visitor v(negated, c); - const_cast(f)->accept(v); + f->accept(v); result = v.result(); } @@ -684,20 +681,20 @@ namespace spot ////////////////////////////////////////////////////////////////////// // Forward declaration. - formula* + const formula* simplify_recursively(const formula* f, ltl_simplifier_cache* c); // X(a) R b or X(a) M b // This returns a. - formula* - is_XRM(formula* f) + const formula* + is_XRM(const formula* f) { - binop* bo = is_binop(f, binop::R, binop::M); + const binop* bo = is_binop(f, binop::R, binop::M); if (!bo) return 0; - unop* uo = is_X(bo->first()); + const unop* uo = is_X(bo->first()); if (!uo) return 0; return uo->child(); @@ -705,13 +702,13 @@ namespace spot // X(a) W b or X(a) U b // This returns a. - formula* - is_XWU(formula* f) + const formula* + is_XWU(const formula* f) { - binop* bo = is_binop(f, binop::W, binop::U); + const binop* bo = is_binop(f, binop::W, binop::U); if (!bo) return 0; - unop* uo = is_X(bo->first()); + const unop* uo = is_X(bo->first()); if (!uo) return 0; return uo->child(); @@ -719,22 +716,22 @@ namespace spot // b & X(b W a) or b & X(b U a) // This returns (b W a) or (b U a). - binop* - is_bXbWU(formula* f) + const binop* + is_bXbWU(const formula* f) { - multop* mo = is_multop(f, multop::And); + const multop* mo = is_multop(f, multop::And); if (!mo) return 0; unsigned s = mo->size(); for (unsigned pos = 0; pos < s; ++pos) { - unop* u = is_X(mo->nth(pos)); + const unop* u = is_X(mo->nth(pos)); if (!u) continue; - binop* bo = is_binop(u->child(), binop::U, binop::W); + const binop* bo = is_binop(u->child(), binop::U, binop::W); if (!bo) continue; - formula* b = mo->all_but(pos); + const formula* b = mo->all_but(pos); bool result = (b == bo->first()); b->destroy(); if (result) @@ -745,22 +742,22 @@ namespace spot // b | X(b R a) or b | X(b M a) // This returns (b R a) or (b M a). - binop* - is_bXbRM(formula* f) + const binop* + is_bXbRM(const formula* f) { - multop* mo = is_multop(f, multop::Or); + const multop* mo = is_multop(f, multop::Or); if (!mo) return 0; unsigned s = mo->size(); for (unsigned pos = 0; pos < s; ++pos) { - unop* u = is_X(mo->nth(pos)); + const unop* u = is_X(mo->nth(pos)); if (!u) continue; - binop* bo = is_binop(u->child(), binop::R, binop::M); + const binop* bo = is_binop(u->child(), binop::R, binop::M); if (!bo) continue; - formula* b = mo->all_but(pos); + const formula* b = mo->all_but(pos); bool result = (b == bo->first()); b->destroy(); if (result) @@ -769,21 +766,21 @@ namespace spot return 0; } - formula* + const formula* unop_multop(unop::type uop, multop::type mop, multop::vec* v) { return unop::instance(uop, multop::instance(mop, v)); } - formula* + const formula* unop_unop_multop(unop::type uop1, unop::type uop2, multop::type mop, multop::vec* v) { return unop::instance(uop1, unop_multop(uop2, mop, v)); } - formula* - unop_unop(unop::type uop1, unop::type uop2, formula* f) + const formula* + unop_unop(unop::type uop1, unop::type uop2, const formula* f) { return unop::instance(uop1, unop::instance(uop2, f)); } @@ -823,14 +820,14 @@ namespace spot res_other = new multop::vec; } - void process(formula* f) + void process(const formula* f) { switch (f->kind()) { case formula::UnOp: { - unop* uo = static_cast(f); - formula* c = uo->child(); + const unop* uo = static_cast(f); + const formula* c = uo->child(); switch (uo->op()) { case unop::X: @@ -842,15 +839,12 @@ namespace spot break; case unop::F: if (res_FG) - { - unop* cc = is_G(c); - if (cc) - { - res_FG->push_back(((split_ & Strip_FG) == Strip_FG - ? cc->child() : f)->clone()); - return; - } - } + if (const unop* cc = is_G(c)) + { + res_FG->push_back(((split_ & Strip_FG) == Strip_FG + ? cc->child() : f)->clone()); + return; + } if (res_F) { res_F->push_back(((split_ & Strip_F) == Strip_F @@ -860,15 +854,12 @@ namespace spot break; case unop::G: if (res_GF) - { - unop* cc = is_F(c); - if (cc) - { - res_GF->push_back(((split_ & Strip_GF) == Strip_GF - ? cc->child() : f)->clone()); - return; - } - } + if (const unop* cc = is_F(c)) + { + res_GF->push_back(((split_ & Strip_GF) == Strip_GF + ? cc->child() : f)->clone()); + return; + } if (res_G) { res_G->push_back(((split_ & Strip_G) == Strip_G @@ -883,7 +874,7 @@ namespace spot break; case formula::BinOp: { - binop* bo = static_cast(f); + const binop* bo = static_cast(f); switch (bo->op()) { case binop::U: @@ -955,14 +946,15 @@ namespace spot delete v; } - mospliter(unsigned split, multop* mo, ltl_simplifier_cache* cache) + mospliter(unsigned split, const multop* mo, + ltl_simplifier_cache* cache) : split_(split), c_(cache) { init(); unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) { - formula* f = simplify_recursively(mo->nth(i), cache); + const formula* f = simplify_recursively(mo->nth(i), cache); process(f); f->destroy(); } @@ -998,30 +990,30 @@ namespace spot { } - formula* + const formula* result() const { return result_; } void - visit(atomic_prop* ap) + visit(const atomic_prop* ap) { result_ = ap->clone(); } void - visit(constant* c) + visit(const constant* c) { result_ = c; } void - visit(bunop* bo) + visit(const bunop* bo) { bunop::type op = bo->op(); unsigned min = bo->min(); - formula* h = recurse(bo->child()); + const formula* h = recurse(bo->child()); switch (op) { case bunop::Star: @@ -1031,7 +1023,7 @@ namespace spot { const formula* s = c_->star_normal_form(h); h->destroy(); - h = const_cast(s); + h = s; } result_ = bunop::instance(op, h, min, bo->max()); break; @@ -1040,8 +1032,9 @@ namespace spot // if !neg build c&X(c&X(...&X(tail))) with n occurences of c // if neg build !c|X(!c|X(...|X(tail))). - formula* - dup_b_x_tail(bool neg, formula* c, formula* tail, unsigned n) + const formula* + dup_b_x_tail(bool neg, const formula* c, + const formula* tail, unsigned n) { c->clone(); multop::type mop; @@ -1065,7 +1058,7 @@ namespace spot } void - visit(unop* uo) + visit(const unop* uo) { result_ = recurse(uo->child()); @@ -1125,10 +1118,10 @@ namespace spot if (opt_.reduce_basics) { // F(a U b) = F(b) - binop* bo = is_U(result_); + const binop* bo = is_U(result_); if (bo) { - formula* r = + const formula* r = unop::instance(unop::F, bo->second()->clone()); bo->destroy(); result_ = recurse_destroy(r); @@ -1139,7 +1132,7 @@ namespace spot bo = is_M(result_); if (bo) { - formula* r = + const formula* r = unop::instance(unop::F, multop::instance(multop::And, bo->first()->clone(), @@ -1150,19 +1143,16 @@ namespace spot } // FX(a) = XF(a) - { - unop* u = is_X(result_); - if (u) - { - formula* res = - unop_unop(unop::X, unop::F, u->child()->clone()); - u->destroy(); - // FXX(a) = XXF(a) ... - // FXG(a) = XFG(a) = FG(a) ... - result_ = recurse_destroy(res); - return; - } - } + if (const unop* u = is_X(result_)) + { + const formula* res = + unop_unop(unop::X, unop::F, u->child()->clone()); + u->destroy(); + // FXX(a) = XXF(a) ... + // FXG(a) = XFG(a) = FG(a) ... + result_ = recurse_destroy(res); + return; + } } // if Fa => a, keep a. @@ -1199,12 +1189,11 @@ namespace spot if (opt_.reduce_basics) { - // G(a R b) = G(b) - binop* bo = is_R(result_); + const binop* bo = is_R(result_); if (bo) { - formula* r = + const formula* r = unop::instance(unop::G, bo->second()->clone()); bo->destroy(); result_ = recurse_destroy(r); @@ -1215,7 +1204,7 @@ namespace spot bo = is_W(result_); if (bo) { - formula* r = + const formula* r = unop::instance(unop::G, multop::instance(multop::Or, bo->first()->clone(), @@ -1226,54 +1215,46 @@ namespace spot } // GX(a) = XG(a) - if (result_->kind() == formula::UnOp) + if (const unop* u = is_X(result_)) { - unop* u = static_cast(result_); - if (u->op() == unop::X) - { - formula* res = - unop_unop(unop::X, unop::G, u->child()->clone()); - u->destroy(); - // GXX(a) = XXG(a) ... - // GXF(a) = XGF(a) = GF(a) ... - result_ = recurse_destroy(res); - return; - } + const formula* res = + unop_unop(unop::X, unop::G, u->child()->clone()); + u->destroy(); + // GXX(a) = XXG(a) ... + // GXF(a) = XGF(a) = GF(a) ... + result_ = recurse_destroy(res); + return; } // G(f1|f2|GF(f3)|GF(f4)|f5|f6) = // G(f1|f2) | GF(f3|f4) | f5 | f6 // if f5 and f6 are both eventual and universal. - if (result_->kind() == formula::MultOp) + if (const multop* mo = is_Or(result_)) { - multop* mo = static_cast(result_); - if (mo->op() == multop::Or) + mo->clone(); + mospliter s(mospliter::Strip_GF | + mospliter::Split_EventUniv, + mo, c_); + s.res_EventUniv-> + push_back(unop_multop(unop::G, multop::Or, + s.res_other)); + s.res_EventUniv-> + push_back(unop_unop_multop(unop::G, unop::F, + multop::Or, s.res_GF)); + result_ = multop::instance(multop::Or, + s.res_EventUniv); + if (result_ != uo) { - mo->clone(); - mospliter s(mospliter::Strip_GF | - mospliter::Split_EventUniv, - mo, c_); - s.res_EventUniv-> - push_back(unop_multop(unop::G, multop::Or, - s.res_other)); - s.res_EventUniv-> - push_back(unop_unop_multop(unop::G, unop::F, - multop::Or, s.res_GF)); - result_ = multop::instance(multop::Or, - s.res_EventUniv); - if (result_ != uo) - { - mo->destroy(); - result_ = recurse_destroy(result_); - return; - } - else - { - // Revert to the previous value of result_, - // for the next simplification. - result_->destroy(); - result_ = mo; - } + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + else + { + // Revert to the previous value of result_, + // for the next simplification. + result_->destroy(); + result_ = mo; } } } @@ -1295,7 +1276,7 @@ namespace spot return; } if (!opt_.reduce_size_strictly) - if (multop* mo = is_OrRat(result_)) + if (const multop* mo = is_OrRat(result_)) { // {aâ‚|aâ‚‚} = {aâ‚}| {aâ‚‚} // !{aâ‚|aâ‚‚} = !{aâ‚}&!{aâ‚‚} @@ -1310,7 +1291,7 @@ namespace spot : multop::And, v)); return; } - if (multop* mo = is_Concat(result_)) + if (const multop* mo = is_Concat(result_)) { unsigned end = mo->size() - 1; // {bâ‚;bâ‚‚;b₃*;eâ‚;fâ‚;eâ‚‚;fâ‚‚;eâ‚‚;e₃;eâ‚„} @@ -1324,8 +1305,8 @@ namespace spot unsigned start = 0; while (start <= end) { - formula* r = mo->nth(start); - bunop* es = is_KleenStar(r); + const formula* r = mo->nth(start); + const bunop* es = is_KleenStar(r); if ((r->is_boolean() && !opt_.reduce_size_strictly) || (es && es->child()->is_boolean())) ++start; @@ -1339,14 +1320,15 @@ namespace spot v->reserve(s); for (unsigned n = start; n <= end; ++n) v->push_back(mo->nth(n)->clone()); - formula* tail = multop::instance(multop::Concat, v); + const formula* tail = + multop::instance(multop::Concat, v); tail = unop::instance(op, tail); bool doneg = op == unop::NegClosure; for (unsigned n = start; n > 0;) { --n; - formula* e = mo->nth(n); + const formula* e = mo->nth(n); // {b;f} = b & X{f} // !{b;f} = !b | X!{f} if (e->is_boolean()) @@ -1366,9 +1348,9 @@ namespace spot // !{b*;f} = !b M !{f} else { - bunop* es = is_KleenStar(e); + const bunop* es = is_KleenStar(e); assert(es); - formula* c = es->child()->clone(); + const formula* c = es->child()->clone(); if (doneg) tail = binop::instance(binop::M, @@ -1386,9 +1368,9 @@ namespace spot // {b[*i..j];c} = b&X(b&X(... b&X{b[*0..j-i];c})) // !{b[*i..j];c} = !b&X(!b&X(... !b&X!{b[*0..j-i];c})) if (!opt_.reduce_size_strictly) - if (bunop* s = is_Star(mo->nth(0))) + if (const bunop* s = is_Star(mo->nth(0))) { - formula* c = s->child(); + const formula* c = s->child(); unsigned min = s->min(); if (c->is_boolean() && min > 0) { @@ -1403,7 +1385,7 @@ namespace spot 0, max)); for (unsigned n = 1; n < ss; ++n) v->push_back(mo->nth(n)->clone()); - formula* tail = + const formula* tail = multop::instance(multop::Concat, v); tail = // {b[*0..j-i]} or !{b[*0..j-i]} unop::instance(op, tail); @@ -1419,14 +1401,14 @@ namespace spot // {b[*i..j]} = b&X(b&X(... b)) with i occurences of b // !{b[*i..j]} = !b&X(!b&X(... !b)) if (!opt_.reduce_size_strictly) - if (bunop* s = is_Star(result_)) + if (const bunop* s = is_Star(result_)) { - formula* c = s->child(); + const formula* c = s->child(); if (c->is_boolean()) { unsigned min = s->min(); assert(min > 0); - formula* tail; + const formula* tail; if (op == unop::NegClosure) tail = dup_b_x_tail(true, @@ -1450,7 +1432,7 @@ namespace spot // Return true iff reduction occurred. bool - reduce_sere_ltl(binop::type bindop, formula* a, formula* b) + reduce_sere_ltl(binop::type bindop, const formula* a, const formula* b) { // All this function is documented assuming bindop == // UConcat, but by changing the following variable it can @@ -1479,7 +1461,7 @@ namespace spot if (!opt_.reduce_basics) return false; - if (bunop* bu = is_Star(a)) + if (const bunop* bu = is_Star(a)) { // {[*]}[]->b = Gb if (a == bunop::one_star()) @@ -1488,14 +1470,14 @@ namespace spot result_ = recurse_destroy(unop::instance(op_g, b)); return true; } - formula* s = bu->child(); + const formula* s = bu->child(); unsigned min = bu->min(); unsigned max = bu->max(); // {s[*]}[]->b = b W !s if s is Boolean. // {s[+]}[]->b = b W !s if s is Boolean. if (s->is_boolean() && max == bunop::unbounded && min <= 1) { - formula* ns = // !s + const formula* ns = // !s doneg ? unop::instance(unop::Not, s->clone()) : s->clone(); result_ = // b W !s binop::instance(op_w, b, ns); @@ -1516,7 +1498,7 @@ namespace spot // Don't rewrite s[1..]. if (min == 0) return false; - formula* tail = // {s[*1..j-i]}[]->b + const formula* tail = // {s[*1..j-i]}[]->b binop::instance(bindop, bunop::instance(bunop::Star, s->clone(), 1, max), @@ -1531,10 +1513,10 @@ namespace spot result_ = recurse_destroy(result_); return true; } - else if (multop* mo = is_Concat(a)) + else if (const multop* mo = is_Concat(a)) { unsigned s = mo->size() - 1; - formula* last = mo->nth(s); + const formula* last = mo->nth(s); // {r;[*]}[]->b = {r}[]->Gb if (last == bunop::one_star()) { @@ -1546,7 +1528,7 @@ namespace spot return true; } - formula* first = mo->nth(0); + const formula* first = mo->nth(0); // {[*];r}[]->b = G({r}[]->b) if (first == bunop::one_star()) { @@ -1563,21 +1545,21 @@ namespace spot // {r;s[*]}[]->b = {r}[]->(b & X(b W !s)) // if s is Boolean and r does not accept [*0]; - if (bunop* l = is_KleenStar(last)) // l = s[*] + if (const bunop* l = is_KleenStar(last)) // l = s[*] if (l->child()->is_boolean()) { - formula* r = mo->all_but(s); + const formula* r = mo->all_but(s); if (!r->accepts_eword()) { - formula* ns = // !s + const formula* ns = // !s doneg ? unop::instance(unop::Not, l->child()->clone()) : l->child()->clone(); - formula* w = // b W !s + const formula* w = // b W !s binop::instance(op_w, b->clone(), ns); - formula* x = // X(b W !s) + const formula* x = // X(b W !s) unop::instance(unop::X, w); - formula* d = // b & X(b W !s) + const formula* d = // b & X(b W !s) multop::instance(op_and, b, x); result_ = // {r}[]->(b & X(b W !s)) binop::instance(bindop, r, d); @@ -1588,17 +1570,17 @@ namespace spot } // {s[*];r}[]->b = !s R ({r}[]->b) // if s is Boolean and r does not accept [*0]; - if (bunop* l = is_KleenStar(first)) + if (const bunop* l = is_KleenStar(first)) if (l->child()->is_boolean()) { - formula* r = mo->all_but(0); + const formula* r = mo->all_but(0); if (!r->accepts_eword()) { - formula* ns = // !s + const formula* ns = // !s doneg ? unop::instance(unop::Not, l->child()->clone()) : l->child()->clone(); - formula* u = // {r}[]->b + const formula* u = // {r}[]->b binop::instance(bindop, r, b); result_ = // !s R ({r}[]->b) binop::instance(op_r, ns, u); @@ -1635,7 +1617,7 @@ namespace spot do r->insert(r->begin(), mo->nth(--pos)->clone()); while (r->front()->accepts_eword()); - formula* tail = // {râ‚‚}[]->b + const formula* tail = // {râ‚‚}[]->b binop::instance(bindop, multop::instance(multop::Concat, r), b); @@ -1670,11 +1652,11 @@ namespace spot { return false; } - else if (multop* mo = is_Fusion(a)) + else if (const multop* mo = is_Fusion(a)) { // {râ‚:râ‚‚:r₃}[]->b = {râ‚}[]->({râ‚‚}[]->({r₃}[]->b)) unsigned s = mo->size(); - formula* tail = b; + const formula* tail = b; do { --s; @@ -1686,14 +1668,14 @@ namespace spot result_ = recurse_destroy(tail); return true; } - else if (multop* mo = is_OrRat(a)) + else if (const multop* mo = is_OrRat(a)) { // {râ‚|râ‚‚|r₃}[]->b = ({râ‚}[]->b)&({râ‚‚}[]->b)&({r₃}[]->b) unsigned s = mo->size(); multop::vec* v = new multop::vec; for (unsigned n = 0; n < s; ++n) { - formula* x = // {râ‚}[]->b + const formula* x = // {râ‚}[]->b binop::instance(bindop, mo->nth(n)->clone(), b->clone()); v->push_back(x); @@ -1707,11 +1689,11 @@ namespace spot } void - visit(binop* bo) + visit(const binop* bo) { binop::type op = bo->op(); - formula* b = recurse(bo->second()); + const formula* b = recurse(bo->second()); if (opt_.event_univ) { @@ -1726,7 +1708,7 @@ namespace spot } } - formula* a = recurse(bo->first()); + const formula* a = recurse(bo->first()); if (opt_.event_univ) { @@ -1734,14 +1716,14 @@ namespace spot If a is a pure universality formula a W b = a|b. */ if (a->is_eventual() && (op == binop::M)) { - formula* tmp = multop::instance(multop::And, a, b); + const formula* tmp = multop::instance(multop::And, a, b); result_ = recurse(tmp); tmp->destroy(); return; } if (a->is_universal() && (op == binop::W)) { - formula* tmp = multop::instance(multop::Or, a, b); + const formula* tmp = multop::instance(multop::Or, a, b); result_ = recurse(tmp); tmp->destroy(); return; @@ -1791,9 +1773,8 @@ namespace spot // if a => c, then a U (b R (c W d)) = (b R (c W d)) // if a => c, then a U (b M (c U d)) = (b M (c U d)) // if a => c, then a U (b M (c W d)) = (b M (c W d)) - if (b->kind() == formula::BinOp) + if (const binop* bo = is_binop(b)) { - binop* bo = static_cast(b); // if a => b, then a U (b U c) = (b U c) // if a => b, then a U (b W c) = (b W c) if ((bo->op() == binop::U || bo->op() == binop::W) @@ -1820,7 +1801,8 @@ namespace spot if ((bo->op() == binop::R || bo->op() == binop::M) && bo->second()->kind() == formula::BinOp) { - binop* cd = static_cast(bo->second()); + const binop* cd = + static_cast(bo->second()); if ((cd->op() == binop::U || cd->op() == binop::W) && c_->implication(a, cd->first())) { @@ -1851,7 +1833,7 @@ namespace spot { // if b => a, then a R (b R c) = b R c // if b => a, then a R (b M c) = b M c - binop* bo = static_cast(b); + const binop* bo = static_cast(b); if ((bo->op() == binop::R || bo->op() == binop::M) && c_->implication(bo->first(), a)) { @@ -1875,7 +1857,7 @@ namespace spot { // if b => a then (a R c) R b = c R b // if b => a then (a M c) R b = c R b - binop* bo = static_cast(a); + const binop* bo = static_cast(a); if ((bo->op() == binop::R || bo->op() == binop::M) && c_->implication(b, bo->first())) { @@ -1915,7 +1897,7 @@ namespace spot // if b => a, then a W (b W c) = (a W c) if (b->kind() == formula::BinOp) { - binop* bo = static_cast(b); + const binop* bo = static_cast(b); // if a => b, then a W (b W c) = (b W c) if (bo->op() == binop::W && c_->implication(a, bo->first())) @@ -1957,7 +1939,7 @@ namespace spot if (b->kind() == formula::BinOp) { // if b => a, then a M (b M c) = b M c - binop* bo = static_cast(b); + const binop* bo = static_cast(b); if (bo->op() == binop::M && c_->implication(bo->first(), a)) { @@ -1981,7 +1963,7 @@ namespace spot if (a->kind() == formula::BinOp) { // if b => a then (a M c) M b = c M b - binop* bo = static_cast(a); + const binop* bo = static_cast(a); if (bo->op() == binop::M && c_->implication(b, bo->first())) { @@ -2066,8 +2048,8 @@ namespace spot return; } - unop* fu1 = is_unop(a); - unop* fu2 = is_unop(b); + const unop* fu1 = is_unop(a); + const unop* fu2 = is_unop(b); // X(a) U X(b) = X(a U b) // X(a) R X(b) = X(a R b) @@ -2077,9 +2059,10 @@ namespace spot && fu1->op() == unop::X && fu2->op() == unop::X) { - formula* bin = binop::instance(op, - fu1->child()->clone(), - fu2->child()->clone()); + const formula* bin = + binop::instance(op, + fu1->child()->clone(), + fu2->child()->clone()); a->destroy(); b->destroy(); result_ = recurse_destroy(unop::instance(unop::X, bin)); @@ -2101,9 +2084,8 @@ namespace spot // a W (b | c | G(a)) = a W (b | c) // a U (a & b & c) = (b & c) M a // a W (a & b & c) = (b & c) R a - if (b->kind() == formula::MultOp) + if (const multop* fm2 = is_multop(b)) { - multop* fm2 = static_cast(b); multop::type bt = fm2->op(); // a U (b | c | G(a)) = a W (b | c) // a W (b | c | G(a)) = a W (b | c) @@ -2112,7 +2094,7 @@ namespace spot int s = fm2->size(); for (int i = 0; i < s; ++i) { - unop* c = is_G(fm2->nth(i)); + const unop* c = is_G(fm2->nth(i)); if (!c || c->child() != a) continue; result_ = @@ -2146,9 +2128,9 @@ namespace spot if (!opt_.reduce_size_strictly && fu1 && fu1->op() == unop::X && b->is_boolean()) { - formula* c = fu1->child()->clone(); + const formula* c = fu1->child()->clone(); fu1->destroy(); - formula* x = + const formula* x = unop::instance(unop::X, binop::instance(op == binop::U ? binop::M @@ -2174,9 +2156,8 @@ namespace spot // a M (b & c & F(a)) = a M (b & c) // a M (b | a | c) == (b | c) U a // a R (b | a | c) == (b | c) W a - if (b->kind() == formula::MultOp) + if (const multop* fm2 = is_multop(b)) { - multop* fm2 = static_cast(b); multop::type bt = fm2->op(); // a R (b & c & F(a)) = a M (b & c) @@ -2186,7 +2167,7 @@ namespace spot int s = fm2->size(); for (int i = 0; i < s; ++i) { - unop* c = is_F(fm2->nth(i)); + const unop* c = is_F(fm2->nth(i)); if (!c || c->child() != a) continue; result_ = @@ -2220,9 +2201,9 @@ namespace spot if (!opt_.reduce_size_strictly && fu1 && fu1->op() == unop::X && b->is_boolean()) { - formula* c = fu1->child()->clone(); + const formula* c = fu1->child()->clone(); fu1->destroy(); - formula* x = + const formula* x = unop::instance(unop::X, binop::instance(op == binop::M ? binop::U @@ -2252,13 +2233,13 @@ namespace spot } void - visit(automatop*) + visit(const automatop*) { assert(0); } void - visit(multop* mo) + visit(const multop* mo) { unsigned mos = mo->size(); multop::vec* res = new multop::vec; @@ -2359,9 +2340,10 @@ namespace spot // a & (b | X(b M a)) = b M a if (!mo->is_X_free()) { - typedef Sgi::hash_set > fset_t; - typedef Sgi::hash_map, + typedef Sgi::hash_map, ptr_hash > fmap_t; fset_t xgset; // XG(...) fset_t xset; // X(...) @@ -2377,7 +2359,7 @@ namespace spot if (!(*res)[n]) continue; - formula* xarg = is_XWU((*res)[n]); + const formula* xarg = is_XWU((*res)[n]); if (xarg) { wuset[xarg].insert(n); @@ -2391,23 +2373,23 @@ namespace spot if ((*res)[n]->is_X_free()) continue; - binop* barg = is_bXbRM((*res)[n]); + const binop* barg = is_bXbRM((*res)[n]); if (barg) { wuset[barg->second()].insert(n); continue; } - unop* uo = is_X((*res)[n]); + const unop* uo = is_X((*res)[n]); if (!uo) continue; - formula* c = uo->child(); - multop* a; - unop* g; + const formula* c = uo->child(); + const multop* a; + const unop* g; if ((g = is_G(c))) { -#define HANDLE_G multop* a2; \ +#define HANDLE_G const multop* a2; \ if ((a2 = is_And(g->child()))) \ { \ unsigned y = a2->size(); \ @@ -2426,7 +2408,7 @@ namespace spot unsigned z = a->size(); for (unsigned m = 0; m < z; ++m) { - formula* x = a->nth(m); + const formula* x = a->nth(m); if ((g = is_G(x))) { HANDLE_G; @@ -2461,16 +2443,17 @@ namespace spot for (g = s.begin(); g != s.end(); ++g) { unsigned pos = *g; - binop* wu = is_binop((*res)[pos]); + const binop* wu = is_binop((*res)[pos]); if (wu) { // a & (Xa W b) = b R a // a & (Xa U b) = b M a binop::type t = (wu->op() == binop::U) ? binop::M : binop::R; - unop* xa = down_cast(wu->first()); - formula* a = xa->child()->clone(); - formula* b = wu->second()->clone(); + const unop* xa = + down_cast(wu->first()); + const formula* a = xa->child()->clone(); + const formula* b = wu->second()->clone(); wu->destroy(); (*res)[pos] = binop::instance(t, b, a); } @@ -2493,14 +2476,14 @@ namespace spot // by 'Ga' and delete XGa. for (unsigned n = 0; n < s; ++n) { - formula* x = (*res)[n]; + const formula* x = (*res)[n]; if (!x) continue; fset_t::const_iterator g = xgset.find(x); if (g != xgset.end()) { // x can appear only once. - formula* gf = *g; + const formula* gf = *g; xgset.erase(g); gf->destroy(); (*res)[n] = unop::instance(unop::G, x); @@ -2522,13 +2505,15 @@ namespace spot fset_t::iterator i; for (i = xgset.begin(); i != xgset.end(); ++i) xgv->push_back(*i); - formula* gv = multop::instance(multop::And, xgv); + const formula* gv = + multop::instance(multop::And, xgv); xv->push_back(unop::instance(unop::G, gv)); } fset_t::iterator j; for (j = xset.begin(); j != xset.end(); ++j) xv->push_back(*j); - formula* av = multop::instance(multop::And, xv); + const formula* av = + multop::instance(multop::And, xv); res->push_back(unop::instance(unop::X, av)); } @@ -2543,8 +2528,9 @@ namespace spot res, c_); // FG(a) & FG(b) = FG(a & b) - formula* allFG = unop_unop_multop(unop::F, unop::G, - multop::And, s.res_FG); + const formula* allFG = + unop_unop_multop(unop::F, unop::G, multop::And, + s.res_FG); // Xa & Xb = X(a & b) // Xa & Xb & FG(c) = X(a & b & FG(c)) @@ -2585,7 +2571,8 @@ namespace spot // F(a) & (a M b) = a M b // F(b) & (a W b) = a U b // F(b) & (a U b) = a U b - typedef Sgi::hash_map > fmap_t; fmap_t uwmap; // associates "b" to "a U b" or "a W b" fmap_t rmmap; // associates "a" to "a R b" or "a M b" @@ -2595,8 +2582,8 @@ namespace spot for (multop::vec::iterator i = s.res_U_or_W->begin(); i != s.res_U_or_W->end(); ++i) { - binop* bo = static_cast(*i); - formula* b = bo->second(); + const binop* bo = static_cast(*i); + const formula* b = bo->second(); fmap_t::iterator j = uwmap.find(b); if (j == uwmap.end()) { @@ -2605,12 +2592,13 @@ namespace spot continue; } // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); + const binop* old = + static_cast(*j->second); binop::type op = binop::W; if (bo->op() == binop::U || old->op() == binop::U) op = binop::U; - formula* fst_arg = + const formula* fst_arg = multop::instance(multop::And, old->first()->clone(), bo->first()->clone()); @@ -2626,8 +2614,8 @@ namespace spot for (multop::vec::iterator i = s.res_R_or_M->begin(); i != s.res_R_or_M->end(); ++i) { - binop* bo = static_cast(*i); - formula* a = bo->first(); + const binop* bo = static_cast(*i); + const formula* a = bo->first(); fmap_t::iterator j = rmmap.find(a); if (j == rmmap.end()) { @@ -2636,12 +2624,13 @@ namespace spot continue; } // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); + const binop* old = + static_cast(*j->second); binop::type op = binop::R; if (bo->op() == binop::M || old->op() == binop::M) op = binop::M; - formula* snd_arg = + const formula* snd_arg = multop::instance(multop::And, old->second()->clone(), bo->second()->clone()); @@ -2659,14 +2648,15 @@ namespace spot i != s.res_F->end(); ++i) { bool superfluous = false; - unop* uo = static_cast(*i); - formula* c = uo->child(); + const unop* uo = static_cast(*i); + const formula* c = uo->child(); fmap_t::iterator j = uwmap.find(c); if (j != uwmap.end()) { superfluous = true; - binop* bo = static_cast(*j->second); + const binop* bo = + static_cast(*j->second); if (bo->op() == binop::W) { *j->second = @@ -2682,7 +2672,8 @@ namespace spot if (j != rmmap.end()) { superfluous = true; - binop* bo = static_cast(*j->second); + const binop* bo = + static_cast(*j->second); if (bo->op() == binop::R) { *j->second = @@ -2739,10 +2730,10 @@ namespace spot } // G(a) & G(b) & ... = G(a & b & ...) - formula* allG = + const formula* allG = unop_multop(unop::G, multop::And, s.res_G); // Xa & Xb & ... = X(a & b & ...) - formula* allX = + const formula* allX = unop_multop(unop::X, multop::And, s.res_X); s.res_other->push_back(allX); @@ -2762,7 +2753,8 @@ namespace spot if (!s.res_Bool->empty()) { // b1 & b2 & b3 = b1 ∧ b2 ∧ b3 - formula* b = multop::instance(multop::And, s.res_Bool); + const formula* b = + multop::instance(multop::And, s.res_Bool); multop::vec* ares = new multop::vec; for (multop::vec::iterator i = s.res_other->begin(); @@ -2771,7 +2763,7 @@ namespace spot { case formula::BUnOp: { - bunop* r = down_cast(*i); + const bunop* r = down_cast(*i); // b && r[*i..j] = b & r if i<=1<=j // = 0 otherwise switch (r->op()) @@ -2788,7 +2780,7 @@ namespace spot } case formula::MultOp: { - multop* r = down_cast(*i); + const multop* r = down_cast(*i); unsigned rs = r->size(); switch (r->op()) { @@ -2807,11 +2799,11 @@ namespace spot // do not accept [*0] // - 0 if more than one ri accept [*0] { - formula* ri = 0; + const formula* ri = 0; unsigned nonempty = 0; for (unsigned j = 0; j < rs; ++j) { - formula* jf = r->nth(j); + const formula* jf = r->nth(j); if (!jf->accepts_eword()) { ri = jf; @@ -2828,7 +2820,7 @@ namespace spot for (unsigned j = 0; j < rs; ++j) sum->push_back(r->nth(j) ->clone()); - formula* sumf = + const formula* sumf = multop::instance(multop::OrRat, sum); ares->push_back(sumf); @@ -2896,8 +2888,8 @@ namespace spot continue; if ((*i)->kind() != formula::MultOp) continue; - multop* f = down_cast(*i); - formula* h = f->nth(0); + const multop* f = down_cast(*i); + const formula* h = f->nth(0); if (!h->is_boolean()) continue; multop::type op = f->op(); @@ -2930,11 +2922,11 @@ namespace spot } if (!head1->empty()) { - formula* h = + const formula* h = multop::instance(multop::And, head1); - formula* t = + const formula* t = multop::instance(multop::AndRat, tail1); - formula* f = + const formula* f = multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } @@ -2945,11 +2937,11 @@ namespace spot } if (!head2->empty()) { - formula* h = + const formula* h = multop::instance(multop::And, head2); - formula* t = + const formula* t = multop::instance(multop::AndRat, tail2); - formula* f = + const formula* f = multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } @@ -2974,9 +2966,9 @@ namespace spot continue; if ((*i)->kind() != formula::MultOp) continue; - multop* f = down_cast(*i); + const multop* f = down_cast(*i); unsigned s = f->size() - 1; - formula* t = f->nth(s); + const formula* t = f->nth(s); if (!t->is_boolean()) continue; multop::type op = f->op(); @@ -3007,11 +2999,11 @@ namespace spot } if (!head3->empty()) { - formula* h = + const formula* h = multop::instance(multop::AndRat, head3); - formula* t = + const formula* t = multop::instance(multop::And, tail3); - formula* f = + const formula* f = multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } @@ -3022,11 +3014,11 @@ namespace spot } if (!head4->empty()) { - formula* h = + const formula* h = multop::instance(multop::AndRat, head4); - formula* t = + const formula* t = multop::instance(multop::And, tail4); - formula* f = + const formula* f = multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } @@ -3054,9 +3046,10 @@ namespace spot // a | (b & X(b U a)) = b U a if (!mo->is_X_free()) { - typedef Sgi::hash_set > fset_t; - typedef Sgi::hash_map, + typedef Sgi::hash_map, ptr_hash > fmap_t; fset_t xfset; // XF(...) fset_t xset; // X(...) @@ -3073,7 +3066,7 @@ namespace spot if (!(*res)[n]) continue; - formula* xarg = is_XRM((*res)[n]); + const formula* xarg = is_XRM((*res)[n]); if (xarg) { rmset[xarg].insert(n); @@ -3087,7 +3080,7 @@ namespace spot if ((*res)[n]->is_X_free()) continue; - binop* barg = is_bXbWU((*res)[n]); + const binop* barg = is_bXbWU((*res)[n]); if (barg) { rmset[barg->second()].insert(n); @@ -3095,16 +3088,16 @@ namespace spot } - unop* uo = is_X((*res)[n]); + const unop* uo = is_X((*res)[n]); if (!uo) continue; - formula* c = uo->child(); - multop* o; - unop* f; + const formula* c = uo->child(); + const multop* o; + const unop* f; if ((f = is_F(c))) { -#define HANDLE_F multop* o2; \ +#define HANDLE_F const multop* o2; \ if ((o2 = is_Or(f->child()))) \ { \ unsigned y = o2->size(); \ @@ -3123,7 +3116,7 @@ namespace spot unsigned z = o->size(); for (unsigned m = 0; m < z; ++m) { - formula* x = o->nth(m); + const formula* x = o->nth(m); if ((f = is_F(x))) { HANDLE_F; @@ -3146,7 +3139,7 @@ namespace spot unsigned allofthem = xfset.size(); for (unsigned n = 0; n < s; ++n) { - formula* x = (*res)[n]; + const formula* x = (*res)[n]; if (!x) continue; fset_t::const_iterator f = xfset.find(x); @@ -3164,16 +3157,17 @@ namespace spot for (g = s.begin(); g != s.end(); ++g) { unsigned pos = *g; - binop* rm = is_binop((*res)[pos]); + const binop* rm = is_binop((*res)[pos]); if (rm) { // a | (Xa R b) = b W a // a | (Xa M b) = b U a binop::type t = (rm->op() == binop::M) ? binop::U : binop::W; - unop* xa = down_cast(rm->first()); - formula* a = xa->child()->clone(); - formula* b = rm->second()->clone(); + const unop* xa = + down_cast(rm->first()); + const formula* a = xa->child()->clone(); + const formula* b = rm->second()->clone(); rm->destroy(); (*res)[pos] = binop::instance(t, b, a); } @@ -3198,14 +3192,14 @@ namespace spot // by 'Fa' and delete XFa. for (unsigned n = 0; n < s; ++n) { - formula* x = (*res)[n]; + const formula* x = (*res)[n]; if (!x) continue; fset_t::const_iterator f = xfset.find(x); if (f != xfset.end()) { // x can appear only once. - formula* ff = *f; + const formula* ff = *f; xfset.erase(f); ff->destroy(); (*res)[n] = unop::instance(unop::F, x); @@ -3234,14 +3228,15 @@ namespace spot fset_t::iterator i; for (i = xfset.begin(); i != xfset.end(); ++i) xfv->push_back(*i); - formula* fv = multop::instance(multop::Or, xfv); + const formula* fv = + multop::instance(multop::Or, xfv); xv->push_back(unop::instance(unop::F, fv)); } // Also gather the remaining Xa | X(b|c) as X(b|c). fset_t::iterator j; for (j = xset.begin(); j != xset.end(); ++j) xv->push_back(*j); - formula* ov = multop::instance(multop::Or, xv); + const formula* ov = multop::instance(multop::Or, xv); res->push_back(unop::instance(unop::X, ov)); } @@ -3255,8 +3250,8 @@ namespace spot mospliter::Split_EventUniv, res, c_); // GF(a) | GF(b) = GF(a | b) - formula* allGF = unop_unop_multop(unop::G, unop::F, - multop::Or, s.res_GF); + const formula* allGF = + unop_unop_multop(unop::G, unop::F, multop::Or, s.res_GF); // Xa | Xb = X(a | b) // Xa | Xb | GF(c) = X(a | b | GF(c)) // For Universal&Eventual formula f1...fn we also have: @@ -3325,7 +3320,8 @@ namespace spot // G(a) | (a W b) = a W b // G(b) | (a R b) = a R b. // G(b) | (a M b) = a R b. - typedef Sgi::hash_map > fmap_t; fmap_t uwmap; // associates "a" to "a U b" or "a W b" fmap_t rmmap; // associates "b" to "a R b" or "a M b" @@ -3335,8 +3331,8 @@ namespace spot for (multop::vec::iterator i = s.res_U_or_W->begin(); i != s.res_U_or_W->end(); ++i) { - binop* bo = static_cast(*i); - formula* a = bo->first(); + const binop* bo = static_cast(*i); + const formula* a = bo->first(); fmap_t::iterator j = uwmap.find(a); if (j == uwmap.end()) { @@ -3345,12 +3341,13 @@ namespace spot continue; } // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); + const binop* old = + static_cast(*j->second); binop::type op = binop::U; if (bo->op() == binop::W || old->op() == binop::W) op = binop::W; - formula* snd_arg = + const formula* snd_arg = multop::instance(multop::Or, old->second()->clone(), bo->second()->clone()); @@ -3366,8 +3363,8 @@ namespace spot for (multop::vec::iterator i = s.res_R_or_M->begin(); i != s.res_R_or_M->end(); ++i) { - binop* bo = static_cast(*i); - formula* b = bo->second(); + const binop* bo = static_cast(*i); + const formula* b = bo->second(); fmap_t::iterator j = rmmap.find(b); if (j == rmmap.end()) { @@ -3376,12 +3373,13 @@ namespace spot continue; } // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); + const binop* old = + static_cast(*j->second); binop::type op = binop::M; if (bo->op() == binop::R || old->op() == binop::R) op = binop::R; - formula* fst_arg = + const formula* fst_arg = multop::instance(multop::Or, old->first()->clone(), bo->first()->clone()); @@ -3399,14 +3397,15 @@ namespace spot i != s.res_G->end(); ++i) { bool superfluous = false; - unop* uo = static_cast(*i); - formula* c = uo->child(); + const unop* uo = static_cast(*i); + const formula* c = uo->child(); fmap_t::iterator j = uwmap.find(c); if (j != uwmap.end()) { superfluous = true; - binop* bo = static_cast(*j->second); + const binop* bo = + static_cast(*j->second); if (bo->op() == binop::U) { *j->second = @@ -3421,7 +3420,8 @@ namespace spot if (j != rmmap.end()) { superfluous = true; - binop* bo = static_cast(*j->second); + const binop* bo = + static_cast(*j->second); if (bo->op() == binop::M) { *j->second = @@ -3439,8 +3439,6 @@ namespace spot } } - - s.res_other->reserve(s.res_other->size() + s.res_G->size() + s.res_U_or_W->size() @@ -3479,9 +3477,11 @@ namespace spot } // F(a) | F(b) | ... = F(a | b | ...) - formula* allF = unop_multop(unop::F, multop::Or, s.res_F); + const formula* allF = + unop_multop(unop::F, multop::Or, s.res_F); // Xa | Xb | ... = X(a | b | ...) - formula* allX = unop_multop(unop::X, multop::Or, s.res_X); + const formula* allX = + unop_multop(unop::X, multop::Or, s.res_X); s.res_other->push_back(allX); s.res_other->push_back(allF); @@ -3502,11 +3502,13 @@ namespace spot if (!s.res_Bool->empty()) { // b1 & b2 & b3 = b1 ∧ b2 ∧ b3 - formula* b = multop::instance(multop::And, s.res_Bool); + const formula* b = + multop::instance(multop::And, s.res_Bool); // now we just consider b & rest - formula* rest = multop::instance(multop::AndNLM, - s.res_other); + const formula* rest = + multop::instance(multop::AndNLM, + s.res_other); // We have b & rest = b : rest if rest does not // accept [*0]. Otherwise b & rest = b | (b : rest) @@ -3518,7 +3520,7 @@ namespace spot // explicitly requested. if (!opt_.reduce_size_strictly) { - formula* brest = + const formula* brest = multop::instance(multop::Fusion, b->clone(), rest); result_ = @@ -3563,8 +3565,8 @@ namespace spot continue; if ((*i)->kind() != formula::MultOp) continue; - multop* f = down_cast(*i); - formula* h = f->nth(0); + const multop* f = down_cast(*i); + const formula* h = f->nth(0); if (!h->is_boolean()) continue; multop::type op = f->op(); @@ -3597,11 +3599,11 @@ namespace spot } if (!head1->empty()) { - formula* h = + const formula* h = multop::instance(multop::And, head1); - formula* t = + const formula* t = multop::instance(multop::AndNLM, tail1); - formula* f = + const formula* f = multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } @@ -3612,11 +3614,11 @@ namespace spot } if (!head2->empty()) { - formula* h = + const formula* h = multop::instance(multop::And, head2); - formula* t = + const formula* t = multop::instance(multop::AndNLM, tail2); - formula* f = + const formula* f = multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } @@ -3641,9 +3643,9 @@ namespace spot continue; if ((*i)->kind() != formula::MultOp) continue; - multop* f = down_cast(*i); + const multop* f = down_cast(*i); unsigned s = f->size() - 1; - formula* t = f->nth(s); + const formula* t = f->nth(s); if (!t->is_boolean()) continue; multop::type op = f->op(); @@ -3674,11 +3676,11 @@ namespace spot } if (!head3->empty()) { - formula* h = + const formula* h = multop::instance(multop::AndNLM, head3); - formula* t = + const formula* t = multop::instance(multop::And, tail3); - formula* f = + const formula* f = multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } @@ -3689,11 +3691,11 @@ namespace spot } if (!head4->empty()) { - formula* h = + const formula* h = multop::instance(multop::AndNLM, head4); - formula* t = + const formula* t = multop::instance(multop::And, tail4); - formula* f = + const formula* f = multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } @@ -3720,34 +3722,34 @@ namespace spot result_ = multop::instance(mo->op(), res); } - formula* - recurse(formula* f) + const formula* + recurse(const formula* f) { return simplify_recursively(f, c_); } - formula* - recurse_destroy(formula* f) + const formula* + recurse_destroy(const formula* f) { - formula* tmp = recurse(f); + const formula* tmp = recurse(f); f->destroy(); return tmp; } protected: - formula* result_; + const formula* result_; ltl_simplifier_cache* c_; const ltl_simplifier_options& opt_; }; - formula* + const formula* simplify_recursively(const formula* f, ltl_simplifier_cache* c) { trace << "** simplify_recursively(" << to_string(f) << ")"; - formula* result = const_cast(c->lookup_simplified(f)); + const formula* result = c->lookup_simplified(f); if (result) { trace << " cached: " << to_string(result) << std::endl; @@ -3759,7 +3761,7 @@ namespace spot } simplify_visitor v(c); - const_cast(f)->accept(v); + f->accept(v); result = v.result(); trace << "** simplify_recursively(" << to_string(f) << ") result: " @@ -4179,22 +4181,22 @@ namespace spot delete todelete; } - formula* + const formula* ltl_simplifier::simplify(const formula* f) { - formula* neno = 0; + const formula* neno = 0; if (!f->is_in_nenoform()) f = neno = negative_normal_form(f, false); - formula* res = const_cast(simplify_recursively(f, cache_)); + const formula* res = simplify_recursively(f, cache_); if (neno) neno->destroy(); return res; } - formula* + const formula* ltl_simplifier::negative_normal_form(const formula* f, bool negated) { - return const_cast(nenoform_recursively(f, negated, cache_)); + return nenoform_recursively(f, negated, cache_); } bool diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 6ef304d42..1b4775eaa 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -77,7 +77,7 @@ namespace spot /// Simplify the formula \a f (using options supplied to the /// constructor). - formula* simplify(const formula* f); + const formula* simplify(const formula* f); /// Build the negative normal form of formula \a f. /// All negations of the formula are pushed in front of the @@ -87,7 +87,8 @@ namespace spot /// \param f The formula to normalize. /// \param negated If \c true, return the negative normal form of /// \c !f - formula* negative_normal_form(const formula* f, bool negated = false); + const formula* + negative_normal_form(const formula* f, bool negated = false); /// \brief Syntactic implication. /// diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index 51d0ad3d1..70c2d9a6c 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -33,7 +33,7 @@ namespace spot // E° class snf_visitor: public visitor { - formula* result_; + const formula* result_; snf_cache* cache_; public: @@ -41,27 +41,27 @@ namespace spot { } - formula* + const formula* result() const { return result_; } void - visit(atomic_prop*) + visit(const atomic_prop*) { assert(!"unexpected operator"); } void - visit(constant* c) + visit(const constant* c) { assert(c == constant::empty_word_instance()); result_ = constant::false_instance(); } void - visit(bunop* bo) + visit(const bunop* bo) { bunop::type op = bo->op(); switch (op) @@ -75,25 +75,25 @@ namespace spot } void - visit(unop*) + visit(const unop*) { assert(!"unexpected operator"); } void - visit(binop*) + visit(const binop*) { assert(!"unexpected operator"); } void - visit(automatop*) + visit(const automatop*) { assert(!"unexpected operator"); } void - visit(multop* mo) + visit(const multop* mo) { multop::type op = mo->op(); switch (op) @@ -134,14 +134,14 @@ namespace spot break; case multop::AndRat: // FIXME: Can we deal with AndRat in a better way - // when it accepts [*0]. + // when it accepts [*0]? result_ = mo->clone(); break; } } - formula* - recurse(formula* f) + const formula* + recurse(const formula* f) { if (!f->accepts_eword()) return f->clone(); @@ -164,11 +164,11 @@ namespace spot } - formula* + const formula* star_normal_form(const formula* sere, snf_cache* cache) { snf_visitor v(cache); - return v.recurse(const_cast(sere)); + return v.recurse(sere); } } diff --git a/src/ltlvisit/snf.hh b/src/ltlvisit/snf.hh index 34843943a..895831b6a 100644 --- a/src/ltlvisit/snf.hh +++ b/src/ltlvisit/snf.hh @@ -52,8 +52,8 @@ namespace spot /// /// \param sere the SERE to rewrite /// \param cache an optional cache - formula* star_normal_form(const formula* sere, - snf_cache* cache = 0); + const formula* star_normal_form(const formula* sere, + snf_cache* cache = 0); } } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 1fc33950a..eec5142aa 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -183,11 +183,11 @@ namespace spot // If the formula has the form (!b)[*], return b. static - formula* + const formula* strip_star_not(const formula* f) { - if (bunop* s = is_Star(f)) - if (unop* n = is_Not(s->child())) + if (const bunop* s = is_Star(f)) + if (const unop* n = is_Not(s->child())) return n->child(); return 0; } @@ -195,11 +195,11 @@ namespace spot // If the formula as position i in multop mo has the form // (!b)[*];b with b being a Boolean formula, return b. static - formula* + const formula* match_goto(const multop *mo, unsigned i) { assert(i + 1 < mo->size()); - formula* b = strip_star_not(mo->nth(i)); + const formula* b = strip_star_not(mo->nth(i)); if (!b || !b->is_boolean()) return 0; if (mo->nth(i + 1) == b) @@ -207,7 +207,7 @@ namespace spot return 0; } - class to_string_visitor: public const_visitor + class to_string_visitor: public visitor { public: to_string_visitor(std::ostream& os, @@ -301,13 +301,13 @@ namespace spot in_ratexp_ = true; top_level_ = true; { - multop* m = is_multop(bo->first(), multop::Concat); + const multop* m = is_multop(bo->first(), multop::Concat); if (m) { unsigned s = m->size(); if (m->nth(s - 1) == constant::true_instance()) { - formula* tmp = m->all_but(s - 1); + const formula* tmp = m->all_but(s - 1); tmp->accept(*this); tmp->destroy(); onelast = true; @@ -409,11 +409,11 @@ namespace spot switch (op) { case bunop::Star: - if (multop* mo = is_Concat(c)) + if (const multop* mo = is_Concat(c)) { unsigned s = mo->size(); if (s == 2) - if (formula* b = match_goto(mo, 0)) + if (const formula* b = match_goto(mo, 0)) { c = b; sugar = Goto; @@ -602,7 +602,7 @@ namespace spot if (i + 1 < max) { // Try to match (!b)[*];b - formula* b = match_goto(mo, i); + const formula* b = match_goto(mo, i); if (b) { emit_bunop_child(b); @@ -622,10 +622,10 @@ namespace spot continue; } // Try to match ((!b)[*];b)[*i..j];(!b)[*] - if (bunop* s = is_Star(mo->nth(i))) - if (formula* b2 = strip_star_not(mo->nth(i + 1))) - if (multop* sc = is_Concat(s->child())) - if (formula* b1 = match_goto(sc, 0)) + if (const bunop* s = is_Star(mo->nth(i))) + if (const formula* b2 = strip_star_not(mo->nth(i + 1))) + if (const multop* sc = is_Concat(s->child())) + if (const formula* b1 = match_goto(sc, 0)) if (b1 == b2) { emit_bunop_child(b1); @@ -754,7 +754,7 @@ namespace spot to_spin_string(const formula* f, std::ostream& os, bool full_parent) { // Remove xor, ->, and <-> first. - formula* fu = unabbreviate_logic(f); + const formula* fu = unabbreviate_logic(f); // Also remove W and M. f = unabbreviate_wm(fu); fu->destroy(); diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 7bbcd6cc2..8343e620b 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -37,7 +37,7 @@ namespace spot } void - unabbreviate_ltl_visitor::visit(unop* uo) + unabbreviate_ltl_visitor::visit(const unop* uo) { switch (uo->op()) { @@ -61,19 +61,19 @@ namespace spot } } - formula* - unabbreviate_ltl_visitor::recurse(formula* f) + const formula* + unabbreviate_ltl_visitor::recurse(const formula* f) { return unabbreviate_ltl(f); } - formula* + const formula* unabbreviate_ltl(const formula* f) { if (f->is_sugar_free_boolean() && f->is_sugar_free_ltl()) return f->clone(); unabbreviate_ltl_visitor v; - const_cast(f)->accept(v); + f->accept(v); return v.result(); } diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh index 8f07ef7c5..3afc58a86 100644 --- a/src/ltlvisit/tunabbrev.hh +++ b/src/ltlvisit/tunabbrev.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -53,9 +54,9 @@ namespace spot virtual ~unabbreviate_ltl_visitor(); using super::visit; - void visit(unop* uo); + void visit(const unop* uo); - formula* recurse(formula* f); + const formula* recurse(const formula* f); }; /// \brief Clone and rewrite a formula to remove most of the @@ -66,7 +67,7 @@ namespace spot /// /// This will also rewrite unary operators such as unop::F, /// and unop::G, using only binop::U, and binop::R. - formula* unabbreviate_ltl(const formula* f); + const formula* unabbreviate_ltl(const formula* f); } } diff --git a/src/ltlvisit/wmunabbrev.cc b/src/ltlvisit/wmunabbrev.cc index f16a6196a..1f6c0eb4e 100644 --- a/src/ltlvisit/wmunabbrev.cc +++ b/src/ltlvisit/wmunabbrev.cc @@ -44,10 +44,10 @@ namespace spot } using super::visit; - void visit(binop* bo) + void visit(const binop* bo) { - formula* f1 = recurse(bo->first()); - formula* f2 = recurse(bo->second()); + const formula* f1 = recurse(bo->first()); + const formula* f2 = recurse(bo->second()); binop::type op = bo->op(); switch (op) { @@ -76,7 +76,7 @@ namespace spot } } - virtual formula* recurse(formula* f) + virtual const formula* recurse(const formula* f) { if (f->is_boolean()) return f->clone(); @@ -86,11 +86,11 @@ namespace spot }; } - formula* + const formula* unabbreviate_wm(const formula* f) { unabbreviate_wm_visitor v; - return v.recurse(const_cast(f)); + return v.recurse(f); } } } diff --git a/src/ltlvisit/wmunabbrev.hh b/src/ltlvisit/wmunabbrev.hh index 3b1e90b26..4604fc2d5 100644 --- a/src/ltlvisit/wmunabbrev.hh +++ b/src/ltlvisit/wmunabbrev.hh @@ -37,7 +37,7 @@ namespace spot /// and a M b is replaced by b U (b & a). /// /// \ingroup ltl_rewriting - formula* unabbreviate_wm(const formula* f); + const formula* unabbreviate_wm(const formula* f); } } diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 5f7bdfda9..acc8a6b95 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -1,5 +1,6 @@ -/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -** de l'Epita (LRDE). +/* -*- coding: utf-8 -*- +** Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. ** @@ -34,7 +35,7 @@ #include "ltlast/constant.hh" #include "public.hh" - typedef std::pair pair; + typedef std::pair pair; } %parse-param {spot::neverclaim_parse_error_list& error_list} @@ -193,7 +194,7 @@ transition: else { spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(*$3, pel); + const spot::ltl::formula* f = spot::ltl::parse(*$3, pel); delete $3; for(spot::ltl::parse_error_list::const_iterator i = pel.begin(); i != pel.end(); ++i) diff --git a/src/sabatest/sabacomplementtgba.cc b/src/sabatest/sabacomplementtgba.cc index e9d50ee3c..852b9d982 100644 --- a/src/sabatest/sabacomplementtgba.cc +++ b/src/sabatest/sabacomplementtgba.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -68,10 +69,9 @@ int main(int argc, char* argv[]) spot::bdd_dict* dict = new spot::bdd_dict(); spot::tgba* a; - spot::ltl::formula* f1 = 0; spot::ltl::parse_error_list p1; - f1 = spot::ltl::parse(formula, p1); + const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1); if (spot::ltl::format_parse_errors(std::cerr, formula, p1)) return 2; diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index eb452d46c..bbd1a1c46 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -153,7 +154,7 @@ namespace spot // FIXME: We could be smarter and reuse unused "$n" numbers. s << ltl::to_string(i->second) << "$" << ++clone_counts[var]; - ltl::formula* f = + const ltl::formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); int res = register_acceptance_variable(f, for_me); diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 66e911ddf..d05e46a07 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -33,7 +33,7 @@ namespace spot namespace { - class formula_to_bdd_visitor: public ltl::const_visitor + class formula_to_bdd_visitor: public ltl::visitor { public: formula_to_bdd_visitor(bdd_dict* d, void* owner) @@ -183,7 +183,7 @@ namespace spot }; // Convert a BDD which is known to be a conjonction into a formula. - static ltl::formula* + static const ltl::formula* conj_to_formula(bdd b, const bdd_dict* d) { if (b == bddfalse) @@ -194,7 +194,7 @@ namespace spot int var = bdd_var(b); bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); assert(isi != d->var_formula_map.end()); - formula* res = isi->second->clone(); + const formula* res = isi->second->clone(); bdd high = bdd_high(b); if (high == bddfalse) diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 53cd55b9f..408e0f51f 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -207,7 +208,8 @@ namespace spot } bounds_t bounds; - for (taa_tgba::state_set::const_iterator i = s->begin(); i != s->end(); ++i) + for (taa_tgba::state_set::const_iterator i = s->begin(); + i != s->end(); ++i) bounds.push_back(std::make_pair((*i)->begin(), (*i)->end())); /// Sorting might make the cartesian product faster by not @@ -409,7 +411,7 @@ namespace spot return ltl::to_string(label); } - ltl::formula* + const ltl::formula* taa_tgba_formula::clone_if(const label_t& label) const { return label->clone(); diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 2ab039659..51b435747 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -346,7 +347,7 @@ namespace spot ~taa_tgba_formula(); protected: virtual std::string label_to_string(const label_t& label) const; - virtual ltl::formula* clone_if(const label_t& label) const; + virtual const ltl::formula* clone_if(const label_t& label) const; }; } diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 6ce0fb967..b13ebb82f 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -35,7 +35,7 @@ namespace spot using namespace ltl; /// \brief Recursively translate a formula into a BDD. - class eltl_trad_visitor : public const_visitor + class eltl_trad_visitor : public visitor { public: eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) @@ -185,9 +185,9 @@ namespace spot bdd finish = bddfalse; bdd acc = bddtrue; - std::vector v; + std::vector v; for (unsigned i = 0; i < node->size(); ++i) - v.push_back(const_cast(node->nth(i))); + v.push_back(node->nth(i)); std::pair vp = recurse_state(node->get_nfa(), @@ -234,7 +234,7 @@ namespace spot std::pair& recurse_state(const nfa::ptr& nfa, const nfa::state* s, - const std::vector& v, + const std::vector& v, nmap& m, bdd& acc, bdd& finish) { bool is_loop = nfa->is_loop(); diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 4ad623479..82f8bfded 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -35,7 +35,7 @@ namespace spot using namespace ltl; /// \brief Recursively translate a formula into a TAA. - class ltl2taa_visitor : public const_visitor + class ltl2taa_visitor : public visitor { public: ltl2taa_visitor(taa_tgba_formula* res, language_containment_checker* lcc, @@ -216,7 +216,7 @@ namespace spot std::vector u; // Union std::vector a; // Acceptance conditions std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end())); - formula* f = i1->condition->clone(); // Refined rule + const formula* f = i1->condition->clone(); // Refined rule if (!refined_ || !contained) { std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end())); @@ -394,8 +394,7 @@ namespace spot { std::vector u; // Union std::vector a; // Acceptance conditions - formula* f = constant::true_instance(); - formula* g = 0; + const formula* f = constant::true_instance(); for (unsigned i = 0; i < vs.size(); ++i) { if (vs[i].succ_.empty()) @@ -405,7 +404,7 @@ namespace spot f = multop::instance(multop::And, ss.condition->clone(), f); for (unsigned i = 0; i < ss.acc.size(); ++i) { - g = ss.acc[i]->clone(); + const formula* g = ss.acc[i]->clone(); a.push_back(g); to_free_.push_back(g); } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 8ddb13724..fc51ff2b5 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -190,7 +190,7 @@ namespace spot return os; } - formula* + const formula* var_to_formula(int var) const { vf_map::const_iterator isi = next_formula_map.find(var); @@ -216,7 +216,7 @@ namespace spot return res; } - formula* + const formula* conj_bdd_to_formula(bdd b, multop::type op = multop::And) const { if (b == bddfalse) @@ -225,7 +225,7 @@ namespace spot while (b != bddtrue) { int var = bdd_var(b); - formula* res = var_to_formula(var); + const formula* res = var_to_formula(var); bdd high = bdd_high(b); if (high == bddfalse) { @@ -243,13 +243,13 @@ namespace spot return multop::instance(op, v); } - formula* + const formula* conj_bdd_to_sere(bdd b) const { return conj_bdd_to_formula(b, multop::AndRat); } - formula* + const formula* bdd_to_formula(bdd f) { if (f == bddfalse) @@ -265,7 +265,7 @@ namespace spot return multop::instance(multop::Or, v); } - formula* + const formula* bdd_to_sere(bdd f) { if (f == bddfalse) @@ -297,7 +297,7 @@ namespace spot } else { - formula* ac = var_to_formula(var); + const formula* ac = var_to_formula(var); if (!a->has_acceptance_condition(ac)) a->declare_acceptance_condition(ac->clone()); @@ -369,14 +369,14 @@ namespace spot using postfix_visitor::doit; virtual void - doit(unop* node) + doit(const unop* node) { if (node->op() == unop::F) res_ &= bdd_ithvar(dict_.register_a_variable(node->child())); } virtual void - doit(binop* node) + doit(const binop* node) { if (node->op() == binop::U) res_ &= bdd_ithvar(dict_.register_a_variable(node->second())); @@ -388,15 +388,15 @@ namespace spot }; bdd translate_ratexp(const formula* f, translate_dict& dict, - formula* to_concat = 0); + const formula* to_concat = 0); // Rewrite rule for rational operators. - class ratexp_trad_visitor: public const_visitor + class ratexp_trad_visitor: public visitor { public: // negated should only be set for constants or atomic properties ratexp_trad_visitor(translate_dict& dict, - formula* to_concat = 0) + const formula* to_concat = 0) : dict_(dict), to_concat_(to_concat) { } @@ -451,15 +451,15 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_sere(dest_bdd); + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest == constant::empty_word_instance()) { out |= label & next_to_concat(); } else { - formula* dest2 = multop::instance(multop::Concat, dest, - to_concat_->clone()); + const formula* dest2 = multop::instance(multop::Concat, dest, + to_concat_->clone()); if (dest2 != constant::false_instance()) { int x = dict_.register_next_variable(dest2); @@ -528,7 +528,7 @@ namespace spot void visit(const bunop* bo) { - formula* f; + const formula* f; unsigned min = bo->min(); unsigned max = bo->max(); @@ -578,8 +578,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_sere(dest_bdd); - formula* dest2; + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); int x; if (dest == constant::empty_word_instance()) { @@ -588,8 +587,9 @@ namespace spot } else { - dest2 = multop::instance(multop::Concat, dest, - f->clone()); + const formula* + dest2 = multop::instance(multop::Concat, dest, + f->clone()); if (dest2 != constant::false_instance()) { x = dict_.register_next_variable(dest2); @@ -644,7 +644,7 @@ namespace spot { delete non_final; // (a* & b*);c = (a*|b*);c - formula* f = multop::instance(multop::OrRat, final); + const formula* f = multop::instance(multop::OrRat, final); res_ = recurse_and_concat(f); f->destroy(); break; @@ -656,17 +656,22 @@ namespace spot // (F_1 & ... & F_n & N_1 & ... & N_m) // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] - formula* f = multop::instance(multop::OrRat, final); - formula* n = multop::instance(multop::AndNLM, non_final); - formula* t = bunop::instance(bunop::Star, - constant::true_instance()); - formula* ft = multop::instance(multop::Concat, - f->clone(), t->clone()); - formula* nt = multop::instance(multop::Concat, - n->clone(), t); - formula* ftn = multop::instance(multop::AndRat, ft, n); - formula* fnt = multop::instance(multop::AndRat, f, nt); - formula* all = multop::instance(multop::OrRat, ftn, fnt); + const formula* f = + multop::instance(multop::OrRat, final); + const formula* n = + multop::instance(multop::AndNLM, non_final); + const formula* t = + bunop::instance(bunop::Star, constant::true_instance()); + const formula* ft = + multop::instance(multop::Concat, f->clone(), t->clone()); + const formula* nt = + multop::instance(multop::Concat, n->clone(), t); + const formula* ftn = + multop::instance(multop::AndRat, ft, n); + const formula* fnt = + multop::instance(multop::AndRat, f, nt); + const formula* all = + multop::instance(multop::OrRat, ftn, fnt); res_ = recurse_and_concat(all); all->destroy(); break; @@ -680,7 +685,7 @@ namespace spot // N_1 && (N_2;[*]) && ... && (N_n;[*]) // | (N_1;[*]) && N_2 && ... && (N_n;[*]) // | (N_1;[*]) && (N_2;[*]) && ... && N_n - formula* star = + const formula* star = bunop::instance(bunop::Star, constant::true_instance()); multop::vec* disj = new multop::vec; for (unsigned n = 0; n < s; ++n) @@ -688,7 +693,7 @@ namespace spot multop::vec* conj = new multop::vec; for (unsigned m = 0; m < s; ++m) { - formula* f = node->nth(m)->clone(); + const formula* f = node->nth(m)->clone(); if (n != m) f = multop::instance(multop::Concat, f, star->clone()); @@ -697,7 +702,7 @@ namespace spot disj->push_back(multop::instance(multop::AndRat, conj)); } star->destroy(); - formula* all = multop::instance(multop::OrRat, disj); + const formula* all = multop::instance(multop::OrRat, disj); res_ = recurse_and_concat(all); all->destroy(); break; @@ -757,7 +762,7 @@ namespace spot bdd res = recurse(node->nth(0)); // the tail - formula* tail = node->all_but(0); + const formula* tail = node->all_but(0); bdd tail_bdd; bool tail_computed = false; @@ -770,7 +775,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_sere(dest_bdd); + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest->accepts_eword()) { @@ -790,11 +795,11 @@ namespace spot // If the destination is not a constant, it // means it can have successors. Fusion the // tail and append anything to concatenate. - formula* dest2 = multop::instance(multop::Fusion, dest, - tail->clone()); + const formula* dest2 = + multop::instance(multop::Fusion, dest, tail->clone()); if (to_concat_) dest2 = multop::instance(multop::Concat, dest2, - to_concat_->clone()); + to_concat_->clone()); if (dest2 != constant::false_instance()) { int x = dict_.register_next_variable(dest2); @@ -814,7 +819,7 @@ namespace spot } bdd - recurse(const formula* f, formula* to_concat = 0) + recurse(const formula* f, const formula* to_concat = 0) { return translate_ratexp(f, dict_, to_concat); } @@ -829,12 +834,12 @@ namespace spot private: translate_dict& dict_; bdd res_; - formula* to_concat_; + const formula* to_concat_; }; bdd translate_ratexp(const formula* f, translate_dict& dict, - formula* to_concat) + const formula* to_concat) { // static unsigned indent = 0; // for (unsigned i = indent; i > 0; --i) @@ -1049,7 +1054,7 @@ namespace spot // The rewrite rules used here are adapted from Jean-Michel // Couvreur's FM paper, augmented to support rational operators. - class ltl_trad_visitor: public const_visitor + class ltl_trad_visitor: public visitor { public: ltl_trad_visitor(translate_dict& dict, bool mark_all = false, @@ -1200,8 +1205,7 @@ namespace spot } else { - formula* dest2 = - unop::instance(op, const_cast(dest)); + const formula* dest2 = unop::instance(op, dest); if (dest2 == constant::false_instance()) continue; int x = dict_.register_next_variable(dest2); @@ -1241,7 +1245,7 @@ namespace spot bdd label = bdd_satoneset(all_props, var_set, bddtrue); all_props -= label; - formula* dest = + const formula* dest = dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); // !{ Exp } is false if Exp accepts the empty word. @@ -1369,7 +1373,7 @@ namespace spot bdd label = bdd_satoneset(all_props, var_set, bddtrue); all_props -= label; - formula* dest = + const formula* dest = dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); @@ -1394,7 +1398,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_sere(dest_bdd); + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest == constant::empty_word_instance()) { @@ -1402,8 +1406,8 @@ namespace spot } else { - formula* dest2 = binop::instance(op, dest, - node->second()->clone()); + const formula* dest2 = + binop::instance(op, dest, node->second()->clone()); if (dest2 != constant::false_instance()) { int x = dict_.register_next_variable(dest2); @@ -1443,8 +1447,8 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_sere(dest_bdd); - formula* dest2 = + const formula* dest = dict_.conj_bdd_to_sere(dest_bdd); + const formula* dest2 = binop::instance(op, dest, node->second()->clone()); bdd udest = @@ -1563,7 +1567,7 @@ namespace spot // Check whether a formula has a R, W, or G operator at its // top-level (preceding logical operators do not count). - class ltl_possible_fair_loop_visitor: public const_visitor + class ltl_possible_fair_loop_visitor: public visitor { public: ltl_possible_fair_loop_visitor() @@ -1737,13 +1741,13 @@ namespace spot { bdd label = bdd_exist(cube, d_.next_set); bdd dest_bdd = bdd_existcomp(cube, d_.next_set); - formula* dest = + const formula* dest = d_.conj_bdd_to_formula(dest_bdd); // Handle a Miyano-Hayashi style unrolling for // rational operators. Marked nodes correspond to // subformulae in the Miyano-Hayashi set. - formula* tmp = d_.mt.simplify_mark(dest); + const formula* tmp = d_.mt.simplify_mark(dest); dest->destroy(); dest = tmp; @@ -1759,7 +1763,7 @@ namespace spot // We have no marked operators, but still // have other rational operator to check. // Start a new marked cycle. - formula* dest2 = d_.mt.mark_concat_ops(dest); + const formula* dest2 = d_.mt.mark_concat_ops(dest); dest->destroy(); dest = dest2; } @@ -1864,7 +1868,7 @@ namespace spot bool fair_loop_approx, const atomic_prop_set* unobs, ltl_simplifier* simplifier) { - formula* f2; + const formula* f2; ltl_simplifier* s = simplifier; // Simplify the formula, if requested. @@ -1942,7 +1946,7 @@ namespace spot // This is in case the initial state is equivalent to true... if (symb_merge) - f2 = const_cast(fc.canonize(f2)); + f2 = fc.canonize(f2); formulae_to_translate.insert(f2); a->set_init_state(f2); @@ -2043,7 +2047,7 @@ namespace spot // Simplify the formula, if requested. if (simplifier) { - formula* tmp = simplifier->simplify(dest); + const formula* tmp = simplifier->simplify(dest); dest->destroy(); dest = tmp; // Ignore the arc if the destination reduces to false. @@ -2072,9 +2076,7 @@ namespace spot succs[label] = dest; else si->second = - multop::instance(multop::Or, - const_cast(si->second), - const_cast(dest)); + multop::instance(multop::Or, si->second, dest); } } if (branching_postponement) diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index dcd360885..ac5bf99cb 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -41,7 +41,7 @@ namespace spot /// /// The algorithm used here is adapted from Jean-Michel Couvreur's /// Probataf tool. - class ltl_trad_visitor: public const_visitor + class ltl_trad_visitor: public visitor { public: ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 0cd19a9da..9d83a8e1d 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -648,7 +648,8 @@ namespace spot { assert(f); - ltl::formula* neg_f = ltl::unop::instance(ltl::unop::Not, f->clone()); + const ltl::formula* neg_f = + ltl::unop::instance(ltl::unop::Not, f->clone()); aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict()); neg_f->destroy(); diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 08e86afd4..00be4b495 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -116,7 +117,7 @@ namespace spot bdd allneg = bddtrue; for (int i = 0; i < n_acc; ++i) { - ltl::formula* f = env->require(acc(i)); + const ltl::formula* f = env->require(acc(i)); int v = dict->register_acceptance_variable(f, res); res->declare_acceptance_condition(f); allneg &= bdd_nithvar(v); diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 2956bbb48..da4517c59 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -1,8 +1,9 @@ -/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -** de l'Epita (LRDE). +/* -*- coding: utf-8 -*- +** Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -** Université Pierre et Marie Curie. +** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +** Université Pierre et Marie Curie. ** ** This file is part of Spot, a model checking library. ** @@ -49,8 +50,8 @@ typedef std::map formula_cache; { int token; std::string* str; - spot::ltl::formula* f; - std::list* list; + const spot::ltl::formula* f; + std::list* list; } %code @@ -80,7 +81,7 @@ typedef std::pair pair; %destructor { delete $$; } %destructor { - for (std::list::iterator i = $$->begin(); + for (std::list::iterator i = $$->begin(); i != $$->end(); ++i) (*i)->destroy(); delete $$; @@ -113,14 +114,15 @@ line: strident ',' strident ',' condition ',' acc_list ';' if (i == fcache.end()) { parse_error_list pel; - formula* f = spot::ltl::parse(*$5, pel, parse_environment); + const formula* f = + spot::ltl::parse(*$5, pel, parse_environment); for (parse_error_list::iterator i = pel.begin(); i != pel.end(); ++i) { // Adjust the diagnostic to the current position. location here = @5; here.end.line = here.begin.line + i->first.end.line - 1; - here.end.column = + here.end.column = here.begin.column + i->first.end.column; here.begin.line += i->first.begin.line - 1; here.begin.column += i->first.begin.column; @@ -139,7 +141,7 @@ line: strident ',' strident ',' condition ',' acc_list ';' } delete $5; } - std::list::iterator i; + std::list::iterator i; for (i = $7->begin(); i != $7->end(); ++i) result->add_acceptance_condition(t, *i); delete $1; @@ -170,7 +172,7 @@ condition: acc_list: { - $$ = new std::list; + $$ = new std::list; } | acc_list strident { @@ -180,7 +182,7 @@ acc_list: } else if (*$2 != "" && *$2 != "false") { - formula* f = parse_envacc.require(*$2); + const formula* f = parse_envacc.require(*$2); if (! result->has_acceptance_condition(f)) { error_list.push_back(spot::tgba_parse_error(@2, @@ -200,7 +202,7 @@ acc_list: acc_decl: | acc_decl strident { - formula* f = parse_envacc.require(*$2); + const formula* f = parse_envacc.require(*$2); if (! f) { std::string s = "acceptance condition `"; diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 3217af462..6db9df3dd 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -162,7 +162,7 @@ int main(int argc, char* argv[]) else if (print_formula) { spot::tgba* a; - spot::ltl::formula* f1 = 0; + const spot::ltl::formula* f1 = 0; spot::ltl::parse_error_list p1; f1 = spot::ltl::parse(file, p1); @@ -186,7 +186,7 @@ int main(int argc, char* argv[]) else if (stats) { spot::tgba* a; - spot::ltl::formula* f1 = 0; + const spot::ltl::formula* f1 = 0; if (formula) { @@ -247,7 +247,7 @@ int main(int argc, char* argv[]) delete a; if (formula) { - spot::ltl::formula* nf1 = + const spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone()); spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict); @@ -266,14 +266,14 @@ int main(int argc, char* argv[]) else { spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(file, p1); + const spot::ltl::formula* f1 = spot::ltl::parse(file, p1); if (spot::ltl::format_parse_errors(std::cerr, file, p1)) return 2; spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict); - spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, - f1->clone()); + const spot::ltl::formula* nf1 = + spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone()); spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba* nAf; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 58564f0c0..6afebe86a 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -659,7 +659,7 @@ main(int argc, char** argv) while (tok) { unobservables->insert - (static_cast(env.require(tok))); + (static_cast(env.require(tok))); tok = strtok(0, ", \t;"); } } @@ -730,7 +730,7 @@ main(int argc, char** argv) input = argv[formula_index]; } - spot::ltl::formula* f = 0; + const spot::ltl::formula* f = 0; if (!from_file) // Reading a formula, not reading an automaton from a file. { switch (translation) @@ -825,7 +825,7 @@ main(int argc, char** argv) if (simp) { tm.start("reducing formula"); - spot::ltl::formula* t = simp->simplify(f); + const spot::ltl::formula* t = simp->simplify(f); f->destroy(); tm.stop("reducing formula"); f = t; diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 7eb66e178..bb1b9b7af 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -49,13 +50,13 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) return 2; spot::ltl::parse_error_list pel2; - spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env); + const spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env); if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2)) return 2; diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index 3b00174f1..eace6ef2a 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -52,7 +53,7 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) return 2; diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index f9b7617b3..55dc8c05f 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -487,7 +487,7 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string s) std::cout << std::setiosflags(old); } -spot::ltl::formula* +const spot::ltl::formula* generate_formula(const spot::ltl::random_ltl& rl, spot::ltl::ltl_simplifier& simp, int opt_f, int opt_s, @@ -499,14 +499,14 @@ generate_formula(const spot::ltl::random_ltl& rl, while (max_tries_u--) { spot::srand(opt_s++); - spot::ltl::formula* f; + const spot::ltl::formula* f; int max_tries_l = 1000; while (max_tries_l--) { f = rl.generate(opt_f); if (opt_l) { - spot::ltl::formula* g = simp.simplify(f); + const spot::ltl::formula* g = simp.simplify(f); f->destroy(); if (spot::ltl::length(g) < opt_l) { @@ -788,7 +788,7 @@ main(int argc, char** argv) } else { - ap->insert(static_cast + ap->insert(static_cast (env.require(argv[argn]))); } } @@ -853,9 +853,8 @@ main(int argc, char** argv) { if (opt_F) { - spot::ltl::formula* f = generate_formula(rl, simp, - opt_f, opt_ec_seed, - opt_l, opt_u); + const spot::ltl::formula* f = + generate_formula(rl, simp, opt_f, opt_ec_seed, opt_l, opt_u); if (!f) exit(1); formula = spot::ltl_to_tgba_fm(f, dict, true); @@ -871,7 +870,7 @@ main(int argc, char** argv) else if (input == "") break; spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(input, pel, env); + const spot::ltl::formula* f = spot::ltl::parse(input, pel, env); if (spot::ltl::format_parse_errors(std::cerr, input, pel)) { exit_code = 1; @@ -882,7 +881,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(dynamic_cast ((*i)->clone())); f->destroy(); delete tmp; @@ -897,7 +896,7 @@ main(int argc, char** argv) for (spot::ltl::atomic_prop_set::iterator i = ap->begin(); i != ap->end(); ++i) - apf->insert(dynamic_cast((*i)->clone())); + apf->insert(static_cast((*i)->clone())); if (!opt_S) { diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc deleted file mode 100644 index f60d79b84..000000000 --- a/src/tgbatest/reductgba.cc +++ /dev/null @@ -1,179 +0,0 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include - -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgbaalgos/reductgba_sim.hh" -#include "tgba/tgbareduc.hh" - -#include "ltlast/allnodes.hh" -#include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgba/bddprint.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/lbtt.hh" -#include "tgba/tgbatba.hh" -#include "tgbaalgos/magic.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/gtec/ce.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/dupexp.hh" -#include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/sccfilter.hh" - -#include "misc/escape.hh" - -void -syntax(char* prog) -{ -#ifdef REDUCCMP - std::cerr << prog << " option file" << std::endl; -#else - std::cerr << prog << " option formula" << std::endl; -#endif - exit(2); -} - -int -main(int argc, char** argv) -{ - if (argc < 3) - syntax(argv[0]); - - int o = spot::Reduce_None; - switch (atoi(argv[1])) - { - case 0: - o = spot::Reduce_Scc; - break; - case 1: - o = spot::Reduce_quotient_Dir_Sim; - break; - case 2: - o = spot::Reduce_transition_Dir_Sim; - break; - case 3: - o = spot::Reduce_quotient_Del_Sim; - break; - case 4: - o = spot::Reduce_transition_Del_Sim; - break; - case 5: - o = spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim | - spot::Reduce_Scc; - break; - case 6: - o = spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim | - spot::Reduce_Scc; - break; - case 7: - // No Reduction - break; - default: - return 2; - } - - int exit_code = 0; - spot::direct_simulation_relation* rel_dir = 0; - spot::delayed_simulation_relation* rel_del = 0; - spot::tgba* automata = 0; - spot::tgba_reduc* automatareduc = 0; - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::bdd_dict* dict = new spot::bdd_dict(); - -#ifdef REDUCCMP - spot::tgba_parse_error_list pel; - automata = spot::tgba_parse(argv[2], pel, dict, env, env, false); - if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel)) - return 2; -#else - spot::ltl::parse_error_list p1; - spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env); - if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) - return 2; - automata = spot::ltl_to_tgba_fm(f, dict, - false, true, - false, true); -#endif - - spot::dotty_reachable(std::cout, automata); - automatareduc = new spot::tgba_reduc(automata); - - if (o & spot::Reduce_quotient_Dir_Sim) - { - rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout); - automatareduc->quotient_state(rel_dir); - } - else if (o & spot::Reduce_quotient_Del_Sim) - { - std::cout << "get delayed" << std::endl; - rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout); - std::cout << "quotient state" << std::endl; - automatareduc->quotient_state(rel_del); - std::cout << "end" << std::endl; - } - - if (rel_dir != 0) - { - automatareduc->display_rel_sim(rel_dir, std::cout); - spot::free_relation_simulation(rel_dir); - } - - if (rel_del != 0) - { - automatareduc->display_rel_sim(rel_del, std::cout); - spot::free_relation_simulation(rel_del); - } - - spot::tgba* res = automatareduc; - - if (o & spot::Reduce_Scc) - { - res = spot::scc_filter(automatareduc); - delete automatareduc; - } - - spot::dotty_reachable(std::cout, res); - - delete res; - delete automata; -#ifndef REDUCCMP - if (f != 0) - f->destroy(); -#endif - - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - - if (dict != 0) - delete dict; - - return exit_code; -}