binop.hh 6.49 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
5
6
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
24
/// \file ltlast/binop.hh
/// \brief LTL binary operators
25
26
///
/// This does not include \c AND and \c OR operators.  These are
27
28
29
/// considered to be multi-operand operators (see spot::ltl::multop).
#ifndef SPOT_LTLAST_BINOP_HH
# define SPOT_LTLAST_BINOP_HH
30
31

#include <map>
32
#include <iosfwd>
33
34
35
36
#include "refformula.hh"

namespace spot
{
37
  namespace ltl
38
39
  {

40
    /// \ingroup ltl_ast
41
    /// \brief Binary operator.
42
    class binop : public ref_formula
43
44
45
46
47
48
    {
    public:
      /// Different kinds of binary opertaors
      ///
      /// And and Or are not here.  Because they
      /// are often nested we represent them as multops.
49
50
51
      enum type { Xor,
		  Implies,
		  Equiv,
52
53
54
55
56
57
58
		  U, ///< until
		  R, ///< release (dual of until)
		  W, ///< weak until
		  M, ///< strong release (dual of weak until)
		  EConcat, ///< Existential Concatenation
		  EConcatMarked, ///< Existential Concatenation, Marked
		  UConcat ///< Universal Concatenation
59
      };
60

61
      /// \brief Build a unary operator with operation \a op and
62
      /// children \a first and \a second.
63
64
65
66
67
68
69
70
71
      ///
      /// Some reordering will be performed on arguments of commutative
      /// operators (Xor and Equiv) to ensure that for instance (a <=> b)
      /// is the same formula as (b <=> a).
      ///
      /// Furthermore, the following trivial simplifications are
      /// performed (the left formula is rewritten as the right
      /// formula):
      ///   - (1 => Exp) = Exp
72
      ///   - (0 => Exp) = 1
73
74
      ///   - (Exp => 1) = 1
      ///   - (Exp => 0) = !Exp
75
      ///   - (Exp => Exp) = 1
76
77
      ///   - (1 ^ Exp) = !Exp
      ///   - (0 ^ Exp) = Exp
78
      ///   - (Exp ^ Exp) = 0
79
80
      ///   - (0 <=> Exp) = !Exp
      ///   - (1 <=> Exp) = Exp
81
      ///   - (Exp <=> Exp) = Exp
82
83
84
      ///   - (Exp U 1) = 1
      ///   - (Exp U 0) = 0
      ///   - (0 U Exp) = Exp
85
      ///   - (Exp U Exp) = Exp
86
87
88
      ///   - (Exp W 1) = 1
      ///   - (0 W Exp) = Exp
      ///   - (1 W Exp) = 1
89
      ///   - (Exp W Exp) = Exp
90
91
92
      ///   - (Exp R 1) = 1
      ///   - (Exp R 0) = 0
      ///   - (1 R Exp) = Exp
93
      ///   - (Exp R Exp) = Exp
94
95
96
      ///   - (Exp M 0) = 0
      ///   - (1 M Exp) = Exp
      ///   - (0 M Exp) = 0
97
      ///   - (Exp M Exp) = Exp
98
99
100
101
102
103
104
105
106
      ///   - 0 <>-> Exp = 0
      ///   - 1 <>-> Exp = Exp
      ///   - [*0] <>-> Exp = 0
      ///   - Exp <>-> 0 = 0
      ///   - boolExp <>-> Exp = boolExp & Exp
      ///   - 0 []-> Exp = 1
      ///   - 1 []-> Exp = Exp
      ///   - [*0] []-> Exp = 1
      ///   - Exp []-> 1 = 1
107
      ///   - boolExp <>-> Exp = !boolExp | Exp
108
109
110
      static const formula* instance(type op,
				     const formula* first,
				     const formula* second);
111

112
      virtual void accept(visitor& v) const;
113
114

      /// Get the first operand.
115
      const formula* first() const;
116
      /// Get the second operand.
117
      const formula* second() const;
118
119
120
121
122
123

      /// Get the type of this operator.
      type op() const;
      /// Get the type of this operator, as a string.
      const char* op_name() const;

124
125
126
      /// Return a canonic representation of the atomic proposition
      virtual std::string dump() const;

127
128
129
      /// Number of instantiated binary operators.  For debugging.
      static unsigned instance_count();

130
131
132
      /// Dump all instances.  For debugging.
      static std::ostream& dump_instances(std::ostream& os);

133
    protected:
134
      typedef std::pair<const formula*, const formula*> pairf;
135
      typedef std::pair<type, pairf> pair;
136
      typedef std::map<pair, const binop*> map;
137
138
      static map instances;

139
      binop(type op, const formula* first, const formula* second);
140
141
142
143
      virtual ~binop();

    private:
      type op_;
144
145
      const formula* first_;
      const formula* second_;
146
147
    };

148
149
150
151
152
    /// \brief Cast \a f into a binop
    ///
    /// Cast \a f into a binop iff it is a binop instance.  Return 0
    /// otherwise.  This is faster than \c dynamic_cast.
    inline
153
154
    const binop*
    is_binop(const formula* f)
155
156
157
    {
      if (f->kind() != formula::BinOp)
	return 0;
158
      return static_cast<const binop*>(f);
159
160
161
162
163
164
165
    }

    /// \brief Cast \a f into a binop if it has type \a op.
    ///
    /// Cast \a f into a binop iff it is a unop instance with operator \a op.
    /// Returns 0 otherwise.
    inline
166
167
    const binop*
    is_binop(const formula* f, binop::type op)
168
    {
169
170
171
172
      if (const binop* bo = is_binop(f))
	if (bo->op() == op)
	  return bo;
      return 0;
173
174
175
176
177
178
179
    }

    /// \brief Cast \a f into a binop if it has type \a op1 or \a op2.
    ///
    /// Cast \a f into a binop iff it is a unop instance with operator \a op1 or
    /// \a op2.  Returns 0 otherwise.
    inline
180
181
    const binop*
    is_binop(const formula* f, binop::type op1, binop::type op2)
182
    {
183
184
185
      if (const binop* bo = is_binop(f))
	if (bo->op() == op1 || bo->op() == op2)
	  return bo;
186
187
188
189
190
191
192
      return 0;
    }

    /// \brief Cast \a f into a binop if it is a U.
    ///
    /// Return 0 otherwise.
    inline
193
194
    const binop*
    is_U(const formula* f)
195
196
197
198
199
200
201
202
    {
      return is_binop(f, binop::U);
    }

    /// \brief Cast \a f into a binop if it is a M.
    ///
    /// Return 0 otherwise.
    inline
203
204
    const binop*
    is_M(const formula* f)
205
206
207
208
209
210
211
212
    {
      return is_binop(f, binop::M);
    }

    /// \brief Cast \a f into a binop if it is a R.
    ///
    /// Return 0 otherwise.
    inline
213
214
    const binop*
    is_R(const formula* f)
215
216
217
218
219
220
221
222
    {
      return is_binop(f, binop::R);
    }

    /// \brief Cast \a f into a binop if it is a W.
    ///
    /// Return 0 otherwise.
    inline
223
224
    const binop*
    is_W(const formula* f)
225
226
227
    {
      return is_binop(f, binop::W);
    }
228
229
230
  }
}

231
#endif // SPOT_LTLAST_BINOP_HH