hoa.cc 9.72 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 "tgba/tgbagraph.hh"
28
#include "hoa.hh"
29
30
31
32
33
#include "reachiter.hh"
#include "misc/escape.hh"
#include "misc/bddlt.hh"
#include "misc/minato.hh"
#include "tgba/formula2bdd.hh"
34
#include "ltlast/atomic_prop.hh"
35
36
37
38
39

namespace spot
{
  namespace
  {
40
    struct metadata final
41
42
43
44
45
46
47
48
    {
      // 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;

      std::vector<bool> common_acc;
49
      bool has_state_acc;
50
51
      bool is_complete;
      bool is_deterministic;
52
53
      bool use_implicit_labels;
      bdd all_ap;
54
55
56
57
58
59

      // 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;

60
      metadata(const const_tgba_digraph_ptr& aut, bool implicit)
61
      {
62
	check_det_and_comp(aut);
63
	use_implicit_labels = implicit && is_deterministic && is_complete;
64
65
66
67
	number_all_ap();
      }

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

89
      void check_det_and_comp(const const_tgba_digraph_ptr& aut)
90
91
92
      {
	std::string empty;

93
94
95
96
97
	unsigned ns = aut->num_states();
	bool deterministic = true;
	bool complete = true;
	bool state_acc = true;
	for (unsigned src = 0; src < ns; ++src)
98
99
100
	  {
	    bdd sum = bddfalse;
	    bdd available = bddtrue;
101
102
103
104
	    bool st_acc = true;
	    bool notfirst = false;
	    acc_cond::mark_t prev = 0U;
	    for (auto& t: aut->out(src))
105
	      {
106
107
108
		if (complete)
		  sum |= t.cond;
		if (deterministic)
109
		  {
110
111
		    if (!bdd_implies(t.cond, available))
		      deterministic = false;
112
		    else
113
		      available -= t.cond;
114
		  }
115
		sup.insert(std::make_pair(t.cond, empty));
116
117
		if (st_acc)
		  {
118
		    if (notfirst && prev != t.acc)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
120
121
		      {
			st_acc = false;
		      }
122
		    else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
123
124
		      {
			notfirst = true;
125
			prev = t.acc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
		      }
127
128
		  }
	      }
129
130
	    if (complete)
	      complete &= sum == bddtrue;
131
132
133
	    common_acc.push_back(st_acc);
	    state_acc &= st_acc;
	  }
134
135
136
	is_deterministic = deterministic;
	is_complete = complete;
	has_state_acc = state_acc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
137
138
139
140
141

	// If the automaton declares that it is deterministic or
	// state-based, make sure that it really is.
	assert(!aut->is_deterministic() || deterministic);
	assert(!aut->has_state_based_acc() || state_acc);
142
143
144
145
146
147
      }

      void number_all_ap()
      {
	sup_map::iterator i;
	bdd all = bddtrue;
148
149
	for (auto& i: sup)
	  all &= bdd_support(i.first);
150
	all_ap = all;
151
152
153
154
155
156
157
158
159

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

160
161
162
	if (use_implicit_labels)
	  return;

163
	for (auto& i: sup)
164
	  {
165
	    bdd cond = i.first;
166
167
	    if (cond == bddtrue)
	      {
168
		i.second = "t";
169
170
171
172
		continue;
	      }
	    if (cond == bddfalse)
	      {
173
		i.second = "f";
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
		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;
	      }
206
	    i.second = s.str();
207
208
209
210
211
212
	  }
      }
    };

  }

213
214
215
216
217
218
219
220
221
  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
    };
222

223
  static std::ostream&
224
  hoa_reachable(std::ostream& os,
225
		const const_tgba_digraph_ptr& aut,
226
		const char* opt)
227
  {
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
    bool newline = true;
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    bool implicit_labels = false;

    if (opt)
      while (*opt)
	{
	  switch (*opt++)
	    {
	    case 'i':
	      implicit_labels = true;
	      break;
	    case 'l':
	      newline = false;
	      break;
	    case 'm':
	      acceptance = Hoa_Acceptance_Mixed;
	      break;
	    case 's':
	      acceptance = Hoa_Acceptance_States;
	      break;
	    case 't':
	      acceptance = Hoa_Acceptance_Transitions;
	      break;
	    }
	}
254

255
256
257
258
    // Calling get_init_state_number() may add a state to empty
    // automata, so it has to be done first.
    unsigned init = aut->get_init_state_number();

259
    metadata md(aut, implicit_labels);
260

261
    if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
262
      acceptance = Hoa_Acceptance_Transitions;
263

264
    unsigned num_states = aut->num_states();
265
266
267

    const char nl = newline ? '\n' : ' ';
    os << "HOA: v1" << nl;
268
    auto n = aut->get_named_prop<std::string>("automaton-name");
269
    if (n)
270
      escape_str(os << "name: \"", *n) << '"' << nl;
271
    unsigned nap = md.vap.size();
272
    os << "States: " << num_states << nl
273
       << "Start: " << init << nl
274
       << "AP: " << nap;
275
    auto d = aut->get_dict();
276
    for (auto& i: md.vap)
277
      {
278
	auto f = ltl::is_atomic_prop(d->bdd_map[i].f);
279
280
281
	assert(f);
	escape_str(os << " \"", f->name()) << '"';
      }
282
    os << nl;
283

284
    unsigned num_acc = aut->acc().num_sets();
285
    if (aut->acc().is_generalized_buchi())
286
      {
287
	if (aut->acc().is_true())
288
	  os << "acc-name: all";
289
	else if (aut->acc().is_buchi())
290
291
292
293
	  os << "acc-name: Buchi";
	else
	  os << "acc-name: generalized-Buchi " << num_acc;
	os << nl;
294
      }
295
296
    os << "Acceptance: " << num_acc << ' ';
    os << aut->acc().get_acceptance();
297
    os << nl;
298
299
300
301
302
303
    os << "properties:";
    implicit_labels = md.use_implicit_labels;
    if (implicit_labels)
      os << " implicit-labels";
    else
      os << " trans-labels explicit-labels";
304
    if (acceptance == Hoa_Acceptance_States)
305
      os << " state-acc";
306
    else if (acceptance == Hoa_Acceptance_Transitions)
307
308
309
310
311
312
      os << " trans-acc";
    if (md.is_complete)
      os << " complete";
    if (md.is_deterministic)
      os << " deterministic";
    os << nl;
313
314
315
316
317
318
319
320
321
322
323
324

    // If we want to output implicit labels, we have to
    // fill a vector with all destinations in order.
    std::vector<unsigned> out;
    std::vector<acc_cond::mark_t> outm;
    if (implicit_labels)
      {
	out.resize(1UL << nap);
	if (acceptance != Hoa_Acceptance_States)
	  outm.resize(1UL << nap);
      }

325
    os << "--BODY--" << nl;
326
    auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
327
328
    for (unsigned i = 0; i < num_states; ++i)
      {
329
330
	hoa_acceptance this_acc = acceptance;
	if (this_acc == Hoa_Acceptance_Mixed)
331
	  this_acc = (md.common_acc[i] ?
332
		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
333
334

	os << "State: " << i;
335
336
	if (sn && i < sn->size() && !(*sn)[i].empty())
	  os << " \"" << (*sn)[i] << '"';
337
338
339
340
341
342
343
344
345
346
	if (this_acc == Hoa_Acceptance_States)
	  {
	    acc_cond::mark_t acc = 0U;
	    for (auto& t: aut->out(i))
	      {
		acc = t.acc;
		break;
	      }
	    md.emit_acc(os, aut, acc);
	  }
347
348
	os << nl;

349
350
351
352
353
354
355
356
357
358
359
	if (!implicit_labels)
	  {
	    for (auto& t: aut->out(i))
	      {
		os << '[' << md.sup[t.cond] << "] " << t.dst;
		if (this_acc == Hoa_Acceptance_Transitions)
		  md.emit_acc(os, aut, t.acc);
		os << nl;
	      }
	  }
	else
360
	  {
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
	    for (auto& t: aut->out(i))
	      {
		bdd cond = t.cond;
		while (cond != bddfalse)
		  {
		    bdd one = bdd_satoneset(cond, md.all_ap, bddfalse);
		    cond -= one;
		    unsigned level = 1;
		    unsigned pos = 0U;
		    while (one != bddtrue)
		      {
			bdd h = bdd_high(one);
			if (h == bddfalse)
			  {
			    one = bdd_low(one);
			  }
			else
			  {
			    pos |= level;
			    one = h;
			  }
			level <<= 1;
		      }
		    out[pos] = t.dst;
		    if (this_acc != Hoa_Acceptance_States)
		      outm[pos] = t.acc;
		  }
	      }
	    unsigned n = out.size();
	    for (unsigned i = 0; i < n;)
	      {
		os << out[i];
		if (this_acc != Hoa_Acceptance_States)
		  {
		    md.emit_acc(os, aut, outm[i]) << nl;
		    ++i;
		  }
		else
		  {
		    ++i;
		    os << (((i & 15) && i < n) ? ' ' : nl);
		  }
	      }
404
405
406
407
408
409
410
	  }
      }
    os << "--END--";		// No newline.  Let the caller decide.
    return os;
  }

  std::ostream&
411
412
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
413
		const char* opt)
414
  {
415
416
417
418
419

    auto a = std::dynamic_pointer_cast<const tgba_digraph>(aut);
    if (!a)
      a = make_tgba_digraph(aut, tgba::prop_set::all());

420
    return hoa_reachable(os, a, opt);
421
422
423
  }

}