hoa.cc 8.37 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
52
53
54
55
56
57
      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;

58
      metadata(const const_tgba_digraph_ptr& aut)
59
      {
60
	check_det_and_comp(aut);
61
62
63
64
	number_all_ap();
      }

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

86
      void check_det_and_comp(const const_tgba_digraph_ptr& aut)
87
88
89
      {
	std::string empty;

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

	// 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);
139
140
141
142
143
144
      }

      void number_all_ap()
      {
	sup_map::iterator i;
	bdd all = bddtrue;
145
146
	for (auto& i: sup)
	  all &= bdd_support(i.first);
147
148
149
150
151
152
153
154
155

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

156
	for (auto& i: sup)
157
	  {
158
	    bdd cond = i.first;
159
160
	    if (cond == bddtrue)
	      {
161
		i.second = "t";
162
163
164
165
		continue;
	      }
	    if (cond == bddfalse)
	      {
166
		i.second = "f";
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
		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;
	      }
199
	    i.second = s.str();
200
201
202
203
204
205
206
	  }
      }

    };

  }

207
208
209
210
211
212
213
214
215
216
  enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
  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
    };
217

218
  static std::ostream&
219
  hoa_reachable(std::ostream& os,
220
		const const_tgba_digraph_ptr& aut,
221
222
223
		hoa_acceptance acceptance,
		hoa_alias alias,
		bool newline)
224
225
226
  {
    (void) alias;

227
228
229
230
    // 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();

231
232
    metadata md(aut);

233
    if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
234
      acceptance = Hoa_Acceptance_Transitions;
235

236
    unsigned num_states = aut->num_states();
237
238
239

    const char nl = newline ? '\n' : ' ';
    os << "HOA: v1" << nl;
240
    auto n = aut->get_named_prop<std::string>("automaton-name");
241
    if (n)
242
      escape_str(os << "name: \"", *n) << '"' << nl;
243
    os << "States: " << num_states << nl
244
       << "Start: " << init << nl
245
       << "AP: " << md.vap.size();
246
    auto d = aut->get_dict();
247
    for (auto& i: md.vap)
248
      {
249
	auto f = ltl::is_atomic_prop(d->bdd_map[i].f);
250
251
252
	assert(f);
	escape_str(os << " \"", f->name()) << '"';
      }
253
    os << nl;
254
    unsigned num_acc = aut->acc().num_sets();
255
256
257
258
259
260
261
262
263
264
    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)
      {
265
	os << " Inf(0";
266
	for (unsigned i = 1; i < num_acc; ++i)
267
	  os << ")&Inf(" << i;
268
269
270
271
272
273
274
275
	os << ')';
      }
    else
      {
	os  << " t";
      }
    os << nl;
    os << "properties: trans-labels explicit-labels";
276
    if (acceptance == Hoa_Acceptance_States)
277
      os << " state-acc";
278
    else if (acceptance == Hoa_Acceptance_Transitions)
279
280
281
282
283
284
285
      os << " trans-acc";
    if (md.is_complete)
      os << " complete";
    if (md.is_deterministic)
      os << " deterministic";
    os << nl;
    os << "--BODY--" << nl;
286
    auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
287
288
    for (unsigned i = 0; i < num_states; ++i)
      {
289
290
	hoa_acceptance this_acc = acceptance;
	if (this_acc == Hoa_Acceptance_Mixed)
291
	  this_acc = (md.common_acc[i] ?
292
		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
293
294

	os << "State: " << i;
295
296
	if (sn && i < sn->size() && !(*sn)[i].empty())
	  os << " \"" << (*sn)[i] << '"';
297
298
299
300
301
302
303
304
305
306
	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);
	  }
307
308
	os << nl;

309
	for (auto& t: aut->out(i))
310
	  {
311
	    os << '[' << md.sup[t.cond] << "] " << t.dst;
312
	    if (this_acc == Hoa_Acceptance_Transitions)
313
	      md.emit_acc(os, aut, t.acc);
314
315
316
317
318
319
320
321
	    os << nl;
	  }
      }
    os << "--END--";		// No newline.  Let the caller decide.
    return os;
  }

  std::ostream&
322
323
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
324
		const char* opt)
325
326
  {
    bool newline = true;
327
328
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    hoa_alias alias = Hoa_Alias_None;
329
330
331
332
333
334
335
336
337
338

    if (opt)
      while (*opt)
	{
	  switch (*opt++)
	    {
	    case 'l':
	      newline = false;
	      break;
	    case 'm':
339
	      acceptance = Hoa_Acceptance_Mixed;
340
341
	      break;
	    case 's':
342
	      acceptance = Hoa_Acceptance_States;
343
344
	      break;
	    case 't':
345
	      acceptance = Hoa_Acceptance_Transitions;
346
347
348
	      break;
	    }
	}
349
350
351
352
353
354

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

    return hoa_reachable(os, a, acceptance, alias, newline);
355
356
357
  }

}