kripke.hh 5.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017 Laboratoire de Recherche
3
// 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
#include <spot/twacube/cube.hh>
Etienne Renault's avatar
Etienne Renault committed
24
#include <memory>
25
26
27

namespace spot
{
28
29
30
31
32
33
34
35
36
  /// \brief This class is a template representation of a Kripke
  /// structure. It is composed of two template parameters: State
  /// represents a state of the Kripke structure, SuccIterator is
  /// an iterator over the (possible) successors of a state.
  ///
  /// Do not delete by hand any states and/or iterator that
  /// are provided by this template class. Specialisations
  /// will handle it.
  template<typename State, typename SuccIterator>
Etienne Renault's avatar
Etienne Renault committed
37
38
  class SPOT_API kripkecube:
    public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
39
40
  {
  public:
41
42
43
    /// \brief Returns the initial State of the System. The \a tid parameter
    /// is used internally for sharing this structure among threads.
    State initial(unsigned tid);
44
45

    /// \brief Provides a string representation of the parameter state
46
    std::string to_string(const State, unsigned tid) const;
47
48

    /// \brief Returns an iterator over the successors of the parameter state.
49
    SuccIterator* succ(const State, unsigned tid);
50
51
52

    /// \brief Allocation and deallocation of iterator is costly. This
    /// method allows to reuse old iterators.
53
    void recycle(SuccIterator*, unsigned tid);
54
55
56
57
58
59
60
61
62
63
64
65

    /// \brief This method allow to deallocate a given state.
    const std::vector<std::string> get_ap();
  };

  /// \brief This method allows to ensure (at compile time) if
  /// a given parameter is of type kripkecube. It also check
  /// if the iterator has the good interface.
  template <typename State, typename SuccIter>
  bool is_a_kripkecube(kripkecube<State, SuccIter>&)
  {
    // Hardly waiting C++17 concepts...
66
    State (kripkecube<State, SuccIter>::*test_initial)(unsigned) =
67
68
      &kripkecube<State, SuccIter>::initial;
    std::string (kripkecube<State, SuccIter>::*test_to_string)
69
70
      (const State, unsigned) const = &kripkecube<State, SuccIter>::to_string;
    auto (kripkecube<State, SuccIter>::*test_recycle)(SuccIter*, unsigned) =
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
      &kripkecube<State, SuccIter>::recycle;
    const std::vector<std::string>
      (kripkecube<State, SuccIter>::*test_get_ap)() =
      &kripkecube<State, SuccIter>::get_ap;
    void (SuccIter::*test_next)() = &SuccIter::next;
    State (SuccIter::*test_state)() const= &SuccIter::state;
    bool (SuccIter::*test_done)() const= &SuccIter::done;
    cube (SuccIter::*test_condition)() const = &SuccIter::condition;

    // suppress warnings about unused variables
    (void) test_initial;
    (void) test_to_string;
    (void) test_recycle;
    (void) test_get_ap;
    (void) test_next;
    (void) test_state;
    (void) test_done;
    (void) test_condition;

    // Always return true since otherwise a compile-time error will be raised.
    return true;
92
  }
93

94
  /// \ingroup kripke
95
  /// \brief Iterator code for Kripke structure
96
97
98
99
100
101
102
103
104
105
  ///
  /// 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()
106
  ///   - kripke_succ_iterator::dst()
107
  ///
108
109
  /// This class implements kripke_succ_iterator::cond(),
  /// and kripke_succ_iterator::acc().
110
  class SPOT_API kripke_succ_iterator : public twa_succ_iterator
111
112
113
114
115
  {
  public:
    /// \brief Constructor
    ///
    /// The \a cond argument will be the one returned
116
    /// by kripke_succ_iterator::cond().
117
118
119
120
121
122
123
124
125
126
    kripke_succ_iterator(const bdd& cond)
      : cond_(cond)
    {
    }

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

127
128
    virtual ~kripke_succ_iterator();

129
130
    virtual bdd cond() const override;
    virtual acc_cond::mark_t acc() const override;
131
132
133
  protected:
    bdd cond_;
  };
134

135
  /// \ingroup kripke
136
  /// \brief Interface for a Kripke structure
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
  ///
  /// 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.
157
  class SPOT_API kripke: public fair_kripke
158
159
  {
  public:
160
161
162
163
164
    kripke(const bdd_dict_ptr& d)
      : fair_kripke(d)
      {
      }

165
166
    virtual ~kripke();

167
    virtual
168
      acc_cond::mark_t state_acceptance_mark(const state*) const override;
169
  };
170
171
172

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