formula.hh 5.63 KB
 Alexandre Duret-Lutz committed Jan 03, 2005 1 ``````// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed Nov 21, 2003 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````// 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. `````` Alexandre Duret-Lutz committed Aug 09, 2004 22 23 ``````/// \file ltlast/formula.hh /// \brief LTL formula interface `````` Alexandre Duret-Lutz committed Jan 03, 2005 24 25 ``````#ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH `````` Alexandre Duret-Lutz committed Apr 15, 2003 26 `````` `````` Alexandre Duret-Lutz committed Jan 20, 2005 27 28 ``````#include #include `````` Alexandre Duret-Lutz committed Apr 15, 2003 29 30 ``````#include "predecl.hh" `````` Alexandre Duret-Lutz committed May 15, 2003 31 ``````namespace spot `````` Alexandre Duret-Lutz committed Apr 15, 2003 32 ``````{ `````` Alexandre Duret-Lutz committed May 15, 2003 33 `````` namespace ltl `````` Alexandre Duret-Lutz committed Apr 15, 2003 34 `````` { `````` Alexandre Duret-Lutz committed Nov 17, 2004 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 `````` /// \defgroup ltl LTL formulae /// /// This module gathers types and definitions related to LTL formulae. /// \addtogroup ltl_essential Essential LTL types /// \ingroup ltl /// \addtogroup ltl_ast LTL Abstract Syntax Tree /// \ingroup ltl /// \addtogroup ltl_environment LTL environments /// \ingroup ltl /// LTL environment implementations. /// \addtogroup ltl_algorithm Algorithms for LTL formulae /// \ingroup ltl /// \addtogroup ltl_io Input/Output of LTL formulae /// \ingroup ltl_algorithm /// \addtogroup ltl_visitor Derivable visitors /// \ingroup ltl_algorithm /// \addtogroup ltl_rewriting Rewriting LTL formulae /// \ingroup ltl_algorithm /// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae /// \ingroup ltl_algorithm `````` Alexandre Duret-Lutz committed Apr 15, 2003 64 `````` `````` Alexandre Duret-Lutz committed Apr 18, 2003 65 `````` /// \brief An LTL formula. `````` Alexandre Duret-Lutz committed Nov 17, 2004 66 67 `````` /// \ingroup ltl_essential /// \ingroup ltl_ast `````` Alexandre Duret-Lutz committed May 15, 2003 68 69 `````` /// /// The only way you can work with a formula is to `````` Alexandre Duret-Lutz committed Apr 18, 2003 70 `````` /// build a spot::ltl::visitor or spot::ltl::const_visitor. `````` Alexandre Duret-Lutz committed May 15, 2003 71 `````` class formula `````` Alexandre Duret-Lutz committed Apr 15, 2003 72 73 `````` { public: `````` Alexandre Duret-Lutz committed Jun 26, 2003 74 `````` /// Entry point for vspot::ltl::visitor instances. `````` Alexandre Duret-Lutz committed Apr 15, 2003 75 `````` virtual void accept(visitor& v) = 0; `````` Alexandre Duret-Lutz committed Jun 26, 2003 76 `````` /// Entry point for vspot::ltl::const_visitor instances. `````` Alexandre Duret-Lutz committed Apr 15, 2003 77 `````` virtual void accept(const_visitor& v) const = 0; `````` Alexandre Duret-Lutz committed May 15, 2003 78 `````` `````` Alexandre Duret-Lutz committed Aug 19, 2003 79 80 81 82 83 84 `````` /// \brief clone this node /// /// This increments the reference counter of this node (if one is /// used). You should almost never use this method directly as /// it doesn't touch the children. If you want to clone a /// whole formula, use spot::ltl::clone() instead. `````` Alexandre Duret-Lutz committed May 15, 2003 85 `````` formula* ref(); `````` Alexandre Duret-Lutz committed Aug 19, 2003 86 87 88 89 90 91 `````` /// \brief release this node /// /// This decrements the reference counter of this node (if one is /// used) and can free the object. You should almost never use /// this method directly as it doesn't touch the children. If you /// want to release a whole formula, use spot::ltl::destroy() instead. `````` Alexandre Duret-Lutz committed May 15, 2003 92 93 `````` static void unref(formula* f); `````` Alexandre Duret-Lutz committed Jan 20, 2005 94 95 96 97 98 99 100 101 102 `````` /// Return a canonic representation of the formula const std::string& dump() const; /// Return a hash_key for the formula. const size_t hash() const { return hash_key_; } `````` Alexandre Duret-Lutz committed May 15, 2003 103 `````` protected: `````` Alexandre Duret-Lutz committed Nov 02, 2004 104 105 `````` virtual ~formula(); `````` Alexandre Duret-Lutz committed May 15, 2003 106 107 108 `````` /// \brief increment reference counter if any virtual void ref_(); /// \brief decrement reference counter if any, return true when `````` Alexandre Duret-Lutz committed Jun 26, 2003 109 `````` /// the instance must be deleted (usually when the counter hits 0). `````` Alexandre Duret-Lutz committed May 15, 2003 110 `````` virtual bool unref_(); `````` Alexandre Duret-Lutz committed Jan 20, 2005 111 112 113 114 115 116 117 118 119 120 121 `````` /// \brief Compute key_ from dump_. /// /// Should be called once in each object, after dump_ has been set. void set_key_(); /// The canonic representation of the formula std::string dump_; /// \brief The hash key of this formula. /// /// Initialized by set_key_(). size_t hash_key_; `````` Alexandre Duret-Lutz committed Apr 15, 2003 122 123 `````` }; `````` Alexandre Duret-Lutz committed Jan 20, 2005 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 `````` /// \brief Strict Weak Ordering for const formula*. /// \ingroup ltl_essentials /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type const formula*. /// /// For instance here is how one could declare /// a map of \c const::formula*. /// \code /// // Remember how many times each formula has been seen. /// std::map seen; /// \endcode struct formula_ptr_less_than: public std::binary_function { bool operator()(const formula* left, const formula* right) const { assert(left); assert(right); `````` Alexandre Duret-Lutz committed Jan 20, 2005 145 146 147 148 149 `````` size_t l = left->hash(); size_t r = right->hash(); if (1 != r) return l < r; return left->dump() < right->dump(); `````` Alexandre Duret-Lutz committed Jan 20, 2005 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 `````` } }; /// \brief Hash Function for const formula*. /// \ingroup ltl_essentials /// \ingroup hash_funcs /// /// This is meant to be used as a hash functor for /// Sgi's \c hash_map whose key are of type const formula*. /// /// For instance here is how one could declare /// a map of \c const::formula*. /// \code /// // Remember how many times each formula has been seen. /// Sgi::hash_map seen; /// \endcode struct formula_ptr_hash: public std::unary_function { size_t operator()(const formula* that) const { assert(that); return that->hash(); } }; `````` Alexandre Duret-Lutz committed Apr 15, 2003 179 180 181 `````` } } `````` Alexandre Duret-Lutz committed Jan 03, 2005 182 ``#endif // SPOT_LTLAST_FORMULA_HH``