twacube.hh 6.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche
// et Développement 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/>.

#pragma once

#include <vector>
#include <iosfwd>
#include <spot/graph/graph.hh>
25
#include <spot/misc/hash.hh>
26
27
#include <spot/twa/acc.hh>
#include <spot/twacube/cube.hh>
Etienne Renault's avatar
Etienne Renault committed
28
#include <spot/twacube/fwd.hh>
29
30
31

namespace spot
{
Etienne Renault's avatar
Etienne Renault committed
32
  /// \brief Class for thread-safe states.
33
34
35
  class SPOT_API cstate
  {
  public:
Etienne Renault's avatar
Etienne Renault committed
36
    cstate() = default;
37
38
    cstate(const cstate& s) = delete;
    cstate(cstate&& s) noexcept;
39
    cstate(unsigned id);
Etienne Renault's avatar
Etienne Renault committed
40
41
    ~cstate() = default;

42
    unsigned label();
43
  private:
44
    unsigned id_;
45
46
  };

Etienne Renault's avatar
Etienne Renault committed
47
  /// \brief Class for representing a transition.
48
49
50
  class SPOT_API transition
  {
  public:
Etienne Renault's avatar
Etienne Renault committed
51
    transition() = default;
52
53
54
    transition(const transition& t) = delete;
    transition(transition&& t) noexcept;
    transition(const cube& cube, acc_cond::mark_t acc);
Etienne Renault's avatar
Etienne Renault committed
55
56
57
58
    ~transition() = default;

    cube cube_;
    acc_cond::mark_t acc_;
59
60
  };

Etienne Renault's avatar
Etienne Renault committed
61
  /// \brief Class for iterators over transitions
62
63
  class SPOT_API trans_index final:
    public std::enable_shared_from_this<trans_index>
64
65
66
67
68
69
  {
  public:
    typedef digraph<cstate, transition> graph_t;
    typedef graph_t::edge_storage_t edge_storage_t;

    trans_index(trans_index& ci) = delete;
Antoine Martin's avatar
Antoine Martin committed
70
    trans_index(unsigned state, const graph_t& g):
71
72
73
74
75
76
77
78
79
80
81
      st_(g.state_storage(state))
    {
      reset();
    }

    trans_index(trans_index&& ci):
      idx_(ci.idx_),
      st_(ci.st_)
    {
    }

Etienne Renault's avatar
Etienne Renault committed
82
    /// Reset the iterator on the first element.
83
84
85
86
87
    inline void reset()
    {
      idx_ = st_.succ;
    }

Etienne Renault's avatar
Etienne Renault committed
88
    /// \brief Iterate over the next transition.
89
90
91
92
93
    inline void next()
    {
      ++idx_;
    }

Etienne Renault's avatar
Etienne Renault committed
94
95
    /// \brief Returns a boolean indicating wether all the transitions
    /// have been iterated.
96
97
98
99
100
    inline bool done() const
    {
      return !idx_ || idx_ > st_.succ_tail;
    }

Etienne Renault's avatar
Etienne Renault committed
101
102
    /// \brief Returns the current transition according to a specific
    /// \a seed. The \a  seed is traditionnally the thread identifier.
103
    inline unsigned current(unsigned seed = 0) const
104
105
106
107
    {
      // no-swarming : since twacube are dedicated for parallelism, i.e.
      // swarming, we expect swarming is activated.
      if (SPOT_UNLIKELY(!seed))
108
        return idx_;
109
110
111
112
113
114
      // Here swarming performs a technique called "primitive
      // root modulo n", i. e.  for i in [1..n]: i*seed (mod n). We
      // also must have seed prime with n: to solve this, we use
      // precomputed primes and seed access one of this primes. Note
      // that the chosen prime must be greater than n.
      SPOT_ASSERT(primes[seed] > (st_.succ_tail-st_.succ+1));
115
116
117
118
      unsigned long long c = (idx_-st_.succ) + 1;
      unsigned long long p = primes[seed];
      unsigned long long s = (st_.succ_tail-st_.succ+1);
      return (unsigned)  (((c*p) % s)+st_.succ);
119
120
121
    }

  private:
122
    unsigned idx_;                   ///< The current transition
Etienne Renault's avatar
Etienne Renault committed
123
    const graph_t::state_storage_t& st_; ///< The underlying states
124
125
  };

Etienne Renault's avatar
Etienne Renault committed
126
  /// \brief Class for representing a thread-safe twa.
Etienne Renault's avatar
Etienne Renault committed
127
  class SPOT_API twacube final: public std::enable_shared_from_this<twacube>
128
129
130
  {
  public:
    twacube() = delete;
Etienne Renault's avatar
Etienne Renault committed
131
132

    /// \brief Build a new automaton from a list of atomic propositions.
133
    twacube(const std::vector<std::string> aps);
Etienne Renault's avatar
Etienne Renault committed
134

135
    virtual ~twacube();
Etienne Renault's avatar
Etienne Renault committed
136
137

    /// \brief Returns the acceptance condition associated to the automaton.
138
139
    const acc_cond& acc() const;
    acc_cond& acc();
Etienne Renault's avatar
Etienne Renault committed
140
141

    /// \brief Returns the names of the atomic properties.
142
    std::vector<std::string> get_ap() const;
Etienne Renault's avatar
Etienne Renault committed
143
144

    /// \brief This method creates a new state.
145
    unsigned new_state();
Etienne Renault's avatar
Etienne Renault committed
146
147

    /// \brief Updates the initial state to \a init
148
    void set_initial(unsigned init);
Etienne Renault's avatar
Etienne Renault committed
149
150

    /// \brief Returns the id of the initial state in the automaton.
151
    unsigned get_initial();
Etienne Renault's avatar
Etienne Renault committed
152
153

    /// \brief Accessor for a state from its id.
154
    cstate* state_from_int(unsigned i);
Etienne Renault's avatar
Etienne Renault committed
155
156
157

    /// \brief create a transition between state \a src and state \a dst,
    /// using \a cube as the labelling cube and \a mark as the acceptance mark.
158
    void create_transition(unsigned src,
Etienne Renault's avatar
Etienne Renault committed
159
160
                           const cube& cube,
                           const acc_cond::mark_t& mark,
161
                           unsigned dst);
Etienne Renault's avatar
Etienne Renault committed
162
163

    /// \brief Accessor the cube's manipulator.
164
    const cubeset& get_cubeset() const;
Etienne Renault's avatar
Etienne Renault committed
165
166
167

    /// \brief Check if all the successors of a state are located contigously
    /// in memory. This is mandatory for swarming techniques.
168
    bool succ_contiguous() const;
Etienne Renault's avatar
Etienne Renault committed
169

170
171
172
173
174
175
176
177
178
    unsigned num_states() const
    {
      return theg_.num_states();
    }

    unsigned num_edges() const
    {
      return theg_.num_edges();
    }
Etienne Renault's avatar
Etienne Renault committed
179

180
    typedef digraph<cstate, transition> graph_t;
Etienne Renault's avatar
Etienne Renault committed
181
182

    /// \brief Returns the underlying graph for this automaton.
183
184
185
186
187
    const graph_t& get_graph()
    {
      return theg_;
    }
    typedef graph_t::edge_storage_t edge_storage_t;
Etienne Renault's avatar
Etienne Renault committed
188
189

    /// \brief Returns the storage associated to a transition.
190
    const graph_t::edge_storage_t&
Etienne Renault's avatar
Etienne Renault committed
191
    trans_storage(std::shared_ptr<trans_index> ci,
192
                  unsigned seed = 0) const
193
194
195
    {
      return theg_.edge_storage(ci->current(seed));
    }
Etienne Renault's avatar
Etienne Renault committed
196
197

    /// \brief Returns the data associated to a transition.
198
    const transition& trans_data(std::shared_ptr<trans_index> ci,
199
                                 unsigned seed = 0) const
200
201
202
203
    {
      return theg_.edge_data(ci->current(seed));
    }

Etienne Renault's avatar
Etienne Renault committed
204
    ///< \brief Returns the successor of state \a i.
Antoine Martin's avatar
Antoine Martin committed
205
    std::shared_ptr<trans_index> succ(unsigned i) const
206
207
208
209
210
    {
      return std::make_shared<trans_index>(i, theg_);
    }

    friend SPOT_API std::ostream& operator<<(std::ostream& os,
211
                                             const twacube& twa);
212
  private:
213
    unsigned init_;                  ///< The Id of the initial state
Etienne Renault's avatar
Etienne Renault committed
214
215
216
217
    acc_cond acc_;                       ///< The acceptance contidion
    const std::vector<std::string> aps_; ///< The name of atomic propositions
    graph_t theg_;                       ///< The underlying graph
    cubeset cubeset_;                    ///< Ease the cube manipulation
218
  };
Etienne Renault's avatar
Etienne Renault committed
219
220
221
222
223

  inline twacube_ptr make_twacube(const std::vector<std::string> aps)
  {
    return std::make_shared<twacube>(aps);
  }
224
}