lbtt.cc 8.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
// Copyright (C) 2003, 2004, 2005 Laboratoire 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 "lbtt.hh"
24
25
#include <map>
#include <string>
26
#include <ostream>
27
28
#include <memory>
#include "tgba/formula2bdd.hh"
29
#include "reachiter.hh"
30
#include "misc/bddlt.hh"
31
#include "priv/accmap.hh"
32
#include "ltlvisit/lbt.hh"
33
#include "ltlparse/public.hh"
34
35
36

namespace spot
{
37
  namespace
38
  {
39
40
    // At some point we'll need to print an acceptance set into LBTT's
    // format.  LBTT expects numbered acceptance sets, so first we'll
41
    // number each acceptance condition, and later when we have to print
42
43
    // them we'll just have to look up each of them.
    class acceptance_cond_splitter
44
    {
45
46
    public:
      acceptance_cond_splitter(bdd all_acc)
47
      {
48
49
	unsigned count = 0;
	while (all_acc != bddfalse)
50
	  {
51
52
53
	    bdd acc = bdd_satone(all_acc);
	    all_acc -= acc;
	    sm[acc] = count++;
54
	  }
55
56
57
58
59
60
      }

      std::ostream&
      split(std::ostream& os, bdd b)
      {
	while (b != bddfalse)
61
	  {
62
63
	    bdd acc = bdd_satone(b);
	    b -= acc;
64
	    os << sm[acc] << ' ';
65
	  }
66
	return os;
67
68
      }

69
70
71
72
    private:
      typedef std::map<bdd, unsigned, bdd_less_than> split_map;
      split_map sm;
    };
73

74
    class lbtt_bfs : public tgba_reachable_iterator_breadth_first
75
    {
76
    public:
77
      lbtt_bfs(const tgba* a, std::ostream& os, bool sba_format)
78
79
	: tgba_reachable_iterator_breadth_first(a),
	  os_(os),
80
81
82
	  all_acc_conds_(a->all_acceptance_conditions()),
	  acs_(all_acc_conds_),
	  sba_format_(sba_format),
83
84
85
86
	  // Check if the automaton can be converted into a
	  // tgba_digraph. This makes the state_is_accepting()
	  // function more efficient.
	  sba_(dynamic_cast<const tgba_digraph*>(a))
87
      {
88
89
	if (sba_ && !sba_->get_bprop(tgba_digraph::SBA))
	  sba_ = nullptr;
90
91
92
93
      }

      bool
      state_is_accepting(const state *s) const
94
      {
95
96
97
98
99
100
101
102
103
104
105
106
	// If the automaton has a SBA type, it's easier to just query the
	// state_is_accepting() method.
	if (sba_)
	  return sba_->state_is_accepting(s);

	// Otherwise, since we are dealing with a degeneralized
	// automaton nonetheless, the transitions leaving an accepting
	// state are either all accepting, or all non-accepting.  So
	// we just check the acceptance of the first transition.  This
	// is not terribly efficient since we have to create the
	// iterator.
	tgba_succ_iterator* it = aut_->succ_iter(s);
107
108
	bool accepting = it->first()
	  && it->current_acceptance_conditions() == all_acc_conds_;
109
	aut_->release_iter(it);
110
	return accepting;
111
112
      }

113

114
      void
115
      process_state(const state* s, int n, tgba_succ_iterator*)
116
117
118
      {
	--n;
	if (n == 0)
119
	  body_ << "0 1";
120
	else
121
122
123
124
125
126
127
128
129
130
131
	  body_ << "-1\n" << n << " 0";
	// Do we have state-based acceptance?
	if (sba_format_)
	  {
	    // We support only one acceptance condition in the
	    // state-based format.
	    if (state_is_accepting(s))
	      body_ << " 0 -1";
	    else
	      body_ << " -1";
	  }
132
	body_ << '\n';
133
      }
134

135
      void
136
137
      process_link(const state*, int,
		   const state*, int out, const tgba_succ_iterator* si)
138
      {
139
	body_ << out - 1 << ' ';
140
141
142
143
144
145
146
147
148
	if (!sba_format_)
	  {
	    acs_.split(body_, si->current_acceptance_conditions());
	    body_ << "-1 ";
	  }
	const ltl::formula* f = bdd_to_formula(si->current_condition(),
					       aut_->get_dict());
	to_lbt_string(f, body_);
	f->destroy();
149
	body_ << '\n';
150
      }
151

152
153
154
      void
      end()
      {
155
	os_ << seen.size() << ' ';
156
	if (sba_format_)
157
	  os_ << '1';
158
	else
159
160
	  os_ << aut_->number_of_acceptance_conditions() << 't';
	os_ << '\n' << body_.str() << "-1" << std::endl;
161
162
163
164
165
      }

    private:
      std::ostream& os_;
      std::ostringstream body_;
166
      bdd all_acc_conds_;
167
      acceptance_cond_splitter acs_;
168
      bool sba_format_;
169
      const tgba_digraph* sba_;
170
171
    };

172
173
174
175
176
177
178
179
180
    static
    const tgba_digraph*
    lbtt_read_tgba(unsigned num_states, unsigned num_acc,
		   std::istream& is, std::string& error,
		   bdd_dict* dict,
		   ltl::environment& env, ltl::environment& envacc)
    {
      auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
      acc_mapper_int acc_b(aut.get(), num_acc, envacc);
181
      aut->new_states(num_states);
182
183
184
185
186
187
188
189
190
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
223
224
225
226
227
228
229
230
231

      for (unsigned n = 0; n < num_states; ++n)
	{
	  int src_state = 0;
	  int initial = 0;
	  is >> src_state >> initial;
	  if (initial)
	    aut->set_init_state(src_state);

	  // Read the transitions.
	  for (;;)
	    {
	      int dst_state = 0;
	      is >> dst_state;
	      if (dst_state == -1)
		break;

	      // Read the acceptance conditions.
	      bdd acc = bddfalse;
	      for (;;)
		{
		  int acc_n = 0;
		  is >> acc_n;
		  if (acc_n == -1)
		    break;
		  auto p = acc_b.lookup(acc_n);
		  if (p.first)
		    {
		      acc |= p.second;
		    }
		  else
		    {
		      error += "more acceptance sets used than declared";
		      return nullptr;
		    }
		}

	      std::string guard;
	      std::getline(is, guard);
	      ltl::parse_error_list pel;
	      const ltl::formula* f = parse_lbt(guard, pel, env);
	      if (!f || !pel.empty())
		{
		  error += "failed to parse guard: " + guard;
		  if (f)
		    f->destroy();
		  return nullptr;
		}
	      bdd cond = formula_to_bdd(f, dict, aut.get());
	      f->destroy();
232
	      aut->new_transition(src_state, dst_state, cond, acc);
233
234
235
236
237
238
239
240
241
242
243
244
245
	    }
	}
      return aut.release();
    }

    const tgba_digraph*
    lbtt_read_gba(unsigned num_states, unsigned num_acc,
		  std::istream& is, std::string& error,
		  bdd_dict* dict,
		  ltl::environment& env, ltl::environment& envacc)
    {
      auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
      acc_mapper_int acc_b(aut.get(), num_acc, envacc);
246
      aut->new_states(num_states);
247
      aut->set_bprop(tgba_digraph::StateBasedAcc);
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297

      for (unsigned n = 0; n < num_states; ++n)
	{
	  int src_state = 0;
	  int initial = 0;
	  is >> src_state >> initial;
	  if (initial)
	    aut->set_init_state(src_state);

	  // Read the acceptance conditions.
	  bdd acc = bddfalse;
	  for (;;)
	    {
	      int acc_n = 0;
	      is >> acc_n;
	      if (acc_n == -1)
		break;
	      auto p = acc_b.lookup(acc_n);
	      if (p.first)
		{
		  acc |= p.second;
		}
	      else
		{
		  error += "more acceptance sets used than declared";
		  return nullptr;
		}
	    }

	  // Read the transitions.
	  for (;;)
	    {
	      int dst_state = 0;
	      is >> dst_state;
	      if (dst_state == -1)
		break;

	      std::string guard;
	      std::getline(is, guard);
	      ltl::parse_error_list pel;
	      const ltl::formula* f = parse_lbt(guard, pel, env);
	      if (!f || !pel.empty())
		{
		  error += "failed to parse guard: " + guard;
		  if (f)
		    f->destroy();
		  return nullptr;
		}
	      bdd cond = formula_to_bdd(f, dict, aut.get());
	      f->destroy();
298
	      aut->new_transition(src_state, dst_state, cond, acc);
299
300
301
302
303
	    }
	}
      return aut.release();
    }

304
  } // anonymous
305

306

307
  std::ostream&
308
  lbtt_reachable(std::ostream& os, const tgba* g, bool sba)
309
  {
310
    lbtt_bfs b(g, os, sba);
311
312
313
    b.run();
    return os;
  }
314

315

316
  const tgba_digraph*
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
  lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict,
	     ltl::environment& env, ltl::environment& envacc)
  {
    is >> std::skipws;

    unsigned num_states = 0;
    is >> num_states;
    if (!is)
      {
	error += "failed to read the number of states";
	return 0;
      }

    // No states?  Read the rest of the line and return an empty automaton.
    if (num_states == 0)
      {
	std::string header;
	std::getline(is, header);
335
	return new tgba_digraph(dict);
336
337
338
339
      }

    unsigned num_acc = 0;
    is >> num_acc;
340
341
342
343
344
345
346

    int type;
    type = is.peek();
    if (type == 't' || type == 'T' || type == 's' || type == 'S')
      type = is.get();

    if (type == 't' || type == 'T')
347
348
349
      return lbtt_read_tgba(num_states, num_acc, is, error, dict,
			    env, envacc);
    else
350
351
      return lbtt_read_gba(num_states, num_acc, is, error, dict,
			   env, envacc);
352
  }
353
}