ec.hh 9.48 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
25
26
27
28
29
30
31
32
33
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// 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 <spot/twa/acc.hh>
#include <spot/mc/unionfind.hh>
#include <spot/mc/intersect.hh>

namespace spot
{
  /// \brief This class implements the sequential emptiness check as
  /// presented in "Three SCC-based Emptiness Checks for Generalized
  /// B\¨uchi Automata" (Renault et al, LPAR 2013). Among the three
  /// emptiness check that has been proposed we opted to implement
  /// the Gabow's one.
  template<typename State, typename SuccIterator,
34
           typename StateHash, typename StateEqual>
35
  class ec_renault13lpar  : public intersect<State, SuccIterator,
36
37
38
                                       StateHash, StateEqual,
                                       ec_renault13lpar<State, SuccIterator,
                                                        StateHash, StateEqual>>
39
40
41
  {
    // Ease the manipulation
    using typename intersect<State, SuccIterator, StateHash, StateEqual,
42
43
44
                             ec_renault13lpar<State, SuccIterator,
                                              StateHash,
                                              StateEqual>>::product_state;
45
46
47

  public:
    ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
48
                     twacube_ptr twa, unsigned tid, bool stop)
49
      : intersect<State, SuccIterator, StateHash, StateEqual,
50
                  ec_renault13lpar<State, SuccIterator,
51
                                   StateHash, StateEqual>>(sys, twa, tid, stop),
52
      acc_(twa->acc()), sccs_(0U)
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
78
79
80
81
82
83
84
85
86
      {
      }

    virtual ~ec_renault13lpar()
    {

    }

    /// \brief This method is called at the begining of the exploration.
    /// here we do not need to setup any information.
    void setup()
    {
    }

    /// \brief This method is called to notify the emptiness checks
    /// that a new state has been discovered. If this method return
    /// false, the state will not be explored. The parameter \a dfsnum
    /// specify an unique id for the state \a s. Parameter \a cond represents
    /// The value on the ingoing edge to \a s.
    bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond)
    {
      uf_.makeset(dfsnum);
      roots_.push_back({dfsnum, cond, 0U});
      return true;
    }

    /// \brief This method is called to notify the emptiness checks
    /// that a state will be popped. If the method return false, then
    /// the state will be popped. Otherwise the state \a newtop will
    /// become the new top of the DFS stack. If the state \a top is
    /// the only one in the DFS stak, the parameter \a is_initial is set
    /// to true and both \a newtop and \a  newtop_dfsnum have inconsistency
    /// values.
    bool pop_state(product_state, unsigned top_dfsnum, bool,
87
                   product_state, unsigned)
88
89
    {
      if (top_dfsnum == roots_.back().dfsnum)
90
91
        {
          roots_.pop_back();
92
          ++sccs_;
93
94
          uf_.markdead(top_dfsnum);
        }
95
      dfs_ = this->todo.size()  > dfs_ ? this->todo.size() : dfs_;
96
97
98
99
100
101
102
103
104
105
      return true;
    }

    /// \brief This method is called for every closing, back, or forward edge.
    /// Return true if a counterexample has been found.
    bool update(product_state, unsigned,
                product_state, unsigned dst_dfsnum,
                acc_cond::mark_t cond)
    {
      if (uf_.isdead(dst_dfsnum))
106
        return false;
107
108
109
110
111
112
113
114
115
116

      while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
        {
          auto& el = roots_.back();
          roots_.pop_back();
          uf_.unite(dst_dfsnum, el.dfsnum);
          cond |= el.acc | el.ingoing;
        }
      roots_.back().acc |= cond;
      found_ = acc_.accepting(roots_.back().acc);
117
118
      if (SPOT_UNLIKELY(found_))
        this->stop_ = true;
119
120
121
122
123
124
125
126
127
128
      return found_;
    }

    bool counterexample_found()
    {
      return found_;
    }

    std::string trace()
    {
129
      SPOT_ASSERT(counterexample_found());
130
131
132
133
      std::string res = "Prefix:\n";

       // Compute the prefix of the accepting run
      for (auto& s : this->todo)
134
135
        res += "  " + std::to_string(s.st.st_prop) +
          + "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
136
137
138
139
140
141

      // Compute the accepting cycle
      res += "Cycle:\n";

      struct ctrx_element
      {
142
143
144
145
        const product_state* prod_st;
        ctrx_element* parent_st;
        SuccIterator* it_kripke;
        std::shared_ptr<trans_index> it_prop;
146
147
148
149
150
151
      };
      std::queue<ctrx_element*> bfs;

      acc_cond::mark_t acc = 0U;

      bfs.push(new ctrx_element({&this->todo.back().st, nullptr,
152
              this->sys_.succ(this->todo.back().st.st_kripke, this->tid_),
153
154
              this->twa_->succ(this->todo.back().st.st_prop)}));
      while (true)
155
156
157
158
159
160
161
162
163
164
        {
        here:
          auto* front = bfs.front();
          bfs.pop();
          // PUSH all successors of the state.
          while (!front->it_kripke->done())
            {
              while (!front->it_prop->done())
                {
                  if (this->twa_->get_cubeset().intersect
165
                      (this->twa_->trans_data(front->it_prop, this->tid_).cube_,
166
167
168
169
170
171
                       front->it_kripke->condition()))
                    {
                      const product_state dst = {
                        front->it_kripke->state(),
                        this->twa_->trans_storage(front->it_prop).dst
                      };
172

173
174
175
176
177
178
179
180
181
                      // Skip Unknown states or not same SCC
                      auto it  = this->map.find(dst);
                      if (it == this->map.end() ||
                          !uf_.sameset(it->second,
                                       this->map[this->todo.back().st]))
                        {
                          front->it_prop->next();
                          continue;
                        }
182

183
184
185
                      // This is a valid transition. If this transition
                      // is the one we are looking for, update the counter-
                      // -example and flush the bfs queue.
186
187
                      auto mark = this->twa_->trans_data(front->it_prop,
                                                         this->tid_).acc_;
188
                      if (!acc.has(mark.id))
189
190
191
192
193
194
195
196
197
198
199
200
201
                        {
                          ctrx_element* current = front;
                          while (current != nullptr)
                            {
                              // FIXME also display acc?
                              res = res + "  " +
                                std::to_string(current->prod_st->st_prop) +
                                + "*" +
                                this->sys_. to_string(current->prod_st
                                                      ->st_kripke) +
                                "\n";
                              current = current->parent_st;
                            }
202

203
204
205
206
207
208
209
                          // empty the queue
                          while (!bfs.empty())
                            {
                              auto* e = bfs.front();
                              bfs.pop();
                              delete e;
                            }
210

211
212
213
214
                          // update acceptance
                          acc |= mark;
                          if (this->twa_->acc().accepting(acc))
                            return res;
215
216
217
218

                          const product_state* q = &(it->first);
                          ctrx_element* root = new ctrx_element({
                              q , nullptr,
219
                              this->sys_.succ(q->st_kripke, this->tid_),
220
221
222
223
224
225
226
227
228
229
                              this->twa_->succ(q->st_prop)
                          });
                          bfs.push(root);
                          goto here;
                        }

                      // Otherwise increment iterator and push successor.
                      const product_state* q = &(it->first);
                      ctrx_element* root = new ctrx_element({
                          q , nullptr,
230
                          this->sys_.succ(q->st_kripke, this->tid_),
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
                          this->twa_->succ(q->st_prop)
                      });
                      bfs.push(root);
                    }
                  front->it_prop->next();
                }
              front->it_prop->reset();
              front->it_kripke->next();
            }
        }

      // never reach here;
      return res;
    }

246
    virtual istats stats() override
247
    {
248
      return {this->states(), this->trans(), sccs_,
249
          (unsigned) roots_.size(), dfs_, found_};
250
251
252
253
    }

  private:

254
    bool found_ = false;        ///< \brief A counterexample is detected?
255
256
257
258
259
260
261
262
263
264
265

    struct root_element {
      unsigned dfsnum;
      acc_cond::mark_t ingoing;
      acc_cond::mark_t acc;
    };

    /// \brief the root stack.
    std::vector<root_element> roots_;
    int_unionfind uf_;
    acc_cond acc_;
266
267
    unsigned sccs_;
    unsigned dfs_;
268
269
  };
}