formula.hh 5.18 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
//
// 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.

22
/// \file ltlast/formula.hh
23
/// \brief LTL formula, AST and visitor interface
24
25
#ifndef SPOT_LTLAST_FORMULA_HH
# define SPOT_LTLAST_FORMULA_HH
26

27
# include "internal/formula.hh"
28
29
30
31
32
# include "internal/atomic_prop.hh"
# include "internal/constant.hh"
# include "internal/unop.hh"
# include "internal/binop.hh"
# include "internal/multop.hh"
33

34
namespace spot
35
{
36
  namespace ltl
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
66
    /// \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

67
68
    struct visitor;
    struct const_visitor;
69

70
    struct ltl_t
71
    {
72
73
      typedef spot::ltl::visitor visitor;
      typedef spot::ltl::const_visitor const_visitor;
74

75
76
      enum binop { Xor, Implies, Equiv, U, R };
      const char* binop_name(binop op) const
77
      {
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
	switch (op)
      	{
	  case Xor:
	    return "Xor";
	  case Implies:
	    return "Implies";
	  case Equiv:
	    return "Equiv";
	  case U:
	    return "U";
	  case R:
	    return "R";
      	}
	// Unreachable code.
	assert(0);
	return 0;
94
95
      }

96
97
      enum unop { Not, X, F, G };
      const char* unop_name(unop op) const
98
      {
99
100
101
102
103
104
105
106
107
108
109
110
111
112
	switch (op)
	{
	  case Not:
	    return "Not";
	  case X:
	    return "X";
	  case F:
	    return "F";
	  case G:
	    return "G";
	}
	// Unreachable code.
	assert(0);
	return 0;
113
114
115
      }
    };

116
117
118
119
120
121
122
    /// \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.
    typedef spot::internal::formula<ltl_t> formula;
123

124
125
    typedef spot::internal::formula_ptr_less_than<ltl_t> formula_ptr_less_than;
    typedef spot::internal::formula_ptr_hash<ltl_t> formula_ptr_hash;
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187



    /// \brief Atomic propositions.
    /// \ingroup ltl_ast
    typedef spot::internal::atomic_prop<ltl_t> atomic_prop;

    /// \brief A constant (True or False)
    /// \ingroup ltl_ast
    typedef spot::internal::constant<ltl_t> constant;

    /// \brief Unary operators.
    /// \ingroup ltl_ast
    typedef spot::internal::unop<ltl_t> unop;

    /// \brief Binary operator.
    /// \ingroup ltl_ast
    typedef spot::internal::binop<ltl_t> binop;

    /// \brief Multi-operand operators.
    /// \ingroup ltl_ast
    ///
    /// These operators are considered commutative and associative.
    typedef spot::internal::multop<ltl_t> multop;


    /// \brief Formula visitor that can modify the formula.
    /// \ingroup ltl_essential
    ///
    /// Writing visitors is the prefered way
    /// to traverse a formula, since it doesn't
    /// involve any cast.
    ///
    /// If you do not need to modify the visited formula, inherit from
    /// spot::ltl:const_visitor instead.
    struct visitor
    {
      virtual ~visitor() {}
      virtual void visit(atomic_prop* node) = 0;
      virtual void visit(constant* node) = 0;
      virtual void visit(binop* node) = 0;
      virtual void visit(unop* node) = 0;
      virtual void visit(multop* node) = 0;
    };

    /// \brief Formula visitor that cannot modify the formula.
    ///
    /// Writing visitors is the prefered way
    /// to traverse a formula, since it doesn't
    /// involve any cast.
    ///
    /// If you want to modify the visited formula, inherit from
    /// spot::ltl:visitor instead.
    struct const_visitor
    {
      virtual ~const_visitor() {}
      virtual void visit(const atomic_prop* node) = 0;
      virtual void visit(const constant* node) = 0;
      virtual void visit(const binop* node) = 0;
      virtual void visit(const unop* node) = 0;
      virtual void visit(const multop* node) = 0;
    };
188
189
190
  }
}

191
#endif // SPOT_LTLAST_FORMULA_HH