hoa.cc 8.01 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;
134
135
136
137
138
139
      }

      void number_all_ap()
      {
	sup_map::iterator i;
	bdd all = bddtrue;
140
141
	for (auto& i: sup)
	  all &= bdd_support(i.first);
142
143
144
145
146
147
148
149
150

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

151
	for (auto& i: sup)
152
	  {
153
	    bdd cond = i.first;
154
155
	    if (cond == bddtrue)
	      {
156
		i.second = "t";
157
158
159
160
		continue;
	      }
	    if (cond == bddfalse)
	      {
161
		i.second = "f";
162
163
164
165
166
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
		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;
	      }
194
	    i.second = s.str();
195
196
197
198
199
200
201
	  }
      }

    };

  }

202
203
204
205
206
207
208
209
210
211
  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
    };
212

213
  static std::ostream&
214
  hoa_reachable(std::ostream& os,
215
		const const_tgba_digraph_ptr& aut,
216
217
218
		hoa_acceptance acceptance,
		hoa_alias alias,
		bool newline)
219
220
221
  {
    (void) alias;

222
223
224
225
    // 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();

226
227
    metadata md(aut);

228
    if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
229
      acceptance = Hoa_Acceptance_Transitions;
230

231
    unsigned num_states = aut->num_states();
232
233
234

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

	os << "State: " << i;
289
290
291
292
293
294
295
296
297
298
	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);
	  }
299
300
	os << nl;

301
	for (auto& t: aut->out(i))
302
	  {
303
	    os << '[' << md.sup[t.cond] << "] " << t.dst;
304
	    if (this_acc == Hoa_Acceptance_Transitions)
305
	      md.emit_acc(os, aut, t.acc);
306
307
308
309
310
311
312
313
	    os << nl;
	  }
      }
    os << "--END--";		// No newline.  Let the caller decide.
    return os;
  }

  std::ostream&
314
315
  hoa_reachable(std::ostream& os,
		const const_tgba_ptr& aut,
316
		const char* opt)
317
318
  {
    bool newline = true;
319
320
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    hoa_alias alias = Hoa_Alias_None;
321
322
323
324
325
326
327
328
329
330

    if (opt)
      while (*opt)
	{
	  switch (*opt++)
	    {
	    case 'l':
	      newline = false;
	      break;
	    case 'm':
331
	      acceptance = Hoa_Acceptance_Mixed;
332
333
	      break;
	    case 's':
334
	      acceptance = Hoa_Acceptance_States;
335
336
	      break;
	    case 't':
337
	      acceptance = Hoa_Acceptance_Transitions;
338
339
340
	      break;
	    }
	}
341
342
343
344
345
346

    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);
347
348
349
  }

}