emptinessta.cc 19.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 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
23
24
25
26
27
28

#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

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

namespace spot
{

37
  ta_check::ta_check(const const_ta_product_ptr& a, option_map o) :
38
39
40
41
42
43
44
45
46
47
    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
48
  ta_check::check(bool disable_second_pass,
49
      bool disable_heuristic_for_livelock_detection)
50
51
52
53
  {

    // We use five main data in this algorithm:

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

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

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

    // * 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
68
    //   form (STATE, ITERATOR) where ITERATOR is a ta_succ_iterator_product
69
70
71
72
73
74
75
76
    //   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;

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

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

81
82
    bool livelock_acceptance_states_not_found = true;

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

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

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

95
96
97
98
    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())
99
      {
100

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

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

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

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

117
        inc_depth();
118

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

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

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

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


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

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

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

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

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

                // Backtrack livelock_roots.
159
160
                if (activate_heuristic && !livelock_roots.empty()
                    && !livelock_roots.top()->compare(curr))
161
162
163
164
165
166
                  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());
167
                if (scc.top().index == std::abs(i->second))
168
169
                  {
                    // removing states
170
                    for (auto j: scc.rem())
171
		      h[j] = -1;
172
173
                    dec_depth(scc.rem().size());
                    scc.pop();
174
175
176
                    assert(!arc.empty());
                    arc.pop();

177
178
179
180
181
182
183
184
185
                  }

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

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

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

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

196
197
198
            // May be Buchi accepting scc or livelock accepting scc
            // (contains a livelock accepting state that have no
            // successors in TA).
199
            scc.top().is_accepting = (a_->is_accepting_state(curr)
200
201
                && (!succ->is_stuttering_transition()
                    || a_->is_livelock_accepting_state(curr)))
202
203
204
205
206
207
208
209
210
211
                || 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?
212
	    auto p = h.emplace(dest, num + 1);
213
            if (p.second)
214
215
216
              {
                // Number it, stack it, and register its successors
                // for later processing.
217
                scc.push(++num);
218
                arc.push(acc_cond);
219

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

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

                continue;
              }

            // If we have reached a dead component, ignore it.
234
            if (p.first->second == -1)
235
236
237
238
239
240
241
242
243
244
245
246
247
              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").
248
            int threshold = std::abs(p.first->second);
249
            std::list<const state*> rem;
250
251
            bool acc = false;

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

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

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

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

              }
268

269
270
271
272
273
274
275
            // 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;
276
            scc.top().condition |= acc_cond;
277
278

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

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

            //ADDLINKS
302
            if (activate_heuristic && a_->is_livelock_accepting_state(curr)
303
304
                && is_stuttering_transition)
              {
305
306
                trace << "PASS 1: heuristic livelock detection \n";
                const state* dest = p.first->first;
307
308
309
310
311
312
313
314
                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())
315
                  h_livelock_root = h[livelock_roots.top()];
316
317

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

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

      }

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

    if (disable_second_pass || livelock_acceptance_states_not_found)
      return false;

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

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

351
    if (hu > 0)
352
353
      {

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

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

  bool
366
  ta_check::livelock_detection(const const_ta_product_ptr& t)
367
368
369
370
371
372
373
374
  {
    // 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)
375
    hash_type h;
376
377
378
379
380
381
382
383
384
385

    // * 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
386
    //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
387
388
389
390
391
392
    //   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
393
    std::queue<const spot::state*> ta_init_it_;
394

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

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

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

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

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

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

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

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

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

                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());
448
                if (sscc.top().index == i->second)
449
450
                  {
                    // removing states
451
452
                    for (auto j: sscc.rem())
		      h[j] = -1;
453
454
455
456
457
458
459
460
461
462
463
464
                    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();
465
            trace << "PASS 2 : transition\n";
466
            // Fetch the values destination state we are interested in...
467
            state* dest = succ->dst();
468
469
470
471
472
473
474

            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.

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

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

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

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

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

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

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

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

            // 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").
530
            int threshold = i->second;
531
            std::list<const state*> rem;
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
            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)
              {
555
                clear(h, todo, ta_init_it_);
556
557
558
559
560
                trace
                  << "PASS 2: SUCCESS" << std::endl;
                return true;
              }
          }
561
562

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

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

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

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

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

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

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

    delete init_states_it;

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

607
608
609
610
611
612
613
614
  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"
615
        << std::endl;
616
617
618
619
620
621
622
623
624
    os << transitions() << " transitions explored" << std::endl;
    os << max_depth() << " items max in DFS search stack" << std::endl;
    return os;
  }

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


}