emptinessta.cc 19.8 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2010-2016, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
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
//#define TRACE
21

22
#include "config.h"
23 24 25 26 27 28 29
#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

30 31
#include <spot/taalgos/emptinessta.hh>
#include <spot/misc/memusage.hh>
32
#include <cstdlib>
33
#include <spot/twa/bddprint.hh>
34 35 36 37

namespace spot
{

38
  ta_check::ta_check(const const_ta_product_ptr& a, option_map o) :
39 40 41 42 43 44 45 46 47 48
    a_(a), o_(o)
  {
    is_full_2_pass_ = o.get("is_full_2_pass", 0);
  }

  ta_check::~ta_check()
  {
  }

  bool
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
49
  ta_check::check(bool disable_second_pass,
50
      bool disable_heuristic_for_livelock_detection)
51 52 53 54
  {

    // We use five main data in this algorithm:

55
    // * scc: (attribute) a stack of strongly connected components (SCC)
56 57

    // * arc, a stack of acceptance conditions between each of these SCC,
58
    std::stack<acc_cond::mark_t> arc;
59

60 61
    // * h: a hash of all visited nodes, with their order,
    //   (it is called "Hash" in Couvreur's paper)
62
    hash_type h;
63 64 65 66 67 68

    // * num: the number of visited nodes.  Used to set the order of each
    //   visited node,
    int num = 1;

    // * todo: the depth-first search stack.  This holds pairs of the
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
69
    //   form (STATE, ITERATOR) where ITERATOR is a ta_succ_iterator_product
70 71 72 73 74 75 76 77
    //   over the successors of STATE.  In our use, ITERATOR should
    //   always be freed when TODO is popped, but STATE should not because
    //   it is also used as a key in H.
    std::stack<pair_state_iter> todo;

    trace
      << "PASS 1" << std::endl;

78
    state_map<std::set<const state*, state_ptr_less_than>> liveset;
79 80 81

    std::stack<spot::state*> livelock_roots;

82 83
    bool livelock_acceptance_states_not_found = true;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
84 85
    bool activate_heuristic = !disable_heuristic_for_livelock_detection
        && (is_full_2_pass_ == disable_second_pass);
86

87
    // Setup depth-first search from initial states.
88 89
    auto& ta_ = a_->get_ta();
    auto& kripke_ = a_->get_kripke();
90
    auto kripke_init_state = kripke_->get_init_state();
91 92
    bdd kripke_init_state_condition = kripke_->state_condition(
        kripke_init_state);
93

94
    auto artificial_initial_state = ta_->get_artificial_initial_state();
95

96 97 98 99
    ta_succ_iterator* ta_init_it_ = ta_->succ_iter(artificial_initial_state,
        kripke_init_state_condition);
    kripke_init_state->destroy();
    for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next())
100
      {
101

102
        state_ta_product* init = new state_ta_product(
103
            (ta_init_it_->dst()), kripke_init_state->clone());
104

105
        if (!h.emplace(init, num + 1).second)
106 107 108 109
          {
            init->destroy();
            continue;
          }
110

111
        scc.push(++num);
112
        arc.push(0U);
113

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
114
        ta_succ_iterator_product* iter = a_->succ_iter(init);
115
        iter->first();
116
        todo.emplace(init, iter);
117

118
        inc_depth();
119

120 121 122
        //push potential root of live-lock accepting cycle
        if (activate_heuristic && a_->is_livelock_accepting_state(init))
          livelock_roots.push(init);
123 124 125

        while (!todo.empty())
          {
126
            auto curr = todo.top().first;
127 128

            // We are looking at the next successor in SUCC.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
129
            ta_succ_iterator_product* succ = todo.top().second;
130 131 132 133 134 135 136 137 138 139

            // If there is no more successor, backtrack.
            if (succ->done())
              {
                // We have explored all successors of state CURR.


                // Backtrack TODO.
                todo.pop();
                dec_depth();
140
                trace << "PASS 1 : backtrack\n";
141

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
142 143
                if (a_->is_livelock_accepting_state(curr)
                    && !a_->is_accepting_state(curr))
144 145
                  {
                    livelock_acceptance_states_not_found = false;
146
                    trace << "PASS 1 : livelock accepting state found\n";
147 148 149
                  }

                // fill rem with any component removed,
150
                auto i = h.find(curr);
151
                assert(i != h.end());
152 153 154 155 156

                scc.rem().push_front(curr);
                inc_depth();

                // set the h value of the Backtracked state to negative value.
157
                i->second = -std::abs(i->second);
158 159

                // Backtrack livelock_roots.
160 161
                if (activate_heuristic && !livelock_roots.empty()
                    && !livelock_roots.top()->compare(curr))
162 163 164 165 166 167
                  livelock_roots.pop();

                // When backtracking the root of an SSCC, we must also
                // remove that SSCC from the ROOT stacks.  We must
                // discard from H all reachable states from this SSCC.
                assert(!scc.empty());
168
                if (scc.top().index == std::abs(i->second))
169 170
                  {
                    // removing states
171
                    for (auto j: scc.rem())
172
                      h[j] = -1;
173 174
                    dec_depth(scc.rem().size());
                    scc.pop();
175 176 177
                    assert(!arc.empty());
                    arc.pop();

178 179 180 181 182 183 184 185 186
                  }

                delete succ;
                // Do not delete CURR: it is a key in H.
                continue;
              }

            // We have a successor to look at.
            inc_transitions();
187
            trace << "PASS 1: transition\n";
188
            // Fetch the values destination state we are interested in...
189
            state* dest = succ->dst();
190

191
            auto acc_cond = succ->acc();
192

193 194 195 196
            bool curr_is_livelock_hole_state_in_ta_component =
                (a_->is_hole_state_in_ta_component(curr))
                    && a_->is_livelock_accepting_state(curr);

197 198 199
            // May be Buchi accepting scc or livelock accepting scc
            // (contains a livelock accepting state that have no
            // successors in TA).
200
            scc.top().is_accepting = (a_->is_accepting_state(curr)
201 202
                && (!succ->is_stuttering_transition()
                    || a_->is_livelock_accepting_state(curr)))
203 204 205 206 207 208 209 210 211 212
                || curr_is_livelock_hole_state_in_ta_component;

            bool is_stuttering_transition = succ->is_stuttering_transition();

            // ... and point the iterator to the next successor, for
            // the next iteration.
            succ->next();
            // We do not need SUCC from now on.

            // Are we going to a new state?
213
            auto p = h.emplace(dest, num + 1);
214
            if (p.second)
215 216 217
              {
                // Number it, stack it, and register its successors
                // for later processing.
218
                scc.push(++num);
219
                arc.push(acc_cond);
220

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
221
                ta_succ_iterator_product* iter = a_->succ_iter(dest);
222
                iter->first();
223
                todo.emplace(dest, iter);
224 225 226
                inc_depth();

                //push potential root of live-lock accepting cycle
227
                if (activate_heuristic && a_->is_livelock_accepting_state(dest)
228 229 230 231 232 233 234
                    && !is_stuttering_transition)
                  livelock_roots.push(dest);

                continue;
              }

            // If we have reached a dead component, ignore it.
235
            if (p.first->second == -1)
236 237 238 239 240 241 242 243 244 245 246 247 248
              continue;

            // Now this is the most interesting case.  We have reached a
            // state S1 which is already part of a non-dead SSCC.  Any such
            // non-dead SSCC has necessarily been crossed by our path to
            // this state: there is a state S2 in our path which belongs
            // to this SSCC too.  We are going to merge all states between
            // this S1 and S2 into this SSCC.
            //
            // This merge is easy to do because the order of the SSCC in
            // ROOT is ascending: we just have to merge all SSCCs from the
            // top of ROOT that have an index greater to the one of
            // the SSCC of S2 (called the "threshold").
249
            int threshold = std::abs(p.first->second);
250
            std::list<const state*> rem;
251 252
            bool acc = false;

253
            trace << "***PASS 1: CYCLE***\n";
254

255 256 257
            while (threshold < scc.top().index)
              {
                assert(!scc.empty());
258
                assert(!arc.empty());
259 260

                acc |= scc.top().is_accepting;
261 262
                acc_cond |= scc.top().condition;
                acc_cond |= arc.top();
263 264 265

                rem.splice(rem.end(), scc.rem());
                scc.pop();
266
                arc.pop();
267 268

              }
269

270 271 272 273 274 275 276
            // Note that we do not always have
            //  threshold == scc.top().index
            // after this loop, the SSCC whose index is threshold might have
            // been merged with a lower SSCC.

            // Accumulate all acceptance conditions into the merged SSCC.
            scc.top().is_accepting |= acc;
277
            scc.top().condition |= acc_cond;
278 279

            scc.rem().splice(scc.rem().end(), rem);
280
            bool is_accepting_sscc = scc.top().is_accepting
281
              || a_->acc().accepting(scc.top().condition);
282 283

            if (is_accepting_sscc)
284 285
              {
                trace
286 287
                  << "PASS 1: SUCCESS: a_->is_livelock_accepting_state(curr): "
                  << a_->is_livelock_accepting_state(curr) << '\n';
288
                trace
289
                  << "PASS 1: scc.top().condition : "
290
                  << scc.top().condition << '\n';
291
                trace
292
                  << "PASS 1: a_->acc().all_sets() : "
293
                  << (a_->acc().all_sets()) << '\n';
294
                trace
295 296 297
                  << ("PASS 1 CYCLE and accepting? ")
                  << a_->acc().accepting(scc.top().condition)
                  << std::endl;
298
                clear(h, todo, ta_init_it_);
299 300 301 302
                return true;
              }

            //ADDLINKS
303
            if (activate_heuristic && a_->is_livelock_accepting_state(curr)
304 305
                && is_stuttering_transition)
              {
306 307
                trace << "PASS 1: heuristic livelock detection \n";
                const state* dest = p.first->first;
308 309 310 311 312 313 314 315
                std::set<const state*, state_ptr_less_than> liveset_dest =
                    liveset[dest];

                std::set<const state*, state_ptr_less_than> liveset_curr =
                    liveset[curr];

                int h_livelock_root = 0;
                if (!livelock_roots.empty())
316
                  h_livelock_root = h[livelock_roots.top()];
317 318

                if (heuristic_livelock_detection(dest, h, h_livelock_root,
319
                                                 liveset_curr))
320
                  {
321
                    clear(h, todo, ta_init_it_);
322 323 324
                    return true;
                  }

325
                for (const state* succ: liveset_dest)
326 327 328 329 330 331
                  if (heuristic_livelock_detection(succ, h, h_livelock_root,
                                                   liveset_curr))
                    {
                      clear(h, todo, ta_init_it_);
                      return true;
                    }
332 333
              }
          }
334 335 336

      }

337
    clear(h, todo, ta_init_it_);
338 339 340 341

    if (disable_second_pass || livelock_acceptance_states_not_found)
      return false;

342 343 344 345 346
    return livelock_detection(a_);
  }

  bool
  ta_check::heuristic_livelock_detection(const state * u,
347
      hash_type& h, int h_livelock_root, std::set<const state*,
348
          state_ptr_less_than> liveset_curr)
349
  {
350
    int hu = h[u];
351

352
    if (hu > 0)
353 354
      {

355
        if (hu >= h_livelock_root)
356
          {
357
            trace << "PASS 1: heuristic livelock detection SUCCESS\n";
358 359
            return true;
          }
360

361
        liveset_curr.insert(u);
362 363 364 365 366
      }
    return false;
  }

  bool
367
  ta_check::livelock_detection(const const_ta_product_ptr& t)
368 369 370 371 372 373 374 375
  {
    // We use five main data in this algorithm:

    // * sscc: a stack of strongly stuttering-connected components (SSCC)


    // * h: a hash of all visited nodes, with their order,
    //   (it is called "Hash" in Couvreur's paper)
376
    hash_type h;
377 378 379 380 381 382 383 384 385 386

    // * num: the number of visited nodes.  Used to set the order of each
    //   visited node,

    trace
      << "PASS 2" << std::endl;

    int num = 0;

    // * todo: the depth-first search stack.  This holds pairs of the
387
    //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
388 389 390 391 392 393
    //   over the successors of STATE.  In our use, ITERATOR should
    //   always be freed when TODO is popped, but STATE should not because
    //   it is also used as a key in H.
    std::stack<pair_state_iter> todo;

    // * init: the set of the depth-first search initial states
394
    std::queue<const spot::state*> ta_init_it_;
395

396 397 398
    auto init_states_set = a_->get_initial_states_set();
    for (auto init_state: init_states_set)
      ta_init_it_.push(init_state);
399

400
    while (!ta_init_it_.empty())
401
      {
402 403
        // Setup depth-first search from initial states.
          {
404
            auto init = ta_init_it_.front();
405
            ta_init_it_.pop();
406

407 408 409 410 411
            if (!h.emplace(init, num + 1).second)
              {
                init->destroy();
                continue;
              }
412 413 414

            sscc.push(num);
            sscc.top().is_accepting = t->is_livelock_accepting_state(init);
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
415
            ta_succ_iterator_product* iter = t->succ_iter(init);
416
            iter->first();
417
            todo.emplace(init, iter);
418 419 420 421 422
            inc_depth();
          }

        while (!todo.empty())
          {
423
            auto curr = todo.top().first;
424 425

            // We are looking at the next successor in SUCC.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
426
            ta_succ_iterator_product* succ = todo.top().second;
427 428 429 430 431 432 433 434 435

            // If there is no more successor, backtrack.
            if (succ->done())
              {
                // We have explored all successors of state CURR.

                // Backtrack TODO.
                todo.pop();
                dec_depth();
436
                trace << "PASS 2 : backtrack\n";
437 438

                // fill rem with any component removed,
439
                auto i = h.find(curr);
440
                assert(i != h.end());
441 442 443 444 445 446 447 448

                sscc.rem().push_front(curr);
                inc_depth();

                // When backtracking the root of an SSCC, we must also
                // remove that SSCC from the ROOT stacks.  We must
                // discard from H all reachable states from this SSCC.
                assert(!sscc.empty());
449
                if (sscc.top().index == i->second)
450 451
                  {
                    // removing states
452
                    for (auto j: sscc.rem())
453
                      h[j] = -1;
454 455 456 457 458 459 460 461 462 463 464 465
                    dec_depth(sscc.rem().size());
                    sscc.pop();
                  }

                delete succ;
                // Do not delete CURR: it is a key in H.

                continue;
              }

            // We have a successor to look at.
            inc_transitions();
466
            trace << "PASS 2 : transition\n";
467
            // Fetch the values destination state we are interested in...
468
            state* dest = succ->dst();
469 470 471 472 473 474 475

            bool is_stuttering_transition = succ->is_stuttering_transition();
            // ... and point the iterator to the next successor, for
            // the next iteration.
            succ->next();
            // We do not need SUCC from now on.

476
            auto i = h.find(dest);
477 478

            // Is this a new state?
479
            if (i == h.end())
480 481 482 483 484 485
              {

                // Are we going to a new state through a stuttering transition?

                if (!is_stuttering_transition)
                  {
486
                    ta_init_it_.push(dest);
487 488 489 490 491
                    continue;
                  }

                // Number it, stack it, and register its successors
                // for later processing.
492
                h[dest] = ++num;
493 494 495
                sscc.push(num);
                sscc.top().is_accepting = t->is_livelock_accepting_state(dest);

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
496
                ta_succ_iterator_product* iter = t->succ_iter(dest);
497
                iter->first();
498
                todo.emplace(dest, iter);
499 500 501
                inc_depth();
                continue;
              }
502 503 504 505
            else
              {
                dest->destroy();
              }
506 507

            // If we have reached a dead component, ignore it.
508
            if (i->second == -1)
509 510 511
              continue;

            //self loop state
512
            if (!curr->compare(i->first))
513 514 515 516 517 518
              if (t->is_livelock_accepting_state(curr))
                {
                  clear(h, todo, ta_init_it_);
                  trace << "PASS 2: SUCCESS\n";
                  return true;
                }
519 520 521 522 523 524 525 526 527 528 529 530

            // Now this is the most interesting case.  We have reached a
            // state S1 which is already part of a non-dead SSCC.  Any such
            // non-dead SSCC has necessarily been crossed by our path to
            // this state: there is a state S2 in our path which belongs
            // to this SSCC too.  We are going to merge all states between
            // this S1 and S2 into this SSCC.
            //
            // This merge is easy to do because the order of the SSCC in
            // ROOT is ascending: we just have to merge all SSCCs from the
            // top of ROOT that have an index greater to the one of
            // the SSCC of S2 (called the "threshold").
531
            int threshold = i->second;
532
            std::list<const state*> rem;
533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
            bool acc = false;

            while (threshold < sscc.top().index)
              {
                assert(!sscc.empty());

                acc |= sscc.top().is_accepting;

                rem.splice(rem.end(), sscc.rem());
                sscc.pop();

              }
            // Note that we do not always have
            //  threshold == sscc.top().index
            // after this loop, the SSCC whose index is threshold might have
            // been merged with a lower SSCC.

            // Accumulate all acceptance conditions into the merged SSCC.
            sscc.top().is_accepting |= acc;

            sscc.rem().splice(sscc.rem().end(), rem);
            if (sscc.top().is_accepting)
              {
556
                clear(h, todo, ta_init_it_);
557 558 559 560 561
                trace
                  << "PASS 2: SUCCESS" << std::endl;
                return true;
              }
          }
562 563

      }
564
    clear(h, todo, ta_init_it_);
565 566 567 568
    return false;
  }

  void
569
  ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo,
570
      std::queue<const spot::state*> init_states)
571 572
  {

573
    set_states(states() + h.size());
574 575 576

    while (!init_states.empty())
      {
577
        a_->free_state(init_states.front());
578
        init_states.pop();
579 580 581 582 583
      }

    // Release all iterators in TODO.
    while (!todo.empty())
      {
584 585 586
        delete todo.top().second;
        todo.pop();
        dec_depth();
587 588 589
      }
  }

590
  void
591
  ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo,
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
592 593
      spot::ta_succ_iterator* init_states_it)
  {
594

595
    set_states(states() + h.size());
596 597 598

    delete init_states_it;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
599 600 601 602 603 604 605 606
    // Release all iterators in TODO.
    while (!todo.empty())
      {
        delete todo.top().second;
        todo.pop();
        dec_depth();
      }
  }
607

608 609 610 611 612 613 614 615
  std::ostream&
  ta_check::print_stats(std::ostream& os) const
  {
    //    ecs_->print_stats(os);
    os << states() << " unique states visited" << std::endl;

    //TODO  sscc;
    os << scc.size() << " strongly connected components in search stack"
616
        << std::endl;
617 618 619 620 621 622 623 624 625
    os << transitions() << " transitions explored" << std::endl;
    os << max_depth() << " items max in DFS search stack" << std::endl;
    return os;
  }

//////////////////////////////////////////////////////////////////////


}