formula.hh 1014 Bytes
Newer Older
1
2
3
4
5
#ifndef SPOT_LTLAST_FORMULAE_HH
# define SPOT_LTLAST_FORMULAE_HH

#include "predecl.hh"

6
namespace spot
7
{
8
  namespace ltl
9
10
  {

11
    /// \brief An LTL formula.
12
13
    ///
    /// The only way you can work with a formula is to
14
    /// build a spot::ltl::visitor or spot::ltl::const_visitor.
15
    class formula
16
17
    {
    public:
18
19
      virtual ~formula();

20
      /// Entry point for vspot::ltl::visitor instances.
21
      virtual void accept(visitor& v) = 0;
22
      /// Entry point for vspot::ltl::const_visitor instances.
23
      virtual void accept(const_visitor& v) const = 0;
24
25
26
27
28
29
30
31
32
33

      /// \brief clone this formula
      formula* ref();
      /// \brief release formula
      static void unref(formula* f);

    protected:
      /// \brief increment reference counter if any
      virtual void ref_();
      /// \brief decrement reference counter if any, return true when
34
      /// the instance must be deleted (usually when the counter hits 0).
35
      virtual bool unref_();
36
37
38
39
40
41
42
43
    };

  }
}



#endif // SPOT_LTLAST_FORMULAE_HH