diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 7781d4bbf..ecfc2cfc6 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -85,18 +85,6 @@ namespace spot v.visit(this); } - const std::string& - atomic_prop::name() const - { - return name_; - } - - environment& - atomic_prop::env() const - { - return *env_; - } - atomic_prop::map atomic_prop::instances; const atomic_prop* diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 75ea65b12..4282427c4 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2012, 2013, 2014 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 @@ -49,9 +49,16 @@ namespace spot virtual void accept(visitor& visitor) const; /// Get the name of the atomic proposition. - const std::string& name() const; + const std::string& name() const + { + return name_; + } + /// Get the environment of the atomic proposition. - environment& env() const; + environment& env() const + { + return *env_; + } /// Return a canonic representation of the atomic proposition virtual std::string dump() const; diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 54d8b7078..3f628c3bf 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -// Recherche et Développement de l'Epita (LRDE) +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +// de Recherche et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -30,6 +30,8 @@ namespace spot automatop::automatop(const nfa::ptr nfa, vec* v, bool negated) : ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated) { + assert(nfa); + is.boolean = false; is.sugar_free_boolean = true; is.in_nenoform = true; @@ -64,7 +66,8 @@ namespace spot instances.erase(i); // Dereference children. - for (unsigned n = 0; n < size(); ++n) + unsigned s = size(); + for (unsigned n = 0; n < s; ++n) nth(n)->destroy(); delete children_; @@ -115,31 +118,6 @@ namespace spot return res; } - unsigned - automatop::size() const - { - return children_->size(); - } - - const formula* - automatop::nth(unsigned n) const - { - return (*children_)[n]; - } - - const spot::ltl::nfa::ptr - automatop::get_nfa() const - { - assert(nfa_ != 0); - return nfa_; - } - - bool - automatop::is_negated() const - { - return negated_; - } - unsigned automatop::instance_count() { diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index 27c1c37eb..eaeac3835 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -52,18 +52,31 @@ namespace spot virtual void accept(visitor& v) const; - /// Get the number of argument. - unsigned size() const; + /// Get the number of arguments. + unsigned size() const + { + return children_->size(); + } + /// \brief Get the nth argument. /// /// Starting with \a n = 0. - const formula* nth(unsigned n) const; + const formula* nth(unsigned n) const + { + return (*children_)[n]; + } /// Get the NFA of this operator. - const spot::ltl::nfa::ptr get_nfa() const; + const spot::ltl::nfa::ptr get_nfa() const + { + return nfa_; + } /// Whether the automaton is negated. - bool is_negated() const; + bool is_negated() const + { + return negated_; + } /// Return a canonic representation of the atomic proposition std::string dump() const; diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 82bb3efa5..e2faf9031 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -275,24 +275,6 @@ namespace spot v.visit(this); } - const formula* - binop::first() const - { - return first_; - } - - const formula* - binop::second() const - { - return second_; - } - - binop::type - binop::op() const - { - return op_; - } - const char* binop::op_name() const { diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index d47a6c181..21b69bc0c 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -112,12 +112,23 @@ namespace spot virtual void accept(visitor& v) const; /// Get the first operand. - const formula* first() const; + const formula* first() const + { + return first_; + } + /// Get the second operand. - const formula* second() const; + const formula* second() const + { + return second_; + } /// Get the type of this operator. - type op() const; + type op() const + { + return op_; + } + /// Get the type of this operator, as a string. const char* op_name() const; diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index e4372cdcf..c5bb78491 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -100,30 +100,6 @@ namespace spot v.visit(this); } - const formula* - bunop::child() const - { - return child_; - } - - unsigned - bunop::min() const - { - return min_; - } - - unsigned - bunop::max() const - { - return max_; - } - - bunop::type - bunop::op() const - { - return op_; - } - const char* bunop::op_name() const { diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 81e087bac..f37b2bc15 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -87,12 +87,22 @@ namespace spot virtual void accept(visitor& v) const; /// Get the sole operand of this operator. - const formula* child() const; + const formula* child() const + { + return child_; + } /// Minimum number of repetition. - unsigned min() const; + unsigned min() const + { + return min_; + } + /// Minimum number of repetition. - unsigned max() const; + unsigned max() const + { + return max_; + } /// \brief A string representation of the operator. /// @@ -100,7 +110,11 @@ namespace spot std::string format() const; /// Get the type of this operator. - type op() const; + type op() const + { + return op_; + } + /// Get the type of this operator, as a string. const char* op_name() const; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 0d2699a22..3ead65b9a 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -111,12 +111,6 @@ namespace spot v.visit(this); } - constant::type - constant::val() const - { - return val_; - } - const char* constant::val_name() const { diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 41ef4250c..96d018c70 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // // This file is part of Spot, a model checking library. @@ -39,7 +39,11 @@ namespace spot virtual void accept(visitor& v) const; /// Return the value of the constant. - type val() const; + type val() const + { + return val_; + } + /// Return the value of the constant as a string. const char* val_name() const; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 93d923ade..77ada7672 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -100,7 +100,8 @@ namespace spot instances.erase(i); // Dereference children. - for (unsigned n = 0; n < size(); ++n) + unsigned s = size(); + for (unsigned n = 0; n < s; ++n) nth(n)->destroy(); delete children_; @@ -124,18 +125,6 @@ namespace spot v.visit(this); } - unsigned - multop::size() const - { - return children_->size(); - } - - const formula* - multop::nth(unsigned n) const - { - return (*children_)[n]; - } - const formula* multop::all_but(unsigned n) const { @@ -176,12 +165,6 @@ namespace spot return instance(op_, v); } - multop::type - multop::op() const - { - return op_; - } - const char* multop::op_name() const { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 550fedd87..a2a970964 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -125,11 +125,18 @@ namespace spot virtual void accept(visitor& v) const; /// Get the number of children. - unsigned size() const; + unsigned size() const + { + return children_->size(); + } + /// \brief Get the nth child. /// /// Starting with \a n = 0. - const formula* nth(unsigned n) const; + const formula* nth(unsigned n) const + { + return (*children_)[n]; + } /// \brief construct a formula without the nth child. /// @@ -156,7 +163,11 @@ namespace spot const formula* boolean_operands(unsigned* width = 0) const; /// Get the type of this operator. - type op() const; + type op() const + { + return op_; + } + /// Get the type of this operator, as a string. const char* op_name() const; diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 72df2f9d9..49e523413 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -167,18 +167,6 @@ namespace spot v.visit(this); } - const formula* - unop::child() const - { - return child_; - } - - unop::type - unop::op() const - { - return op_; - } - const char* unop::op_name() const { diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 4f2843571..c861f2595 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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. @@ -91,10 +91,17 @@ namespace spot virtual void accept(visitor& v) const; /// Get the sole operand of this operator. - const formula* child() const; + const formula* child() const + { + return child_; + } /// Get the type of this operator. - type op() const; + type op() const + { + return op_; + } + /// Get the type of this operator, as a string. const char* op_name() const;