eltl2tgba_lacim.cc 7.53 KB
Newer Older
1
2
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
// 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
	  case unop::Star:
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
	    assert(!"unsupported operator");
	  }
	/* Unreachable code.  */
	assert(0);
      }

      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:
130
131
	  case binop::W:
	  case binop::M:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132
133
	  case binop::UConcat:
	  case binop::EConcat:
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
	    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;
160
161
	  case multop::Concat:
	    assert(!"unsupported operator");
162
163
164
165
	  }
	assert(op != -1);
	unsigned s = node->size();
	for (unsigned n = 0; n < s; ++n)
166
	  res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
167
168
169
      }

      void
170
      visit(const automatop* node)
171
172
      {
	nmap m;
173
	bdd finish = bddfalse;
174
	bdd acc = bddtrue;
175
176
177
178
179

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

180
	std::pair<int, int> vp =
181
182
	  recurse_state(node->get_nfa(),
			node->get_nfa()->get_init_state(), v, m, acc, finish);
183
184
185

	// Update finish_ with finish(node).
	// FIXME: when node is loop, it does not make sense; hence the bddtrue.
186
	finish_[node] = !node->get_nfa()->is_loop() ? bddtrue : finish;
187
188
189
190
191
192
193

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

194
195
196
	fact_.declare_acceptance_condition(acc, node);
	res_ = node->is_negated() ?
	  bdd_nithvar(vp.first) : bdd_ithvar(vp.first);
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
      }

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

212
213
214
215
216
217
      /// 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_;

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

281
282
283
284
285
286
287
288
289
290
291
292
293
294
	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);
295
    f1->destroy();
296
297
298
299

    // 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
300
    f2->accept(v);
301
    f2->destroy();
302
303
304
305
306
307
    fact.finish();

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