binop.hh 6.53 KB
Newer Older
1
2
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
4
5
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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.

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

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

namespace spot
{
38
  namespace ltl
39
40
  {

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

62
      /// \brief Build a unary operator with operation \a op and
63
      /// children \a first and \a second.
64
65
66
67
68
69
70
71
72
      ///
      /// 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
73
      ///   - (0 => Exp) = 1
74
75
      ///   - (Exp => 1) = 1
      ///   - (Exp => 0) = !Exp
76
      ///   - (Exp => Exp) = 1
77
78
      ///   - (1 ^ Exp) = !Exp
      ///   - (0 ^ Exp) = Exp
79
      ///   - (Exp ^ Exp) = 0
80
81
      ///   - (0 <=> Exp) = !Exp
      ///   - (1 <=> Exp) = Exp
82
      ///   - (Exp <=> Exp) = Exp
83
84
85
      ///   - (Exp U 1) = 1
      ///   - (Exp U 0) = 0
      ///   - (0 U Exp) = Exp
86
      ///   - (Exp U Exp) = Exp
87
88
89
      ///   - (Exp W 1) = 1
      ///   - (0 W Exp) = Exp
      ///   - (1 W Exp) = 1
90
      ///   - (Exp W Exp) = Exp
91
92
93
      ///   - (Exp R 1) = 1
      ///   - (Exp R 0) = 0
      ///   - (1 R Exp) = Exp
94
      ///   - (Exp R Exp) = Exp
95
96
97
      ///   - (Exp M 0) = 0
      ///   - (1 M Exp) = Exp
      ///   - (0 M Exp) = 0
98
      ///   - (Exp M Exp) = Exp
99
100
101
102
103
104
105
106
107
      ///   - 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
108
      ///   - boolExp <>-> Exp = !boolExp | Exp
109
110
111
      static const formula* instance(type op,
				     const formula* first,
				     const formula* second);
112

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

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

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

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

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

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

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

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

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

149
150
151
152
153
    /// \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
154
155
    const binop*
    is_binop(const formula* f)
156
157
158
    {
      if (f->kind() != formula::BinOp)
	return 0;
159
      return static_cast<const binop*>(f);
160
161
162
163
164
165
166
    }

    /// \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
167
168
    const binop*
    is_binop(const formula* f, binop::type op)
169
    {
170
171
172
173
      if (const binop* bo = is_binop(f))
	if (bo->op() == op)
	  return bo;
      return 0;
174
175
176
177
178
179
180
    }

    /// \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
181
182
    const binop*
    is_binop(const formula* f, binop::type op1, binop::type op2)
183
    {
184
185
186
      if (const binop* bo = is_binop(f))
	if (bo->op() == op1 || bo->op() == op2)
	  return bo;
187
188
189
190
191
192
193
      return 0;
    }

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

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

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

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

232
#endif // SPOT_LTLAST_BINOP_HH