hoa.cc 8.3 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
	: state_acc(true), is_complete(true), is_deterministic(true)
      {
	number_all_states_and_fill_sup(aut);
	number_all_ap();
      }

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

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

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

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

182
	for (auto& i: sup)
183
	  {
184
	    bdd cond = i.first;
185
186
	    if (cond == bddtrue)
	      {
187
		i.second = "t";
188
189
190
191
		continue;
	      }
	    if (cond == bddfalse)
	      {
192
		i.second = "f";
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
		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;
	      }
225
	    i.second = s.str();
226
227
228
229
230
231
232
233
234
	  }
      }

    };

  }


  std::ostream&
235
236
237
238
239
240
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
		const ltl::formula* f,
		hoa_acceptance acceptance,
		hoa_alias alias,
		bool newline)
241
242
243
244
245
  {
    (void) alias;

    metadata md(aut);

246
    if (acceptance == Hoa_Acceptance_States && !md.state_acc)
247
      acceptance = Hoa_Acceptance_Transitions;
248
249
250
251
252

    unsigned num_states = md.nm.size();

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

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

	os << "State: " << i;
312
	if (this_acc == Hoa_Acceptance_States && !j->done())
313
	  md.emit_acc(os, aut, j->current_acceptance_conditions());
314
315
316
317
318
319
	os << nl;

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

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

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

}