formula.hh 3.4 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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.

22
23
/// \file ltlast/formula.hh
/// \brief LTL formula interface
24
25
26
27
28
#ifndef SPOT_LTLAST_FORMULAE_HH
# define SPOT_LTLAST_FORMULAE_HH

#include "predecl.hh"

29
namespace spot
30
{
31
  namespace ltl
32
  {
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

62

63
    /// \brief An LTL formula.
64
65
    /// \ingroup ltl_essential
    /// \ingroup ltl_ast
66
67
    ///
    /// The only way you can work with a formula is to
68
    /// build a spot::ltl::visitor or spot::ltl::const_visitor.
69
    class formula
70
71
    {
    public:
72
      /// Entry point for vspot::ltl::visitor instances.
73
      virtual void accept(visitor& v) = 0;
74
      /// Entry point for vspot::ltl::const_visitor instances.
75
      virtual void accept(const_visitor& v) const = 0;
76

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.
83
      formula* ref();
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.
90
91
92
      static void unref(formula* f);

    protected:
93
94
      virtual ~formula();

95
96
97
      /// \brief increment reference counter if any
      virtual void ref_();
      /// \brief decrement reference counter if any, return true when
98
      /// the instance must be deleted (usually when the counter hits 0).
99
      virtual bool unref_();
100
101
102
103
104
105
106
107
    };

  }
}



#endif // SPOT_LTLAST_FORMULAE_HH