hoa.cc 8.15 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
253
254
255
256
257

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

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

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

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

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

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

}