tgbamask.hh 3.25 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// de l'Epita (LRDE).
//
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

#ifndef SPOT_TGBA_TGBAMASK_HH
# define SPOT_TGBA_TGBAMASK_HH

#include "tgbaproxy.hh"
24
#include "bdd.h"
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

namespace spot
{

  /// \ingroup tgba_on_the_fly_algorithms
  /// \brief A masked TGBA (abstract).
  ///
  /// Ignores some states from a TGBA.  What state are preserved or
  /// ignored is controlled by the wanted() method.
  ///
  /// This is an abstract class. You should inherit from it and
  /// supply a wanted() method to specify which states to keep.
  class SPOT_API tgba_mask: public tgba_proxy
  {
  protected:
    /// \brief Constructor.
    /// \param masked The automaton to mask
    /// \param init Any state to use as initial state. This state will be
    /// destroyed by the destructor.
    tgba_mask(const tgba* masked, const state* init = 0);

  public:
    virtual ~tgba_mask();

    virtual state* get_init_state() const;

    virtual tgba_succ_iterator*
52
    succ_iter(const state* local_state) const;
53

54
    virtual bool wanted(const state* s, const bdd& acc) const = 0;
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

  protected:
    const state* init_;
  };

  /// \ingroup tgba_on_the_fly_algorithms
  /// \brief Mask a TGBA, keeping a given set of states.
  ///
  /// Mask the TGBA \a to_mask, keeping only the
  /// states from \a to_keep.  The initial state
  /// can optionally be reset to \a init.
  SPOT_API const tgba*
  build_tgba_mask_keep(const tgba* to_mask,
		       const state_set& to_keep,
		       const state* init = 0);

  /// \ingroup tgba_on_the_fly_algorithms
  /// \brief Mask a TGBA, rejecting a given set of states.
  ///
  /// Mask the TGBA \a to_mask, keeping only the states that are not
  /// in \a to_ignore.  The initial state can optionally be reset to
  /// \a init.
  SPOT_API const tgba*
  build_tgba_mask_ignore(const tgba* to_mask,
			 const state_set& to_ignore,
			 const state* init = 0);

82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

  /// \ingroup tgba_on_the_fly_algorithms
  /// \brief Mask a TGBA, rejecting some acceptance set of transitions.
  ///
  /// This will ignore all transitions labeled by the acceptance ACC
  /// such that ACC & TO_IGNORE != bddfalse.  The initial state can
  /// optionally be reset to \a init.
  ///
  /// Note that the acceptance condition of the automaton (i.e. the
  /// set of all acceptance set) is not changed, because so far this
  /// function is only needed in graph algorithms that do not call
  /// all_acceptance_conditions().
  SPOT_API const tgba*
  build_tgba_mask_acc_ignore(const tgba* to_mask,
			     const bdd to_ignore,
			     const state* init = 0);

99
100
101
}

#endif // SPOT_TGBA_TGBAMASK_HH