formula.hh 2.47 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003  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.

22
23
24
25
26
#ifndef SPOT_LTLAST_FORMULAE_HH
# define SPOT_LTLAST_FORMULAE_HH

#include "predecl.hh"

27
namespace spot
28
{
29
  namespace ltl
30
31
  {

32
    /// \brief An LTL formula.
33
34
    ///
    /// The only way you can work with a formula is to
35
    /// build a spot::ltl::visitor or spot::ltl::const_visitor.
36
    class formula
37
38
    {
    public:
39
40
      virtual ~formula();

41
      /// Entry point for vspot::ltl::visitor instances.
42
      virtual void accept(visitor& v) = 0;
43
      /// Entry point for vspot::ltl::const_visitor instances.
44
      virtual void accept(const_visitor& v) const = 0;
45

46
47
48
49
50
51
      /// \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.
52
      formula* ref();
53
54
55
56
57
58
      /// \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.
59
60
61
62
63
64
      static void unref(formula* f);

    protected:
      /// \brief increment reference counter if any
      virtual void ref_();
      /// \brief decrement reference counter if any, return true when
65
      /// the instance must be deleted (usually when the counter hits 0).
66
      virtual bool unref_();
67
68
69
70
71
72
73
74
    };

  }
}



#endif // SPOT_LTLAST_FORMULAE_HH