formula.hh 3.16 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
23
/// \file ltlast/formula.hh
/// \brief LTL formula interface
24
25
#ifndef SPOT_LTLAST_FORMULA_HH
# define SPOT_LTLAST_FORMULA_HH
26

27
# include "internal/formula.hh"
28

29
namespace spot
30
{
31
  namespace ltl
32
  {
33
34
35
36
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
    /// \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

62
63
    struct visitor;
    struct const_visitor;
64

65
    struct ltl_t
66
    {
67
68
      typedef spot::ltl::visitor visitor;
      typedef spot::ltl::const_visitor const_visitor;
69

70
71
      enum binop { Xor, Implies, Equiv, U, R };
      const char* binop_name(binop op) const
72
      {
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
	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;
89
90
      }

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

111
112
113
114
115
116
117
    /// \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;
118

119
120
    typedef spot::internal::formula_ptr_less_than<ltl_t> formula_ptr_less_than;
    typedef spot::internal::formula_ptr_hash<ltl_t> formula_ptr_hash;
121
122
123
  }
}

124
#endif // SPOT_LTLAST_FORMULA_HH