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

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

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

}