hoa.cc 8.27 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et
// 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
33
#include "reachiter.hh"
#include "misc/escape.hh"
#include "misc/bddlt.hh"
#include "misc/minato.hh"
#include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh"
34
#include "ltlast/atomic_prop.hh"
35
36
37
38
39
40
41
42
43
44
45
46
47
48

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.
49
50
      typedef std::unordered_map<const state*, unsigned,
				 state_ptr_hash, state_ptr_equal> state_map;
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
      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;

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

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

95
      void number_all_states_and_fill_sup(const const_tgba_ptr& aut)
96
97
98
99
100
101
102
103
104
105
106
107
108
      {
	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())
	  {
109
	    auto src = todo.front();
110
	    todo.pop_front();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
111
112
	    bool notfirst = false;
	    acc_cond::mark_t prev = 0U;
113
114
115
	    bool st_acc = true;
	    bdd sum = bddfalse;
	    bdd available = bddtrue;
116
	    for (auto i: aut->succ(src))
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
	      {
		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)
		  {
141
		    acc_cond::mark_t acc = i->current_acceptance_conditions();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142
143
144
145
		    if (notfirst && prev != acc)
		      {
			st_acc = false;
		      }
146
		    else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
147
148
149
150
		      {
			notfirst = true;
			prev = acc;
		      }
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
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
		  }
	      }
	    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;
	for (i = sup.begin(); i != sup.end(); ++i)
	  all &= bdd_support(i->first);

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

	for (i = sup.begin(); i != sup.end(); ++i)
	  {
	    bdd cond = i->first;
	    if (cond == bddtrue)
	      {
		i->second = "t";
		continue;
	      }
	    if (cond == bddfalse)
	      {
		i->second = "f";
		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;
	      }
	    i->second = s.str();
	  }
      }

    };

  }


  std::ostream&
229
230
231
232
233
234
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
		const ltl::formula* f,
		hoa_acceptance acceptance,
		hoa_alias alias,
		bool newline)
235
236
237
238
239
  {
    (void) alias;

    metadata md(aut);

240
    if (acceptance == Hoa_Acceptance_States
241
	&& !md.state_acc)
242
      acceptance = Hoa_Acceptance_Transitions;
243
244
245
246
247
248
249
250
251
252

    unsigned num_states = md.nm.size();

    const char nl = newline ? '\n' : ' ';
    os << "HOA: v1" << nl;
    if (f)
      escape_str(os << "name: \"", to_string(f)) << '"' << nl;
    os << "States: " << num_states << nl
       << "Start: 0" << nl
       << "AP: " << md.vap.size();
253
    auto d = aut->get_dict();
254
255
    for (metadata::vap_t::const_iterator i = md.vap.begin();
	 i != md.vap.end(); ++i)
256
257
258
259
260
      {
	auto f = ltl::is_atomic_prop(d->bdd_map[*i].f);
	assert(f);
	escape_str(os << " \"", f->name()) << '"';
      }
261
    os << nl;
262
    unsigned num_acc = aut->acc().num_sets();
263
264
265
266
267
268
269
270
271
272
    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)
      {
273
	os << " Inf(0";
274
	for (unsigned i = 1; i < num_acc; ++i)
275
	  os << ")&Inf(" << i;
276
277
278
279
280
281
282
283
	os << ')';
      }
    else
      {
	os  << " t";
      }
    os << nl;
    os << "properties: trans-labels explicit-labels";
284
    if (acceptance == Hoa_Acceptance_States)
285
      os << " state-acc";
286
    else if (acceptance == Hoa_Acceptance_Transitions)
287
288
289
290
291
292
293
294
295
      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)
      {
296
297
	hoa_acceptance this_acc = acceptance;
	if (this_acc == Hoa_Acceptance_Mixed)
298
	  this_acc = (md.common_acc[i] ?
299
		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
300
301
302
303
304

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

	os << "State: " << i;
305
	if (this_acc == Hoa_Acceptance_States && !j->done())
306
	  md.emit_acc(os, aut, j->current_acceptance_conditions());
307
308
309
310
311
312
	os << nl;

	for (; !j->done(); j->next())
	  {
	    const state* dst = j->current_state();
	    os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst];
313
	    if (this_acc == Hoa_Acceptance_Transitions)
314
	      md.emit_acc(os, aut, j->current_acceptance_conditions());
315
316
317
	    os << nl;
	    dst->destroy();
	  }
318
	aut->release_iter(j);
319
320
321
322
323
324
325
326
      }
    os << "--END--";		// No newline.  Let the caller decide.
    for (unsigned i = 0; i < num_states; ++i)
      md.nm[i]->destroy();
    return os;
  }

  std::ostream&
327
328
329
330
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
		const char* opt,
		const ltl::formula* f)
331
332
  {
    bool newline = true;
333
334
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    hoa_alias alias = Hoa_Alias_None;
335
336
337
338
339
340
341
342
343
344

    if (opt)
      while (*opt)
	{
	  switch (*opt++)
	    {
	    case 'l':
	      newline = false;
	      break;
	    case 'm':
345
	      acceptance = Hoa_Acceptance_Mixed;
346
347
	      break;
	    case 's':
348
	      acceptance = Hoa_Acceptance_States;
349
350
	      break;
	    case 't':
351
	      acceptance = Hoa_Acceptance_Transitions;
352
353
354
	      break;
	    }
	}
355
    return hoa_reachable(os, aut, f, acceptance, alias, newline);
356
357
358
  }

}