eltl2tgba_lacim.cc 7.7 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
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
// (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
17
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
19
20

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

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

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

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

      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:
136
137
	  case binop::W:
	  case binop::M:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
138
139
	  case binop::UConcat:
	  case binop::EConcat:
140
	  case binop::EConcatMarked:
141
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
	    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;
167
	  case multop::Concat:
168
	  case multop::Fusion:
169
	  case multop::AndNLM:
170
171
	  case multop::AndRat:
	  case multop::OrRat:
172
	    assert(!"unsupported operator");
173
174
175
176
	  }
	assert(op != -1);
	unsigned s = node->size();
	for (unsigned n = 0; n < s; ++n)
177
	  res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
178
179
180
      }

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

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

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

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

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

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

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

223
224
225
226
227
228
      /// 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_;

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

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

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

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