emptiness.cc 17.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
3
// Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// et Marie Curie.
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
#include <sstream>
24
25
26
27
28
29
30
31
32
33
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/gv04.hh>
#include <spot/twaalgos/magic.hh>
#include <spot/misc/hash.hh>
#include <spot/twaalgos/se05.hh>
#include <spot/twaalgos/tau03.hh>
#include <spot/twaalgos/tau03opt.hh>
#include <spot/twa/bddprint.hh>
34
35
36

namespace spot
{
37
38
39

  // emptiness_check_result
  //////////////////////////////////////////////////////////////////////
40

41
  twa_run_ptr
42
43
  emptiness_check_result::accepting_run()
  {
44
    return nullptr;
45
46
  }

47
48
49
50
51
52
  const unsigned_statistics*
  emptiness_check_result::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
  const char*
  emptiness_check_result::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check_result::options_updated(const option_map&)
  {
  }


68
69
70
  // emptiness_check
  //////////////////////////////////////////////////////////////////////

71
72
73
74
  emptiness_check::~emptiness_check()
  {
  }

75
76
77
78
79
80
  const unsigned_statistics*
  emptiness_check::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

81
82
83
84
85
86
  const ec_statistics*
  emptiness_check::emptiness_check_statistics() const
  {
    return dynamic_cast<const ec_statistics*>(this);
  }

87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
  const char*
  emptiness_check::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check::options_updated(const option_map&)
  {
  }

  bool
  emptiness_check::safe() const
  {
    return true;
  }

107
108
109
110
111
  std::ostream&
  emptiness_check::print_stats(std::ostream& os) const
  {
    return os;
  }
112

113
114
115
116
117
118
119
120
  // emptiness_check_instantiator
  //////////////////////////////////////////////////////////////////////

  namespace
  {
    struct ec_algo
    {
      const char* name;
121
      emptiness_check_ptr(*construct)(const const_twa_ptr&,
122
				      spot::option_map);
123
124
125
126
127
128
      unsigned int min_acc;
      unsigned int max_acc;
    };

    ec_algo ec_algos[] =
      {
129
130
131
132
133
134
	{ "Cou99",     couvreur99,                    0, -1U },
	{ "CVWY90",    magic_search,                  0,   1 },
	{ "GV04",      explicit_gv04_check,           0,   1 },
	{ "SE05",      se05,                          0,   1 },
	{ "Tau03",     explicit_tau03_search,         1, -1U },
	{ "Tau03_opt", explicit_tau03_opt_search,     0, -1U },
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
      };
  }

  emptiness_check_instantiator::emptiness_check_instantiator(option_map o,
							     void* i)
    : o_(o), info_(i)
  {
  }

  unsigned int
  emptiness_check_instantiator::min_acceptance_conditions() const
  {
    return static_cast<ec_algo*>(info_)->min_acc;
  }

  unsigned int
  emptiness_check_instantiator::max_acceptance_conditions() const
  {
    return static_cast<ec_algo*>(info_)->max_acc;
  }

156
  emptiness_check_ptr
157
  emptiness_check_instantiator::instantiate(const const_twa_ptr& a) const
158
159
160
161
  {
    return static_cast<ec_algo*>(info_)->construct(a, o_);
  }

162
163
  emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err)
164
165
166
167
168
169
170
171
172
173
174
175
176
177
  {
    // Skip spaces.
    while (*name && strchr(" \t\n", *name))
      ++name;

    const char* opt_str = strchr(name, '(');
    option_map o;
    if (opt_str)
      {
	const char* opt_start = opt_str + 1;
	const char* opt_end = strchr(opt_start, ')');
	if (!opt_end)
	  {
	    *err = opt_start;
178
	    return nullptr;
179
180
181
182
183
184
185
	  }
	std::string opt(opt_start, opt_end);

	const char* res = o.parse_options(opt.c_str());
	if (res)
	  {
	    *err  = opt.c_str() - res + opt_start;
186
	    return nullptr;
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
	  }
      }

    if (!opt_str)
      opt_str = name + strlen(name);

    // Ignore spaces before `(' (or trailing spaces).
    while (opt_str > name && strchr(" \t\n", *--opt_str))
      continue;
    std::string n(name, opt_str + 1);


    ec_algo* info = ec_algos;
    for (unsigned i = 0; i < sizeof(ec_algos)/sizeof(*ec_algos); ++i, ++info)
      if (n == info->name)
202
	{
203
	  *err = nullptr;
204
205
206
207
208
209
210
211
212
213

	  struct emptiness_check_instantiator_aux:
            public emptiness_check_instantiator
	  {
	    emptiness_check_instantiator_aux(option_map o, void* i):
	      emptiness_check_instantiator(o, i)
	    {
	    }
	  };
	  return std::make_shared<emptiness_check_instantiator_aux>(o, info);
214
	}
215
    *err = name;
216
    return nullptr;
217
218
  }

219
  // twa_run
220
221
  //////////////////////////////////////////////////////////////////////

222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
  twa_run::~twa_run()
  {
    for (auto i : prefix)
      i.s->destroy();
    for (auto i : cycle)
      i.s->destroy();
  }

  twa_run::twa_run(const twa_run& run)
  {
    aut = run.aut;
    for (step s : run.prefix)
      {
	s.s = s.s->clone();
	prefix.push_back(s);
      }
    for (step s : run.cycle)
      {
	s.s = s.s->clone();
	cycle.push_back(s);
      }
  }

  twa_run&
  twa_run::operator=(const twa_run& run)
  {
    if (&run != this)
      {
	this->~twa_run();
	new(this) twa_run(run);
      }
    return *this;
  }

  std::ostream&
257
  operator<<(std::ostream& os, const twa_run& run)
258
  {
259
    auto& a = run.aut;
260
261
262
263
264
265
266
267
268
269
270
    bdd_dict_ptr d = a->get_dict();

    auto pstep = [&](const twa_run::step& st)
    {
      os << "  " << a->format_state(st.s) << "\n  |  ";
      bdd_print_formula(os, d, st.label);
      if (st.acc)
	os << '\t' << st.acc;
      os << '\n';
    };

271
272
    os << "Prefix:\n";
    for (auto& s: run.prefix)
273
      pstep(s);
274
275
    os << "Cycle:\n";
    for (auto& s: run.cycle)
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
      pstep(s);
    return os;
  }

  namespace
  {
    class shortest_path: public bfs_steps
    {
    public:
      shortest_path(const const_twa_ptr& a)
        : bfs_steps(a), target(nullptr)
      {
      }

      ~shortest_path()
      {
        state_set::const_iterator i = seen.begin();
        while (i != seen.end())
          {
            const state* ptr = *i;
            ++i;
            ptr->destroy();
          }
      }

      void
      set_target(const state_set* t)
      {
        target = t;
      }

      const state*
      search(const state* start, twa_run::steps& l)
      {
	return this->bfs_steps::search(filter(start), l);
      }

      const state*
      filter(const state* s)
      {
        state_set::const_iterator i = seen.find(s);
        if (i == seen.end())
          seen.insert(s);
        else
          {
            s->destroy();
            s = *i;
          }
        return s;
      }

      bool
      match(twa_run::step&, const state* dest)
      {
        return target->find(dest) != target->end();
      }

    private:
      state_set seen;
      const state_set* target;
    };
  }

  twa_run_ptr twa_run::reduce() const
  {
    auto& a = aut;
    auto res = std::make_shared<twa_run>(a);
    state_set ss;
    shortest_path shpath(a);
    shpath.set_target(&ss);

    // We want to find a short segment of the original cycle that
    // contains all acceptance conditions.

    const state* segment_start; // The initial state of the segment.
    const state* segment_next; // The state immediately after the segment.

    // Start from the end of the original cycle, and rewind until all
    // acceptance sets have been seen.
    acc_cond::mark_t seen_acc = 0U;
    twa_run::steps::const_iterator seg = cycle.end();
    do
      {
        assert(seg != cycle.begin());
	--seg;
        seen_acc |= seg->acc;
      }
    while (!a->acc().accepting(seen_acc));
    segment_start = seg->s;

    // Now go forward and ends the segment as soon as we have seen all
    // acceptance sets, cloning it in our result along the way.
    seen_acc = 0U;
    do
      {
        assert(seg != cycle.end());
        seen_acc |= seg->acc;

	twa_run::step st = { seg->s->clone(), seg->label, seg->acc };
	res->cycle.push_back(st);

	++seg;
      }
    while (!a->acc().accepting(seen_acc));
    segment_next = seg == cycle.end() ? cycle.front().s : seg->s;

    // Close this cycle if needed, that is, compute a cycle going
    // from the state following the segment to its starting state.
    if (segment_start != segment_next)
      {
        ss.insert(segment_start);
        const state* s = shpath.search(segment_next->clone(), res->cycle);
        ss.clear();
        assert(s->compare(segment_start) == 0);
	(void)s;
      }

    // Compute the prefix: it's the shortest path from the initial
    // state of the automata to any state of the cycle.

    // Register all states from the cycle as target of the BFS.
    for (twa_run::steps::const_iterator i = res->cycle.begin();
	 i != res->cycle.end(); ++i)
      ss.insert(i->s);

    const state* prefix_start = a->get_init_state();
    // There are two cases: either the initial state is already on
    // the cycle, or it is not.  If it is, we will have to rotate
    // the cycle so it begins on this position.  Otherwise we will shift
    // the cycle so it begins on the state that follows the prefix.
    // cycle_entry_point is that state.
    const state* cycle_entry_point;
    state_set::const_iterator ps = ss.find(prefix_start);
    if (ps != ss.end())
      {
	// The initial state is on the cycle.
	prefix_start->destroy();
	cycle_entry_point = *ps;
      }
    else
      {
	// This initial state is outside the cycle.  Compute the prefix.
        cycle_entry_point = shpath.search(prefix_start, res->prefix);
      }

    // Locate cycle_entry_point on the cycle.
    twa_run::steps::iterator cycle_ep_it;
    for (cycle_ep_it = res->cycle.begin();
	 cycle_ep_it != res->cycle.end()
	   && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
      continue;
    assert(cycle_ep_it != res->cycle.end());

    // Now shift the cycle so it starts on cycle_entry_point.
    res->cycle.splice(res->cycle.end(), res->cycle,
		      res->cycle.begin(), cycle_ep_it);

    return res;
  }

  namespace
  {
    static void
    print_annotation(std::ostream& os,
		     const const_twa_ptr& a,
		     const twa_succ_iterator* i)
    {
      std::string s = a->transition_annotation(i);
      if (s == "")
	return;
      os << ' ' << s;
    }
  }

  bool twa_run::replay(std::ostream& os, bool debug) const
  {
    const state* s = aut->get_init_state();
    int serial = 1;
    const twa_run::steps* l;
    std::string in;
    acc_cond::mark_t all_acc = 0U;
    bool all_acc_seen = false;
458
    state_map<std::set<int>> seen;
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493

    if (prefix.empty())
      {
	l = &cycle;
	in = "cycle";
	if (!debug)
	  os << "No prefix.\nCycle:\n";
      }
    else
      {
	l = &prefix;
	in = "prefix";
	if (!debug)
	  os << "Prefix:\n";
      }

    twa_run::steps::const_iterator i = l->begin();

    if (s->compare(i->s))
      {
	if (debug)
	  os << "ERROR: First state of run (in " << in << "): "
	     << aut->format_state(i->s)
	     << "\ndoes not match initial state of automata: "
	     << aut->format_state(s) << '\n';
	s->destroy();
	return false;
      }

    for (; i != l->end(); ++serial)
      {
	if (debug)
	  {
	    // Keep track of the serial associated to each state so we
	    // can note duplicate states and make the replay easier to read.
494
	    auto o = seen.find(s);
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
	    std::ostringstream msg;
	    if (o != seen.end())
	      {
		for (auto d: o->second)
		  msg << " == " << d;
		o->second.insert(serial);
		s->destroy();
		s = o->first;
	      }
	    else
	      {
		seen[s].insert(serial);
	      }
	    os << "state " << serial << " in " << in << msg.str() << ": ";
	  }
	else
	  {
	    os << "  ";
	  }
	os << aut->format_state(s) << '\n';

	// expected outgoing transition
	bdd label = i->label;
	acc_cond::mark_t acc = i->acc;

	// compute the next expected state
	const state* next;
	++i;
	if (i != l->end())
	  {
	    next = i->s;
	  }
	else
	  {
	    if (l == &prefix)
	      {
		l = &cycle;
		in = "cycle";
		i = l->begin();
		if (!debug)
		  os << "Cycle:\n";
	      }
	    next = l->begin()->s;
	  }

	// browse the actual outgoing transitions
	twa_succ_iterator* j = aut->succ_iter(s);
	// When not debugging, S is not used as key in SEEN, so we can
	// destroy it right now.
	if (!debug)
	  s->destroy();
	if (j->first())
	  do
	    {
549
550
	      if (j->cond() != label
		  || j->acc() != acc)
551
552
		continue;

553
	      const state* s2 = j->dst();
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
	      if (s2->compare(next))
		{
		  s2->destroy();
		  continue;
		}
	      else
		{
		  s = s2;
		  break;
		}
	    }
	  while (j->next());
	if (j->done())
	  {
	    if (debug)
	      {
		os << "ERROR: no transition with label="
		   << bdd_format_formula(aut->get_dict(), label)
		   << " and acc=" << aut->acc().format(acc)
		   << " leaving state " << serial
		   << " for state " << aut->format_state(next) << '\n'
		   << "The following transitions leave state " << serial
		   << ":\n";
		if (j->first())
		  do
		    {
580
		      const state* s2 = j->dst();
581
582
583
584
		      os << "  *";
		      print_annotation(os, aut, j);
		      os << " label="
			 << bdd_format_formula(aut->get_dict(),
585
					       j->cond())
586
587
			 << " and acc="
			 << (aut->acc().format
588
			     (j->acc()))
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
			 << " going to " << aut->format_state(s2) << '\n';
		      s2->destroy();
		    }
		  while (j->next());
	      }
	    aut->release_iter(j);
	    s->destroy();
	    return false;
	  }
	if (debug)
	  {
	    os << "transition";
	    print_annotation(os, aut, j);
	    os << " with label="
	       << bdd_format_formula(aut->get_dict(), label)
	       << " and acc=" << aut->acc().format(acc)
	       << std::endl;
	  }
	else
	  {
	    os << "  |  ";
	    print_annotation(os, aut, j);
	    bdd_print_formula(os, aut->get_dict(), label);
	    os << '\t';
	    aut->acc().format(acc);
	    os << std::endl;
	  }
	aut->release_iter(j);

	// Sum acceptance conditions.
	//
	// (Beware l and i designate the next step to consider.
	// Therefore if i is at the beginning of the cycle, `acc'
	// contains the acceptance conditions of the last transition
	// in the prefix; we should not account it.)
	if (l == &cycle && i != l->begin())
	  {
	    all_acc |= acc;
	    if (!all_acc_seen && aut->acc().accepting(all_acc))
	      {
		all_acc_seen = true;
		if (debug)
		  os << "all acceptance conditions ("
		     << aut->acc().format(all_acc)
		     << ") have been seen\n";
	      }
	  }
      }
    s->destroy();
    if (!aut->acc().accepting(all_acc))
      {
	if (debug)
	  os << "ERROR: The cycle's acceptance conditions ("
	     << aut->acc().format(all_acc)
	     << ") do not\nmatch those of the automaton ("
	     << aut->acc().format(aut->acc().all_sets())
	     << ")\n";
	return false;
      }

649
    auto o = seen.begin();
650
651
652
653
654
655
656
657
658
659
660
    while (o != seen.end())
      {
	// Advance the iterator before deleting the "key" pointer.
	const state* ptr = o->first;
	++o;
	ptr->destroy();
      }

    return true;
  }

661
  twa_graph_ptr
662
  twa_run::as_twa() const
663
  {
664
    auto d = aut->get_dict();
665
    auto res = make_twa_graph(d);
666
667
    res->copy_ap_of(aut);
    res->copy_acceptance_of(aut);
668

669
    const state* s = aut->get_init_state();
670
671
    unsigned src;
    unsigned dst;
672
    const twa_run::steps* l;
673
    acc_cond::mark_t seen_acc = 0U;
674

675
    state_map<unsigned> seen;
676

677
678
    if (prefix.empty())
        l = &cycle;
679
    else
680
        l = &prefix;
681

682
    twa_run::steps::const_iterator i = l->begin();
683
684

    assert(s->compare(i->s) == 0);
685
    src = res->new_state();
686
    seen.emplace(i->s, src);
687

688
    for (; i != l->end();)
689
690
691
      {
        // expected outgoing transition
        bdd label = i->label;
692
	acc_cond::mark_t acc = i->acc;
693
694
695
696
697
698
699
700
701
702

        // compute the next expected state
        const state* next;
        ++i;
        if (i != l->end())
          {
            next = i->s;
          }
        else
          {
703
            if (l == &prefix)
704
              {
705
                l = &cycle;
706
707
708
709
710
                i = l->begin();
              }
            next = l->begin()->s;
          }

711
712
713
        // browse the actual outgoing transitions and
	// look for next;
	const state* the_next = nullptr;
714
	for (auto j: aut->succ(s))
715
          {
716
717
            if (j->cond() != label
                || j->acc() != acc)
718
719
              continue;

720
            const state* s2 = j->dst();
721
            if (s2->compare(next) == 0)
722
              {
723
724
725
726
		the_next = s2;
		break;
	      }
	    s2->destroy();
727
          }
728
729
730
        assert(res);
        s->destroy();
	s = the_next;
731
732


733
	auto p = seen.emplace(next, 0);
734
	if (p.second)
735
	  p.first->second = res->new_state();
736
737
	dst = p.first->second;

738
	res->new_edge(src, dst, label, acc);
739
	src = dst;
740
741

        // Sum acceptance conditions.
742
        if (l == &cycle && i != l->begin())
743
	  seen_acc |= acc;
744
      }
745

746
    s->destroy();
747

748
    assert(aut->acc().accepting(seen_acc));
749
750
751
    return res;
  }

752
}