formula.hh 5.63 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
//
// 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
#ifndef SPOT_LTLAST_FORMULA_HH
# define SPOT_LTLAST_FORMULA_HH
26

27
28
#include <string>
#include <cassert>
29
30
#include "predecl.hh"

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

64

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

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

94
95
96
97
      /// Return a canonic representation of the formula
      const std::string& dump() const;

      /// Return a hash_key for the formula.
98
      size_t
99
100
101
102
      hash() const
      {
	return hash_key_;
      }
103
    protected:
104
105
      virtual ~formula();

106
107
108
      /// \brief increment reference counter if any
      virtual void ref_();
      /// \brief decrement reference counter if any, return true when
109
      /// the instance must be deleted (usually when the counter hits 0).
110
      virtual bool unref_();
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_;
122
123
    };

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 <code>const formula*</code>.
    /// \ingroup ltl_essentials
    ///
    /// This is meant to be used as a comparison functor for
    /// STL \c map whose key are of type <code>const formula*</code>.
    ///
    /// 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<const spot::ltl::formula*, int,
    ///            spot::formula_ptr_less_than> seen;
    /// \endcode
    struct formula_ptr_less_than:
      public std::binary_function<const formula*, const formula*, bool>
    {
      bool
      operator()(const formula* left, const formula* right) const
      {
	assert(left);
	assert(right);
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();
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 <code>const formula*</code>.
    /// \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 <code>const formula*</code>.
    ///
    /// 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<const spot::ltl::formula*, int,
    ///                 const spot::ltl::formula_ptr_hash> seen;
    /// \endcode
    struct formula_ptr_hash:
      public std::unary_function<const formula*, size_t>
    {
      size_t
      operator()(const formula* that) const
      {
	assert(that);
	return that->hash();
      }
    };


179
180
181
  }
}

182
#endif // SPOT_LTLAST_FORMULA_HH