formula.hh 3.4 KB
 Alexandre Duret-Lutz committed Aug 09, 2004 1 ``````// Copyright (C) 2003, 2004 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 Apr 15, 2003 24 25 26 27 28 ``````#ifndef SPOT_LTLAST_FORMULAE_HH # define SPOT_LTLAST_FORMULAE_HH #include "predecl.hh" `````` Alexandre Duret-Lutz committed May 15, 2003 29 ``````namespace spot `````` Alexandre Duret-Lutz committed Apr 15, 2003 30 ``````{ `````` Alexandre Duret-Lutz committed May 15, 2003 31 `````` namespace ltl `````` Alexandre Duret-Lutz committed Apr 15, 2003 32 `````` { `````` Alexandre Duret-Lutz committed Nov 17, 2004 33 34 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 `````` /// \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 62 `````` `````` Alexandre Duret-Lutz committed Apr 18, 2003 63 `````` /// \brief An LTL formula. `````` Alexandre Duret-Lutz committed Nov 17, 2004 64 65 `````` /// \ingroup ltl_essential /// \ingroup ltl_ast `````` Alexandre Duret-Lutz committed May 15, 2003 66 67 `````` /// /// The only way you can work with a formula is to `````` Alexandre Duret-Lutz committed Apr 18, 2003 68 `````` /// build a spot::ltl::visitor or spot::ltl::const_visitor. `````` Alexandre Duret-Lutz committed May 15, 2003 69 `````` class formula `````` Alexandre Duret-Lutz committed Apr 15, 2003 70 71 `````` { public: `````` Alexandre Duret-Lutz committed Jun 26, 2003 72 `````` /// Entry point for vspot::ltl::visitor instances. `````` Alexandre Duret-Lutz committed Apr 15, 2003 73 `````` virtual void accept(visitor& v) = 0; `````` Alexandre Duret-Lutz committed Jun 26, 2003 74 `````` /// Entry point for vspot::ltl::const_visitor instances. `````` Alexandre Duret-Lutz committed Apr 15, 2003 75 `````` virtual void accept(const_visitor& v) const = 0; `````` Alexandre Duret-Lutz committed May 15, 2003 76 `````` `````` Alexandre Duret-Lutz committed Aug 19, 2003 77 78 79 80 81 82 `````` /// \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 83 `````` formula* ref(); `````` Alexandre Duret-Lutz committed Aug 19, 2003 84 85 86 87 88 89 `````` /// \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 90 91 92 `````` static void unref(formula* f); protected: `````` Alexandre Duret-Lutz committed Nov 02, 2004 93 94 `````` virtual ~formula(); `````` Alexandre Duret-Lutz committed May 15, 2003 95 96 97 `````` /// \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 98 `````` /// the instance must be deleted (usually when the counter hits 0). `````` Alexandre Duret-Lutz committed May 15, 2003 99 `````` virtual bool unref_(); `````` Alexandre Duret-Lutz committed Apr 15, 2003 100 101 102 103 104 105 106 107 `````` }; } } #endif // SPOT_LTLAST_FORMULAE_HH``````