1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010-2018, 2021 Laboratoire de Recherche et 3 // Développement de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // 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 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // 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 #include "config.h" 23 #include <iostream> 24 #ifdef TRACE 25 #define trace std::clog 26 #else 27 #define trace while (0) std::clog 28 #endif 29 30 #include <spot/twa/formula2bdd.hh> 31 #include <cassert> 32 #include <spot/twa/bddprint.hh> 33 #include <stack> 34 #include <spot/taalgos/tgba2ta.hh> 35 #include <spot/taalgos/statessetbuilder.hh> 36 #include <spot/ta/tgtaexplicit.hh> 37 38 using namespace std; 39 40 namespace spot 41 { 42 43 namespace 44 { 45 typedef std::pair<const spot::state*, twa_succ_iterator*> pair_state_iter; 46 47 static void 48 transform_to_single_pass_automaton 49 (const ta_explicit_ptr& testing_automata, 50 state_ta_explicit* artificial_livelock_acc_state = nullptr) 51 { 52 53 if (artificial_livelock_acc_state) 54 { 55 auto artificial_livelock_acc_state_added = 56 testing_automata->add_state(artificial_livelock_acc_state); 57 58 // unique artificial_livelock_acc_state 59 assert(artificial_livelock_acc_state_added 60 == artificial_livelock_acc_state); 61 (void)artificial_livelock_acc_state_added; 62 artificial_livelock_acc_state->set_livelock_accepting_state(true); 63 artificial_livelock_acc_state->free_transitions(); 64 } 65 66 ta::states_set_t states_set = testing_automata->get_states_set(); 67 ta::states_set_t::iterator it; 68 69 state_ta_explicit::transitions* transitions_to_livelock_states = 70 new state_ta_explicit::transitions; 71 72 for (it = states_set.begin(); it != states_set.end(); ++it) 73 { 74 auto source = const_cast<state_ta_explicit*> 75 (static_cast<const state_ta_explicit*>(*it)); 76 77 transitions_to_livelock_states->clear(); 78 79 state_ta_explicit::transitions* trans = source->get_transitions(); 80 state_ta_explicit::transitions::iterator it_trans; 81 82 if (trans) 83 for (it_trans = trans->begin(); it_trans != trans->end();) 84 { 85 auto dest = const_cast<state_ta_explicit*>((*it_trans)->dest); 86 87 state_ta_explicit::transitions* dest_trans = 88 dest->get_transitions(); 89 bool dest_trans_empty = !dest_trans || dest_trans->empty(); 90 91 //select transitions where a destination is a livelock state 92 // which isn't a Buchi accepting state and has successors 93 if (dest->is_livelock_accepting_state() 94 && (!dest->is_accepting_state()) && (!dest_trans_empty)) 95 transitions_to_livelock_states->push_front(*it_trans); 96 97 // optimization to have, after minimization, a unique 98 // livelock state which has no successors 99 if (dest->is_livelock_accepting_state() && (dest_trans_empty)) 100 dest->set_accepting_state(false); 101 102 ++it_trans; 103 } 104 105 for (auto* trans: *transitions_to_livelock_states) 106 testing_automata->create_transition 107 (source, trans->condition, 108 trans->acceptance_conditions, 109 artificial_livelock_acc_state ? 110 artificial_livelock_acc_state : 111 trans->dest->stuttering_reachable_livelock, true); 112 } 113 delete transitions_to_livelock_states; 114 115 for (it = states_set.begin(); it != states_set.end(); ++it) 116 { 117 state_ta_explicit* state = static_cast<state_ta_explicit*> (*it); 118 state_ta_explicit::transitions* state_trans = 119 (state)->get_transitions(); 120 bool state_trans_empty = !state_trans || state_trans->empty(); 121 122 if (state->is_livelock_accepting_state() 123 && (!state->is_accepting_state()) && (!state_trans_empty)) 124 state->set_livelock_accepting_state(false); 125 } 126 } 127 128 static void 129 compute_livelock_acceptance_states(const ta_explicit_ptr& testing_aut, 130 bool single_pass_emptiness_check, 131 state_ta_explicit* 132 artificial_livelock_acc_state) 133 { 134 // We use five main data in this algorithm: 135 // * sscc: a stack of strongly stuttering-connected components (SSCC) 136 scc_stack_ta sscc; 137 138 // * arc, a stack of acceptance conditions between each of these SCC, 139 std::stack<acc_cond::mark_t> arc; 140 141 // * h: a hash of all visited nodes, with their order, 142 // (it is called "Hash" in Couvreur's paper) 143 state_map<int> h; ///< Heap of visited states. 144 145 // * num: the number of visited nodes. Used to set the order of each 146 // visited node, 147 int num = 0; 148 149 // * todo: the depth-first search stack. This holds pairs of the 150 // form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator 151 // over the successors of STATE. In our use, ITERATOR should 152 // always be freed when TODO is popped, but STATE should not because 153 // it is also used as a key in H. 154 std::stack<pair_state_iter> todo; 155 156 // * init: the set of the depth-first search initial states 157 std::stack<const state*> init_set; 158 159 for (auto s: testing_aut->get_initial_states_set()) 160 init_set.push(s); 161 162 while (!init_set.empty()) 163 { 164 // Setup depth-first search from initial states. 165 166 { 167 auto init = down_cast<const state_ta_explicit*> (init_set.top()); 168 init_set.pop(); 169 170 if (!h.emplace(init, num + 1).second) 171 { 172 init->destroy(); 173 continue; 174 } 175 176 sscc.push(++num); 177 arc.push({}); 178 sscc.top().is_accepting 179 = testing_aut->is_accepting_state(init); 180 twa_succ_iterator* iter = testing_aut->succ_iter(init); 181 iter->first(); 182 todo.emplace(init, iter); 183 } 184 185 while (!todo.empty()) 186 { 187 auto curr = todo.top().first; 188 189 auto i = h.find(curr); 190 // If we have reached a dead component, ignore it. 191 if (i != h.end() && i->second == -1) 192 { 193 todo.pop(); 194 continue; 195 } 196 197 // We are looking at the next successor in SUCC. 198 twa_succ_iterator* succ = todo.top().second; 199 200 // If there is no more successor, backtrack. 201 if (succ->done()) 202 { 203 // We have explored all successors of state CURR. 204 205 // Backtrack TODO. 206 todo.pop(); 207 208 // fill rem with any component removed, 209 assert(i != h.end()); 210 sscc.rem().push_front(curr); 211 212 // When backtracking the root of an SSCC, we must also 213 // remove that SSCC from the ROOT stacks. We must 214 // discard from H all reachable states from this SSCC. 215 assert(!sscc.empty()); 216 if (sscc.top().index == i->second) 217 { 218 // removing states 219 bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) 220 && ((sscc.top().is_accepting) || 221 (testing_aut->acc(). 222 accepting(sscc.top().condition))); 223 trace << "*** sscc.size() = ***" << sscc.size() << '\n'; 224 for (auto j: sscc.rem()) 225 { 226 h[j] = -1; 227 228 if (is_livelock_accepting_sscc) 229 { 230 // if it is an accepting sscc add the state to 231 // G (=the livelock-accepting states set) 232 trace << "*** sscc.size() > 1: states: ***" 233 << testing_aut->format_state(j) 234 << '\n'; 235 auto livelock_accepting_state = 236 const_cast<state_ta_explicit*> 237 (down_cast<const state_ta_explicit*>(j)); 238 239 livelock_accepting_state-> 240 set_livelock_accepting_state(true); 241 242 if (single_pass_emptiness_check) 243 { 244 livelock_accepting_state 245 ->set_accepting_state(true); 246 livelock_accepting_state 247 ->stuttering_reachable_livelock 248 = livelock_accepting_state; 249 } 250 } 251 } 252 253 assert(!arc.empty()); 254 sscc.pop(); 255 arc.pop(); 256 } 257 258 // automata reduction 259 testing_aut->delete_stuttering_and_hole_successors(curr); 260 261 delete succ; 262 // Do not delete CURR: it is a key in H. 263 continue; 264 } 265 266 // Fetch the values destination state we are interested in... 267 auto dest = succ->dst(); 268 269 auto acc_cond = succ->acc(); 270 // ... and point the iterator to the next successor, for 271 // the next iteration. 272 succ->next(); 273 // We do not need SUCC from now on. 274 275 // Are we going to a new state through a stuttering transition? 276 bool is_stuttering_transition = 277 testing_aut->get_state_condition(curr) 278 == testing_aut->get_state_condition(dest); 279 auto id = h.find(dest); 280 281 // Is this a new state? 282 if (id == h.end()) 283 { 284 if (!is_stuttering_transition) 285 { 286 init_set.push(dest); 287 dest->destroy(); 288 continue; 289 } 290 291 // Number it, stack it, and register its successors 292 // for later processing. 293 h[dest] = ++num; 294 sscc.push(num); 295 arc.push(acc_cond); 296 sscc.top().is_accepting = 297 testing_aut->is_accepting_state(dest); 298 299 twa_succ_iterator* iter = testing_aut->succ_iter(dest); 300 iter->first(); 301 todo.emplace(dest, iter); 302 continue; 303 } 304 dest->destroy(); 305 306 // If we have reached a dead component, ignore it. 307 if (id->second == -1) 308 continue; 309 310 trace << "***compute_livelock_acceptance_states: CYCLE***\n"; 311 312 if (!curr->compare(id->first)) 313 { 314 auto self_loop_state = const_cast<state_ta_explicit*> 315 (down_cast<const state_ta_explicit*>(curr)); 316 317 if (testing_aut->is_accepting_state(self_loop_state) 318 || (testing_aut->acc().accepting(acc_cond))) 319 { 320 self_loop_state->set_livelock_accepting_state(true); 321 if (single_pass_emptiness_check) 322 { 323 self_loop_state->set_accepting_state(true); 324 self_loop_state->stuttering_reachable_livelock 325 = self_loop_state; 326 } 327 } 328 329 trace 330 << "***compute_livelock_acceptance_states: CYCLE: " 331 << "self_loop_state***\n"; 332 } 333 334 // Now this is the most interesting case. We have reached a 335 // state S1 which is already part of a non-dead SSCC. Any such 336 // non-dead SSCC has necessarily been crossed by our path to 337 // this state: there is a state S2 in our path which belongs 338 // to this SSCC too. We are going to merge all states between 339 // this S1 and S2 into this SSCC. 340 // 341 // This merge is easy to do because the order of the SSCC in 342 // ROOT is ascending: we just have to merge all SSCCs from the 343 // top of ROOT that have an index greater to the one of 344 // the SSCC of S2 (called the "threshold"). 345 int threshold = id->second; 346 std::list<const state*> rem; 347 bool acc = false; 348 349 while (threshold < sscc.top().index) 350 { 351 assert(!sscc.empty()); 352 assert(!arc.empty()); 353 acc |= sscc.top().is_accepting; 354 acc_cond |= sscc.top().condition; 355 acc_cond |= arc.top(); 356 rem.splice(rem.end(), sscc.rem()); 357 sscc.pop(); 358 arc.pop(); 359 } 360 361 // Note that we do not always have 362 // threshold == sscc.top().index 363 // after this loop, the SSCC whose index is threshold might have 364 // been merged with a lower SSCC. 365 366 // Accumulate all acceptance conditions into the merged SSCC. 367 sscc.top().is_accepting |= acc; 368 sscc.top().condition |= acc_cond; 369 370 sscc.rem().splice(sscc.rem().end(), rem); 371 372 } 373 374 } 375 376 if (artificial_livelock_acc_state || single_pass_emptiness_check) 377 transform_to_single_pass_automaton(testing_aut, 378 artificial_livelock_acc_state); 379 } 380 381 ta_explicit_ptr 382 build_ta(const ta_explicit_ptr& ta, bdd atomic_propositions_set_, 383 bool degeneralized, 384 bool single_pass_emptiness_check, 385 bool artificial_livelock_state_mode, 386 bool no_livelock) 387 { 388 389 std::stack<state_ta_explicit*> todo; 390 const_twa_ptr tgba_ = ta->get_tgba(); 391 392 // build Initial states set: 393 auto tgba_init_state = tgba_->get_init_state(); 394 395 bdd tgba_condition = [&]() 396 { 397 bdd cond = bddfalse; 398 for (auto i: tgba_->succ(tgba_init_state)) 399 cond |= i->cond(); 400 return cond; 401 }(); 402 403 bool is_acc = false; 404 if (degeneralized) 405 { 406 twa_succ_iterator* it = tgba_->succ_iter(tgba_init_state); 407 it->first(); 408 if (!it->done()) 409 is_acc = !!it->acc(); 410 delete it; 411 } 412 413 for (bdd satone_tgba_condition: minterms_of(tgba_condition, 414 atomic_propositions_set_)) 415 { 416 state_ta_explicit* init_state = new 417 state_ta_explicit(tgba_init_state->clone(), 418 satone_tgba_condition, true, is_acc); 419 state_ta_explicit* s = ta->add_state(init_state); 420 assert(s == init_state); 421 ta->add_to_initial_states_set(s); 422 423 todo.push(init_state); 424 } 425 tgba_init_state->destroy(); 426 427 while (!todo.empty()) 428 { 429 state_ta_explicit* source = todo.top(); 430 todo.pop(); 431 432 twa_succ_iterator* twa_succ_it = 433 tgba_->succ_iter(source->get_tgba_state()); 434 for (twa_succ_it->first(); !twa_succ_it->done(); 435 twa_succ_it->next()) 436 { 437 const state* tgba_state = twa_succ_it->dst(); 438 bdd tgba_condition = twa_succ_it->cond(); 439 acc_cond::mark_t tgba_acceptance_conditions = 440 twa_succ_it->acc(); 441 for (bdd satone_tgba_condition: 442 minterms_of(tgba_condition, atomic_propositions_set_)) 443 { 444 bool is_acc = false; 445 if (degeneralized) 446 { 447 twa_succ_iterator* it = tgba_->succ_iter(tgba_state); 448 it->first(); 449 if (!it->done()) 450 is_acc = !!it->acc(); 451 delete it; 452 } 453 454 if (satone_tgba_condition == source->get_tgba_condition()) 455 for (bdd dest_condition: 456 minterms_of(bddtrue, atomic_propositions_set_)) 457 { 458 state_ta_explicit* new_dest = 459 new state_ta_explicit(tgba_state->clone(), 460 dest_condition, false, is_acc); 461 state_ta_explicit* dest = ta->add_state(new_dest); 462 463 if (dest != new_dest) 464 { 465 // the state dest already exists in the automaton 466 new_dest->get_tgba_state()->destroy(); 467 delete new_dest; 468 } 469 else 470 { 471 todo.push(dest); 472 } 473 474 bdd cs = bdd_setxor(source->get_tgba_condition(), 475 dest->get_tgba_condition()); 476 ta->create_transition(source, cs, 477 tgba_acceptance_conditions, dest); 478 } 479 } 480 tgba_state->destroy(); 481 } 482 delete twa_succ_it; 483 } 484 485 if (no_livelock) 486 return ta; 487 488 state_ta_explicit* artificial_livelock_acc_state = nullptr; 489 490 trace << "*** build_ta: artificial_livelock_acc_state_mode = ***" 491 << artificial_livelock_state_mode << std::endl; 492 493 if (artificial_livelock_state_mode) 494 { 495 single_pass_emptiness_check = true; 496 artificial_livelock_acc_state = 497 new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue, 498 false, false, true, nullptr); 499 trace 500 << "*** build_ta: artificial_livelock_acc_state = ***" 501 << artificial_livelock_acc_state << std::endl; 502 } 503 504 compute_livelock_acceptance_states(ta, single_pass_emptiness_check, 505 artificial_livelock_acc_state); 506 return ta; 507 } 508 } 509 510 ta_explicit_ptr 511 tgba_to_ta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_, 512 bool degeneralized, bool artificial_initial_state_mode, 513 bool single_pass_emptiness_check, 514 bool artificial_livelock_state_mode, 515 bool no_livelock) 516 { 517 ta_explicit_ptr ta; 518 519 auto tgba_init_state = tgba_->get_init_state(); 520 if (artificial_initial_state_mode) 521 { 522 state_ta_explicit* artificial_init_state = 523 new state_ta_explicit(tgba_init_state->clone(), bddfalse, true); 524 525 ta = make_ta_explicit(tgba_, tgba_->acc().num_sets(), 526 artificial_init_state); 527 } 528 else 529 { 530 ta = make_ta_explicit(tgba_, tgba_->acc().num_sets()); 531 } 532 tgba_init_state->destroy(); 533 534 // build ta automaton 535 build_ta(ta, atomic_propositions_set_, degeneralized, 536 single_pass_emptiness_check, artificial_livelock_state_mode, 537 no_livelock); 538 539 // (degeneralized=true) => TA 540 if (degeneralized) 541 return ta; 542 543 // (degeneralized=false) => GTA 544 // adapt a GTA to remove acceptance conditions from states 545 ta::states_set_t states_set = ta->get_states_set(); 546 ta::states_set_t::iterator it; 547 for (it = states_set.begin(); it != states_set.end(); ++it) 548 { 549 state_ta_explicit* state = static_cast<state_ta_explicit*> (*it); 550 551 if (state->is_accepting_state()) 552 { 553 state_ta_explicit::transitions* trans = state->get_transitions(); 554 state_ta_explicit::transitions::iterator it_trans; 555 556 for (it_trans = trans->begin(); it_trans != trans->end(); 557 ++it_trans) 558 (*it_trans)->acceptance_conditions = ta->acc().all_sets(); 559 560 state->set_accepting_state(false); 561 } 562 } 563 564 return ta; 565 } 566 567 tgta_explicit_ptr 568 tgba_to_tgta(const const_twa_ptr& tgba_, bdd atomic_propositions_set_) 569 { 570 auto tgba_init_state = tgba_->get_init_state(); 571 auto artificial_init_state = new state_ta_explicit(tgba_init_state->clone(), 572 bddfalse, true); 573 tgba_init_state->destroy(); 574 575 auto tgta = make_tgta_explicit(tgba_, tgba_->acc().num_sets(), 576 artificial_init_state); 577 578 // build a Generalized TA automaton involving a single_pass_emptiness_check 579 // (without an artificial livelock state): 580 auto ta = tgta->get_ta(); 581 build_ta(ta, atomic_propositions_set_, false, true, false, false); 582 583 trace << "***tgba_to_tgbta: POST build_ta***" << std::endl; 584 585 // adapt a ta automata to build tgta automata : 586 ta::states_set_t states_set = ta->get_states_set(); 587 ta::states_set_t::iterator it; 588 twa_succ_iterator* initial_states_iter = 589 ta->succ_iter(ta->get_artificial_initial_state()); 590 initial_states_iter->first(); 591 if (initial_states_iter->done()) 592 { 593 delete initial_states_iter; 594 return tgta; 595 } 596 bdd first_state_condition = initial_states_iter->cond(); 597 delete initial_states_iter; 598 599 bdd bdd_stutering_transition = bdd_setxor(first_state_condition, 600 first_state_condition); 601 602 for (it = states_set.begin(); it != states_set.end(); ++it) 603 { 604 state_ta_explicit* state = static_cast<state_ta_explicit*> (*it); 605 606 state_ta_explicit::transitions* trans = state->get_transitions(); 607 if (state->is_livelock_accepting_state()) 608 { 609 bool trans_empty = !trans || trans->empty(); 610 if (trans_empty || state->is_accepting_state()) 611 { 612 ta->create_transition(state, bdd_stutering_transition, 613 ta->acc().all_sets(), state); 614 } 615 } 616 617 if (state->compare(ta->get_artificial_initial_state())) 618 ta->create_transition(state, bdd_stutering_transition, 619 {}, state); 620 621 state->set_livelock_accepting_state(false); 622 state->set_accepting_state(false); 623 trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl; 624 } 625 626 return tgta; 627 } 628 } 629