ltl2tgba_fm.cc 47.4 KB
Newer Older
1
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
2
3
// 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
#include "ltlvisit/nenoform.hh"
#include "ltlvisit/tostring.hh"
32
#include "ltlvisit/postfix.hh"
33
#include "ltlvisit/apcollect.hh"
34
35
#include "ltlvisit/mark.hh"
#include "ltlvisit/tostring.hh"
36
#include <cassert>
37
#include <memory>
38
#include "ltl2tgba_fm.hh"
39
#include "ltlvisit/contain.hh"
40
#include "tgba/bddprint.hh"
41
42
43
44
45
46
47
48

namespace spot
{
  using namespace ltl;

  namespace
  {

49
50
    // Helper dictionary.  We represent formulae using BDDs to
    // simplify them, and then translate BDDs back into formulae.
51
52
53
54
55
    //
    // 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.
56
    class translate_dict
57
58
59
    {
    public:

60
61
      translate_dict(bdd_dict* dict)
	: dict(dict),
62
63
64
65
66
67
68
69
70
71
	  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)
72
	  i->first->destroy();
73
	dict->unregister_all_my_variables(this);
74
75
      }

76
77
      bdd_dict* dict;

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

      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
89
      register_proposition(const formula* f)
90
      {
91
	int num = dict->register_proposition(f, this);
92
93
94
95
96
	var_set &= bdd_ithvar(num);
	return num;
      }

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

      int
105
      register_next_variable(const formula* f)
106
107
108
109
110
111
112
113
114
115
      {
	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
	  {
116
	    f = f->clone();
117
	    num = dict->register_anonymous_variables(1, this);
118
119
120
121
122
123
124
	    next_map[f] = num;
	    next_formula_map[num] = f;
	  }
	next_set &= bdd_ithvar(num);
	return num;
      }

125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
      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;
      }

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

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

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

191
192
193
194
195
196
197
198
199
	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);
      }
200
201

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

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


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

237
238
239
240
241
242
243
      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);
244
245
246
247
	  bdd_print_set(std::cerr, d.dict, label) << " => ";
	  bdd_print_set(std::cerr, d.dict, dest_bdd) << " = "
						     << to_string(dest)
						     << std::endl;
248
249
250
251
252
253
	  dest->destroy();
	}
      return std::cerr;
    }


254
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

    // 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_;
    };

297
298
299
300
    // Rewrite rule for rational operators.
    class ratexp_trad_visitor: public const_visitor
    {
    public:
301
302
303
304
305
      // 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)
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
      {
      }

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

      bdd
      result() const
      {
	return res_;
      }

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

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

335
	return bddfalse;
336
337
338
339
340
      }

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

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

	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;
	      }
	  }

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
	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:
393
394
	  case unop::Closure:
	  case unop::NegClosure:
395
396
	    assert(!"not a rational operator");
	    return;
397
398
	  case unop::Not:
	    {
399
400
	      // Not can only appear in front of Boolean
	      // expressions.
401
402
	      // propositions.
	      const formula* f = node->child();
403
	      assert(f->is_boolean());
404
	      res_ = recurse_and_concat(f, true);
405
406
	      return;
	    }
407
408
409
410
	  }
	/* Unreachable code.  */
	assert(0);
      }
411

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

	assert(max > 0);

421
422
423
424
425
426
427
428
429
430
431
432
433
	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());

434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
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
	    if (!bo->child()->accepts_eword())
	      {
		//   f*;g  ->  f;f*;g | g
		//
		// If f does not accept the empty word, we can easily
		// add "f*;g" as to_concat_ when translating f.
		res_ = recurse(bo->child(), f);
		if (min == 0)
		  res_ |= now_to_concat();
	      }
	    else
	      {
		// if "f" accepts the empty words, doing the above would
		// lead to an infinite loop:
		//   f*;g -> f;f*;g | g
		//   f;f*;g -> f*;g | ...
		//
		// So we do in two steps:
		//  1. translate f,
		//  2. append f*;g to all destinations
		//  3. add |g
		res_ = recurse(bo->child());

		//   f*;g  ->  f;f*;g
		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);
		    formula* dest2;
		    int x;
		    if (dest == constant::empty_word_instance())
		      {
			x = dict_.register_next_variable(f);
			res_ |= label & bdd_ithvar(x);
		      }
		    else
		      {
			dest2 = multop::instance(multop::Concat, dest,
						 f->clone());
			if (dest2 != constant::false_instance())
			  {
			    x = dict_.register_next_variable(dest2);
			    dest2->destroy();
			    res_ |= label & bdd_ithvar(x);
			  }
		      }
		  }
		f->destroy();
		res_ |= now_to_concat();
	      }
489
	    return;
490
	  case bunop::Equal:
491
	  case bunop::Goto:
492
493
494
495
496
497
	    {
	      // 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.

498
499
500
501
502
503
	      // 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]
504
505
506
507
508
		multop::instance(multop::Concat,
				 unop::instance(unop::Not,
						bo->child()->clone()),
				 bo->clone());

509
	      formula* f2 = // b;b[=min-1..max-1]  or  b;b[->min-1..max-1]
510
511
		multop::instance(multop::Concat,
				 bo->child()->clone(),
512
				 bunop::instance(op,
513
514
515
516
517
518
519
520
521
						 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;
	    }
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
	  }
	/* 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)
      {
542
543
	multop::type op = node->op();
	switch (op)
544
	  {
545
	  case multop::AndNLM:
546
547
548
	  case multop::And:
	    {
	      unsigned s = node->size();
549
550
551
552
553
554
555
556
557

	      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);
558
		      if (f->accepts_eword())
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
			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);
582
583
		      formula* t = bunop::instance(bunop::Star,
						   constant::true_instance());
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
		      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;
605
	      for (unsigned n = 0; n < s; ++n)
606
607
608
609
610
		{
		  bdd res = recurse(node->nth(n));
		  // trace_ltl_bdd(dict_, res);
		  res_ &= res;
		}
611
612
613
614
615
616

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

	      if (to_concat_)
		{
617
		  // If we have translated (a* && b*) in (a* && b*);c, we
618
619
620
621
622
623
624
625
626
		  // 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);
627
628
		      formula* dest =
			dict_.conj_bdd_to_formula(dest_bdd, op);
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
		      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);
			    }
645
			  if (node->accepts_eword())
646
647
648
649
			    res_ |= label & next_to_concat();
			}
		    }
		}
650
	      if (node->accepts_eword())
651
		res_ |= now_to_concat();
652
653
654
655
656
657
658

	      break;
	    }
	  case multop::Or:
	    {
	      res_ = bddfalse;
	      unsigned s = node->size();
659
660
	      for (unsigned n = 0; n < s; ++n)
		res_ |= recurse_and_concat(node->nth(n));
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
	      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;
	    }
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
	  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);

704
		  if (dest->accepts_eword())
705
706
707
708
709
		    {
		      // The destination is a final state.  Make sure we
		      // can also exit if tail is satisfied.
		      if (!tail_computed)
			{
710
			  tail_bdd = recurse_and_concat(tail);
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
			  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;
	    }
738
739
740
741
	  }
      }

      bdd
742
      recurse(const formula* f, formula* to_concat = 0, bool negated = false)
743
      {
744
	ratexp_trad_visitor v(dict_, to_concat, negated);
745
746
747
748
	f->accept(v);
	return v.result();
      }

749
      bdd
750
      recurse_and_concat(const formula* f, bool negated = false)
751
      {
752
	return recurse(f, to_concat_ ? to_concat_->clone() : 0, negated);
753
      }
754
755
756
757
758

    private:
      translate_dict& dict_;
      bdd res_;
      formula* to_concat_;
759
      bool negated_;
760
761
    };

762

763
    // The rewrite rules used here are adapted from Jean-Michel
764
    // Couvreur's FM paper, augmented to support rational operators.
765
766
767
    class ltl_trad_visitor: public const_visitor
    {
    public:
768
769
770
771
      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)
772
773
774
775
776
777
778
779
      {
      }

      virtual
      ~ltl_trad_visitor()
      {
      }

780
781
782
783
784
785
786
787
      void
      reset(bool mark_all)
      {
	rat_seen_ = false;
	has_marked_ = false;
	mark_all_ = mark_all;
      }

788
789
      bdd
      result() const
790
791
792
793
      {
	return res_;
      }

794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
      const translate_dict&
      get_dict() const
      {
	return dict_;
      }

      bool
      has_rational() const
      {
	return rat_seen_;
      }

      bool
      has_marked() const
      {
	return has_marked_;
      }

812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
      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;
829
	  case constant::EmptyWord:
830
831
	    assert(!"Not an LTL operator");
	    return;
832
833
834
835
836
837
838
839
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const unop* node)
      {
840
841
842
	unop::type op = node->op();

	switch (op)
843
844
845
846
	  {
	  case unop::F:
	    {
	      // r(Fy) = r(y) + a(y)r(XFy)
847
848
849
	      const formula* child = node->child();
	      bdd y = recurse(child);
	      int a = dict_.register_a_variable(child);
850
851
	      int x = dict_.register_next_variable(node);
	      res_ = y | (bdd_ithvar(a) & bdd_ithvar(x));
852
	      break;
853
854
855
	    }
	  case unop::G:
	    {
856
857
858
859
860
861
862
863
864
865
866
867
	      // 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)
868
	      const formula* child = node->child();
869
	      int x = dict_.register_next_variable(node);
870
871
	      bdd y = recurse(child);
	      res_ = y & bdd_ithvar(x);
872
	      break;
873
874
875
	    }
	  case unop::Not:
	    {
876
	      // r(!y) = !r(y)
877
	      res_ = bdd_not(recurse(node->child()));
878
	      break;
879
880
881
	    }
	  case unop::X:
	    {
882
	      // r(Xy) = Next[y]
883
884
	      int x = dict_.register_next_variable(node->child());
	      res_ = bdd_ithvar(x);
885
	      break;
886
	    }
887
888
889
	  case unop::Closure:
	    {
	      rat_seen_ = true;
890
	      if (node->child()->accepts_eword())
891
892
893
894
895
896
		{
		  res_ = bddtrue;
		  return;
		}

	      ratexp_trad_visitor v(dict_);
897
898
899
900
	      node->child()->accept(v);
	      bdd f1 = v.result();
	      res_ = bddfalse;

901

902
903
904
905
906
907
908
909
910
911
912
913
914
915
	      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;
916
		      if (dest->accepts_eword())
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
			{
			  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;
943
		      if (dest->accepts_eword())
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
			{
			  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;
966

967
	      if (node->child()->accepts_eword())
968
969
970
971
972
973
		{
		  res_ = bddfalse;
		  return;
		}

	      ratexp_trad_visitor v(dict_);
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
	      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.
997
		  if (dest->accepts_eword())
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
		    {
		      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;

1015
1016
	  case unop::Finish:
	    assert(!"unsupported operator");
1017
	    break;
1018
1019
1020
	  }
      }

1021
1022
1023
1024
1025
1026
      void
      visit(const bunop*)
      {
	assert(!"Not an LTL operator");
      }

1027
1028
1029
      void
      visit(const binop* node)
      {
1030
	binop::type op = node->op();
1031

1032
	switch (op)
1033
	  {
1034
	    // r(f1 logical-op f2) = r(f1) logical-op r(f2)
1035
	  case binop::Xor:
1036
1037
1038
1039
1040
1041
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_xor);
	      return;
	    }
1042
	  case binop::Implies:
1043
1044
1045
1046
1047
1048
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_imp);
	      return;
	    }
1049
	  case binop::Equiv:
1050
1051
1052
1053
1054
1055
	    {
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
	      res_ = bdd_apply(f1, f2, bddop_biimp);
	      return;
	    }
1056
1057
	  case binop::U:
	    {
1058
1059
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1060
1061
1062
1063
	      // 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));
1064
	      break;
1065
	    }
1066
1067
	  case binop::W:
	    {
1068
1069
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1070
1071
1072
	      // 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));
1073
	      break;
1074
	    }
1075
1076
	  case binop::R:
	    {
1077
1078
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1079
1080
1081
	      // 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));
1082
	      break;
1083
	    }
1084
1085
	  case binop::M:
	    {
1086
1087
	      bdd f1 = recurse(node->first());
	      bdd f2 = recurse(node->second());
1088
1089
1090
1091
	      // 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));
1092
	      break;
1093
	    }
1094
1095
1096
	  case binop::EConcatMarked:
	    has_marked_ = true;
	    /* fall through */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1097
	  case binop::EConcat:
1098
1099
	    rat_seen_ = true;
	    {
1100
1101
	      // Recognize f2 on transitions going to destinations
	      // that accept the empty word.
1102
	      bdd f2 = recurse(node->second());
1103
	      ratexp_trad_visitor v(dict_);
1104
1105
	      node->first()->accept(v);
	      bdd f1 = v.result();
1106
	      res_ = bddfalse;
1107
1108
1109
1110
1111
1112
1113

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

1114
	      if (exprop_)
1115
		{
1116
1117
1118
		  bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
		  bdd all_props = bdd_existcomp(f1, dict_.var_set);
		  while (all_props != bddfalse)
1119
		    {
1120
		      bdd label = bdd_satoneset(all_props, var_set, bddtrue);
1121
1122
1123
1124
1125
1126
1127
1128
1129
		      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());

1130
1131
		      if (dest2 != constant::false_instance())
			{
1132
			  int x = dict_.register_next_variable(dest2);
1133
1134
1135
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
1136
		      if (dest->accepts_eword())
1137
1138
1139
			res_ |= label & f2;
		    }
		}
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
	      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);
			    }
1164
			  if (dest->accepts_eword())
1165
1166
1167
1168
			    res_ |= label & f2;
			}
		    }
		}
1169
1170
1171
1172
1173
	    }
	    break;

	  case binop::UConcat:
	    {
1174
1175
1176
	      // Transitions going to destinations accepting the empty
	      // word should recognize f2, and the automaton for f1
	      // should be understood as universal.
1177
	      bdd f2 = recurse(node->second());
1178
	      ratexp_trad_visitor v(dict_);
1179
1180
1181
	      node->first()->accept(v);
	      bdd f1 = v.result();
	      res_ = bddtrue;
1182

1183
1184
1185
	      bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
	      bdd all_props = bdd_existcomp(f1, dict_.var_set);
	      while (all_props != bddfalse)
1186
1187
		{

1188
1189
1190
1191
		  bdd one_prop_set = bddtrue;
		  if (exprop_)
		    one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
		  all_props -= one_prop_set;
1192

1193
		  minato_isop isop(f1 & one_prop_set);
1194
1195
1196
1197
1198
1199
		  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);
1200
1201
		      formula* dest2 =
			binop::instance(op, dest, node->second()->clone());
1202

1203
1204
		      bdd udest =
			bdd_ithvar(dict_.register_next_variable(dest2));
1205

1206
		      if (dest->accepts_eword())
1207
1208
1209
1210
			udest &= f2;

		      dest2->destroy();

1211
		      res_ &= bdd_apply(label, udest, bddop_imp);
1212
		    }
1213
1214
		}
	    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1215
	    break;
1216
1217
1218
	  }
      }

1219
1220
1221
1222
1223
1224
      void
      visit(const automatop*)
      {
	assert(!"unsupported operator");
      }

1225
1226
1227
1228
1229
1230
      void
      visit(const multop* node)
      {
	switch (node->op())
	  {
	  case multop::And:
1231
1232
1233
1234
1235
1236
	    {
	      res_ = bddtrue;
	      unsigned s = node->size();
	      for (unsigned n = 0; n < s; ++n)
		{
		  bdd res = recurse(node->nth(n));
1237
1238
1239
		  //std::cerr << "== in And (" << to_string(node->nth(n))
		  // << ")" << std::endl;
		  // trace_ltl_bdd(dict_, res);
1240
1241
		  res_ &= res;
		}
1242
1243
	      //std::cerr << "=== And final" << std::endl;
	      // trace_ltl_bdd(dict_, res_);
1244
1245
	      break;
	    }
1246
	  case multop::Or:
1247
1248
1249
1250
1251
1252
1253
	    {
	      res_ = bddfalse;
	      unsigned s = node->size();
	      for (unsigned n = 0; n < s; ++n)
		res_ |= recurse(node->nth(n));
	      break;
	    }
1254
	  case multop::Concat:
1255
	  case multop::Fusion:
1256
	  case multop::AndNLM:
1257
1258
	    assert(!"Not an LTL operator");
	    break;
1259
	  }
1260

1261
1262
1263
1264
1265
      }

      bdd
      recurse(const formula* f)
      {
1266
	ltl_trad_visitor v(dict_, mark_all_, exprop_);
1267
	f->accept(v);
1268
1269
	rat_seen_ |= v.has_rational();
	has_marked_ |= v.has_marked();
1270
1271
1272
1273
1274
1275
1276
	return v.result();
      }


    private:
      translate_dict& dict_;
      bdd res_;
1277
1278
1279
      bool rat_seen_;
      bool has_marked_;
      bool mark_all_;
1280
      bool exprop_;
1281
1282
    };

1283

1284
1285
    // Check whether a formula has a R, W, or G operator at its
    // top-level (preceding logical operators do not count).
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
    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:
1336
	  case binop::M:
1337
1338
	    return;
	  case binop::R:
1339
	  case binop::W:
1340
1341
	    res_ = true;
	    return;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1342
1343
	  case binop::UConcat:
	  case binop::EConcat:
1344
	  case binop::EConcatMarked:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1345
	    node->second()->accept(*this);
1346
	    // FIXME: we might need to add Acc[1]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1347
	    return;
1348
1349
1350
1351
1352
	  }
	/* Unreachable code.  */
	assert(0);
      }

1353
1354
1355
1356
1357
1358
      void
      visit(const automatop*)
      {
	assert(!"unsupported operator");
      }

1359
1360
1361
1362
1363
1364
      void
      visit(const bunop*)
      {
	assert(!"unsupported operator");
      }

1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
      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)
      {
1387
1388
	pfl_map::const_iterator i = pfl_.find(f);
	if (i != pfl_.end())
1389
1390
1391
1392
	  return i->second;
	ltl_possible_fair_loop_visitor v;
	f->accept(v);
	bool rel = v.result();
1393
	pfl_[f] = rel;
1394
1395
1396
1397
	return rel;
      }

    private:
1398
      typedef Sgi::hash_map<const formula*, bool, formula_ptr_hash> pfl_map;
1399
      pfl_map pfl_;
1400
1401
    };

1402
1403
1404
    class formula_canonizer
    {
    public:
1405
      formula_canonizer(translate_dict& d,
1406
1407
			bool fair_loop_approx, bdd all_promises, bool exprop)
	: v_(d, false, exprop),