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

namespace spot
{
  namespace
  {
41
    struct metadata final
42
43
44
45
46
47
48
49
    {
      // 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;
50
      bool has_state_acc;
51
52
      bool is_complete;
      bool is_deterministic;
53
54
      bool use_implicit_labels;
      bdd all_ap;
55
56
57
58
59
60

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

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

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

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

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

	// 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);
143
144
145
146
147
148
      }

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

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

161
162
163
	if (use_implicit_labels)
	  return;

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

  }

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

224
  static std::ostream&
225
  hoa_reachable(std::ostream& os,
226
		const const_tgba_digraph_ptr& aut,
227
		const char* opt)
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
254
    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;
	    }
	}
255

256
257
258
259
    // 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();

260
    metadata md(aut, implicit_labels);
261

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

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

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

285
    unsigned num_acc = aut->acc().num_sets();
286
    if (aut->acc().is_generalized_buchi())
287
      {
288
	if (aut->acc().is_true())
289
	  os << "acc-name: all";
290
	else if (aut->acc().is_buchi())
291
292
293
294
	  os << "acc-name: Buchi";
	else
	  os << "acc-name: generalized-Buchi " << num_acc;
	os << nl;
295
      }
296
297
    os << "Acceptance: " << num_acc << ' ';
    os << aut->acc().get_acceptance();
298
    os << nl;
299
    os << "properties:";
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317

    // Make sure the property line is not too large,
    // otherwise our test cases do not fit in 80 columns...
    unsigned prop_len = 60;
    auto prop = [&](const char* str)
      {
	if (newline)
	  {
	    auto l = strlen(str);
	    if (prop_len < l)
	      {
		prop_len = 60;
		os << "\nproperties:";
	      }
	    prop_len -= l;
	  }
	os << str;
      };
318
319
    implicit_labels = md.use_implicit_labels;
    if (implicit_labels)
320
      prop(" implicit-labels");
321
    else
322
      prop(" trans-labels explicit-labels");
323
    if (acceptance == Hoa_Acceptance_States)
324
      prop(" state-acc");
325
    else if (acceptance == Hoa_Acceptance_Transitions)
326
      prop(" trans-acc");
327
    if (md.is_complete)
328
      prop(" complete");
329
    if (md.is_deterministic)
330
331
332
333
334
      prop(" deterministic");
    if (aut->is_stutter_invariant())
      prop(" stutter-invariant");
    if (aut->is_inherently_weak())
      prop(" inherently-weak");
335
    os << nl;
336
337
338
339
340
341
342
343
344
345
346
347

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

348
    os << "--BODY--" << nl;
349
    auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
350
351
    for (unsigned i = 0; i < num_states; ++i)
      {
352
353
	hoa_acceptance this_acc = acceptance;
	if (this_acc == Hoa_Acceptance_Mixed)
354
	  this_acc = (md.common_acc[i] ?
355
		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
356
357

	os << "State: " << i;
358
359
	if (sn && i < sn->size() && !(*sn)[i].empty())
	  os << " \"" << (*sn)[i] << '"';
360
361
362
363
364
365
366
367
368
369
	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);
	  }
370
371
	os << nl;

372
373
374
375
376
377
378
379
380
381
382
	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
383
	  {
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
	    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);
		  }
	      }
427
428
429
430
431
432
433
	  }
      }
    os << "--END--";		// No newline.  Let the caller decide.
    return os;
  }

  std::ostream&
434
435
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
436
		const char* opt)
437
  {
438
439
440
441
442

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

443
    return hoa_reachable(os, a, opt);
444
445
446
  }

}