unop.hh 5.54 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
//
// 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
11
// the Free Software Foundation; either version 3 of the License, or
12
13
14
15
16
17
18
19
// (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
20
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
21

22
23
24
25
/// \file ltlast/unop.hh
/// \brief LTL unary operators
#ifndef SPOT_LTLAST_UNOP_HH
# define SPOT_LTLAST_UNOP_HH
26
27

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

namespace spot
{
34
  namespace ltl
35
36
  {

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

51
      /// \brief Build an unary operator with operation \a op and
52
      /// child \a child.
53
54
55
56
57
58
59
60
      ///
      /// 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
61
      ///   - X(0) = 0
62
63
      ///   - F(1) = 1
      ///   - G(1) = 1
64
      ///   - X(1) = 1
65
66
      ///   - !1 = 0
      ///   - !0 = 1
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
67
      ///   - ![*0] = 1[+]     (read below)
68
      ///   - !!Exp = Exp
69
70
      ///   - !Closure(Exp) = NegClosure(Exp)
      ///   - !NegClosure(Exp) = Closure(Exp)
71
      ///   - Closure([*0]) = 1
72
73
      ///   - Closure(1) = 1
      ///   - Closure(0) = 0
74
      ///   - Closure(b) = b
75
      ///   - NegClosure([*0]) = 0
76
77
      ///   - NegClosure(1) = 0
      ///   - NegClosure(0) = 1
78
      ///   - NegClosure(b) = !b
79
80
81
82
      ///
      /// 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
83
84
85
86
87
      ///
      /// 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.
88
      static const formula* instance(type op, const formula* child);
89

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

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

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

100
101
102
      /// Return a canonic representation of the atomic proposition
      virtual std::string dump() const;

103
104
105
      /// Number of instantiated unary operators.  For debugging.
      static unsigned instance_count();

106
107
108
      /// Dump all instances.  For debugging.
      static std::ostream& dump_instances(std::ostream& os);

109
    protected:
110
111
      typedef std::pair<type, const formula*> pair;
      typedef std::map<pair, const unop*> map;
112
113
      static map instances;

114
      unop(type op, const formula* child);
115
116
117
118
      virtual ~unop();

    private:
      type op_;
119
      const formula* child_;
120
121
    };

122
123
124
125
126
127

    /// \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
128
    const unop*
129
    is_unop(const formula* f)
130
131
132
    {
      if (f->kind() != formula::UnOp)
	return 0;
133
      return static_cast<const unop*>(f);
134
135
136
137
138
139
140
    }

    /// \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
141
    const unop*
142
    is_unop(const formula* f, unop::type op)
143
    {
144
145
146
147
      if (const unop* uo = is_unop(f))
	if (uo->op() == op)
	  return uo;
      return 0;
148
149
    }

150
151
152
153
    /// \brief Cast \a f into a unop if it is a Not.
    ///
    /// Return 0 otherwise.
    inline
154
    const unop*
155
156
157
158
159
    is_Not(const formula* f)
    {
      return is_unop(f, unop::Not);
    }

160
161
162
163
    /// \brief Cast \a f into a unop if it is a X.
    ///
    /// Return 0 otherwise.
    inline
164
    const unop*
165
    is_X(const formula* f)
166
167
168
169
170
171
172
173
    {
      return is_unop(f, unop::X);
    }

    /// \brief Cast \a f into a unop if it is a F.
    ///
    /// Return 0 otherwise.
    inline
174
    const unop*
175
    is_F(const formula* f)
176
177
178
179
180
181
182
183
    {
      return is_unop(f, unop::F);
    }

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

    /// \brief Cast \a f into a unop if has the form GF(...).
    ///
    /// Return 0 otherwise.
    inline
194
    const unop*
195
    is_GF(const formula* f)
196
    {
197
198
199
      if (const unop* op = is_G(f))
	return is_F(op->child());
      return 0;
200
201
202
203
204
205
    }

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

216
#endif // SPOT_LTLAST_UNOP_HH