magic.hh 3.94 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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
24
#ifndef SPOT_TGBAALGOS_MAGIC_HH
# define SPOT_TGBAALGOS_MAGIC_HH

25
#include <cstddef>
26
27
28

namespace spot
{
29
30
  class tgba;
  class emptiness_check;
31
32
33
34
35

  /// \addtogroup emptiness_check_algorithms
  /// @{

  /// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
36
37
38
39
  ///
  /// \pre The automaton \a a must have at most one accepting condition (i.e.
  /// it is a TBA).
  ///
40
41
42
  /// During the visit of \a a, the returned checker stores explicitely all
  /// the traversed states.
  /// The method \a check() of the checker can be called several times
43
  /// (until it returns a null pointer) to enumerate all the visited accepting
44
  /// paths. The implemented algorithm is the following:
45
46
  ///
  /// \verbatim
47
  /// procedure check ()
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  /// begin
  ///   call dfs_blue(s0);
  /// end;
  ///
  /// procedure dfs_blue (s)
  /// begin
  ///   s.color = blue;
  ///   for all t in post(s) do
  ///     if t.color == white then
  ///       call dfs_blue(t);
  ///     end if;
  ///     if (the edge (s,t) is accepting) then
  ///       target = s;
  ///       call dfs_red(t);
  ///     end if;
  ///   end for;
  /// end;
  ///
  /// procedure dfs_red(s)
  /// begin
  ///   s.color = red;
  ///   if s == target then
  ///     report cycle
  ///   end if;
  ///   for all t in post(s) do
  ///     if t.color != red then
  ///       call dfs_red(t);
  ///     end if;
  ///   end for;
  /// end;
78
  /// \endverbatim
79
  ///
80
81
  /// This algorithm is an adaptation to TBA of the one
  /// (which deals with accepting states) presented in
82
83
84
  ///
  /// \verbatim
  ///  Article{         courcoubertis.92.fmsd,
85
  ///    author        = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
86
87
88
89
90
91
92
93
94
  ///                    Wolper and Mihalis Yannakakis},
  ///    title         = {Memory-Efficient Algorithm for the Verification of
  ///                    Temporal Properties},
  ///    journal       = {Formal Methods in System Design},
  ///    pages         = {275--288},
  ///    year          = {1992},
  ///    volume        = {1}
  ///  }
  /// \endverbatim
95
  ///
96
  emptiness_check* explicit_magic_search(const tgba *a);
97

98
  /// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
99
100
101
102
  ///
  /// \pre The automaton \a a must have at most one accepting condition (i.e.
  /// it is a TBA).
  ///
103
104
  /// During the visit of \a a, the returned checker does not store explicitely
  /// the traversed states but uses the bit-state hashing technic presented in:
105
  ///
106
  /// \verbatim
107
108
109
110
111
112
113
  /// @book{Holzmann91,
  ///    author = {G.J. Holzmann},
  ///    title = {Design and Validation of Computer Protocols},
  ///    publisher = {Prentice-Hall},
  ///    address = {Englewood Cliffs, New Jersey},
  ///    year = {1991}
  /// }
114
115
  /// \endverbatim
  ///
116
  /// Consequently, the detection of an acceptence cycle is not ensured. The
117
  /// implemented algorithm is the same as the one of
118
  /// spot::explicit_magic_search.
119
  ///
120
  /// \sa spot::explicit_magic_search
121
  ///
122
  emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size);
123

124
  /// @}
125
126
127
}

#endif // SPOT_TGBAALGOS_MAGIC_HH