tgba2ta.cc 19.6 KB
Newer Older
1 2 3
// -*- coding: utf-8 -*-
// 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
//#define TRACE
21 22 23 24 25 26 27 28

#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

29 30 31 32 33 34 35 36 37 38
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh"
#include <cassert>
#include "ltlvisit/tostring.hh"
#include <iostream>
#include "tgba/bddprint.hh"
#include <stack>
#include "tgba2ta.hh"
#include "taalgos/statessetbuilder.hh"
39
#include "ta/tgtaexplicit.hh"
40 41 42 43 44 45

using namespace std;

namespace spot
{

46 47
  namespace
  {
48
    typedef std::pair<spot::state*, twa_succ_iterator*> pair_state_iter;
49

50 51
    static void
    transform_to_single_pass_automaton
52
    (const ta_explicit_ptr& testing_automata,
53 54
     state_ta_explicit* artificial_livelock_acc_state = 0)
    {
55

56 57 58 59
      if (artificial_livelock_acc_state != 0)
	{
	  state_ta_explicit* artificial_livelock_acc_state_added =
            testing_automata->add_state(artificial_livelock_acc_state);
60

61 62 63
	  // unique artificial_livelock_acc_state
	  assert(artificial_livelock_acc_state_added
		 == artificial_livelock_acc_state);
64
	  (void)artificial_livelock_acc_state_added;
65 66 67
	  artificial_livelock_acc_state->set_livelock_accepting_state(true);
	  artificial_livelock_acc_state->free_transitions();
	}
68

69 70
      ta::states_set_t states_set = testing_automata->get_states_set();
      ta::states_set_t::iterator it;
71

72
      state_ta_explicit::transitions* transitions_to_livelock_states =
73 74
        new state_ta_explicit::transitions;

75 76 77
      for (it = states_set.begin(); it != states_set.end(); ++it)
	{
	  state_ta_explicit* source = static_cast<state_ta_explicit*> (*it);
78

79
	  transitions_to_livelock_states->clear();
80

81 82
	  state_ta_explicit::transitions* trans = source->get_transitions();
	  state_ta_explicit::transitions::iterator it_trans;
83

84 85 86 87
	  if (trans != 0)
	    for (it_trans = trans->begin(); it_trans != trans->end();)
	      {
		state_ta_explicit* dest = (*it_trans)->dest;
88

89
		state_ta_explicit::transitions* dest_trans =
90
                  (dest)->get_transitions();
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 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 140
		bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();

		//select transitions where a destination is a livelock state
		// which isn't a Buchi accepting state and has successors
		if (dest->is_livelock_accepting_state()
		    && (!dest->is_accepting_state()) && (!dest_trans_empty))
		  transitions_to_livelock_states->push_front(*it_trans);

		// optimization to have, after minimization, an unique
		// livelock state which has no successors
		if (dest->is_livelock_accepting_state() && (dest_trans_empty))
		  dest->set_accepting_state(false);

		++it_trans;
	      }

	  if (transitions_to_livelock_states != 0)
	    {
	      state_ta_explicit::transitions::iterator it_trans;

	      for (it_trans = transitions_to_livelock_states->begin();
		   it_trans != transitions_to_livelock_states->end();
		   ++it_trans)
		{
		  if (artificial_livelock_acc_state != 0)
		    {
		      testing_automata->create_transition
			(source,
			 (*it_trans)->condition,
			 (*it_trans)->acceptance_conditions,
			 artificial_livelock_acc_state, true);
		    }
		  else
		    {
		      testing_automata->create_transition
			(source,
			 (*it_trans)->condition,
			 (*it_trans)->acceptance_conditions,
			 ((*it_trans)->dest)->stuttering_reachable_livelock,
			 true);
		    }
		}
	    }
	}
      delete transitions_to_livelock_states;

      for (it = states_set.begin(); it != states_set.end(); ++it)
	{
	  state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
	  state_ta_explicit::transitions* state_trans =
141
            (state)->get_transitions();
142
	  bool state_trans_empty = state_trans == 0 || state_trans->empty();
143

144 145 146 147
	  if (state->is_livelock_accepting_state()
	      && (!state->is_accepting_state()) && (!state_trans_empty))
	    state->set_livelock_accepting_state(false);
	}
148 149
    }

150
    static void
151
    compute_livelock_acceptance_states(const ta_explicit_ptr& testing_aut,
152 153 154
				       bool single_pass_emptiness_check,
				       state_ta_explicit*
				       artificial_livelock_acc_state)
155
    {
156 157 158 159 160
      // We use five main data in this algorithm:
      // * sscc: a stack of strongly stuttering-connected components (SSCC)
      scc_stack_ta sscc;

      // * arc, a stack of acceptance conditions between each of these SCC,
161
      std::stack<acc_cond::mark_t> arc;
162 163 164

      // * h: a hash of all visited nodes, with their order,
      //   (it is called "Hash" in Couvreur's paper)
165 166 167
      typedef std::unordered_map<const state*, int,
				 state_ptr_hash, state_ptr_equal> hash_type;
      hash_type h; ///< Heap of visited states.
168 169 170 171 172 173

      // * num: the number of visited nodes.  Used to set the order of each
      //   visited node,
      int num = 0;

      // * todo: the depth-first search stack.  This holds pairs of the
174
      //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
175 176 177 178 179 180 181 182
      //   over the successors of STATE.  In our use, ITERATOR should
      //   always be freed when TODO is popped, but STATE should not because
      //   it is also used as a key in H.
      std::stack<pair_state_iter> todo;

      // * init: the set of the depth-first search initial states
      std::stack<state*> init_set;

183
      for (state* s: testing_aut->get_initial_states_set())
184
	init_set.push(s);
185 186 187 188 189 190 191

      while (!init_set.empty())
	{
	  // Setup depth-first search from initial states.

	  {
	    state_ta_explicit* init =
192
	      down_cast<state_ta_explicit*> (init_set.top());
193
	    init_set.pop();
194

195
	    if (!h.emplace(init, num + 1).second)
196 197 198 199
	      {
		init->destroy();
		continue;
	      }
200

201
	    sscc.push(++num);
202
	    arc.push(0U);
203
	    sscc.top().is_accepting
204
              = testing_aut->is_accepting_state(init);
205
	    twa_succ_iterator* iter = testing_aut->succ_iter(init);
206
	    iter->first();
207
	    todo.emplace(init, iter);
208 209 210 211 212 213
	  }

	  while (!todo.empty())
	    {
	      state* curr = todo.top().first;

214
	      auto i = h.find(curr);
215
	      // If we have reached a dead component, ignore it.
216
	      if (i != h.end() && i->second == -1)
217 218 219 220 221 222
		{
		  todo.pop();
		  continue;
		}

	      // We are looking at the next successor in SUCC.
223
	      twa_succ_iterator* succ = todo.top().second;
224 225 226 227 228 229 230 231 232 233

	      // If there is no more successor, backtrack.
	      if (succ->done())
		{
		  // We have explored all successors of state CURR.

		  // Backtrack TODO.
		  todo.pop();

		  // fill rem with any component removed,
234
		  assert(i != h.end());
235 236 237 238 239 240
		  sscc.rem().push_front(curr);

		  // When backtracking the root of an SSCC, we must also
		  // remove that SSCC from the ROOT stacks.  We must
		  // discard from H all reachable states from this SSCC.
		  assert(!sscc.empty());
241
		  if (sscc.top().index == i->second)
242 243 244 245
		    {
		      // removing states
		      std::list<state*>::iterator i;
		      bool is_livelock_accepting_sscc = (sscc.rem().size() > 1)
246 247 248
			&& ((sscc.top().is_accepting) ||
			    (testing_aut->acc().
			     accepting(sscc.top().condition)));
249 250
		      trace << "*** sscc.size()  = ***" <<  sscc.size() << '\n';
		      for (auto j: sscc.rem())
251
			{
252
			  h[j] = -1;
253

254
			  if (is_livelock_accepting_sscc)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
255
			    {
256 257 258
			      // if it is an accepting sscc add the state to
			      // G (=the livelock-accepting states set)
			      trace << "*** sscc.size() > 1: states: ***"
259
				    << testing_aut->format_state(j)
260 261 262
				    << '\n';
			      state_ta_explicit* livelock_accepting_state =
				down_cast<state_ta_explicit*>(j);
263 264 265 266 267 268 269 270 271 272 273 274

			      livelock_accepting_state->
				set_livelock_accepting_state(true);

			      if (single_pass_emptiness_check)
				{
				  livelock_accepting_state
				    ->set_accepting_state(true);
				  livelock_accepting_state
				    ->stuttering_reachable_livelock
				    = livelock_accepting_state;
				}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
275
			    }
276
			}
277

278 279 280 281 282 283 284
		      assert(!arc.empty());
		      sscc.pop();
		      arc.pop();

		    }

		  // automata reduction
285
		  testing_aut->delete_stuttering_and_hole_successors(curr);
286 287 288 289 290 291 292 293 294

		  delete succ;
		  // Do not delete CURR: it is a key in H.
		  continue;
		}

	      // Fetch the values destination state we are interested in...
	      state* dest = succ->current_state();

295
	      auto acc_cond = succ->current_acceptance_conditions();
296 297 298 299 300 301 302
	      // ... and point the iterator to the next successor, for
	      // the next iteration.
	      succ->next();
	      // We do not need SUCC from now on.

	      // Are we going to a new state through a stuttering transition?
	      bool is_stuttering_transition =
303 304
		testing_aut->get_state_condition(curr)
		== testing_aut->get_state_condition(dest);
305
	      auto id = h.find(dest);
306 307

	      // Is this a new state?
308
	      if (id == h.end())
309 310 311 312
		{
		  if (!is_stuttering_transition)
		    {
		      init_set.push(dest);
313
		      dest->destroy();
314 315 316 317 318
		      continue;
		    }

		  // Number it, stack it, and register its successors
		  // for later processing.
319
		  h[dest] = ++num;
320 321 322
		  sscc.push(num);
		  arc.push(acc_cond);
		  sscc.top().is_accepting =
323
		    testing_aut->is_accepting_state(dest);
324

325
		  twa_succ_iterator* iter = testing_aut->succ_iter(dest);
326
		  iter->first();
327
		  todo.emplace(dest, iter);
328 329
		  continue;
		}
330
	      dest->destroy();
331 332

	      // If we have reached a dead component, ignore it.
333
	      if (id->second == -1)
334 335 336 337
		continue;

	      trace << "***compute_livelock_acceptance_states: CYCLE***\n";

338
	      if (!curr->compare(id->first))
339 340 341 342 343
		{
		  state_ta_explicit * self_loop_state =
		    down_cast<state_ta_explicit*> (curr);
		  assert(self_loop_state);

344 345
		  if (testing_aut->is_accepting_state(self_loop_state)
		      || (testing_aut->acc().accepting(acc_cond)))
346 347 348
		    {
		      self_loop_state->set_livelock_accepting_state(true);
		      if (single_pass_emptiness_check)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
349
			{
350 351 352
			  self_loop_state->set_accepting_state(true);
			  self_loop_state->stuttering_reachable_livelock
			    = self_loop_state;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
353
			}
354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
		    }

		  trace
		    << "***compute_livelock_acceptance_states: CYCLE: "
		    << "self_loop_state***\n";
		}

	      // Now this is the most interesting case.  We have reached a
	      // state S1 which is already part of a non-dead SSCC.  Any such
	      // non-dead SSCC has necessarily been crossed by our path to
	      // this state: there is a state S2 in our path which belongs
	      // to this SSCC too.  We are going to merge all states between
	      // this S1 and S2 into this SSCC.
	      //
	      // This merge is easy to do because the order of the SSCC in
	      // ROOT is ascending: we just have to merge all SSCCs from the
	      // top of ROOT that have an index greater to the one of
	      // the SSCC of S2 (called the "threshold").
372
	      int threshold = id->second;
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
	      std::list<state*> rem;
	      bool acc = false;

	      while (threshold < sscc.top().index)
		{
		  assert(!sscc.empty());
		  assert(!arc.empty());
		  acc |= sscc.top().is_accepting;
		  acc_cond |= sscc.top().condition;
		  acc_cond |= arc.top();
		  rem.splice(rem.end(), sscc.rem());
		  sscc.pop();
		  arc.pop();
		}

	      // Note that we do not always have
	      //  threshold == sscc.top().index
	      // after this loop, the SSCC whose index is threshold might have
	      // been merged with a lower SSCC.

	      // Accumulate all acceptance conditions into the merged SSCC.
	      sscc.top().is_accepting |= acc;
	      sscc.top().condition |= acc_cond;

	      sscc.rem().splice(sscc.rem().end(), rem);

	    }

	}

      if ((artificial_livelock_acc_state != 0)
	  || single_pass_emptiness_check)
405
	transform_to_single_pass_automaton(testing_aut,
406 407
					   artificial_livelock_acc_state);
    }
408

409 410 411
    ta_explicit_ptr
    build_ta(const ta_explicit_ptr& ta, bdd atomic_propositions_set_,
	     bool degeneralized,
412
	     bool single_pass_emptiness_check,
413 414
	     bool artificial_livelock_state_mode,
	     bool no_livelock)
415
    {
416

417
      std::stack<state_ta_explicit*> todo;
418
      const_twa_ptr tgba_ = ta->get_tgba();
419 420 421 422 423 424

      // build Initial states set:
      state* tgba_init_state = tgba_->get_init_state();

      bdd tgba_condition = tgba_->support_conditions(tgba_init_state);

425 426 427
      bool is_acc = false;
      if (degeneralized)
	{
428
	  twa_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
429 430
	  it->first();
	  if (!it->done())
431
	    is_acc = it->current_acceptance_conditions() != 0U;
432 433 434
	  delete it;
	}

435 436 437 438 439 440
      bdd satone_tgba_condition;
      while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
						    atomic_propositions_set_,
						    bddtrue)) != bddfalse)
	{
	  tgba_condition -= satone_tgba_condition;
441 442 443
	  state_ta_explicit* init_state = new
	    state_ta_explicit(tgba_init_state->clone(),
			      satone_tgba_condition, true, is_acc);
444 445 446 447 448 449 450
	  state_ta_explicit* s = ta->add_state(init_state);
	  assert(s == init_state);
	  ta->add_to_initial_states_set(s);

	  todo.push(init_state);
	}
      tgba_init_state->destroy();
451

452 453 454 455 456
      while (!todo.empty())
	{
	  state_ta_explicit* source = todo.top();
	  todo.pop();

457
	  twa_succ_iterator* tgba_succ_it =
458 459 460 461 462 463
	    tgba_->succ_iter(source->get_tgba_state());
	  for (tgba_succ_it->first(); !tgba_succ_it->done();
	       tgba_succ_it->next())
	    {
	      const state* tgba_state = tgba_succ_it->current_state();
	      bdd tgba_condition = tgba_succ_it->current_condition();
464
	      acc_cond::mark_t tgba_acceptance_conditions =
465 466 467 468 469 470 471 472 473 474 475
                tgba_succ_it->current_acceptance_conditions();
	      bdd satone_tgba_condition;
	      while ((satone_tgba_condition =
		      bdd_satoneset(tgba_condition,
				    atomic_propositions_set_, bddtrue))
		     != bddfalse)
		{
		  tgba_condition -= satone_tgba_condition;

		  bdd all_props = bddtrue;
		  bdd dest_condition;
476 477 478 479

		  bool is_acc = false;
		  if (degeneralized)
		  {
480
		    twa_succ_iterator* it = tgba_->succ_iter(tgba_state);
481 482
		    it->first();
		    if (!it->done())
483
		      is_acc = it->current_acceptance_conditions() != 0U;
484 485 486
		    delete it;
		  }

487 488 489 490 491 492 493
		  if (satone_tgba_condition == source->get_tgba_condition())
		    while ((dest_condition =
			    bdd_satoneset(all_props,
					  atomic_propositions_set_, bddtrue))
			   != bddfalse)
		      {
			all_props -= dest_condition;
494 495 496
			state_ta_explicit* new_dest =
			  new state_ta_explicit(tgba_state->clone(),
						dest_condition, false, is_acc);
497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
			state_ta_explicit* dest = ta->add_state(new_dest);

			if (dest != new_dest)
			  {
			    // the state dest already exists in the automaton
			    new_dest->get_tgba_state()->destroy();
			    delete new_dest;
			  }
			else
			  {
			    todo.push(dest);
			  }

			bdd cs = bdd_setxor(source->get_tgba_condition(),
					    dest->get_tgba_condition());
			ta->create_transition(source, cs,
					      tgba_acceptance_conditions, dest);
		      }
		}
	      tgba_state->destroy();
	    }
	  delete tgba_succ_it;
	}

521 522 523
      if (no_livelock)
	return ta;

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
      state_ta_explicit* artificial_livelock_acc_state = 0;

      trace << "*** build_ta: artificial_livelock_acc_state_mode = ***"
	    << artificial_livelock_state_mode << std::endl;

      if (artificial_livelock_state_mode)
	{
	  single_pass_emptiness_check = true;
	  artificial_livelock_acc_state =
	    new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue,
				  false, false, true, 0);
	  trace
	    << "*** build_ta: artificial_livelock_acc_state = ***"
	    << artificial_livelock_acc_state << std::endl;
	}

      compute_livelock_acceptance_states(ta, single_pass_emptiness_check,
					 artificial_livelock_acc_state);
      return ta;
    }
544 545
  }

546
  ta_explicit_ptr
547
  tgba_to_ta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_,
548 549 550 551
	     bool degeneralized, bool artificial_initial_state_mode,
	     bool single_pass_emptiness_check,
	     bool artificial_livelock_state_mode,
	     bool no_livelock)
552
  {
553
    ta_explicit_ptr ta;
554 555 556 557

    state* tgba_init_state = tgba_->get_init_state();
    if (artificial_initial_state_mode)
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
558 559
        state_ta_explicit* artificial_init_state =
	  new state_ta_explicit(tgba_init_state->clone(), bddfalse, true);
560

561
        ta = make_ta_explicit(tgba_, tgba_->acc().num_sets(),
562
			      artificial_init_state);
563 564 565
      }
    else
      {
566
        ta = make_ta_explicit(tgba_, tgba_->acc().num_sets());
567 568 569
      }
    tgba_init_state->destroy();

570
    // build ta automaton
571
    build_ta(ta, atomic_propositions_set_, degeneralized,
572 573
	     single_pass_emptiness_check, artificial_livelock_state_mode,
	     no_livelock);
574 575 576 577 578 579 580 581 582

    // (degeneralized=true) => TA
    if (degeneralized)
      return ta;

    // (degeneralized=false) => GTA
    // adapt a GTA to remove acceptance conditions from states
    ta::states_set_t states_set = ta->get_states_set();
    ta::states_set_t::iterator it;
583
    for (it = states_set.begin(); it != states_set.end(); ++it)
584 585 586 587 588 589 590 591
      {
        state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);

        if (state->is_accepting_state())
          {
            state_ta_explicit::transitions* trans = state->get_transitions();
            state_ta_explicit::transitions::iterator it_trans;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
592
            for (it_trans = trans->begin(); it_trans != trans->end();
593
		 ++it_trans)
594
	      (*it_trans)->acceptance_conditions = ta->acc().all_sets();
595 596 597 598 599

            state->set_accepting_state(false);
          }
      }

600 601 602
    return ta;
  }

603
  tgta_explicit_ptr
604
  tgba_to_tgta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_)
605 606
  {
    state* tgba_init_state = tgba_->get_init_state();
607 608
    auto artificial_init_state = new state_ta_explicit(tgba_init_state->clone(),
						       bddfalse, true);
609 610
    tgba_init_state->destroy();

611
    auto tgta = make_tgta_explicit(tgba_, tgba_->acc().num_sets(),
612
				   artificial_init_state);
613

614 615
    // build a Generalized TA automaton involving a single_pass_emptiness_check
    // (without an artificial livelock state):
616
    auto ta = tgta->get_ta();
617
    build_ta(ta, atomic_propositions_set_, false, true, false, false);
618

619
    trace << "***tgba_to_tgbta: POST build_ta***" << std::endl;
620

621
    // adapt a ta automata to build tgta automata :
622
    ta::states_set_t states_set = ta->get_states_set();
623
    ta::states_set_t::iterator it;
624
    twa_succ_iterator* initial_states_iter =
625
      ta->succ_iter(ta->get_artificial_initial_state());
626 627
    initial_states_iter->first();
    if (initial_states_iter->done())
628 629 630 631 632
      {
	delete initial_states_iter;
	return tgta;
      }
    bdd first_state_condition = initial_states_iter->current_condition();
633 634 635
    delete initial_states_iter;

    bdd bdd_stutering_transition = bdd_setxor(first_state_condition,
636
					      first_state_condition);
637

638
    for (it = states_set.begin(); it != states_set.end(); ++it)
639 640 641 642 643 644 645
      {
        state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);

        state_ta_explicit::transitions* trans = state->get_transitions();
        if (state->is_livelock_accepting_state())
          {
            bool trans_empty = (trans == 0 || trans->empty());
646
            if (trans_empty || state->is_accepting_state())
647
              {
648
                ta->create_transition(state, bdd_stutering_transition,
649
				      ta->acc().all_sets(), state);
650 651 652
              }
          }

653
        if (state->compare(ta->get_artificial_initial_state()))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
          ta->create_transition(state, bdd_stutering_transition,
655
				0U, state);
656

657 658
        state->set_livelock_accepting_state(false);
        state->set_accepting_state(false);
659
        trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl;
660 661
      }

662
    return tgta;
663
  }
664
}