ltl2tgba_fm.cc 46.1 KB
Newer Older
1
2
3
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
4
5
// d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis
// Coopratifs (SRC), Universit Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

24
#include "misc/hash.hh"
25
#include "misc/bddalloc.hh"
26
#include "misc/bddlt.hh"
27
#include "misc/minato.hh"
28
29
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
30
31
32
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh"
#include "ltlvisit/tostring.hh"
33
#include "ltlvisit/postfix.hh"
34
#include "ltlvisit/apcollect.hh"
35
36
#include "ltlvisit/mark.hh"
#include "ltlvisit/tostring.hh"
37
#include <cassert>
38
#include <memory>
39
#include "ltl2tgba_fm.hh"
40
#include "ltlvisit/contain.hh"
41
#include "tgba/bddprint.hh"
42
43
44
45
46
47
48
49

namespace spot
{
  using namespace ltl;

  namespace
  {

50
51
    // Helper dictionary.  We represent formulae using BDDs to
    // simplify them, and then translate BDDs back into formulae.
52
53
54
55
56
    //
    // The name of the variables are inspired from Couvreur's FM paper.
    //   "a" variables are promises (written "a" in the paper)
    //   "next" variables are X's operands (the "r_X" variables from the paper)
    //   "var" variables are atomic propositions.
57
    class translate_dict
58
59
60
    {
    public:

61
62
      translate_dict(bdd_dict* dict)
	: dict(dict),
63
64
65
66
67
68
69
70
71
72
	  a_set(bddtrue),
	  var_set(bddtrue),
	  next_set(bddtrue)
      {
      }

      ~translate_dict()
      {
	fv_map::iterator i;
	for (i = next_map.begin(); i != next_map.end(); ++i)
73
	  i->first->destroy();
74
	dict->unregister_all_my_variables(this);
75
76
      }

77
78
      bdd_dict* dict;

79
80
      typedef bdd_dict::fv_map fv_map;
      typedef bdd_dict::vf_map vf_map;
81
82
83
84
85
86
87
88
89

      fv_map next_map;	       ///< Maps "Next" variables to BDD variables
      vf_map next_formula_map; ///< Maps BDD variables to "Next" variables

      bdd a_set;
      bdd var_set;
      bdd next_set;

      int
90
      register_proposition(const formula* f)
91
      {
92
	int num = dict->register_proposition(f, this);
93
94
95
96
97
	var_set &= bdd_ithvar(num);
	return num;
      }

      int
98
      register_a_variable(const formula* f)
99
      {
100
	int num = dict->register_acceptance_variable(f, this);
101
102
103
104
105
	a_set &= bdd_ithvar(num);
	return num;
      }

      int
106
      register_next_variable(const formula* f)
107
108
109
110
111
112
113
114
115
116
      {
	int num;
	// Do not build a Next variable that already exists.
	fv_map::iterator sii = next_map.find(f);
	if (sii != next_map.end())
	  {
	    num = sii->second;
	  }
	else
	  {
117
	    f = f->clone();
118
	    num = dict->register_anonymous_variables(1, this);
119
120
121
122
123
124
125
	    next_map[f] = num;
	    next_formula_map[num] = f;
	  }
	next_set &= bdd_ithvar(num);
	return num;
      }

126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
      std::ostream&
      dump(std::ostream& os) const
      {
	fv_map::const_iterator fi;
	os << "Next Variables:" << std::endl;
	for (fi = next_map.begin(); fi != next_map.end(); ++fi)
	{
	  os << "  " << fi->second << ": Next[";
	  to_string(fi->first, os) << "]" << std::endl;
	}
	os << "Shared Dict:" << std::endl;
	dict->dump(os);
	return os;
      }

141
      formula*
142
143
144
145
      var_to_formula(int var) const
      {
	vf_map::const_iterator isi = next_formula_map.find(var);
	if (isi != next_formula_map.end())
146
	  return isi->second->clone();
147
148
	isi = dict->acc_formula_map.find(var);
	if (isi != dict->acc_formula_map.end())
149
	  return isi->second->clone();
150
151
	isi = dict->var_formula_map.find(var);
	if (isi != dict->var_formula_map.end())
152
	  return isi->second->clone();
153
	assert(0);
154
155
156
	// Never reached, but some GCC versions complain about
	// a missing return otherwise.
	return 0;
157
158
      }

159
      formula*
160
      conj_bdd_to_formula(bdd b, multop::type op = multop::And) const
161
162
      {
	if (b == bddfalse)
163
164
	  return constant::false_instance();
	multop::vec* v = new multop::vec;
165
166
167
	while (b != bddtrue)
	  {
	    int var = bdd_var(b);
168
	    formula* res = var_to_formula(var);
169
170
171
	    bdd high = bdd_high(b);
	    if (high == bddfalse)
	      {
172
		res = unop::instance(unop::Not, res);
173
174
175
176
		b = bdd_low(b);
	      }
	    else
	      {
177
		assert(bdd_low(b) == bddfalse);
178
179
180
181
182
		b = high;
	      }
	    assert(b != bddfalse);
	    v->push_back(res);
	  }
183
	return multop::instance(op, v);
184
185
      }

186
      formula*
187
      bdd_to_formula(bdd f)
188
      {
189
	if (f == bddfalse)
190
	  return constant::false_instance();
191

192
193
194
195
196
197
198
199
200
	multop::vec* v = new multop::vec;

	minato_isop isop(f);
	bdd cube;
	while ((cube = isop.next()) != bddfalse)
	  v->push_back(conj_bdd_to_formula(cube));

	return multop::instance(multop::Or, v);
      }
201
202

      void
203
      conj_bdd_to_acc(tgba_explicit_formula* a, bdd b,
Pierre PARUTTO's avatar
Pierre PARUTTO committed
204
		      state_explicit_formula::transition* t)
205
206
207
208
209
210
211
212
      {
	assert(b != bddfalse);
	while (b != bddtrue)
	  {
	    int var = bdd_var(b);
	    bdd high = bdd_high(b);
	    if (high == bddfalse)
	      {
213
		// Simply ignore negated acceptance variables.
214
215
216
217
		b = bdd_low(b);
	      }
	    else
	      {
218
		formula* ac = var_to_formula(var);
219

220
		if (!a->has_acceptance_condition(ac))
221
		  a->declare_acceptance_condition(ac->clone());
222
		a->add_acceptance_condition(t, ac);
223
224
225
226
227
228
229
230
		b = high;
	      }
	    assert(b != bddfalse);
	  }
      }
    };


231
232
233
234
    // Debugging function.
    std::ostream&
    trace_ltl_bdd(const translate_dict& d, bdd f)
    {
235
236
237
      std::cerr << "Displaying BDD ";
      bdd_print_set(std::cerr, d.dict, f) << ":" << std::endl;

238
239
240
241
242
243
244
      minato_isop isop(f);
      bdd cube;
      while ((cube = isop.next()) != bddfalse)
	{
	  bdd label = bdd_exist(cube, d.next_set);
	  bdd dest_bdd = bdd_existcomp(cube, d.next_set);
	  const formula* dest = d.conj_bdd_to_formula(dest_bdd);
245
246
247
248
	  bdd_print_set(std::cerr, d.dict, label) << " => ";
	  bdd_print_set(std::cerr, d.dict, dest_bdd) << " = "
						     << to_string(dest)
						     << std::endl;
249
250
251
252
253
254
	  dest->destroy();
	}
      return std::cerr;
    }


255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297

    // Gather all promises of a formula.  These are the
    // right-hand sides of U or F operators.
    class ltl_promise_visitor: public postfix_visitor
    {
    public:
      ltl_promise_visitor(translate_dict& dict)
	: dict_(dict), res_(bddtrue)
      {
      }

      virtual
      ~ltl_promise_visitor()
      {
      }

      bdd
      result() const
      {
	return res_;
      }

      using postfix_visitor::doit;

      virtual void
      doit(unop* node)
      {
	if (node->op() == unop::F)
	  res_ &= bdd_ithvar(dict_.register_a_variable(node->child()));
      }

      virtual void
      doit(binop* node)
      {
	if (node->op() == binop::U)
	  res_ &= bdd_ithvar(dict_.register_a_variable(node->second()));
      }

    private:
      translate_dict& dict_;
      bdd res_;
    };

298
299
300
301
    // Rewrite rule for rational operators.
    class ratexp_trad_visitor: public const_visitor
    {
    public:
302
303
304
305
306
      // negated should only be set for constants or atomic properties
      ratexp_trad_visitor(translate_dict& dict,
			  formula* to_concat = 0,
			  bool negated = false)
	: dict_(dict), to_concat_(to_concat), negated_(negated)
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
      {
      }

      virtual
      ~ratexp_trad_visitor()
      {
	if (to_concat_)
	  to_concat_->destroy();
      }

      bdd
      result() const
      {
	return res_;
      }

      bdd next_to_concat()
      {
	if (!to_concat_)
326
	  to_concat_ = constant::empty_word_instance();
327
328
329
330
331
332
	int x = dict_.register_next_variable(to_concat_);
	return bdd_ithvar(x);
      }

      bdd now_to_concat()
      {
333
334
335
	if (to_concat_ && to_concat_ != constant::empty_word_instance())
	  return recurse(to_concat_);

336
	return bddfalse;
337
338
339
340
341
      }

      void
      visit(const atomic_prop* node)
      {
342
343
344
345
346
	if (negated_)
	  res_ = bdd_nithvar(dict_.register_proposition(node));
	else
	  res_ = bdd_ithvar(dict_.register_proposition(node));
	res_ &= next_to_concat();
347
348
349
350
351
      }

      void
      visit(const constant* node)
      {
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368

	if (negated_)
	  {
	    switch (node->val())
	      {
	      case constant::True:
		res_ = bddfalse;
		return;
	      case constant::False:
		res_ = next_to_concat();
		return;
	      case constant::EmptyWord:
		assert(!"EmptyWord should not be negated");
		return;
	      }
	  }

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
	switch (node->val())
	  {
	  case constant::True:
	    res_ = next_to_concat();
	    return;
	  case constant::False:
	    res_ = bddfalse;
	    return;
	  case constant::EmptyWord:
	    res_ = now_to_concat();
	    return;
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const unop* node)
      {
	switch (node->op())
	  {
	  case unop::F:
	  case unop::G:
	  case unop::X:
	  case unop::Finish:
394
395
	  case unop::Closure:
	  case unop::NegClosure:
396
397
	    assert(!"not a rational operator");
	    return;
398
399
400
401
402
403
404
	  case unop::Not:
	    {
	      // Not can only appear in front of constants or atomic
	      // propositions.
	      const formula* f = node->child();
	      assert(dynamic_cast<const atomic_prop*>(f)
		     || dynamic_cast<const constant*>(f));
405
	      res_ = recurse_and_concat(f, true);
406
407
	      return;
	    }
408
409
410
411
	  }
	/* Unreachable code.  */
	assert(0);
      }
412

413
414
415
416
417
418
      void
      visit(const bunop* bo)
      {
	formula* f;
	unsigned min = bo->min();
	unsigned max = bo->max();
419
420
421

	assert(max > 0);

422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
	unsigned min2 = (min == 0) ? 0 : (min - 1);
	unsigned max2 =
	  (max == bunop::unbounded) ? bunop::unbounded : (max - 1);

	bunop::type op = bo->op();
	switch (op)
	  {
	  case bunop::Star:
	    f = bunop::instance(op, bo->child()->clone(), min2, max2);

	    if (to_concat_)
	      f = multop::instance(multop::Concat, f, to_concat_->clone());

	    res_ = recurse(bo->child(), f);
	    if (min == 0)
	      res_ |= now_to_concat();
438

439
	    return;
440
	  case bunop::Equal:
441
	  case bunop::Goto:
442
443
444
445
446
447
	    {
	      // b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1])
	      // b[=0..max]   == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1])
	      // Note: b[=0] == (!b)[*] is a trivial identity, so it will
	      // never occur here.

448
449
450
451
452
453
	      // b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1])
	      // b[->0..max]   == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1])
	      // Note: b[->0] == [*0] is a trivial identity, so it will
	      // never occur here.

	      formula* f1 = // !b;b[=min..max]  or  !b;b[->min..max]
454
455
456
457
458
		multop::instance(multop::Concat,
				 unop::instance(unop::Not,
						bo->child()->clone()),
				 bo->clone());

459
	      formula* f2 = // b;b[=min-1..max-1]  or  b;b[->min-1..max-1]
460
461
		multop::instance(multop::Concat,
				 bo->child()->clone(),
462
				 bunop::instance(op,
463
464
465
466
467
468
469
470
471
						 bo->child()->clone(),
						 min2, max2));
	      f = multop::instance(multop::Or, f1, f2);
	      res_ = recurse_and_concat(f);
	      f->destroy();
	      if (min == 0)
		res_ |= now_to_concat();
	      return;
	    }
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const binop*)
      {
	assert(!"not a rational operator");
      }

      void
      visit(const automatop*)
      {
	assert(!"not a rational operator");
      }

      void
      visit(const multop* node)
      {
492
493
	multop::type op = node->op();
	switch (op)
494
	  {
495
	  case multop::AndNLM:
496
497
498
	  case multop::And:
	    {
	      unsigned s = node->size();
499
500
501
502
503
504
505
506
507

	      if (op == multop::AndNLM)
		{
		  multop::vec* final = new multop::vec;
		  multop::vec* non_final = new multop::vec;

		  for (unsigned n = 0; n < s; ++n)
		    {
		      const formula* f = node->nth(n);
508
		      if (f->accepts_eword())
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
			final->push_back(f->clone());
		      else
			non_final->push_back(f->clone());
		    }

		  if (non_final->empty())
		    {
		      delete non_final;
		      // (a* & b*);c = (a*|b*);c
		      formula* f = multop::instance(multop::Or, final);
		      res_ = recurse_and_concat(f);
		      f->destroy();
		      break;
		    }
		  if (!final->empty())
		    {
		      // let F_i be final formulae
		      //     N_i be non final formula
		      // (F_1 & ... & F_n & N_1 & ... & N_m)
		      // =   (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
		      //   | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
		      formula* f = multop::instance(multop::Or, final);
		      formula* n = multop::instance(multop::AndNLM, non_final);
532
533
		      formula* t = bunop::instance(bunop::Star,
						   constant::true_instance());
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
		      formula* ft = multop::instance(multop::Concat,
						     f->clone(), t->clone());
		      formula* nt = multop::instance(multop::Concat,
						     n->clone(), t);
		      formula* ftn = multop::instance(multop::And, ft, n);
		      formula* fnt = multop::instance(multop::And, f, nt);
		      formula* all = multop::instance(multop::Or, ftn, fnt);
		      res_ = recurse_and_concat(all);
		      all->destroy();
		      break;
		    }
		  // No final formula.
		  // Apply same rule as &&, until we reach a point where
		  // we have final formulae.
		  delete final;
		  for (unsigned n = 0; n < s; ++n)
		    (*non_final)[n]->destroy();
		  delete non_final;
		}

	      res_ = bddtrue;
555
	      for (unsigned n = 0; n < s; ++n)
556
557
558
559
560
		{
		  bdd res = recurse(node->nth(n));
		  // trace_ltl_bdd(dict_, res);
		  res_ &= res;
		}
561
562
563
564
565
566

	      //std::cerr << "Pre-Concat:" << std::endl;
	      //trace_ltl_bdd(dict_, res_);

	      if (to_concat_)
		{
567
		  // If we have translated (a* && b*) in (a* && b*);c, we
568
569
570
571
572
573
574
575
576
		  // have to append ";c" to all destinations.

		  minato_isop isop(res_);
		  bdd cube;
		  res_ = bddfalse;
		  while ((cube = isop.next()) != bddfalse)
		    {
		      bdd label = bdd_exist(cube, dict_.next_set);
		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
577
578
		      formula* dest =
			dict_.conj_bdd_to_formula(dest_bdd, op);
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
		      formula* dest2;
		      int x;
		      if (dest == constant::empty_word_instance())
			{
			  res_ |= label & next_to_concat();
			}
		      else
			{
			  dest2 = multop::instance(multop::Concat, dest,
						   to_concat_->clone());
			  if (dest2 != constant::false_instance())
			    {
			      x = dict_.register_next_variable(dest2);
			      dest2->destroy();
			      res_ |= label & bdd_ithvar(x);
			    }
595
			  if (node->accepts_eword())
596
597
598
599
			    res_ |= label & next_to_concat();
			}
		    }
		}
600
	      if (node->accepts_eword())
601
		res_ |= now_to_concat();
602
603
604
605
606
607
608

	      break;
	    }
	  case multop::Or:
	    {
	      res_ = bddfalse;
	      unsigned s = node->size();
609
610
	      for (unsigned n = 0; n < s; ++n)
		res_ |= recurse_and_concat(node->nth(n));
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
	      break;
	    }
	  case multop::Concat:
	    {
	      multop::vec* v = new multop::vec;
	      unsigned s = node->size();
	      v->reserve(s);
	      for (unsigned n = 1; n < s; ++n)
		v->push_back(node->nth(n)->clone());
	      if (to_concat_)
		v->push_back(to_concat_->clone());
	      res_ = recurse(node->nth(0),
			     multop::instance(multop::Concat, v));
	      break;
	    }
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
	  case multop::Fusion:
	    {
	      assert(node->size() >= 2);

	      // the head
	      bdd res = recurse(node->nth(0));

	      // the tail
	      multop::vec* v = new multop::vec;
	      unsigned s = node->size();
	      v->reserve(s - 1);
	      for (unsigned n = 1; n < s; ++n)
		v->push_back(node->nth(n)->clone());
	      formula* tail = multop::instance(multop::Fusion, v);
	      bdd tail_bdd;
	      bool tail_computed = false;

	      //trace_ltl_bdd(dict_, res);

	      minato_isop isop(res);
	      bdd cube;
	      res_ = bddfalse;
	      while ((cube = isop.next()) != bddfalse)
		{
		  bdd label = bdd_exist(cube, dict_.next_set);
		  bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
		  formula* dest = dict_.conj_bdd_to_formula(dest_bdd);

654
		  if (dest->accepts_eword())
655
656
657
658
659
		    {
		      // The destination is a final state.  Make sure we
		      // can also exit if tail is satisfied.
		      if (!tail_computed)
			{
660
			  tail_bdd = recurse_and_concat(tail);
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
			  tail_computed = true;
			}
		      res_ |= label & tail_bdd;
		    }

		  if (dynamic_cast<constant*>(dest) == 0)
		    {
		      // If the destination is not a constant, it
		      // means it can have successors.  Fusion the
		      // tail and append anything to concatenate.
		      formula* dest2 = multop::instance(multop::Fusion, dest,
							tail->clone());
		      if (to_concat_)
			 dest2 = multop::instance(multop::Concat, dest2,
						 to_concat_->clone());
		      if (dest2 != constant::false_instance())
			{
			  int x = dict_.register_next_variable(dest2);
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
		    }
		}

	      tail->destroy();
	      break;
	    }
688
689
690
691
	  }
      }

      bdd
692
      recurse(const formula* f, formula* to_concat = 0, bool negated = false)
693
      {
694
	ratexp_trad_visitor v(dict_, to_concat, negated);
695
696
697
698
	f->accept(v);
	return v.result();
      }

699
      bdd
700
      recurse_and_concat(const formula* f, bool negated = false)
701
      {
702
	return recurse(f, to_concat_ ? to_concat_->clone() : 0, negated);
703
      }
704
705
706
707
708

    private:
      translate_dict& dict_;
      bdd res_;
      formula* to_concat_;
709
      bool negated_;
710
711
    };

712

713
    // The rewrite rules used here are adapted from Jean-Michel
714
    // Couvreur's FM paper, augmented to support rational operators.
715
716
717
    class ltl_trad_visitor: public const_visitor
    {
    public:
718
719
720
721
      ltl_trad_visitor(translate_dict& dict, bool mark_all = false,
		       bool exprop = false)
	: dict_(dict), rat_seen_(false), has_marked_(false),
	  mark_all_(mark_all), exprop_(exprop)
722
723
724
725
726
727
728
729
      {
      }

      virtual
      ~ltl_trad_visitor()
      {
      }

730
731
732
733
734
735
736
737
      void
      reset(bool mark_all)
      {
	rat_seen_ = false;
	has_marked_ = false;
	mark_all_ = mark_all;
      }

738
739
      bdd
      result() const
740
741
742
743
      {
	return res_;
      }

744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
      const translate_dict&
      get_dict() const
      {
	return dict_;
      }

      bool
      has_rational() const
      {
	return rat_seen_;
      }

      bool
      has_marked() const
      {
	return has_marked_;
      }

762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
      void
      visit(const atomic_prop* node)
      {
	res_ = bdd_ithvar(dict_.register_proposition(node));
      }

      void
      visit(const constant* node)
      {
	switch (node->val())
	  {
	  case constant::True:
	    res_ = bddtrue;
	    return;
	  case constant::False:
	    res_ = bddfalse;
	    return;
779
	  case constant::EmptyWord:
780
781
	    assert(!"Not an LTL operator");
	    return;
782
783
784
785
786
787
788
789
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const unop* node)
      {
790
791
792
	unop::type op = node->op();

	switch (op)
793
794
795
796
	  {
	  case unop::F:
	    {
	      // r(Fy) = r(y) + a(y)r(XFy)
797
798
799
	      const formula* child = node->child();
	      bdd y = recurse(child);
	      int a = dict_.register_a_variable(child);
800
801
	      int x = dict_.register_next_variable(node);
	      res_ = y | (bdd_ithvar(a) & bdd_ithvar(x));
802
	      break;
803
804
805
	    }
	  case unop::G:
	    {
806
807
808
809
810
811
812
813
814
815
816
817
	      // The paper suggests that we optimize GFy
	      // as
	      //   r(GFy) = (r(y) + a(y))r(XGFy)
	      // instead of
	      //   r(GFy) = (r(y) + a(y)r(XFy)).r(XGFy)
	      // but this is just a particular case
	      // of the "merge all states with the same
	      // symbolic rewriting" optimization we do later.
	      // (r(Fy).r(GFy) and r(GFy) have the same symbolic
	      // rewriting.)  Let's keep things simple here.

	      // r(Gy) = r(y)r(XGy)
818
	      const formula* child = node->child();
819
	      int x = dict_.register_next_variable(node);
820
821
	      bdd y = recurse(child);
	      res_ = y & bdd_ithvar(x);
822
	      break;
823
824
825
	    }
	  case unop::Not:
	    {
826
	      // r(!y) = !r(y)
827
	      res_ = bdd_not(recurse(node->child()));
828
	      break;
829
830
831
	    }
	  case unop::X:
	    {
832
	      // r(Xy) = Next[y]
833
834
	      int x = dict_.register_next_variable(node->child());
	      res_ = bdd_ithvar(x);
835
	      break;
836
	    }
837
838
839
	  case unop::Closure:
	    {
	      rat_seen_ = true;
840
	      if (node->child()->accepts_eword())
841
842
843
844
845
846
		{
		  res_ = bddtrue;
		  return;
		}

	      ratexp_trad_visitor v(dict_);
847
848
849
850
	      node->child()->accept(v);
	      bdd f1 = v.result();
	      res_ = bddfalse;

851

852
853
854
855
856
857
858
859
860
861
862
863
864
865
	      if (exprop_)
		{
		  bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
		  bdd all_props = bdd_existcomp(f1, dict_.var_set);
		  while (all_props != bddfalse)
		    {
		      bdd label = bdd_satoneset(all_props, var_set, bddtrue);
		      all_props -= label;

		      formula* dest =
			dict_.bdd_to_formula(bdd_exist(f1 & label,
						       dict_.var_set));

		      const formula* dest2;
866
		      if (dest->accepts_eword())
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
			{
			  dest->destroy();
			  res_ |= label;
			}
		      else
			{
			  dest2 = unop::instance(op, dest);
			  if (dest2 == constant::false_instance())
			    continue;
			  int x = dict_.register_next_variable(dest2);
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
		    }
		}
	      else
		{
		  minato_isop isop(f1);
		  bdd cube;
		  while ((cube = isop.next()) != bddfalse)
		    {
		      bdd label = bdd_exist(cube, dict_.next_set);
		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
		      formula* dest = dict_.conj_bdd_to_formula(dest_bdd);

		      const formula* dest2;
893
		      if (dest->accepts_eword())
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
			{
			  dest->destroy();
			  res_ |= label;
			}
		      else
			{
			  dest2 = unop::instance(op, dest);
			  if (dest2 == constant::false_instance())
			    continue;
			  int x = dict_.register_next_variable(dest2);
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
		    }
		}
	    }
	    break;

	  case unop::NegClosure:
	    {
	      rat_seen_ = true;
	      has_marked_ = true;
916

917
	      if (node->child()->accepts_eword())
918
919
920
921
922
923
		{
		  res_ = bddfalse;
		  return;
		}

	      ratexp_trad_visitor v(dict_);
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
	      node->child()->accept(v);
	      bdd f1 = v.result();

	      // trace_ltl_bdd(dict_, f1);

	      bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
	      bdd all_props = bdd_existcomp(f1, dict_.var_set);

	      res_ = !all_props &
		// stick X(1) to preserve determinism.
		bdd_ithvar(dict_.register_next_variable
			   (constant::true_instance()));

	      while (all_props != bddfalse)
		{
		  bdd label = bdd_satoneset(all_props, var_set, bddtrue);
		  all_props -= label;

		  formula* dest =
		    dict_.bdd_to_formula(bdd_exist(f1 & label,
						   dict_.var_set));

		  // !{ Exp } is false if Exp accepts the empty word.
947
		  if (dest->accepts_eword())
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
		    {
		      dest->destroy();
		      continue;
		    }

		  const formula* dest2 = unop::instance(op, dest);

		  if (dest == constant::false_instance())
		    continue;

		  int x = dict_.register_next_variable(dest2);
		  dest2->destroy();
		  res_ |= label & bdd_ithvar(x);
		}
	    }
	    break;

965
966
	  case unop::Finish:
	    assert(!"unsupported operator");
967
	    break;
968
969
970
	  }
      }

971
972
973
974
975
976
      void
      visit(const bunop*)
      {
	assert(!"Not an LTL operator");
      }

977
978
979
      void
      visit(const binop* node)
      {
980
	binop::type op = node->op();
981

982
	switch (op)
983
	  {
984
	    // r(f1 logical-op f2) = r(f1) logical-op r(f2)
985
	  case binop::Xor:
986
987
988
989
990
991
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_xor);
	      return;
	    }
992
	  case binop::Implies:
993
994
995
996
997
998
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_imp);
	      return;
	    }
999
	  case binop::Equiv:
1000
1001
1002
1003
1004
1005
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_biimp);
	      return;
	    }
1006
1007
	  case binop::U:
	    {
1008
1009
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1010
1011
1012
1013
	      // r(f1 U f2) = r(f2) + a(f2)r(f1)r(X(f1 U f2))
	      int a = dict_.register_a_variable(node->second());
	      int x = dict_.register_next_variable(node);
	      res_ = f2 | (bdd_ithvar(a) & f1 & bdd_ithvar(x));
1014
	      break;
1015
	    }
1016
1017
	  case binop::W:
	    {
1018
1019
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1020
1021
1022
	      // r(f1 W f2) = r(f2) + r(f1)r(X(f1 U f2))
	      int x = dict_.register_next_variable(node);
	      res_ = f2 | (f1 & bdd_ithvar(x));
1023
	      break;
1024
	    }
1025
1026
	  case binop::R:
	    {
1027
1028
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1029
1030
1031
	      // r(f1 R f2) = r(f1)r(f2) + r(f2)r(X(f1 U f2))
	      int x = dict_.register_next_variable(node);
	      res_ = (f1 & f2) | (f2 & bdd_ithvar(x));
1032
	      break;
1033
	    }
1034
1035
	  case binop::M:
	    {
1036
1037
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1038
1039
1040
1041
	      // r(f1 M f2) = r(f1)r(f2) + a(f1)r(f2)r(X(f1 M f2))
	      int a = dict_.register_a_variable(node->first());
	      int x = dict_.register_next_variable(node);
	      res_ = (f1 & f2) | (bdd_ithvar(a) & f2 & bdd_ithvar(x));
1042
	      break;
1043
	    }
1044
1045
1046
	  case binop::EConcatMarked:
	    has_marked_ = true;
	    /* fall through */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1047
	  case binop::EConcat:
1048
1049
	    rat_seen_ = true;
	    {
1050
1051
	      // Recognize f2 on transitions going to destinations
	      // that accept the empty word.
1052
	      bdd f2 = recurse(node->second());
1053
	      ratexp_trad_visitor v(dict_);
1054
1055
	      node->first()->accept(v);
	      bdd f1 = v.result();
1056
	      res_ = bddfalse;
1057
1058
1059
1060
1061
1062
1063

	      if (mark_all_)
		{
		  op = binop::EConcatMarked;
		  has_marked_ = true;
		}

1064
	      if (exprop_)
1065
		{
1066
1067
1068
		  bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
		  bdd all_props = bdd_existcomp(f1, dict_.var_set);
		  while (all_props != bddfalse)
1069
		    {
1070
		      bdd label = bdd_satoneset(all_props, var_set, bddtrue);
1071
1072
1073
1074
1075
1076
1077
1078
1079
		      all_props -= label;

		      formula* dest =
			dict_.bdd_to_formula(bdd_exist(f1 & label,
						       dict_.var_set));

		      const formula* dest2 =
			binop::instance(op, dest, node->second()->clone());

1080
1081
		      if (dest2 != constant::false_instance())
			{
1082
			  int x = dict_.register_next_variable(dest2);
1083
1084
1085
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
1086
		      if (dest->accepts_eword())
1087
1088
1089
			res_ |= label & f2;
		    }
		}
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
	      else
		{
		  minato_isop isop(f1);
		  bdd cube;
		  while ((cube = isop.next()) != bddfalse)
		    {
		      bdd label = bdd_exist(cube, dict_.next_set);
		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
		      formula* dest = dict_.conj_bdd_to_formula(dest_bdd);

		      if (dest == constant::empty_word_instance())
			{
			  res_ |= label & f2;
			}
		      else
			{
			  formula* dest2 = binop::instance(op, dest,
						  node->second()->clone());
			  if (dest2 != constant::false_instance())
			    {
			      int x = dict_.register_next_variable(dest2);
			      dest2->destroy();
			      res_ |= label & bdd_ithvar(x);
			    }
1114
			  if (dest->accepts_eword())
1115
1116
1117
1118
			    res_ |= label & f2;
			}
		    }
		}
1119
1120
1121
1122
1123
	    }
	    break;

	  case binop::UConcat:
	    {
1124
1125
1126
	      // Transitions going to destinations accepting the empty
	      // word should recognize f2, and the automaton for f1
	      // should be understood as universal.
1127
	      bdd f2 = recurse(node->second());
1128
	      ratexp_trad_visitor v(dict_);
1129
1130
1131
	      node->first()->accept(v);
	      bdd f1 = v.result();
	      res_ = bddtrue;
1132

1133
1134
1135
	      bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
	      bdd all_props = bdd_existcomp(f1, dict_.var_set);
	      while (all_props != bddfalse)
1136
1137
		{

1138
1139
1140
1141
		  bdd one_prop_set = bddtrue;
		  if (exprop_)
		    one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
		  all_props -= one_prop_set;
1142

1143
		  minato_isop isop(f1 & one_prop_set);
1144
1145
1146
1147
1148
1149
		  bdd cube;
		  while ((cube = isop.next()) != bddfalse)
		    {
		      bdd label = bdd_exist(cube, dict_.next_set);
		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
		      formula* dest = dict_.conj_bdd_to_formula(dest_bdd);
1150
1151
		      formula* dest2 =
			binop::instance(op, dest, node->second()->clone());
1152

1153
1154
		      bdd udest =
			bdd_ithvar(dict_.register_next_variable(dest2));
1155

1156
		      if (dest->accepts_eword())
1157
1158
1159
1160
			udest &= f2;

		      dest2->destroy();

1161
		      res_ &= bdd_apply(label, udest, bddop_imp);
1162
		    }
1163
1164
		}
	    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1165
	    break;
1166
1167
1168
	  }
      }

1169
1170
1171
1172
1173
1174
      void
      visit(const automatop*)
      {
	assert(!"unsupported operator");
      }

1175
1176
1177
1178
1179
1180
      void
      visit(const multop* node)
      {
	switch (node->op())
	  {
	  case multop::And:
1181
1182
1183
1184
1185
1186
	    {
	      res_ = bddtrue;
	      unsigned s = node->size();
	      for (unsigned n = 0; n < s; ++n)
		{
		  bdd res = recurse(node->nth(n));
1187
1188
1189
		  //std::cerr << "== in And (" << to_string(node->nth(n))
		  // << ")" << std::endl;
		  // trace_ltl_bdd(dict_, res);
1190
1191
		  res_ &= res;
		}
1192
1193
	      //std::cerr << "=== And final" << std::endl;
	      // trace_ltl_bdd(dict_, res_);
1194
1195
	      break;
	    }
1196
	  case multop::Or:
1197
1198
1199
1200
1201
1202
1203
	    {
	      res_ = bddfalse;
	      unsigned s = node->size();
	      for (unsigned n = 0; n < s; ++n)
		res_ |= recurse(node->nth(n));
	      break;
	    }
1204
	  case multop::Concat:
1205
	  case multop::Fusion:
1206
	  case multop::AndNLM:
1207
1208
	    assert(!"Not an LTL operator");
	    break;
1209
	  }
1210

1211
1212
1213
1214
1215
      }

      bdd
      recurse(const formula* f)
      {
1216
	ltl_trad_visitor v(dict_, mark_all_, exprop_);
1217
	f->accept(v);
1218
1219
	rat_seen_ |= v.has_rational();
	has_marked_ |= v.has_marked();
1220
1221
1222
1223
1224
1225
1226
	return v.result();
      }


    private:
      translate_dict& dict_;
      bdd res_;
1227
1228
1229
      bool rat_seen_;
      bool has_marked_;
      bool mark_all_;
1230
      bool exprop_;
1231
1232
    };

1233

1234
1235
    // Check whether a formula has a R, W, or G operator at its
    // top-level (preceding logical operators do not count).
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
    class ltl_possible_fair_loop_visitor: public const_visitor
    {
    public:
      ltl_possible_fair_loop_visitor()
	: res_(false)
      {
      }

      virtual
      ~ltl_possible_fair_loop_visitor()
      {
      }

      bool
      result() const
      {
	return res_;
      }

      void
      visit(const atomic_prop*)
      {
      }

      void
      visit(const constant*)
      {
      }

      void
      visit(const unop* node)
      {
	if (node->op() == unop::G)
	  res_ = true;
      }

      void
      visit(const binop* node)
      {
	switch (node->op())
	  {
	    // r(f1 logical-op f2) = r(f1) logical-op r(f2)
	  case binop::Xor:
	  case binop::Implies:
	  case binop::Equiv:
	    node->first()->accept(*this);
	    if (!res_)
	      node->second()->accept(*this);
	    return;
	  case binop::U:
1286
	  case binop::M:
1287
1288
	    return;
	  case binop::R:
1289
	  case binop::W:
1290
1291
	    res_ = true;
	    return;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1292
1293
	  case binop::UConcat:
	  case binop::EConcat:
1294
	  case binop::EConcatMarked:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1295
	    node->second()->accept(*this);
1296
	    // FIXME: we might need to add Acc[1]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1297
	    return;
1298
1299
1300
1301
1302
	  }
	/* Unreachable code.  */
	assert(0);
      }

1303
1304
1305
1306
1307
1308
      void
      visit(const automatop*)
      {
	assert(!"unsupported operator");
      }

1309
1310
1311
1312
1313
1314
      void
      visit(const bunop*)
      {
	assert(!"unsupported operator");
      }

1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
      void
      visit(const multop* node)
      {
	unsigned s = node->size();
	for (unsigned n = 0; n < s && !res_; ++n)
	  {
	    node->nth(n)->accept(*this);
	  }
      }

    private:
      bool res_;
    };

    // Check whether a formula can be part of a fair loop.
    // Cache the result for efficiency.
    class possible_fair_loop_checker
    {
    public:
      bool
      check(const formula* f)
      {
1337
1338
	pfl_map::const_iterator i = pfl_.find(f);
	if (i != pfl_.end())
1339
1340
1341
1342
	  return i->second;
	ltl_possible_fair_loop_visitor v;
	f->accept(v);
	bool rel = v.result();
1343
	pfl_[f] = rel;
1344
1345
1346
1347
	return rel;
      }

    private:
1348
      typedef Sgi::hash_map<const formula*, bool, formula_ptr_hash> pfl_map;
1349
      pfl_map pfl_;
1350
1351
    };

1352
1353
1354
    class formula_canonizer
    {
    public:
1355
      formula_canonizer(translate_dict& d,
1356
1357
			bool fair_loop_approx, bdd all_promises, bool exprop)
	: v_(d, false, exprop),
1358
	  fair_loop_approx_(fair_loop_approx),
1359
1360
	  all_promises_(all_promises),
	  d_(d)
1361
1362
1363
1364
1365
      {
	// For cosmetics, register 1 initially, so the algorithm will
	// not register an equivalent formula first.
	b2f_[bddtrue] = constant::true_instance();
      }
1366

1367
1368
      ~formula_canonizer()
      {
1369
	while (!f2b_.empty())
1370
	  {
1371
1372
1373
	    formula_to_bdd_map::iterator i = f2b_.begin();
	    const formula* f = i->first;
	    f2b_.erase(i);
1374
	    f->destroy();
1375
	  }
1376
1377
      }

1378
1379
1380
1381
1382
1383
1384
1385
      struct translated
      {
	bdd symbolic;
	bool has_rational:1;
	bool has_marked:1;
      };

      const translated&
1386
      translate(const formula* f, bool* new_flag = 0)
1387
1388
1389
1390
1391
1392
      {
	// Use the cached result if available.
	formula_to_bdd_map::const_iterator i = f2b_.find(f);
	if (i != f2b_.end())
	  return i->second;

1393
1394
1395
	if (new_flag)
	  *new_flag = true;

1396
	// Perform the actual translation.
1397
	v_.reset(!f->is_marked());
1398
	f->accept(v_);
1399