eltl2tgba_lacim.cc 7.78 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
4
5
6
7
8
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21

#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
22
#include "ltlast/formula_tree.hh"
23
24
25
26
27
28
29
30
31
32
33
34
35
36
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh"
#include "tgba/tgbabddconcretefactory.hh"
#include <cassert>

#include "eltl2tgba_lacim.hh"

namespace spot
{
  namespace
  {
    using namespace ltl;

    /// \brief Recursively translate a formula into a BDD.
37
    class eltl_trad_visitor : public visitor
38
39
40
    {
    public:
      eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
41
	  : fact_(fact), root_(root), finish_()
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
      {
      }

      virtual
      ~eltl_trad_visitor()
      {
      }

      bdd
      result()
      {
	return res_;
      }

      void
      visit(const atomic_prop* node)
      {
	res_ = bdd_ithvar(fact_.create_atomic_prop(node));
      }

      void
      visit(const constant* node)
      {
	switch (node->val())
	  {
	  case constant::True:
	    res_ = bddtrue;
	    return;
	  case constant::False:
	    res_ = bddfalse;
	    return;
73
74
	  case constant::EmptyWord:
	    assert(!"unsupported operator");
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const unop* node)
      {
	switch (node->op())
	  {
	  case unop::Not:
	    {
	      res_ = bdd_not(recurse(node->child()));
	      return;
	    }
90
91
92
93
	  case unop::Finish:
	    {
	      // Ensure finish_[node->child()] has been computed if
	      // node->child() is an automaton operator.
94
	      res_ = recurse(node->child());
95
	      finish_map_::const_iterator it = finish_.find(node->child());
96
	      if (it != finish_.end())
97
98
99
		res_ = finish_[node->child()];
	      return;
	    }
100
101
102
	  case unop::X:
	  case unop::F:
          case unop::G:
103
104
	  case unop::Closure:
	  case unop::NegClosure:
105
	  case unop::NegClosureMarked:
106
107
108
109
110
	    assert(!"unsupported operator");
	  }
	/* Unreachable code.  */
	assert(0);
      }
111
112
113
114
115
116

      void
      visit(const bunop*)
      {
	assert(!"unsupported operator");
      }
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

      void
      visit(const binop* node)
      {
	bdd f1 = recurse(node->first());
	bdd f2 = recurse(node->second());

	switch (node->op())
	  {
	  case binop::Xor:
	    res_ = bdd_apply(f1, f2, bddop_xor);
	    return;
	  case binop::Implies:
	    res_ = bdd_apply(f1, f2, bddop_imp);
	    return;
	  case binop::Equiv:
	    res_ = bdd_apply(f1, f2, bddop_biimp);
	    return;
	  case binop::U:
	  case binop::R:
137
138
	  case binop::W:
	  case binop::M:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
139
140
	  case binop::UConcat:
	  case binop::EConcat:
141
	  case binop::EConcatMarked:
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
	    assert(!"unsupported operator");
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const multop* node)
      {
	int op = -1;
	bool root = false;
	switch (node->op())
	  {
	  case multop::And:
	    op = bddop_and;
	    res_ = bddtrue;
	    // When the root formula is a conjunction it's ok to
	    // consider all children as root formulae.  This allows the
	    // root-G trick to save many more variable.  (See the
	    // translation of G.)
	    root = root_;
	    break;
	  case multop::Or:
	    op = bddop_or;
	    res_ = bddfalse;
	    break;
168
	  case multop::Concat:
169
	  case multop::Fusion:
170
	  case multop::AndNLM:
171
172
	  case multop::AndRat:
	  case multop::OrRat:
173
	    assert(!"unsupported operator");
174
175
176
177
	  }
	assert(op != -1);
	unsigned s = node->size();
	for (unsigned n = 0; n < s; ++n)
178
	  res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
179
180
181
      }

      void
182
      visit(const automatop* node)
183
184
      {
	nmap m;
185
	bdd finish = bddfalse;
186
	bdd acc = bddtrue;
187

188
	std::vector<const formula*> v;
189
	for (unsigned i = 0; i < node->size(); ++i)
190
	  v.push_back(node->nth(i));
191

192
	std::pair<int, int> vp =
193
194
	  recurse_state(node->get_nfa(),
			node->get_nfa()->get_init_state(), v, m, acc, finish);
195
196
197

	// Update finish_ with finish(node).
	// FIXME: when node is loop, it does not make sense; hence the bddtrue.
198
199
200
201
	if (!node->get_nfa()->is_loop())
	  finish_[node] = bddtrue;
	else
	  finish_[node] = finish;
202
203
204
205
206
207
208

	bdd tmp = bddtrue;
	for (nmap::iterator it = m.begin(); it != m.end(); ++it)
	  tmp &= bdd_apply(bdd_ithvar(it->second.first  + 1),
			   bdd_ithvar(it->second.second + 1), bddop_biimp);
	fact_.constrain_relation(bdd_apply(acc, tmp, bddop_imp));

209
210
211
	fact_.declare_acceptance_condition(acc, node);
	res_ = node->is_negated() ?
	  bdd_nithvar(vp.first) : bdd_ithvar(vp.first);
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
      }

      bdd
      recurse(const formula* f, bool root = false)
      {
	eltl_trad_visitor v(fact_, root);
	f->accept(v);
	return v.result();
      }

    private:
      bdd res_;
      tgba_bdd_concrete_factory& fact_;
      bool root_;

227
      /// BDD associated to each automatop A representing finish(A).
228
229
      typedef std::unordered_map<const ltl::formula*, bdd,
				 ltl::formula_ptr_hash> finish_map_;
230
231
232

      finish_map_ finish_;

233
234
      // Table containing the two now variables associated with each state.
      // TODO: a little documentation about that.
235
236
237
      typedef std::unordered_map<const nfa::state*,
				 std::pair<int, int>,
				 ptr_hash<nfa::state>> nmap;
238
239

      std::pair<int, int>&
240
      recurse_state(const nfa::ptr& nfa, const nfa::state* s,
241
		    const std::vector<const formula*>& v,
242
		    nmap& m, bdd& acc, bdd& finish)
243
      {
244
	bool is_loop = nfa->is_loop();
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
	nmap::iterator it;
	it = m.find(s);

	int v1 = 0;
	int v2 = 0;
	if (it != m.end())
	  return it->second;
	else
	{
	  v1 = fact_.create_anonymous_state();
	  v2 = fact_.create_anonymous_state();
	  m[s] = std::make_pair(v1, v2);
	}

	bdd tmp1 = bddfalse;
	bdd tmp2 = bddfalse;
261
	bdd tmpacc = bddfalse;
262
263
	for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i)
	{
264
265
	  const formula* lbl = formula_tree::instanciate((*i)->lbl, v);
	  bdd f = recurse(lbl);
266
	  lbl->destroy();
267
268
269
270
271
	  if (nfa->is_final((*i)->dst))
	  {
	    tmp1 |= f;
	    tmp2 |= f;
	    tmpacc |= f;
272
	    finish |= bdd_ithvar(v1) & f;
273
274
275
	  }
	  else
	  {
276
277
	    std::pair<int, int> vp =
	      recurse_state(nfa, (*i)->dst, v, m, acc, finish);
278
279
	    tmp1 |= (f & bdd_ithvar(vp.first + 1));
	    tmp2 |= (f & bdd_ithvar(vp.second + 1));
280
281
	    if (is_loop)
	      tmpacc |= f;
282
283
284
	  }
	}
	fact_.constrain_relation(bdd_apply(bdd_ithvar(v1), tmp1, bddop_biimp));
285
286
287
	if (is_loop)
	{
	  acc &= bdd_ithvar(v2) | !tmpacc;
288
289
	  fact_.constrain_relation(
	    bdd_apply(bdd_ithvar(v2), tmp2, bddop_invimp));
290
291
292
293
	}
	else
	{
	  acc &= bdd_nithvar(v2) | tmpacc;
294
	  fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp));
295
296
	}

297
298
299
300
301
302
303
304
305
306
307
308
309
310
	return m[s];
      }
    };
  } // anonymous

  tgba_bdd_concrete*
  eltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict)
  {
    // Normalize the formula.  We want all the negations on
    // the atomic propositions.  We also suppress logic
    // abbreviations such as <=>, =>, or XOR, since they
    // would involve negations at the BDD level.
    const ltl::formula* f1 = ltl::unabbreviate_logic(f);
    const ltl::formula* f2 = ltl::negative_normal_form(f1);
311
    f1->destroy();
312
313
314
315

    // Traverse the formula and draft the automaton in a factory.
    tgba_bdd_concrete_factory fact(dict);
    eltl_trad_visitor v(fact, true);
Damien Lefortier's avatar
Damien Lefortier committed
316
    f2->accept(v);
317
    f2->destroy();
318
319
320
321
322
323
    fact.finish();

    // Finally setup the resulting automaton.
    return new tgba_bdd_concrete(fact, v.result());
  }
}