hoa.cc 8.51 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
// Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

#include <ostream>
#include <sstream>
#include <map>
#include "tgba/tgba.hh"
27
#include "hoa.hh"
28
29
30
31
32
#include "reachiter.hh"
#include "misc/escape.hh"
#include "misc/bddlt.hh"
#include "misc/minato.hh"
#include "tgba/formula2bdd.hh"
33
#include "ltlast/atomic_prop.hh"
34
35
36
37
38
39
40
41
42
43
44
45
46
47

namespace spot
{
  namespace
  {
    struct metadata
    {
      // Assign a number to each atomic proposition.
      typedef std::map<int, unsigned> ap_map;
      ap_map ap;
      typedef std::vector<int> vap_t;
      vap_t vap;

      // Map each state to a number.
48
49
      typedef std::unordered_map<const state*, unsigned,
				 state_ptr_hash, state_ptr_equal> state_map;
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
      state_map sm;
      // Map each number to its states.
      typedef std::vector<const state*> number_map;
      number_map nm;

      std::vector<bool> common_acc;
      bool state_acc;
      bool is_complete;
      bool is_deterministic;

      // Label support: the set of all conditions occurring in the
      // automaton.
      typedef std::map<bdd, std::string, bdd_less_than> sup_map;
      sup_map sup;

65
      metadata(const const_tgba_ptr& aut)
66
67
68
69
70
71
	: state_acc(true), is_complete(true), is_deterministic(true)
      {
	number_all_states_and_fill_sup(aut);
	number_all_ap();
      }

72
73
74
75
76
77
      ~metadata()
      {
	for (auto s: nm)
	  s->destroy();
      }

78
      std::ostream&
79
80
81
      emit_acc(std::ostream& os,
	       const const_tgba_ptr& aut,
	       acc_cond::mark_t b)
82
83
      {
	// FIXME: We could use a cache for this.
84
	if (b == 0U)
85
86
87
	  return os;
	os << " {";
	bool notfirst = false;
88
	for (auto v: aut->acc().sets(b))
89
90
91
92
93
	  {
	    if (notfirst)
	      os << ' ';
	    else
	      notfirst = true;
94
	    os << v;
95
96
97
98
99
	  }
	os << '}';
	return os;
      }

100
      void number_all_states_and_fill_sup(const const_tgba_ptr& aut)
101
102
103
104
105
106
107
108
109
110
111
112
113
      {
	std::string empty;

	// Scan the whole automaton to number states.
	std::deque<const state*> todo;

	const state* init = aut->get_init_state();
	sm[init] = 0;
	nm.push_back(init);
	todo.push_back(init);

	while (!todo.empty())
	  {
114
	    auto src = todo.front();
115
	    todo.pop_front();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
117
	    bool notfirst = false;
	    acc_cond::mark_t prev = 0U;
118
119
120
	    bool st_acc = true;
	    bdd sum = bddfalse;
	    bdd available = bddtrue;
121
	    for (auto i: aut->succ(src))
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
	      {
		const state* dst = i->current_state();
		bdd cond = i->current_condition();
		if (is_complete)
		  sum |= cond;
		if (is_deterministic)
		  {
		    if (!bdd_implies(cond, available))
		      is_deterministic = false;
		    else
		      available -= cond;
		  }
		sup.insert(std::make_pair(cond, empty));
		if (sm.insert(std::make_pair(dst, nm.size())).second)
		  {
		    nm.push_back(dst);
		    todo.push_back(dst);
		  }
		else
		  {
		    dst->destroy();
		  }
		if (st_acc)
		  {
146
		    acc_cond::mark_t acc = i->current_acceptance_conditions();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
147
148
149
150
		    if (notfirst && prev != acc)
		      {
			st_acc = false;
		      }
151
		    else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
153
154
155
		      {
			notfirst = true;
			prev = acc;
		      }
156
157
158
159
160
161
162
163
164
165
166
167
168
169
		  }
	      }
	    if (is_complete)
	      is_complete &= sum == bddtrue;

	    common_acc.push_back(st_acc);
	    state_acc &= st_acc;
	  }
      }

      void number_all_ap()
      {
	sup_map::iterator i;
	bdd all = bddtrue;
170
171
	for (auto& i: sup)
	  all &= bdd_support(i.first);
172
173
174
175
176
177
178
179
180

	while (all != bddtrue)
	  {
	    int v = bdd_var(all);
	    all = bdd_high(all);
	    ap.insert(std::make_pair(v, vap.size()));
	    vap.push_back(v);
	  }

181
	for (auto& i: sup)
182
	  {
183
	    bdd cond = i.first;
184
185
	    if (cond == bddtrue)
	      {
186
		i.second = "t";
187
188
189
190
		continue;
	      }
	    if (cond == bddfalse)
	      {
191
		i.second = "f";
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
		continue;
	      }
	    std::ostringstream s;
	    bool notfirstor = false;

	    minato_isop isop(cond);
	    bdd cube;
	    while ((cube = isop.next()) != bddfalse)
	      {
		if (notfirstor)
		  s << " | ";
		bool notfirstand = false;
		while (cube != bddtrue)
		  {
		    if (notfirstand)
		      s << '&';
		    else
		      notfirstand = true;
		    bdd h = bdd_high(cube);
		    if (h == bddfalse)
		      {
			s << '!' << ap[bdd_var(cube)];
			cube = bdd_low(cube);
		      }
		    else
		      {
			s << ap[bdd_var(cube)];
			cube = h;
		      }
		  }
		notfirstor = true;
	      }
224
	    i.second = s.str();
225
226
227
228
229
230
231
	  }
      }

    };

  }

232
233
234
235
236
237
238
239
240
241
  enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
  enum hoa_acceptance
    {
      Hoa_Acceptance_States,	/// state-based acceptance if
				/// (globally) possible
				/// transition-based acceptance
				/// otherwise.
      Hoa_Acceptance_Transitions, /// transition-based acceptance globally
      Hoa_Acceptance_Mixed    /// mix state-based and transition-based
    };
242
243

  std::ostream&
244
245
246
247
248
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
		hoa_acceptance acceptance,
		hoa_alias alias,
		bool newline)
249
250
251
252
253
  {
    (void) alias;

    metadata md(aut);

254
    if (acceptance == Hoa_Acceptance_States && !md.state_acc)
255
      acceptance = Hoa_Acceptance_Transitions;
256
257
258
259
260

    unsigned num_states = md.nm.size();

    const char nl = newline ? '\n' : ' ';
    os << "HOA: v1" << nl;
261
    auto n = aut->get_named_prop<std::string>("automaton-name");
262
    if (n)
263
      escape_str(os << "name: \"", *n) << '"' << nl;
264
265
266
    os << "States: " << num_states << nl
       << "Start: 0" << nl
       << "AP: " << md.vap.size();
267
    auto d = aut->get_dict();
268
    for (auto& i: md.vap)
269
      {
270
	auto f = ltl::is_atomic_prop(d->bdd_map[i].f);
271
272
273
	assert(f);
	escape_str(os << " \"", f->name()) << '"';
      }
274
    os << nl;
275
    unsigned num_acc = aut->acc().num_sets();
276
277
278
279
280
281
282
283
284
285
    if (num_acc == 0)
      os << "acc-name: all";
    else if (num_acc == 1)
      os << "acc-name: Buchi";
    else
      os << "acc-name: generalized-Buchi " << num_acc;
    os << nl;
    os << "Acceptance: " << num_acc;
    if (num_acc > 0)
      {
286
	os << " Inf(0";
287
	for (unsigned i = 1; i < num_acc; ++i)
288
	  os << ")&Inf(" << i;
289
290
291
292
293
294
295
296
	os << ')';
      }
    else
      {
	os  << " t";
      }
    os << nl;
    os << "properties: trans-labels explicit-labels";
297
    if (acceptance == Hoa_Acceptance_States)
298
      os << " state-acc";
299
    else if (acceptance == Hoa_Acceptance_Transitions)
300
301
302
303
304
305
306
307
308
      os << " trans-acc";
    if (md.is_complete)
      os << " complete";
    if (md.is_deterministic)
      os << " deterministic";
    os << nl;
    os << "--BODY--" << nl;
    for (unsigned i = 0; i < num_states; ++i)
      {
309
310
	hoa_acceptance this_acc = acceptance;
	if (this_acc == Hoa_Acceptance_Mixed)
311
	  this_acc = (md.common_acc[i] ?
312
		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
313
314
315
316
317

	tgba_succ_iterator* j = aut->succ_iter(md.nm[i]);
	j->first();

	os << "State: " << i;
318
	if (this_acc == Hoa_Acceptance_States && !j->done())
319
	  md.emit_acc(os, aut, j->current_acceptance_conditions());
320
321
322
323
324
325
	os << nl;

	for (; !j->done(); j->next())
	  {
	    const state* dst = j->current_state();
	    os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst];
326
	    if (this_acc == Hoa_Acceptance_Transitions)
327
	      md.emit_acc(os, aut, j->current_acceptance_conditions());
328
329
330
	    os << nl;
	    dst->destroy();
	  }
331
	aut->release_iter(j);
332
333
334
335
336
337
      }
    os << "--END--";		// No newline.  Let the caller decide.
    return os;
  }

  std::ostream&
338
339
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
340
		const char* opt)
341
342
  {
    bool newline = true;
343
344
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    hoa_alias alias = Hoa_Alias_None;
345
346
347
348
349
350
351
352
353
354

    if (opt)
      while (*opt)
	{
	  switch (*opt++)
	    {
	    case 'l':
	      newline = false;
	      break;
	    case 'm':
355
	      acceptance = Hoa_Acceptance_Mixed;
356
357
	      break;
	    case 's':
358
	      acceptance = Hoa_Acceptance_States;
359
360
	      break;
	    case 't':
361
	      acceptance = Hoa_Acceptance_Transitions;
362
363
364
	      break;
	    }
	}
365
    return hoa_reachable(os, aut, acceptance, alias, newline);
366
367
368
  }

}