kripke.hh 3 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2013, 2014, 2016 Laboratoire de Recherche
// et Developpement de l'Epita
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#pragma once
21

22
#include <spot/kripke/fairkripke.hh>
23
24
25
26

namespace spot
{

27
  /// \ingroup kripke
28
  /// \brief Iterator code for Kripke structure
29
30
31
32
33
34
35
36
37
38
  ///
  /// This iterator can be used to simplify the writing
  /// of an iterator on a Kripke structure (or lookalike).
  ///
  /// If you inherit from this iterator, you should only
  /// redefine
  ///
  ///   - kripke_succ_iterator::first()
  ///   - kripke_succ_iterator::next()
  ///   - kripke_succ_iterator::done()
39
  ///   - kripke_succ_iterator::dst()
40
  ///
41
42
  /// This class implements kripke_succ_iterator::cond(),
  /// and kripke_succ_iterator::acc().
43
  class SPOT_API kripke_succ_iterator : public twa_succ_iterator
44
45
46
47
48
  {
  public:
    /// \brief Constructor
    ///
    /// The \a cond argument will be the one returned
49
    /// by kripke_succ_iterator::cond().
50
51
52
53
54
55
56
57
58
59
    kripke_succ_iterator(const bdd& cond)
      : cond_(cond)
    {
    }

    void recycle(const bdd& cond)
    {
      cond_ = cond;
    }

60
61
    virtual ~kripke_succ_iterator();

62
63
    virtual bdd cond() const override;
    virtual acc_cond::mark_t acc() const override;
64
65
66
  protected:
    bdd cond_;
  };
67

68
  /// \ingroup kripke
69
  /// \brief Interface for a Kripke structure
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
  ///
  /// A Kripke structure is a graph in which each node (=state) is
  /// labeled by a conjunction of atomic proposition.
  ///
  /// Such a structure can be seen as spot::tgba without
  /// any acceptance condition.
  ///
  /// A programmer that develops an instance of Kripke structure needs
  /// just provide an implementation for the following methods:
  ///
  ///   - kripke::get_init_state()
  ///   - kripke::succ_iter()
  ///   - kripke::state_condition()
  ///   - kripke::format_state()
  ///
  /// The other methods of the tgba interface (like those dealing with
  /// acceptance conditions) are supplied by this kripke class and
  /// need not be defined.
  ///
  /// See also spot::kripke_succ_iterator.
90
  class SPOT_API kripke: public fair_kripke
91
92
  {
  public:
93
94
95
96
97
    kripke(const bdd_dict_ptr& d)
      : fair_kripke(d)
      {
      }

98
99
    virtual ~kripke();

100
    virtual acc_cond::mark_t state_acceptance_conditions(const state*) const;
101
  };
102
103
104

  typedef std::shared_ptr<kripke> kripke_ptr;
  typedef std::shared_ptr<const kripke> const_kripke_ptr;
105
}