minimize.cc 17.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
4 5 6 7 8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10 11 12 13 14 15 16 17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20 21 22 23 24 25 26 27 28

//#define TRACE

#ifdef TRACE
#  define trace std::cerr
#else
#  define trace while (0) std::cerr
#endif

29
#include <queue>
30 31 32
#include <deque>
#include <set>
#include <list>
33
#include <vector>
34
#include <sstream>
35 36
#include "minimize.hh"
#include "misc/hash.hh"
37
#include "misc/bddlt.hh"
38 39 40 41 42 43 44 45 46
#include "twaalgos/product.hh"
#include "twaalgos/powerset.hh"
#include "twaalgos/gtec/gtec.hh"
#include "twaalgos/safety.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/bfssteps.hh"
#include "twaalgos/isdet.hh"
47 48
#include "twaalgos/complement.hh"
#include "twaalgos/remfin.hh"
49 50 51

namespace spot
{
52 53
  // FIXME: do we really want to use unordered_set instead of set here?
  // This calls for benchmarking.
54 55 56 57
  typedef std::unordered_set<const state*,
			     state_ptr_hash, state_ptr_equal> hash_set;
  typedef std::unordered_map<const state*, unsigned,
			     state_ptr_hash, state_ptr_equal> hash_map;
58

59 60 61
  namespace
  {
    static std::ostream&
62
    dump_hash_set(const hash_set* hs,
63
		  const const_twa_ptr& aut,
64
		  std::ostream& out)
65
    {
66
      out << '{';
67 68 69 70 71 72
      const char* sep = "";
      for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i)
	{
	  out << sep << aut->format_state(*i);
	  sep = ", ";
	}
73
      out << '}';
74 75 76 77
      return out;
    }

    static std::string
78
    format_hash_set(const hash_set* hs, const_twa_ptr aut)
79 80 81 82 83 84
    {
      std::ostringstream s;
      dump_hash_set(hs, aut, s);
      return s.str();
    }

85 86 87 88 89 90 91 92 93 94 95 96 97
    // Find all states of an automaton.
    static void
    build_state_set(const const_twa_ptr& a, hash_set* seen)
    {
      std::queue<const state*> tovisit;
      // Perform breadth-first traversal.
      const state* init = a->get_init_state();
      tovisit.push(init);
      seen->insert(init);
      while (!tovisit.empty())
	{
	  const state* src = tovisit.front();
	  tovisit.pop();
98

99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
	  for (auto sit: a->succ(src))
	    {
	      const state* dst = sit->current_state();
	      // Is it a new state ?
	      if (seen->find(dst) == seen->end())
		{
		  // Register the successor for later processing.
		  tovisit.push(dst);
		  seen->insert(dst);
		}
	      else
		dst->destroy();
	    }
	}
    }
114

115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    // From the base automaton and the list of sets, build the minimal
    // resulting automaton
    static twa_graph_ptr
    build_result(const const_twa_ptr& a,
		 std::list<hash_set*>& sets,
		 hash_set* final)
    {
      auto dict = a->get_dict();
      auto res = make_twa_graph(dict);
      res->copy_ap_of(a);
      res->prop_state_based_acc();

      // For each set, create a state in the resulting automaton.
      // For a state s, state_num[s] is the number of the state in the minimal
      // automaton.
      hash_map state_num;
      std::list<hash_set*>::iterator sit;
      for (sit = sets.begin(); sit != sets.end(); ++sit)
	{
	  hash_set::iterator hit;
	  hash_set* h = *sit;
	  unsigned num = res->new_state();
	  for (hit = h->begin(); hit != h->end(); ++hit)
	    state_num[*hit] = num;
	}
140

141 142
      // For each transition in the initial automaton, add the corresponding
      // transition in res.
143

144 145
      if (!final->empty())
	res->set_buchi();
146

147 148 149
      for (sit = sets.begin(); sit != sets.end(); ++sit)
	{
	  hash_set* h = *sit;
150

151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
	  // Pick one state.
	  const state* src = *h->begin();
	  unsigned src_num = state_num[src];
	  bool accepting = (final->find(src) != final->end());

	  // Connect it to all destinations.
	  for (auto succit: a->succ(src))
	    {
	      const state* dst = succit->current_state();
	      hash_map::const_iterator i = state_num.find(dst);
	      dst->destroy();
	      if (i == state_num.end()) // Ignore useless destinations.
		continue;
	      res->new_acc_edge(src_num, i->second,
				succit->current_condition(), accepting);
	    }
	}
      res->merge_edges();
      if (res->num_states() > 0)
	{
	  const state* init_state = a->get_init_state();
	  unsigned init_num = state_num[init_state];
	  init_state->destroy();
	  res->set_init_state(init_num);
	}
      return res;
    }
178 179 180

    struct wdba_search_acc_loop : public bfs_steps
    {
181
      wdba_search_acc_loop(const const_twa_ptr& det_a,
182
			   unsigned scc_n, scc_info& sm,
183 184 185
			   power_map& pm, const state* dest)
	: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
      {
186
	seen(dest);
187 188 189 190 191
      }

      virtual const state*
      filter(const state* s)
      {
192
	s = seen(s);
193
	if (sm.scc_of(std::static_pointer_cast<const twa_graph>(a_)
194
		      ->state_number(s)) != scc_n)
195
	  return nullptr;
196 197 198 199
	return s;
      }

      virtual bool
200
      match(twa_run::step&, const state* to)
201 202 203 204 205
      {
	return to == dest;
      }

      unsigned scc_n;
206
      scc_info& sm;
207 208
      power_map& pm;
      const state* dest;
209
      state_unicity_table seen;
210 211 212 213
    };


    bool
214 215
    wdba_scc_is_accepting(const const_twa_graph_ptr& det_a, unsigned scc_n,
			  const const_twa_graph_ptr& orig_a, scc_info& sm,
216
			  power_map& pm)
217 218
    {
      // Get some state from the SCC #n.
219
      const state* start = det_a->state_from_number(sm.one_state_of(scc_n));
220 221 222

      // Find a loop around START in SCC #n.
      wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start);
223
      twa_run::steps loop;
224 225 226 227 228
      const state* reached = wsal.search(start, loop);
      assert(reached == start);
      (void)reached;

      // Build an automaton representing this loop.
229
      auto loop_a = make_twa_graph(det_a->get_dict());
230
      twa_run::steps::const_iterator i;
231
      int loop_size = loop.size();
232
      loop_a->new_states(loop_size);
233 234 235
      int n;
      for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
	{
236
	  loop_a->new_edge(n - 1, n, i->label);
237
	  i->s->destroy();
238 239
	}
      assert(i != loop.end());
240
      loop_a->new_edge(n - 1, 0, i->label);
241
      i->s->destroy();
242 243
      assert(++i == loop.end());

244
      loop_a->set_init_state(0U);
245 246 247 248 249

      // Check if the loop is accepting in the original automaton.
      bool accepting = false;

      // Iterate on each original state corresponding to start.
250 251
      const power_map::power_state& ps =
	pm.states_of(det_a->state_number(start));
252
      for (auto& s: ps)
253
	{
254
	  // Construct a product between LOOP_A and ORIG_A starting in
255 256
	  // S.  FIXME: This could be sped up a lot!
	  if (!product(loop_a, orig_a, 0U, s)->is_empty())
257 258 259 260
	    {
	      accepting = true;
	      break;
	    }
261 262 263 264 265
	}

      return accepting;
    }

266 267 268 269 270 271
    static twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a,
				      hash_set* final, hash_set* non_final)
    {
      typedef std::list<hash_set*> partition_t;
      partition_t cur_run;
      partition_t next_run;
272

273 274
      // The list of equivalent states.
      partition_t done;
275

276
      hash_map state_set_map;
277

278 279 280 281 282 283
      // Size of det_a
      unsigned size = final->size() + non_final->size();
      // Use bdd variables to number sets.  set_num is the first variable
      // available.
      unsigned set_num =
	det_a->get_dict()->register_anonymous_variables(size, det_a);
284

285 286 287 288
      std::set<int> free_var;
      for (unsigned i = set_num; i < set_num + size; ++i)
	free_var.insert(i);
      std::map<int, int> used_var;
289

290
      hash_set* final_copy;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
291

292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
      if (!final->empty())
	{
	  unsigned s = final->size();
	  used_var[set_num] = s;
	  free_var.erase(set_num);
	  if (s > 1)
	    cur_run.push_back(final);
	  else
	    done.push_back(final);
	  for (hash_set::const_iterator i = final->begin();
	       i != final->end(); ++i)
	    state_set_map[*i] = set_num;

	  final_copy = new hash_set(*final);
	}
      else
	{
	  final_copy = final;
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
311

312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
      if (!non_final->empty())
	{
	  unsigned s = non_final->size();
	  unsigned num = set_num + 1;
	  used_var[num] = s;
	  free_var.erase(num);
	  if (s > 1)
	    cur_run.push_back(non_final);
	  else
	    done.push_back(non_final);
	  for (hash_set::const_iterator i = non_final->begin();
	       i != non_final->end(); ++i)
	    state_set_map[*i] = num;
	}
      else
	{
	  delete non_final;
	}
330

331 332 333
      // A bdd_states_map is a list of formulae (in a BDD form)
      // associated with a destination set of states.
      typedef std::map<bdd, hash_set*, bdd_less_than> bdd_states_map;
334

335
      bool did_split = true;
336

337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 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 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
      while (did_split)
	{
	  did_split = false;
	  while (!cur_run.empty())
	    {
	      // Get a set to process.
	      hash_set* cur = cur_run.front();
	      cur_run.pop_front();

	      trace << "processing " << format_hash_set(cur, det_a)
		    << std::endl;

	      hash_set::iterator hi;
	      bdd_states_map bdd_map;
	      for (hi = cur->begin(); hi != cur->end(); ++hi)
		{
		  const state* src = *hi;
		  bdd f = bddfalse;
		  for (auto si: det_a->succ(src))
		    {
		      const state* dst = si->current_state();
		      hash_map::const_iterator i = state_set_map.find(dst);
		      dst->destroy();
		      if (i == state_set_map.end())
			// The destination state is not in our
			// partition.  This can happen if the initial
			// FINAL and NON_FINAL supplied to the algorithm
			// do not cover the whole automaton (because we
			// want to ignore some useless states).  Simply
			// ignore these states here.
			continue;
		      f |= (bdd_ithvar(i->second) & si->current_condition());
		    }

		  // Have we already seen this formula ?
		  bdd_states_map::iterator bsi = bdd_map.find(f);
		  if (bsi == bdd_map.end())
		    {
		      // No, create a new set.
		      hash_set* new_set = new hash_set;
		      new_set->insert(src);
		      bdd_map[f] = new_set;
		    }
		  else
		    {
		      // Yes, add the current state to the set.
		      bsi->second->insert(src);
		    }
		}

	      bdd_states_map::iterator bsi = bdd_map.begin();
	      if (bdd_map.size() == 1)
		{
		  // The set was not split.
		  trace << "set " << format_hash_set(bsi->second, det_a)
			<< " was not split" << std::endl;
		  next_run.push_back(bsi->second);
		}
	      else
		{
		  did_split = true;
		  for (; bsi != bdd_map.end(); ++bsi)
		    {
		      hash_set* set = bsi->second;
		      // Free the number associated to these states.
		      unsigned num = state_set_map[*set->begin()];
		      assert(used_var.find(num) != used_var.end());
		      unsigned left = (used_var[num] -= set->size());
		      // Make sure LEFT does not become negative (hence bigger
		      // than SIZE when read as unsigned)
		      assert(left < size);
		      if (left == 0)
			{
			  used_var.erase(num);
			  free_var.insert(num);
			}
		      // Pick a free number
		      assert(!free_var.empty());
		      num = *free_var.begin();
		      free_var.erase(free_var.begin());
		      used_var[num] = set->size();
		      for (hash_set::iterator hit = set->begin();
			   hit != set->end(); ++hit)
			state_set_map[*hit] = num;
		      // Trivial sets can't be splitted any further.
		      if (set->size() == 1)
			{
			  trace << "set " << format_hash_set(set, det_a)
				<< " is minimal" << std::endl;
			  done.push_back(set);
			}
		      else
			{
			  trace << "set " << format_hash_set(set, det_a)
				<< " should be processed further" << std::endl;
			  next_run.push_back(set);
			}
		    }
		}
	      delete cur;
	    }
	  if (did_split)
	    trace << "splitting did occur during this pass." << std::endl;
	  else
	    trace << "splitting did not occur during this pass." << std::endl;
	  std::swap(cur_run, next_run);
	}
444

445
      done.splice(done.end(), cur_run);
446 447

#ifdef TRACE
448 449 450 451
      trace << "Final partition: ";
      for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
	trace << format_hash_set(*i, det_a) << ' ';
      trace << std::endl;
452
#endif
Felix Abecassis's avatar
Felix Abecassis committed
453

454 455
      // Build the result.
      auto res = build_result(det_a, done, final_copy);
Felix Abecassis's avatar
Felix Abecassis committed
456

457 458 459 460 461 462 463 464 465 466 467
      // Free all the allocated memory.
      delete final_copy;
      hash_map::iterator hit;
      for (hit = state_set_map.begin(); hit != state_set_map.end();)
	{
	  hash_map::iterator old = hit++;
	  old->first->destroy();
	}
      std::list<hash_set*>::iterator it;
      for (it = done.begin(); it != done.end(); ++it)
	delete *it;
Felix Abecassis's avatar
Felix Abecassis committed
468

469 470
      return res;
    }
471
  }
472

473
  twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a)
474 475
  {
    hash_set* final = new hash_set;
476
    hash_set* non_final = new hash_set;
477
    twa_graph_ptr det_a = tgba_powerset(a);
478 479

    // non_final contain all states.
480
    // final is empty: there is no acceptance condition
481
    build_state_set(det_a, non_final);
482
    auto res = minimize_dfa(det_a, final, non_final);
483
    res->prop_copy(a, { false, false, false, true });
484 485
    res->prop_deterministic();
    res->prop_inherently_weak();
486
    res->prop_state_based_acc();
487
    return res;
488 489
  }

490
  twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a)
491 492
  {
    hash_set* final = new hash_set;
493 494
    hash_set* non_final = new hash_set;

495
    twa_graph_ptr det_a;
496 497 498 499 500

    {
      power_map pm;
      det_a = tgba_powerset(a, pm);

501 502 503 504 505
      // For each SCC of the deterministic automaton, determine if it
      // is accepting or not.

      // This corresponds to the algorithm in Fig. 1 of "Efficient
      // minimization of deterministic weak omega-automata" written by
506
      // Christof Löding and published in Information Processing
507 508 509 510 511
      // Letters 79 (2001) pp 105--109.

      // We also keep track of whether an SCC is useless
      // (i.e., it is not the start of any accepting word).

512
      scc_info sm(det_a);
513
      sm.determine_unknown_acceptance();
514
      unsigned scc_count = sm.scc_count();
515 516
      // SCC that have been marked as useless.
      std::vector<bool> useless(scc_count);
517 518 519 520 521 522 523
      // The "color".  Even number correspond to
      // accepting SCCs.
      std::vector<unsigned> d(scc_count);

      // An even number larger than scc_count.
      unsigned k = (scc_count | 1) + 1;

524
      // SCC are numbered in topological order
525
      // (but in the reverse order as Löding's)
526
      for (unsigned m = 0; m < scc_count; ++m)
527
	{
528
	  bool is_useless = true;
529 530
	  bool transient = sm.is_trivial(m);
	  auto& succ = sm.succ(m);
531

532
	  if (transient && succ.empty())
533
	    {
534 535 536 537 538 539 540 541 542 543
	      // A trivial SCC without successor is useless.
	      useless[m] = true;
	      d[m] = k - 1;
	      continue;
	    }

	  // Compute the minimum color l of the successors.
	  // Also SCCs are useless if all their successor are
	  // useless.
	  unsigned l = k;
544
	  for (unsigned j: succ)
545
	    {
546 547
	      is_useless &= useless[j];
	      unsigned dj = d[j];
548 549 550 551 552 553 554
	      if (dj < l)
		l = dj;
	    }

	  if (transient)
	    {
	      d[m] = l;
555 556 557 558
	    }
	  else
	    {
	      // Regular SCCs are accepting if any of their loop
559 560
	      // corresponds to an accepted word in the original
	      // automaton.
561
	      if (wdba_scc_is_accepting(det_a, m, a, sm, pm))
562 563
		{
		  is_useless = false;
564
		  d[m] = l & ~1; // largest even number inferior or equal
565 566 567
		}
	      else
		{
568
		  d[m] = (l - 1) | 1; // largest odd number inferior or equal
569
		}
570
	    }
571

572
	  useless[m] = is_useless;
573

574 575
	  if (!is_useless)
	    {
576
	      hash_set* dest_set = (d[m] & 1) ? non_final : final;
577 578
	      for (auto s: sm.states_of(m))
		dest_set->insert(det_a->state_from_number(s));
579
	    }
580 581 582
	}
    }

583
    auto res = minimize_dfa(det_a, final, non_final);
584
    res->prop_copy(a, { false, false, false, true });
585 586 587
    res->prop_deterministic();
    res->prop_inherently_weak();
    return res;
588 589
  }

590 591
  twa_graph_ptr
  minimize_obligation(const const_twa_graph_ptr& aut_f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
592
		      formula f,
593
		      const_twa_graph_ptr aut_neg_f,
594
		      bool reject_bigger)
595
  {
596
    auto min_aut_f = minimize_wdba(aut_f);
597

598 599 600
    if (reject_bigger)
      {
	// Abort if min_aut_f has more states than aut_f.
601
	unsigned orig_states = aut_f->num_states();
602
	if (orig_states < min_aut_f->num_states())
603
	  return std::const_pointer_cast<twa_graph>(aut_f);
604 605
      }

606 607 608 609 610
    // If the input automaton was already weak and deterministic, the
    // output is necessary correct.
    if (aut_f->is_inherently_weak() && aut_f->is_deterministic())
      return min_aut_f;

611 612
    // if f is a syntactic obligation formula, the WDBA minimization
    // must be correct.
613
    if (f && f.is_syntactic_obligation())
614 615
      return min_aut_f;

616
    // If aut_f is a guarantee automaton, the WDBA minimization must be
617
    // correct.
618
    if (is_guarantee_automaton(aut_f))
619
      return min_aut_f;
620 621 622 623

    // Build negation automaton if not supplied.
    if (!aut_neg_f)
      {
624 625 626 627
	if (f)
	  {
	    // If we know the formula, simply build the automaton for
	    // its negation.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
628
	    aut_neg_f = ltl_to_tgba_fm(formula::Not(f), aut_f->get_dict());
629
	    // Remove useless SCCs.
630
	    aut_neg_f = scc_filter(aut_neg_f, true);
631 632 633 634 635
	  }
	else if (is_deterministic(aut_f))
	  {
	    // If the automaton is deterministic, complementing is
	    // easy.
636
	    aut_neg_f = remove_fin(dtwa_complement(aut_f));
637 638 639 640
	  }
	else
	  {
	    // Otherwise, we cannot check if the minimization is safe.
641
	    return nullptr;
642
	  }
643 644
      }

645
    // If the negation is a guarantee automaton, then the
646
    // minimization is correct.
647
    if (is_guarantee_automaton(aut_neg_f))
648 649 650 651 652 653
      {
	return min_aut_f;
      }

    bool ok = false;

654
    if (product(min_aut_f, aut_neg_f)->is_empty())
655
      {
656
	// Complement the minimized WDBA.
657
	assert(min_aut_f->is_inherently_weak());
658
	auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
659 660 661 662
	if (product(aut_f, neg_min_aut_f)->is_empty())
	  // Finally, we are now sure that it was safe
	  // to minimize the automaton.
	  ok = true;
663 664 665 666
      }

    if (ok)
      return min_aut_f;
667
    return std::const_pointer_cast<twa_graph>(aut_f);
668
  }
669
}