ltl2tgba_fm.cc 65 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
4
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
5
6
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
//
// 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

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

namespace spot
{
  using namespace ltl;

  namespace
  {

50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

    // This should only be called on And formulae and return
    // the set of subformula that are implied by the formulas
    // already in the And.
    // If f = Ga & (b R c) & G(d & (e R (g R h)) & Xj) & Xk this
    // returns the set {a,  # implied by Ga
    //                  c,  # implied by b R c
    //                  d, e R (g R h), g R h, h, Xj # implied by G(d & ...)
    //                 }
    // Leave recurring to false on first call.
    typedef std::set<const formula*, formula_ptr_less_than> formula_set;
    void
    implied_subformulae(const formula* in, formula_set& rec,
			bool recurring = false)
    {
      const multop* f = is_And(in);
      if (!f)
	{
	  // Only recursive calls should be made with an operator that
	  // is not And.
	  assert(recurring);
	  rec.insert(in);
	  return;
	}
      unsigned s = f->size();
      for (unsigned n = 0; n < s; ++n)
	{
	  const formula* sub = f->nth(n);
	  // Recurring is set if we are under "G(...)" or "0 R (...)"
	  // or (...) W 0".
	  if (recurring)
	    rec.insert(sub);
	  if (const unop* g = is_G(sub))
	    {
	      implied_subformulae(g->child(), rec, true);
	    }
	  else if (const binop* w = is_W(sub))
	    {
	      // f W 0 = Gf
	      if (w->second() == constant::false_instance())
		implied_subformulae(w->first(), rec, true);
	    }
	  else
	    while (const binop* b = is_binop(sub, binop::R, binop::M))
	      {
		// in 'f R g' and 'f M g' always evaluate 'g'.
		sub = b->second();
		if (b->first() == constant::false_instance())
		  {
		    assert(b->op() == binop::R); // because 0 M g = 0
		    // 0 R f = Gf
		    implied_subformulae(sub, rec, true);
		    break;
		  }
		rec.insert(sub);
	      }
	}
    }

109
110
111
112
    class translate_dict;

    class ratexp_to_dfa
    {
113
      typedef typename twa_graph::namer<const formula*>::type namer;
114
115
    public:
      ratexp_to_dfa(translate_dict& dict);
116
      std::tuple<const_twa_graph_ptr, const namer*, const state*>
117
      succ(const formula* f);
118
119
120
      ~ratexp_to_dfa();

    protected:
121
      typedef std::pair<twa_graph_ptr, const namer*> labelled_aut;
122
      labelled_aut translate(const formula* f);
123
124
125

    private:
      translate_dict& dict_;
126
      typedef std::unordered_map<const formula*, labelled_aut> f2a_t;
127
      std::vector<labelled_aut> automata_;
128
129
130
      f2a_t f2a_;
    };

131
132
    // Helper dictionary.  We represent formulae using BDDs to
    // simplify them, and then translate BDDs back into formulae.
133
134
135
136
137
    //
    // 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.
138
    class translate_dict
139
140
141
    {
    public:

142
143
144
      translate_dict(const bdd_dict_ptr& dict,
		     acc_cond& acc,
		     ltl_simplifier* ls, bool exprop,
145
		     bool single_acc)
146
	: dict(dict),
147
	  ls(ls),
148
149
	  a_set(bddtrue),
	  var_set(bddtrue),
150
	  next_set(bddtrue),
151
	  transdfa(*this),
152
	  exprop(exprop),
153
154
	  single_acc(single_acc),
	  acc(acc)
155
156
157
158
159
160
      {
      }

      ~translate_dict()
      {
	fv_map::iterator i;
161
162
	for (auto& i: next_map)
	  i.first->destroy();
163
	dict->unregister_all_my_variables(this);
164

165
	flagged_formula_to_bdd_map::iterator j = ltl_bdd_.begin();
166
	// Advance the iterator before destroying previous value.
167
168
	while (j != ltl_bdd_.end())
	  j++->first.f->destroy();
169
170
      }

171
      bdd_dict_ptr dict;
172
      ltl_simplifier* ls;
173
      mark_tools mt;
174

175
      typedef bdd_dict::fv_map fv_map;
176
      typedef std::vector<const formula*> vf_map;
177
178
179
180
181
182
183
184

      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;

185
      ratexp_to_dfa transdfa;
186
      bool exprop;
187
      bool single_acc;
188
189
190
      acc_cond& acc;
      // Map BDD variables to acceptance marks.
      std::map<int, unsigned> bm;
191

192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
      enum translate_flags
	{
	  flags_none = 0,
	  // Keep these bits slightly apart as we will use them as-is
	  // in the hash function for flagged_formula.
	  flags_mark_all = (1<<10),
	  flags_recurring = (1<<14),
	};

      struct flagged_formula
      {
	const formula* f;
	unsigned flags;		// a combination of translate_flags

	bool
	operator==(const flagged_formula& other) const
	{
	  return this->f == other.f && this->flags == other.flags;
	}
      };

      struct flagged_formula_hash:
	public std::unary_function<flagged_formula, size_t>
      {
	size_t
	operator()(const flagged_formula& that) const
	{
	  return that.f->hash() ^ size_t(that.flags);
	}
      };

223
224
225
226
227
228
229
      struct translated
      {
	bdd symbolic;
	bool has_rational:1;
	bool has_marked:1;
      };

230
231
232
      typedef
      std::unordered_map<flagged_formula, translated,
			 flagged_formula_hash> flagged_formula_to_bdd_map;
233
    private:
234
      flagged_formula_to_bdd_map ltl_bdd_;
235
236

    public:
237

238

239
      int
240
      register_proposition(const formula* f)
241
      {
242
	int num = dict->register_proposition(f, this);
243
244
245
246
	var_set &= bdd_ithvar(num);
	return num;
      }

247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
      acc_cond::mark_t
      bdd_to_mark(bdd a)
      {
	bdd o = a;
	if (a == bddtrue)
	  return 0U;
	assert(a != bddfalse);
	std::vector<unsigned> t;
	do
	  {
	    int v = bdd_var(a);
	    bdd h = bdd_high(a);
	    a = bdd_low(a);
	    if (h != bddfalse)
	      {
		t.push_back(bm[v]);
		if (a == bddfalse)
		  a = h;
	      }
	  }
	while (a != bddtrue);
	return acc.marks(t.begin(), t.end());
      }

271
      int
272
      register_a_variable(const formula* f)
273
      {
274
275
276
277
278
	if (single_acc)
	  {
	    int num = dict->register_acceptance_variable
	      (ltl::constant::true_instance(), this);
	    a_set &= bdd_ithvar(num);
279
280
281
282

	    auto p = bm.emplace(num, 0U);
	    if (p.second)
	      p.first->second = acc.add_set();
283
284
	    return num;
	  }
285
286
287
288
289
290
291
292
293
294
295
	// A promise of 'x', noted P(x) is pretty much like the F(x)
	// LTL formula, it ensure that 'x' will be fulfilled (= not
	// promised anymore) eventually.
	// So   a U b = ((a&Pb) W b)
	//      a U (b U c) = (a&P(b U c)) W (b&P(c) W c)
	// the latter encoding may be simplified to
	//      a U (b U c) = (a&P(c)) W (b&P(c) W c)
	//
	// Similarly
	//      a M b = (a R (b&P(a)))
	//      (a M b) M c = (a R (b & Pa)) R (c & P(a M b))
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
	//                  = (a R (b & Pa)) R (c & P(a & b))
	//
	// The code below therefore implement the following
	// rules:
	// P(a U b) = P(b)
	// P(F(a))  = P(a)
	// P(a M b) = P(a & b)
	//
	// The latter rule INCORRECTLY appears as P(a M b)=P(a)
	// in section 3.5 of
	//    "LTL translation improvements in Spot 1.0",
	//     A. Duret-Lutz. IJCCBS 5(1/2):31-54, March 2014.
	// and was unfortunately implemented this way until Spot
	// 1.2.4.  A counterexample is given by the formula
	//    G(Fa & ((a M b) U ((c U !d) M d)))
	// that was found by Joachim Klein.  Here P((c U !d) M d)
	// and P(c U !d) should not both be simplified to P(!d).
	for (;;)
314
	  {
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
	    if (const binop* b = is_binop(f))
	      {
		binop::type op = b->op();
		if (op == binop::U)
		  {
		    // P(a U b) = P(b)
		    f = b->second();
		  }
		else if (op == binop::M)
		  {
		    // P(a M b) = P(a & b)
		    const formula* g =
		      multop::instance(multop::And,
				       b->first()->clone(),
				       b->second()->clone());
		    int num = dict->register_acceptance_variable(g, this);
		    a_set &= bdd_ithvar(num);
		    g->destroy();
333
334
335
336
337

		    auto p = bm.emplace(num, 0U);
		    if (p.second)
		      p.first->second = acc.add_set();

338
339
340
341
342
343
344
345
346
347
348
349
		    return num;
		  }
		else
		  {
		    break;
		  }
	      }
	    else if (const unop* u = is_unop(f, unop::F))
	      {
		// P(F(a)) = P(a)
		f = u->child();
	      }
350
	    else
351
352
353
	      {
		break;
	      }
354
	  }
355
	int num = dict->register_acceptance_variable(f, this);
356
	a_set &= bdd_ithvar(num);
357
358
359
360
361

	auto p = bm.emplace(num, 0U);
	if (p.second)
	  p.first->second = acc.add_set();

362
363
364
365
	return num;
      }

      int
366
      register_next_variable(const formula* f)
367
368
369
370
371
372
373
374
375
376
      {
	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
	  {
377
	    f = f->clone();
378
	    num = dict->register_anonymous_variables(1, this);
379
	    next_map[f] = num;
380
	    next_formula_map.resize(bdd_varnum());
381
382
383
384
385
386
	    next_formula_map[num] = f;
	  }
	next_set &= bdd_ithvar(num);
	return num;
      }

387
388
389
390
391
      std::ostream&
      dump(std::ostream& os) const
      {
	fv_map::const_iterator fi;
	os << "Next Variables:" << std::endl;
392
	for (auto& fi: next_map)
393
	{
394
	  os << "  " << fi.second << ": Next[";
395
	  to_string(fi.first, os) << ']' << std::endl;
396
397
398
399
400
401
	}
	os << "Shared Dict:" << std::endl;
	dict->dump(os);
	return os;
      }

402
      const formula*
403
404
      var_to_formula(int var) const
      {
405
	const bdd_dict::bdd_info& i = dict->bdd_map[var];
406
407
408
409
410
411
412
413
	if (i.type != bdd_dict::anon)
	  {
	    assert(i.type == bdd_dict::acc || i.type == bdd_dict::var);
	    return i.f->clone();
	  }
	const formula* f = next_formula_map[var];
	assert(f);
	return f->clone();
414
415
      }

416
417
418
419
420
421
422
423
      bdd
      boolean_to_bdd(const formula* f)
      {
	bdd res = ls->as_bdd(f);
	var_set &= bdd_support(res);
	return res;
      }

424
      const formula*
425
      conj_bdd_to_formula(bdd b, multop::type op = multop::And) const
426
427
      {
	if (b == bddfalse)
428
429
	  return constant::false_instance();
	multop::vec* v = new multop::vec;
430
431
432
	while (b != bddtrue)
	  {
	    int var = bdd_var(b);
433
	    const formula* res = var_to_formula(var);
434
435
436
	    bdd high = bdd_high(b);
	    if (high == bddfalse)
	      {
437
		res = unop::instance(unop::Not, res);
438
439
440
441
		b = bdd_low(b);
	      }
	    else
	      {
442
		assert(bdd_low(b) == bddfalse);
443
444
445
446
447
		b = high;
	      }
	    assert(b != bddfalse);
	    v->push_back(res);
	  }
448
	return multop::instance(op, v);
449
450
      }

451
      const formula*
452
453
454
455
456
      conj_bdd_to_sere(bdd b) const
      {
	return conj_bdd_to_formula(b, multop::AndRat);
      }

457
      const formula*
458
      bdd_to_formula(bdd f)
459
      {
460
	if (f == bddfalse)
461
	  return constant::false_instance();
462

463
464
465
466
467
468
469
470
471
	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);
      }
472

473
      const formula*
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
      bdd_to_sere(bdd f)
      {
	if (f == bddfalse)
	  return constant::false_instance();

	multop::vec* v = new multop::vec;

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

	return multop::instance(multop::OrRat, v);
      }

489
      const translated&
490
      ltl_to_bdd(const formula* f, bool mark_all, bool recurring = false);
491

492
493
    };

494
495
496
497
498
#ifdef __GNUC__
#  define unused __attribute__((unused))
#else
#  define unused
#endif
499

500
    // Debugging function.
501
    static unused
502
503
504
    std::ostream&
    trace_ltl_bdd(const translate_dict& d, bdd f)
    {
505
      std::cerr << "Displaying BDD ";
506
      bdd_print_set(std::cerr, d.dict, f) << ":\n";
507

508
509
510
511
512
513
514
      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);
515
516
517
	  bdd_print_set(std::cerr, d.dict, label) << " => ";
	  bdd_print_set(std::cerr, d.dict, dest_bdd) << " = "
						     << to_string(dest)
518
						     << '\n';
519
520
521
522
523
524
	  dest->destroy();
	}
      return std::cerr;
    }


525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549

    // 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
550
      doit(const unop* node)
551
552
553
554
555
556
      {
	if (node->op() == unop::F)
	  res_ &= bdd_ithvar(dict_.register_a_variable(node->child()));
      }

      virtual void
557
      doit(const binop* node)
558
559
560
561
562
563
564
565
566
567
      {
	if (node->op() == binop::U)
	  res_ &= bdd_ithvar(dict_.register_a_variable(node->second()));
      }

    private:
      translate_dict& dict_;
      bdd res_;
    };

568
    bdd translate_ratexp(const formula* f, translate_dict& dict,
569
			 const formula* to_concat = 0);
570

571
    // Rewrite rule for rational operators.
572
    class ratexp_trad_visitor: public visitor
573
574
    {
    public:
575
576
      // negated should only be set for constants or atomic properties
      ratexp_trad_visitor(translate_dict& dict,
577
			  const formula* to_concat = 0)
578
	: dict_(dict), to_concat_(to_concat)
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
      {
      }

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

      bdd
      result() const
      {
	return res_;
      }

      bdd next_to_concat()
      {
597
598
599
600
601
602
603
604
	// Encoding X[*0] when there is nothing to concatenate is a
	// way to ensure that we distinguish the rational formula "a"
	// (encoded as "a&X[*0]") from the rational formula "a;[*]"
	// (encoded as "a&X[*]").
	//
	// It's important that when we do "a && (a;[*])" we do not get
	// "a;[*]" as it would occur if we had simply encoded "a" as
	// "a".
605
	if (!to_concat_)
606
	  to_concat_ = constant::empty_word_instance();
607
608
609
610
611
612
	int x = dict_.register_next_variable(to_concat_);
	return bdd_ithvar(x);
      }

      bdd now_to_concat()
      {
613
614
615
	if (to_concat_ && to_concat_ != constant::empty_word_instance())
	  return recurse(to_concat_);

616
	return bddfalse;
617
618
      }

619
620
621
622
623
624
625
626
627
628
629
630
631
      // Append to_concat_ to all Next variables in IN.
      bdd
      concat_dests(bdd in)
      {
	if (!to_concat_)
	  return in;
	minato_isop isop(in);
	bdd cube;
	bdd out = bddfalse;
	while ((cube = isop.next()) != bddfalse)
	  {
	    bdd label = bdd_exist(cube, dict_.next_set);
	    bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
632
	    const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
633
634
635
636
637
638
	    if (dest == constant::empty_word_instance())
	      {
		out |= label & next_to_concat();
	      }
	    else
	      {
639
640
		const formula* dest2 = multop::instance(multop::Concat, dest,
							to_concat_->clone());
641
642
643
644
645
646
647
648
649
650
651
		if (dest2 != constant::false_instance())
		  {
		    int x = dict_.register_next_variable(dest2);
		    dest2->destroy();
		    out |= label & bdd_ithvar(x);
		  }
	      }
	  }
	return out;
      }

652
653
654
      void
      visit(const atomic_prop* node)
      {
655
	res_ = bdd_ithvar(dict_.register_proposition(node));
656
	res_ &= next_to_concat();
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
      }

      void
      visit(const constant* node)
      {
	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;
	  }
674
	SPOT_UNREACHABLE();
675
676
677
678
679
680
681
682
683
684
      }

      void
      visit(const unop* node)
      {
	switch (node->op())
	  {
	  case unop::F:
	  case unop::G:
	  case unop::X:
685
686
	  case unop::Closure:
	  case unop::NegClosure:
687
	  case unop::NegClosureMarked:
688
	    SPOT_UNREACHABLE();	// Because not rational operator
689
690
	  case unop::Not:
	    {
691
692
	      // Not can only appear in front of Boolean
	      // expressions.
693
	      const formula* f = node->child();
694
	      assert(f->is_boolean());
695
696
	      res_ = !recurse(f);
	      res_ &= next_to_concat();
697
698
	      return;
	    }
699
	  }
700
	SPOT_UNREACHABLE();
701
      }
702

703
704
705
      void
      visit(const bunop* bo)
      {
706
	const formula* f;
707
708
	unsigned min = bo->min();
	unsigned max = bo->max();
709
710

	assert(max > 0);
711
	bunop::type op = bo->op();
712

713
714
715
716
717
718
719
720
	// we will interpret
	//         c[*i..j]
	//     or  c[:*i..j]
	// as
	//         c;c[*i-1..j-1]
	//     or  c:c[*i-1..j-1]
	//           \........../
	//            this is f
721
722
723
	unsigned min2 = (min == 0) ? 0 : (min - 1);
	unsigned max2 =
	  (max == bunop::unbounded) ? bunop::unbounded : (max - 1);
724
725
726
727
728
729
730
	f = bunop::instance(op, bo->child()->clone(), min2, max2);

	// If we have something to append, we can actually append it
	// to f.  This is correct even in the case of FStar, as f
	// cannot accept [*0].
	if (to_concat_)
	  f = multop::instance(multop::Concat, f, to_concat_->clone());
731
732
733
734

	switch (op)
	  {
	  case bunop::Star:
735
736
737
738
739
740
741
742
743
744
745
746
	    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
	      {
747
		// if "f" accepts the empty word, doing the above would
748
749
750
751
		// lead to an infinite loop:
		//   f*;g -> f;f*;g | g
		//   f;f*;g -> f*;g | ...
		//
752
		// So we do it in three steps:
753
754
755
756
757
758
759
760
761
762
763
764
765
		//  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);
766
		    const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
767
768
769
770
771
772
773
774
		    int x;
		    if (dest == constant::empty_word_instance())
		      {
			x = dict_.register_next_variable(f);
			res_ |= label & bdd_ithvar(x);
		      }
		    else
		      {
775
776
777
			const formula*
			  dest2 = multop::instance(multop::Concat, dest,
						   f->clone());
778
779
780
781
782
783
784
785
786
787
788
			if (dest2 != constant::false_instance())
			  {
			    x = dict_.register_next_variable(dest2);
			    dest2->destroy();
			    res_ |= label & bdd_ithvar(x);
			  }
		      }
		  }
		f->destroy();
		res_ |= now_to_concat();
	      }
789
	    return;
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
	  case bunop::FStar:
	    {
	      res_ = recurse(bo->child());
	      bdd tail_bdd;
	      bool tail_computed = false;

	      minato_isop isop(res_);
	      bdd cube;
	      res_ = bddfalse;
	      if (min == 0)
		{
		  // f[:*0..j];g  can be satisfied by X(g).
		  res_ = next_to_concat();
		}
	      while ((cube = isop.next()) != bddfalse)
		{
		  bdd label = bdd_exist(cube, dict_.next_set);
		  bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
		  const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);

		  // The destination is a final state.  Make sure we
		  // can also exit if tail is satisfied.  We do not
		  // even have to check the tail if min == 0.
		  if (dest->accepts_eword() && min != 0)
		    {
		      if (!tail_computed)
			{
			  tail_bdd = recurse(f);
			  tail_computed = true;
			}
		      res_ |= label & tail_bdd;
		    }

		  // If the destination is not 0 or [*0], it means it
		  // can have successors.  Fusion the tail.
		  if (dest != constant::false_instance()
		      && dest != constant::empty_word_instance())
		    {
		      const formula* dest2 =
			multop::instance(multop::Fusion, dest, f->clone());
		      if (dest2 != constant::false_instance())
			{
			  int x = dict_.register_next_variable(dest2);
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
		    }
		}
	      f->destroy();
	    }
	    return;
841
	  }
842
	SPOT_UNREACHABLE();
843
844
845
846
847
      }

      void
      visit(const binop*)
      {
848
	SPOT_UNREACHABLE();	// Not a rational operator
849
850
851
852
853
      }

      void
      visit(const multop* node)
      {
854
855
	multop::type op = node->op();
	switch (op)
856
	  {
857
	  case multop::AndNLM:
858
859
	    {
	      unsigned s = node->size();
860
861
	      multop::vec* final = new multop::vec;
	      multop::vec* non_final = new multop::vec;
862

863
	      for (unsigned n = 0; n < s; ++n)
864
		{
865
866
867
868
869
870
		  const formula* f = node->nth(n);
		  if (f->accepts_eword())
		    final->push_back(f->clone());
		  else
		    non_final->push_back(f->clone());
		}
871

872
873
874
875
	      if (non_final->empty())
		{
		  delete non_final;
		  // (a* & b*);c = (a*|b*);c
876
		  const formula* f = multop::instance(multop::OrRat, final);
877
878
879
880
881
882
883
884
885
886
887
		  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);[*]
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
		  const formula* f =
		    multop::instance(multop::OrRat, final);
		  const formula* n =
		    multop::instance(multop::AndNLM, non_final);
		  const formula* t =
		    bunop::instance(bunop::Star, constant::true_instance());
		  const formula* ft =
		    multop::instance(multop::Concat, f->clone(), t->clone());
		  const formula* nt =
		    multop::instance(multop::Concat, n->clone(), t);
		  const formula* ftn =
		    multop::instance(multop::AndRat, ft, n);
		  const formula* fnt =
		    multop::instance(multop::AndRat, f, nt);
		  const formula* all =
		    multop::instance(multop::OrRat, ftn, fnt);
904
905
906
907
908
909
910
911
912
913
914
915
916
		  res_ = recurse_and_concat(all);
		  all->destroy();
		  break;
		}
	      // No final formula.
	      delete final;
	      for (unsigned n = 0; n < s; ++n)
		(*non_final)[n]->destroy();
	      delete non_final;
	      // Translate N_1 & N_2 & ... & N_n into
	      //   N_1 && (N_2;[*]) && ... && (N_n;[*])
	      // | (N_1;[*]) && N_2 && ... && (N_n;[*])
	      // | (N_1;[*]) && (N_2;[*]) && ... && N_n
917
	      const formula* star =
918
919
920
921
922
923
		bunop::instance(bunop::Star, constant::true_instance());
	      multop::vec* disj = new multop::vec;
	      for (unsigned n = 0; n < s; ++n)
		{
		  multop::vec* conj = new multop::vec;
		  for (unsigned m = 0; m < s; ++m)
924
		    {
925
		      const formula* f = node->nth(m)->clone();
926
927
928
929
		      if (n != m)
			f = multop::instance(multop::Concat,
					     f, star->clone());
		      conj->push_back(f);
930
		    }
931
		  disj->push_back(multop::instance(multop::AndRat, conj));
932
		}
933
	      star->destroy();
934
	      const formula* all = multop::instance(multop::OrRat, disj);
935
936
937
938
	      res_ = recurse_and_concat(all);
	      all->destroy();
	      break;
	    }
939
	  case multop::AndRat:
940
941
	    {
	      unsigned s = node->size();
942
943

	      res_ = bddtrue;
944
	      for (unsigned n = 0; n < s; ++n)
945
946
947
948
949
		{
		  bdd res = recurse(node->nth(n));
		  // trace_ltl_bdd(dict_, res);
		  res_ &= res;
		}
950
951
952
953

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

954
955
956
	      // If we have translated (a* && b*) in (a* && b*);c, we
	      // have to append ";c" to all destinations.
	      res_ = concat_dests(res_);
957

958
	      if (node->accepts_eword())
959
		res_ |= now_to_concat();
960

961
962
	      if (op == multop::AndNLM)
		node->destroy();
963
964
	      break;
	    }
965
	  case multop::OrRat:
966
967
968
	    {
	      res_ = bddfalse;
	      unsigned s = node->size();
969
970
	      for (unsigned n = 0; n < s; ++n)
		res_ |= recurse_and_concat(node->nth(n));
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
	      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;
	    }
986
987
988
989
990
991
992
993
	  case multop::Fusion:
	    {
	      assert(node->size() >= 2);

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

	      // the tail
994
	      const formula* tail = node->all_but(0);
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
	      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);
1007
		  const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
1008

1009
		  if (dest->accepts_eword())
1010
1011
1012
1013
1014
		    {
		      // The destination is a final state.  Make sure we
		      // can also exit if tail is satisfied.
		      if (!tail_computed)
			{
1015
			  tail_bdd = recurse(tail);
1016
1017
			  tail_computed = true;
			}
1018
1019
		      res_ |= concat_dests(label & tail_bdd);

1020
1021
		    }

1022
1023
1024
		  // If the destination is not 0 or [*0], it means it
		  // can have successors.  Fusion the tail and append
		  // anything to concatenate.
1025
1026
		  if (dest != constant::false_instance()
		      && dest != constant::empty_word_instance())
1027
		    {
1028
1029
		      const formula* dest2 =
			multop::instance(multop::Fusion, dest, tail->clone());
1030
1031
		      if (to_concat_)
			 dest2 = multop::instance(multop::Concat, dest2,
1032
						  to_concat_->clone());
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
		      if (dest2 != constant::false_instance())
			{
			  int x = dict_.register_next_variable(dest2);
			  dest2->destroy();
			  res_ |= label & bdd_ithvar(x);
			}
		    }
		}

	      tail->destroy();
	      break;
	    }
1045
1046
	  case multop::And:
	  case multop::Or:
1047
	    SPOT_UNREACHABLE();	// Not a rational operator
1048
1049
1050
1051
	  }
      }

      bdd
1052
      recurse(const formula* f, const formula* to_concat = 0)
1053
      {
1054
	return translate_ratexp(f, dict_, to_concat);
1055
1056
      }

1057
      bdd
1058
      recurse_and_concat(const formula* f)
1059
      {
1060
1061
	return translate_ratexp(f, dict_,
				to_concat_ ? to_concat_->clone() : 0);
1062
      }
1063
1064
1065
1066

    private:
      translate_dict& dict_;
      bdd res_;
1067
      const formula* to_concat_;
1068
1069
    };

1070
1071
    bdd
    translate_ratexp(const formula* f, translate_dict& dict,
1072
		     const formula* to_concat)
1073
1074
1075
    {
      // static unsigned indent = 0;
      // for (unsigned i = indent; i > 0; --i)
1076
      // 	std::cerr << "| ";
1077
1078
      // std::cerr << "translate_ratexp[" << to_string(f);
      // if (to_concat)
1079
      // 	std::cerr << ", " << to_string(to_concat);
1080
      // std::cerr << ']' << std::endl;
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
      // ++indent;
      bdd res;
      if (!f->is_boolean())
	{
	  ratexp_trad_visitor v(dict, to_concat);
	  f->accept(v);
	  res = v.result();
	}
      else
	{
	  res = dict.boolean_to_bdd(f);
	  // See comment for similar code in next_to_concat.
	  if (!to_concat)
	    to_concat = constant::empty_word_instance();
	  int x = dict.register_next_variable(to_concat);
	  res &= bdd_ithvar(x);
	  to_concat->destroy();
	}
      // --indent;
      // for (unsigned i = indent; i > 0; --i)
1101
      // 	std::cerr << "| ";
1102
1103
1104
1105
1106
1107
      // std::cerr << "\\ ";
      // bdd_print_set(std::cerr, dict.dict, res) << std::endl;
      return res;
    }


1108
1109
1110
1111
1112
1113
1114
    ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict)
      : dict_(dict)
    {
    }

    ratexp_to_dfa::~ratexp_to_dfa()
    {
1115
      for (auto i: automata_)
1116
1117
1118
1119
1120
	{
	  for (auto n: i.second->names())
	    n->destroy();
	  delete i.second;
	}
1121
1122
    }

1123
    ratexp_to_dfa::labelled_aut
1124
1125
1126
1127
    ratexp_to_dfa::translate(const formula* f)
    {
      assert(f->is_in_nenoform());

1128
      auto a = make_twa_graph(dict_.dict);
1129
      auto namer = a->create_namer<const formula*>();
1130
1131
1132
1133
1134
1135

      typedef std::set<const formula*, formula_ptr_less_than> set_type;
      set_type formulae_to_translate;

      f->clone();
      formulae_to_translate.insert(f);
1136
1137
      namer->new_state(f);
      //a->set_init_state(f);
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156

      while (!formulae_to_translate.empty())
	{
	  // Pick one formula.
	  const formula* now = *formulae_to_translate.begin();
	  formulae_to_translate.erase(formulae_to_translate.begin());

	  // Translate it
	  bdd res = translate_ratexp(now, dict_);

	  // Generate (deterministic) successors
	  bdd var_set = bdd_existcomp(bdd_support(res), dict_.var_set);
	  bdd all_props = bdd_existcomp(res, dict_.var_set);
	  while (all_props != bddfalse)
	    {
	      bdd label = bdd_satoneset(all_props, var_set, bddtrue);
	      all_props -= label;

	      const formula* dest =
1157
		dict_.bdd_to_sere(bdd_exist(res & label, dict_.var_set));
1158

1159
	      f2a_t::const_iterator i = f2a_.find(dest);
1160
	      if (i != f2a_.end() && i->second.first == nullptr)
1161
1162
1163
1164
1165
1166
		{
		  // This state is useless.  Ignore it.
		  dest->destroy();
		  continue;
		}

1167
1168
1169
1170
1171
	      if (!namer->has_state(dest))
		{
		  formulae_to_translate.insert(dest);
		  namer->new_state(dest);
		}
1172
	      else
1173
1174
1175
1176
1177
		{
		  dest->destroy();
		}

	      namer->new_transition(now, dest, label);
1178
1179
	    }
	}
1180
1181
1182
1183
1184
1185
1186

      // Register all known propositions for a. This may contain
      // proposition from other parts of the formula being translated,
      // but this is not really important as this automaton will be
      // short-lived.  (Maybe it would even work without this line.)
      dict_.dict->register_propositions(dict_.var_set, a);

1187
      //dotty_reachable(std::cerr, a);
1188
1189
1190
1191
1192

      // The following code trims the automaton in a crude way by
      // eliminating SCCs that are not coaccessible.  It does not
      // actually remove the states, it simply marks the corresponding
      // formulae as associated to the null pointer in the f2a_ map.
1193
      // The method succ() interprets this as False.
1194

1195
      scc_info* sm = new scc_info(a);
1196
1197
1198
1199
1200
1201
1202
1203
      unsigned scc_count = sm->scc_count();
      // Remember whether each SCC is coaccessible.
      std::vector<bool> coaccessible(scc_count);
      // SCC are numbered in topological order
      for (unsigned n = 0; n < scc_count; ++n)
	{
	  // The SCC is coaccessible if any of its states
	  // is final (i.e., it accepts [*0])...
1204
	  bool coacc = false;
1205
	  auto& st = sm->states_of(n);
1206
	  for (auto l: st)
1207
	    if (namer->get_name(l)->accepts_eword())
1208
1209
1210
1211
1212
1213
1214
	      {
		coacc = true;
		break;
	      }
	  if (!coacc)
	    {
	      // ... or if any of its successors is coaccessible.
1215
	      for (auto& i: sm->succ(n))
1216
		if (coaccessible[i.dst])
1217
1218
1219
1220
1221
1222
1223
1224
		  {
		    coacc = true;
		    break;
		  }
	    }
	  if (!coacc)
	    {
	      // Mark all formulas of this SCC as useless.
1225
	      for (auto f: st)
1226
1227
1228
		f2a_.emplace(std::piecewise_construct,
			     std::forward_as_tuple(namer->get_name(f)),
			     std::forward_as_tuple(nullptr, nullptr));
1229
1230
1231
	    }
	  else
	    {
1232
	      for (auto f: st)
1233
1234
1235
		f2a_.emplace(std::piecewise_construct,
			     std::forward_as_tuple(namer->get_name(f)),
			     std::forward_as_tuple(a, namer));
1236
1237
1238
1239
1240
1241
	    }
	  coaccessible[n] = coacc;
	}
      delete sm;
      if (coaccessible[scc_count - 1])
	{
1242
1243
	  automata_.emplace_back(a, namer);
	  return labelled_aut(a, namer);
1244
1245
1246
	}
      else
	{
1247
1248
1249
1250
	  for (auto n: namer->names())
	    n->destroy();
	  delete namer;
	  return labelled_aut(nullptr, nullptr);
1251
	}
1252
1253
    }

1254
    // FIXME: use the new tgba::succ() interface
1255
    std::tuple<const_twa_graph_ptr,
1256
1257
	       const ratexp_to_dfa::namer*,
	       const state*>
1258
1259
1260
    ratexp_to_dfa::succ(const formula* f)
    {
      f2a_t::const_iterator it = f2a_.find(f);
1261
      labelled_aut a;
1262
1263
1264
1265
1266
      if (it != f2a_.end())
	a = it->second;
      else
	a = translate(f);

1267
1268
1269
      // If a is null, f has an empty language.
      if (!a.first)
	return std::forward_as_tuple(nullptr, nullptr, nullptr);
1270

1271
1272
1273
1274
      auto namer = a.second;
      assert(namer->has_state(f));
      auto st = a.first->state_from_number(namer->get_state(f));
      return std::forward_as_tuple(a.first, namer, st);
1275
1276
    }

1277
    // The rewrite rules used here are adapted from Jean-Michel
1278
    // Couvreur's FM paper, augmented to support rational operators.
1279
    class ltl_trad_visitor: public visitor
1280
1281
    {
    public:
1282
      ltl_trad_visitor(translate_dict& dict, bool mark_all = false,
1283
		       bool exprop = false, bool recurring = false)
1284
	: dict_(dict), rat_seen_(false), has_marked_(false),
1285
	  mark_all_(mark_all), exprop_(exprop), recurring_(recurring)
1286
1287
1288
1289
1290
1291
1292
1293
      {
      }

      virtual
      ~ltl_trad_visitor()
      {
      }

1294
1295
1296
1297
1298
1299
1300
1301
      void
      reset(bool mark_all)
      {
	rat_seen_ = false;
	has_marked_ = false;
	mark_all_ = mark_all;
      }

1302
1303
      bdd
      result() const
1304
1305
1306
1307
      {
	return res_;
      }

1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
      const translate_dict&
      get_dict() const
      {
<