eltl2tgba_lacim.cc 7.77 KB
Newer Older
1
// Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et
2
// Dveloppement de l'Epita (LRDE).
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
//
// 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.

#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
23
#include "ltlast/formula_tree.hh"
24
25
26
27
28
29
30
31
32
33
34
35
36
37
#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.
Damien Lefortier's avatar
Damien Lefortier committed
38
    class eltl_trad_visitor : public const_visitor
39
40
41
    {
    public:
      eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
42
	  : fact_(fact), root_(root), finish_()
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
73
      {
      }

      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;
74
75
	  case constant::EmptyWord:
	    assert(!"unsupported operator");
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
	  }
	/* Unreachable code.  */
	assert(0);
      }

      void
      visit(const unop* node)
      {
	switch (node->op())
	  {
	  case unop::Not:
	    {
	      res_ = bdd_not(recurse(node->child()));
	      return;
	    }
91
92
93
94
	  case unop::Finish:
	    {
	      // Ensure finish_[node->child()] has been computed if
	      // node->child() is an automaton operator.
95
	      res_ = recurse(node->child());
96
	      finish_map_::const_iterator it = finish_.find(node->child());
97
	      if (it != finish_.end())
98
99
100
		res_ = finish_[node->child()];
	      return;
	    }
101
102
103
	  case unop::X:
	  case unop::F:
          case unop::G:
104
105
	  case unop::Closure:
	  case unop::NegClosure:
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
189
190
191

	std::vector<formula*> v;
	for (unsigned i = 0; i < node->size(); ++i)
	  v.push_back(const_cast<formula*>(node->nth(i)));

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
	finish_[node] = !node->get_nfa()->is_loop() ? bddtrue : finish;
199
200
201
202
203
204
205

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

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

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

224
225
226
227
228
229
      /// BDD associated to each automatop A representing finish(A).
      typedef Sgi::hash_map<const ltl::formula*, bdd,
			    ltl::formula_ptr_hash> finish_map_;

      finish_map_ finish_;

230
231
232
233
234
235
      // Table containing the two now variables associated with each state.
      // TODO: a little documentation about that.
      typedef Sgi::hash_map<
	const nfa::state*, std::pair<int, int>, ptr_hash<nfa::state> > nmap;

      std::pair<int, int>&
236
237
238
      recurse_state(const nfa::ptr& nfa, const nfa::state* s,
		    const std::vector<formula*>& v,
		    nmap& m, bdd& acc, bdd& finish)
239
      {
240
	bool is_loop = nfa->is_loop();
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
	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;
257
	bdd tmpacc = bddfalse;
258
259
	for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i)
	{
260
261
	  const formula* lbl = formula_tree::instanciate((*i)->lbl, v);
	  bdd f = recurse(lbl);
262
	  lbl->destroy();
263
264
265
266
267
	  if (nfa->is_final((*i)->dst))
	  {
	    tmp1 |= f;
	    tmp2 |= f;
	    tmpacc |= f;
268
	    finish |= bdd_ithvar(v1) & f;
269
270
271
	  }
	  else
	  {
272
273
	    std::pair<int, int> vp =
	      recurse_state(nfa, (*i)->dst, v, m, acc, finish);
274
275
	    tmp1 |= (f & bdd_ithvar(vp.first + 1));
	    tmp2 |= (f & bdd_ithvar(vp.second + 1));
276
277
	    if (is_loop)
	      tmpacc |= f;
278
279
280
	  }
	}
	fact_.constrain_relation(bdd_apply(bdd_ithvar(v1), tmp1, bddop_biimp));
281
282
283
	if (is_loop)
	{
	  acc &= bdd_ithvar(v2) | !tmpacc;
284
285
	  fact_.constrain_relation(
	    bdd_apply(bdd_ithvar(v2), tmp2, bddop_invimp));
286
287
288
289
	}
	else
	{
	  acc &= bdd_nithvar(v2) | tmpacc;
290
	  fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp));
291
292
	}

293
294
295
296
297
298
299
300
301
302
303
304
305
306
	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);
307
    f1->destroy();
308
309
310
311

    // 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
312
    f2->accept(v);
313
    f2->destroy();
314
315
316
317
318
319
    fact.finish();

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