formula.hh 12.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
//
// 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.

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

28
29
30
#include <string>
#include <cassert>
#include "predecl.hh"
31
#include <list>
32

33
namespace spot
34
{
35
  namespace ltl
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
64
65
    /// \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

66

67
68
69
70
71
72
    /// \brief An LTL formula.
    /// \ingroup ltl_essential
    /// \ingroup ltl_ast
    ///
    /// The only way you can work with a formula is to
    /// build a spot::ltl::visitor or spot::ltl::const_visitor.
73
    class formula
74
    {
75
    public:
76
77
78
79
80
81
82
83
84
85
      /// Kind of a sub-formula
      enum opkind { Constant,
		    AtomicProp,
		    UnOp,
		    BinOp,
		    MultOp,
		    BUnOp,
		    AutomatOp };

      formula(opkind k) : count_(max_count++), kind_(k)
86
87
88
      {
	// If the counter of formulae ever loops, we want to skip the
	// first three values, because they are permanently associated
89
	// to constants, and it is convenient to have constants smaller
90
91
92
93
	// than all other formulae.
	if (max_count == 0)
	  max_count = 3;
      }
94

95
96
97
98
99
100
101
102
      /// Entry point for vspot::ltl::visitor instances.
      virtual void accept(visitor& v) = 0;
      /// Entry point for vspot::ltl::const_visitor instances.
      virtual void accept(const_visitor& v) const = 0;

      /// \brief clone this node
      ///
      /// This increments the reference counter of this node (if one is
103
      /// used).
104
      formula* clone() const;
105
106
107
      /// \brief release this node
      ///
      /// This decrements the reference counter of this node (if one is
108
      /// used) and can free the object.
109
      void destroy() const;
110
111

      /// Return a canonic representation of the formula
112
      virtual std::string dump() const = 0;
113

114
115
116
117
118
119
      /// Return the kind of the top-level operator.
      opkind kind() const
      {
	return kind_;
      }

120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
      ////////////////
      // Properties //
      ////////////////

      /// Whether the formula use only boolean operators.
      bool is_boolean() const
      {
	return is.boolean;
      }

      /// Whether the formula use only AND, OR, and NOT operators.
      bool is_sugar_free_boolean() const
      {
	return is.sugar_free_boolean;
      }

      /// \brief Whether the formula is in negative normal form.
      ///
      /// A formula is in negative normal form if the not operators
      /// occur only in front of atomic propositions.
      bool is_in_nenoform() const
      {
	return is.in_nenoform;
      }

145
      /// Whether the formula avoids the X operator.
146
147
148
149
150
      bool is_X_free() const
      {
	return is.X_free;
      }

151
      /// Whether the formula avoids the F and G operators.
152
153
154
155
156
      bool is_sugar_free_ltl() const
      {
	return is.sugar_free_ltl;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
      /// Whether the formula uses only LTL operators.
158
159
160
161
162
      bool is_ltl_formula() const
      {
	return is.ltl_formula;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
163
      /// Whether the formula uses only ELTL operators.
164
165
166
167
168
      bool is_eltl_formula() const
      {
	return is.eltl_formula;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
169
      /// Whether the formula uses only PSL operators.
170
171
172
173
174
      bool is_psl_formula() const
      {
	return is.psl_formula;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
175
      /// Whether the formula uses only SERE operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
176
177
178
179
180
      bool is_sere_formula() const
      {
	return is.sere_formula;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
181
182
183
184
185
186
187
      /// Whether a SERE describes a finite language, or an LTL
      /// formula uses no temporal operator but X.
      bool is_finite() const
      {
	return is.finite;
      }

188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
      /// \brief Whether the formula is purely eventual.
      ///
      /// Pure eventuality formulae are defined in
      /// \verbatim
      /// @InProceedings{	  etessami.00.concur,
      /// author  	= {Kousha Etessami and Gerard J. Holzmann},
      /// title		= {Optimizing {B\"u}chi Automata},
      /// booktitle	= {Proceedings of the 11th International Conference on
      /// 		  Concurrency Theory (Concur'2000)},
      /// pages		= {153--167},
      /// year		= {2000},
      /// editor  	= {C. Palamidessi},
      /// volume  	= {1877},
      /// series  	= {Lecture Notes in Computer Science},
      /// publisher	= {Springer-Verlag}
      /// }
      /// \endverbatim
      ///
      /// A word that satisfies a pure eventuality can be prefixed by
      /// anything and still satisfies the formula.
      bool is_eventual() const
      {
	return is.eventual;
      }

      /// \brief Whether a formula is purely universal.
      ///
      /// Purely universal formulae are defined in
      /// \verbatim
      /// @InProceedings{	  etessami.00.concur,
      /// author  	= {Kousha Etessami and Gerard J. Holzmann},
      /// title		= {Optimizing {B\"u}chi Automata},
      /// booktitle	= {Proceedings of the 11th International Conference on
      /// 		  Concurrency Theory (Concur'2000)},
      /// pages		= {153--167},
      /// year		= {2000},
      /// editor  	= {C. Palamidessi},
      /// volume  	= {1877},
      /// series  	= {Lecture Notes in Computer Science},
      /// publisher	= {Springer-Verlag}
      /// }
      /// \endverbatim
      ///
      /// Any (non-empty) suffix of a word that satisfies a purely
      /// universal formula also satisfies the formula.
      bool is_universal() const
      {
	return is.universal;
      }

238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
      /// Whether a PSL/LTL formula is syntactic safety property.
      bool is_syntactic_safety() const
      {
	return is.syntactic_safety;
      }

      /// Whether a PSL/LTL formula is syntactic guarantee property.
      bool is_syntactic_guarantee() const
      {
	return is.syntactic_guarantee;
      }

      /// Whether a PSL/LTL formula is syntactic obligation property.
      bool is_syntactic_obligation() const
      {
	return is.syntactic_obligation;
      }

      /// Whether a PSL/LTL formula is syntactic recurrence property.
      bool is_syntactic_recurrence() const
      {
	return is.syntactic_recurrence;
      }

      /// Whether a PSL/LTL formula is syntactic persistence property.
      bool is_syntactic_persistence() const
      {
	return is.syntactic_persistence;
      }

268
269
270
271
272
273
      /// Whether the formula has an occurrence of EConcatMarked.
      bool is_marked() const
      {
	return !is.not_marked;
      }

274
275
276
277
278
279
      /// Whether the formula accepts [*0].
      bool accepts_eword() const
      {
	return is.accepting_eword;
      }

280
281
282
283
284
285
      /// The properties as a field of bits.  For internal use.
      unsigned get_props() const
      {
	return props;
      }

286
      /// Return a hash key for the formula.
287
288
      size_t
      hash() const
289
      {
290
	return count_;
291
      }
292
293
294
295
296
297
298
299
300
301
    protected:
      virtual ~formula();

      /// \brief increment reference counter if any
      virtual void ref_();
      /// \brief decrement reference counter if any, return true when
      /// the instance must be deleted (usually when the counter hits 0).
      virtual bool unref_();

      /// \brief The hash key of this formula.
302
303
      size_t count_;

304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
      struct ltl_prop
      {
	// All properties here should be expressed in such a a way
	// that property(f && g) is just property(f)&property(g).
	// This allows us to compute all properties of a compound
	// formula in one operation.
	//
	// For instance we do not use a property that says "has
	// temporal operator", because it would require an OR between
	// the two arguments.  Instead we have a property that
	// says "no temporal operator", and that one is computed
	// with an AND between the arguments.
	//
	// Also choose a name that makes sense when prefixed with
	// "the formula is".
	bool boolean:1;		   // No temporal operators.
	bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
321
	bool in_nenoform:1;	   // Negative Normal Form.
322
323
324
325
326
	bool X_free:1;		   // No X operators.
	bool sugar_free_ltl:1;	   // No F and G operators.
	bool ltl_formula:1;	   // Only LTL operators.
	bool eltl_formula:1;	   // Only ELTL operators.
	bool psl_formula:1;	   // Only PSL operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
327
	bool sere_formula:1;	   // Only SERE operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
328
	bool finite:1;		   // Finite SERE formulae, or Bool+X forms.
329
330
	bool eventual:1;	   // Purely eventual formula.
	bool universal:1;	   // Purely universal formula.
331
332
333
334
335
	bool syntactic_safety:1;   // Syntactic Safety Property.
	bool syntactic_guarantee:1;   // Syntactic Guarantee Property.
	bool syntactic_obligation:1;  // Syntactic Obligation Property.
	bool syntactic_recurrence:1;  // Syntactic Recurrence Property.
	bool syntactic_persistence:1; // Syntactic Persistence Property.
336
337
	bool not_marked:1;	   // No occurrence of EConcatMarked.
	bool accepting_eword:1;	   // Accepts the empty word.
338
339
340
341
342
343
344
345
      };
      union
      {
	// Use an unsigned for fast computation of all properties.
	unsigned props;
	ltl_prop is;
      };

346
347
348
    private:
      /// \brief Number of formulae created so far.
      static size_t max_count;
349
      opkind kind_;
350
351
    };

352
353
    /// \brief Strict Weak Ordering for <code>const formula*</code>.
    /// \ingroup ltl_essentials
354
    ///
355
356
    /// This is meant to be used as a comparison functor for
    /// STL \c map whose key are of type <code>const formula*</code>.
357
    ///
358
359
360
361
362
363
364
365
366
    /// 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>
367
    {
368
369
370
371
372
      bool
      operator()(const formula* left, const formula* right) const
      {
	assert(left);
	assert(right);
373
374
	if (left == right)
	  return false;
375
376
	size_t l = left->hash();
	size_t r = right->hash();
377
	if (l != r)
378
	  return l < r;
379
380
381
382
383
384
385
386
387
388
	// Because the hash code assigned to each formula is the
	// number of formulae constructed so far, it is very unlikely
	// that we will ever reach a case were two different formulae
	// have the same hash.  This will happen only ever with have
	// produced 256**sizeof(size_t) formulae (i.e. max_count has
	// looped back to 0 and started over).  In that case we can
	// order two formulae by looking at their text representation.
	// We could be more efficient and look at their AST, but it's
	// not worth the burden.  (Also ordering pointers is ruled out
	// because it breaks the determinism of the implementation.)
389
390
	return left->dump() < right->dump();
      }
391
392
    };

393
394
395
    /// \brief Hash Function for <code>const formula*</code>.
    /// \ingroup ltl_essentials
    /// \ingroup hash_funcs
396
    ///
397
398
    /// 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>.
399
    ///
400
401
402
403
404
405
406
407
408
    /// 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>
409
    {
410
411
412
413
414
415
      size_t
      operator()(const formula* that) const
      {
	assert(that);
	return that->hash();
      }
416
    };
417

418
419
420
421
    /// Print the properties of formula \a f on stream \a out.
    std::ostream& print_formula_props(std::ostream& out,
				      const formula* f,
				      bool abbreviated = false);
422

423
424
    /// List the properties of formula \a f.
    std::list<std::string> list_formula_props(const formula* f);
425
426
427
  }
}

428
#endif // SPOT_LTLAST_FORMULA_HH