unop.hh 5.65 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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
25
26
/// \file ltlast/unop.hh
/// \brief LTL unary operators
#ifndef SPOT_LTLAST_UNOP_HH
# define SPOT_LTLAST_UNOP_HH
27
28

#include <map>
29
#include <iosfwd>
30
#include "refformula.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
31
#include "bunop.hh"
32
33
34

namespace spot
{
35
  namespace ltl
36
37
  {

38
    /// \ingroup ltl_ast
39
    /// \brief Unary operators.
40
    class SPOT_API unop : public ref_formula
41
42
    {
    public:
43
44
45
46
47
      enum type {
	// LTL
	Not, X, F, G,
	// ELTL
	Finish,
48
	// Closure
49
	Closure, NegClosure, NegClosureMarked
50
	};
51

52
      /// \brief Build an unary operator with operation \a op and
53
      /// child \a child.
54
55
56
57
58
59
60
61
      ///
      /// The following trivial simplifications are performed
      /// automatically (the left expression is rewritten as the right
      /// expression):
      ///   - FF(Exp) = F(Exp)
      ///   - GG(Exp) = G(Exp)
      ///   - F(0) = 0
      ///   - G(0) = 0
62
      ///   - X(0) = 0
63
64
      ///   - F(1) = 1
      ///   - G(1) = 1
65
      ///   - X(1) = 1
66
67
      ///   - !1 = 0
      ///   - !0 = 1
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
68
      ///   - ![*0] = 1[+]     (read below)
69
      ///   - !!Exp = Exp
70
71
      ///   - !Closure(Exp) = NegClosure(Exp)
      ///   - !NegClosure(Exp) = Closure(Exp)
72
      ///   - Closure([*0]) = 1
73
74
      ///   - Closure(1) = 1
      ///   - Closure(0) = 0
75
      ///   - Closure(b) = b
76
      ///   - NegClosure([*0]) = 0
77
78
      ///   - NegClosure(1) = 0
      ///   - NegClosure(0) = 1
79
      ///   - NegClosure(b) = !b
80
81
82
83
      ///
      /// This rewriting implies that it is not possible to build an
      /// LTL formula object that is SYNTACTICALLY equal to one of
      /// these left expressions.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84
85
86
87
88
      ///
      /// Note that the "![*0]" form cannot be read using the PSL
      /// grammar.  Spot cannot read it either.  However some
      /// BDD-based algorithm may need to negate any constant, so we
      /// handle this one as well.
89
      static const formula* instance(type op, const formula* child);
90

91
      virtual void accept(visitor& v) const;
92
93

      /// Get the sole operand of this operator.
94
95
96
97
      const formula* child() const
      {
	return child_;
      }
98
99

      /// Get the type of this operator.
100
101
102
103
104
      type op() const
      {
	return op_;
      }

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

108
109
110
      /// Return a canonic representation of the atomic proposition
      virtual std::string dump() const;

111
112
113
      /// Number of instantiated unary operators.  For debugging.
      static unsigned instance_count();

114
115
116
      /// Dump all instances.  For debugging.
      static std::ostream& dump_instances(std::ostream& os);

117
    protected:
118
119
      typedef std::pair<type, const formula*> pair;
      typedef std::map<pair, const unop*> map;
120
121
      static map instances;

122
      unop(type op, const formula* child);
123
124
125
126
      virtual ~unop();

    private:
      type op_;
127
      const formula* child_;
128
129
    };

130
131
132
133
134
135

    /// \brief Cast \a f into a unop
    ///
    /// Cast \a f into a unop iff it is a unop instance.  Return 0
    /// otherwise.  This is faster than \c dynamic_cast.
    inline
136
    const unop*
137
    is_unop(const formula* f)
138
139
140
    {
      if (f->kind() != formula::UnOp)
	return 0;
141
      return static_cast<const unop*>(f);
142
143
144
145
146
147
148
    }

    /// \brief Cast \a f into a unop if it has type \a op.
    ///
    /// Cast \a f into a unop iff it is a unop instance with operator \a op.
    /// Returns 0 otherwise.
    inline
149
    const unop*
150
    is_unop(const formula* f, unop::type op)
151
    {
152
153
154
155
      if (const unop* uo = is_unop(f))
	if (uo->op() == op)
	  return uo;
      return 0;
156
157
    }

158
159
160
161
    /// \brief Cast \a f into a unop if it is a Not.
    ///
    /// Return 0 otherwise.
    inline
162
    const unop*
163
164
165
166
167
    is_Not(const formula* f)
    {
      return is_unop(f, unop::Not);
    }

168
169
170
171
    /// \brief Cast \a f into a unop if it is a X.
    ///
    /// Return 0 otherwise.
    inline
172
    const unop*
173
    is_X(const formula* f)
174
175
176
177
178
179
180
181
    {
      return is_unop(f, unop::X);
    }

    /// \brief Cast \a f into a unop if it is a F.
    ///
    /// Return 0 otherwise.
    inline
182
    const unop*
183
    is_F(const formula* f)
184
185
186
187
188
189
190
191
    {
      return is_unop(f, unop::F);
    }

    /// \brief Cast \a f into a unop if it is a G.
    ///
    /// Return 0 otherwise.
    inline
192
    const unop*
193
    is_G(const formula* f)
194
195
196
197
198
199
200
201
    {
      return is_unop(f, unop::G);
    }

    /// \brief Cast \a f into a unop if has the form GF(...).
    ///
    /// Return 0 otherwise.
    inline
202
    const unop*
203
    is_GF(const formula* f)
204
    {
205
206
207
      if (const unop* op = is_G(f))
	return is_F(op->child());
      return 0;
208
209
210
211
212
213
    }

    /// \brief Cast \a f into a unop if has the form FG(...).
    ///
    /// Return 0 otherwise.
    inline
214
    const unop*
215
    is_FG(const formula* f)
216
    {
217
218
219
      if (const unop* op = is_F(f))
	return is_G(op->child());
      return 0;
220
    }
221
222
223
  }
}

224
#endif // SPOT_LTLAST_UNOP_HH