1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010-2016, 2018 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/taalgos/emptinessta.hh> 31 #include <spot/misc/memusage.hh> 32 #include <cstdlib> 33 #include <spot/twa/bddprint.hh> 34 35 namespace spot 36 { 37 ta_check(const const_ta_product_ptr & a,option_map o)38 ta_check::ta_check(const const_ta_product_ptr& a, option_map o) : 39 a_(a), o_(o) 40 { 41 is_full_2_pass_ = o.get("is_full_2_pass", 0); 42 } 43 ~ta_check()44 ta_check::~ta_check() 45 { 46 } 47 48 bool check(bool disable_second_pass,bool disable_heuristic_for_livelock_detection)49 ta_check::check(bool disable_second_pass, 50 bool disable_heuristic_for_livelock_detection) 51 { 52 53 // We use five main data in this algorithm: 54 55 // * scc: (attribute) a stack of strongly connected components (SCC) 56 57 // * arc, a stack of acceptance conditions between each of these SCC, 58 std::stack<acc_cond::mark_t> arc; 59 60 // * h: a hash of all visited nodes, with their order, 61 // (it is called "Hash" in Couvreur's paper) 62 hash_type h; 63 64 // * num: the number of visited nodes. Used to set the order of each 65 // visited node, 66 int num = 1; 67 68 // * todo: the depth-first search stack. This holds pairs of the 69 // form (STATE, ITERATOR) where ITERATOR is a ta_succ_iterator_product 70 // over the successors of STATE. In our use, ITERATOR should 71 // always be freed when TODO is popped, but STATE should not because 72 // it is also used as a key in H. 73 std::stack<pair_state_iter> todo; 74 75 trace 76 << "PASS 1" << std::endl; 77 78 state_map<std::set<const state*, state_ptr_less_than>> liveset; 79 80 std::stack<spot::state*> livelock_roots; 81 82 bool livelock_acceptance_states_not_found = true; 83 84 bool activate_heuristic = !disable_heuristic_for_livelock_detection 85 && (is_full_2_pass_ == disable_second_pass); 86 87 // Setup depth-first search from initial states. 88 auto& ta_ = a_->get_ta(); 89 auto& kripke_ = a_->get_kripke(); 90 auto kripke_init_state = kripke_->get_init_state(); 91 bdd kripke_init_state_condition = kripke_->state_condition( 92 kripke_init_state); 93 94 auto artificial_initial_state = ta_->get_artificial_initial_state(); 95 96 ta_succ_iterator* ta_init_it_ = ta_->succ_iter(artificial_initial_state, 97 kripke_init_state_condition); 98 kripke_init_state->destroy(); 99 for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next()) 100 { 101 102 state_ta_product* init = new state_ta_product( 103 (ta_init_it_->dst()), kripke_init_state->clone()); 104 105 if (!h.emplace(init, num + 1).second) 106 { 107 init->destroy(); 108 continue; 109 } 110 111 scc.push(++num); 112 arc.push({}); 113 114 ta_succ_iterator_product* iter = a_->succ_iter(init); 115 iter->first(); 116 todo.emplace(init, iter); 117 118 inc_depth(); 119 120 //push potential root of live-lock accepting cycle 121 if (activate_heuristic && a_->is_livelock_accepting_state(init)) 122 livelock_roots.push(init); 123 124 while (!todo.empty()) 125 { 126 auto curr = todo.top().first; 127 128 // We are looking at the next successor in SUCC. 129 ta_succ_iterator_product* succ = todo.top().second; 130 131 // If there is no more successor, backtrack. 132 if (succ->done()) 133 { 134 // We have explored all successors of state CURR. 135 136 137 // Backtrack TODO. 138 todo.pop(); 139 dec_depth(); 140 trace << "PASS 1 : backtrack\n"; 141 142 if (a_->is_livelock_accepting_state(curr) 143 && !a_->is_accepting_state(curr)) 144 { 145 livelock_acceptance_states_not_found = false; 146 trace << "PASS 1 : livelock accepting state found\n"; 147 } 148 149 // fill rem with any component removed, 150 auto i = h.find(curr); 151 assert(i != h.end()); 152 153 scc.rem().push_front(curr); 154 inc_depth(); 155 156 // set the h value of the Backtracked state to negative value. 157 i->second = -std::abs(i->second); 158 159 // Backtrack livelock_roots. 160 if (activate_heuristic && !livelock_roots.empty() 161 && !livelock_roots.top()->compare(curr)) 162 livelock_roots.pop(); 163 164 // When backtracking the root of an SSCC, we must also 165 // remove that SSCC from the ROOT stacks. We must 166 // discard from H all reachable states from this SSCC. 167 assert(!scc.empty()); 168 if (scc.top().index == std::abs(i->second)) 169 { 170 // removing states 171 for (auto j: scc.rem()) 172 h[j] = -1; 173 dec_depth(scc.rem().size()); 174 scc.pop(); 175 assert(!arc.empty()); 176 arc.pop(); 177 178 } 179 180 delete succ; 181 // Do not delete CURR: it is a key in H. 182 continue; 183 } 184 185 // We have a successor to look at. 186 inc_transitions(); 187 trace << "PASS 1: transition\n"; 188 // Fetch the values destination state we are interested in... 189 state* dest = succ->dst(); 190 191 auto acc_cond = succ->acc(); 192 193 bool curr_is_livelock_hole_state_in_ta_component = 194 (a_->is_hole_state_in_ta_component(curr)) 195 && a_->is_livelock_accepting_state(curr); 196 197 // May be Buchi accepting scc or livelock accepting scc 198 // (contains a livelock accepting state that have no 199 // successors in TA). 200 scc.top().is_accepting = (a_->is_accepting_state(curr) 201 && (!succ->is_stuttering_transition() 202 || a_->is_livelock_accepting_state(curr))) 203 || curr_is_livelock_hole_state_in_ta_component; 204 205 bool is_stuttering_transition = succ->is_stuttering_transition(); 206 207 // ... and point the iterator to the next successor, for 208 // the next iteration. 209 succ->next(); 210 // We do not need SUCC from now on. 211 212 // Are we going to a new state? 213 auto p = h.emplace(dest, num + 1); 214 if (p.second) 215 { 216 // Number it, stack it, and register its successors 217 // for later processing. 218 scc.push(++num); 219 arc.push(acc_cond); 220 221 ta_succ_iterator_product* iter = a_->succ_iter(dest); 222 iter->first(); 223 todo.emplace(dest, iter); 224 inc_depth(); 225 226 //push potential root of live-lock accepting cycle 227 if (activate_heuristic && a_->is_livelock_accepting_state(dest) 228 && !is_stuttering_transition) 229 livelock_roots.push(dest); 230 231 continue; 232 } 233 234 // If we have reached a dead component, ignore it. 235 if (p.first->second == -1) 236 continue; 237 238 // Now this is the most interesting case. We have reached a 239 // state S1 which is already part of a non-dead SSCC. Any such 240 // non-dead SSCC has necessarily been crossed by our path to 241 // this state: there is a state S2 in our path which belongs 242 // to this SSCC too. We are going to merge all states between 243 // this S1 and S2 into this SSCC. 244 // 245 // This merge is easy to do because the order of the SSCC in 246 // ROOT is ascending: we just have to merge all SSCCs from the 247 // top of ROOT that have an index greater to the one of 248 // the SSCC of S2 (called the "threshold"). 249 int threshold = std::abs(p.first->second); 250 std::list<const state*> rem; 251 bool acc = false; 252 253 trace << "***PASS 1: CYCLE***\n"; 254 255 while (threshold < scc.top().index) 256 { 257 assert(!scc.empty()); 258 assert(!arc.empty()); 259 260 acc |= scc.top().is_accepting; 261 acc_cond |= scc.top().condition; 262 acc_cond |= arc.top(); 263 264 rem.splice(rem.end(), scc.rem()); 265 scc.pop(); 266 arc.pop(); 267 268 } 269 270 // Note that we do not always have 271 // threshold == scc.top().index 272 // after this loop, the SSCC whose index is threshold might have 273 // been merged with a lower SSCC. 274 275 // Accumulate all acceptance conditions into the merged SSCC. 276 scc.top().is_accepting |= acc; 277 scc.top().condition |= acc_cond; 278 279 scc.rem().splice(scc.rem().end(), rem); 280 bool is_accepting_sscc = scc.top().is_accepting 281 || a_->acc().accepting(scc.top().condition); 282 283 if (is_accepting_sscc) 284 { 285 trace 286 << "PASS 1: SUCCESS: a_->is_livelock_accepting_state(curr): " 287 << a_->is_livelock_accepting_state(curr) << '\n'; 288 trace 289 << "PASS 1: scc.top().condition : " 290 << scc.top().condition << '\n'; 291 trace 292 << "PASS 1: a_->acc().all_sets() : " 293 << (a_->acc().all_sets()) << '\n'; 294 trace 295 << ("PASS 1 CYCLE and accepting? ") 296 << a_->acc().accepting(scc.top().condition) 297 << std::endl; 298 clear(h, todo, ta_init_it_); 299 return true; 300 } 301 302 //ADDLINKS 303 if (activate_heuristic && a_->is_livelock_accepting_state(curr) 304 && is_stuttering_transition) 305 { 306 trace << "PASS 1: heuristic livelock detection \n"; 307 const state* dest = p.first->first; 308 std::set<const state*, state_ptr_less_than> liveset_dest = 309 liveset[dest]; 310 311 std::set<const state*, state_ptr_less_than> liveset_curr = 312 liveset[curr]; 313 314 int h_livelock_root = 0; 315 if (!livelock_roots.empty()) 316 h_livelock_root = h[livelock_roots.top()]; 317 318 if (heuristic_livelock_detection(dest, h, h_livelock_root, 319 liveset_curr)) 320 { 321 clear(h, todo, ta_init_it_); 322 return true; 323 } 324 325 for (const state* succ: liveset_dest) 326 if (heuristic_livelock_detection(succ, h, h_livelock_root, 327 liveset_curr)) 328 { 329 clear(h, todo, ta_init_it_); 330 return true; 331 } 332 } 333 } 334 335 } 336 337 clear(h, todo, ta_init_it_); 338 339 if (disable_second_pass || livelock_acceptance_states_not_found) 340 return false; 341 342 return livelock_detection(a_); 343 } 344 345 bool heuristic_livelock_detection(const state * u,hash_type & h,int h_livelock_root,std::set<const state *,state_ptr_less_than> liveset_curr)346 ta_check::heuristic_livelock_detection(const state * u, 347 hash_type& h, int h_livelock_root, std::set<const state*, 348 state_ptr_less_than> liveset_curr) 349 { 350 int hu = h[u]; 351 352 if (hu > 0) 353 { 354 355 if (hu >= h_livelock_root) 356 { 357 trace << "PASS 1: heuristic livelock detection SUCCESS\n"; 358 return true; 359 } 360 361 liveset_curr.insert(u); 362 } 363 return false; 364 } 365 366 bool livelock_detection(const const_ta_product_ptr & t)367 ta_check::livelock_detection(const const_ta_product_ptr& t) 368 { 369 // We use five main data in this algorithm: 370 371 // * sscc: a stack of strongly stuttering-connected components (SSCC) 372 373 374 // * h: a hash of all visited nodes, with their order, 375 // (it is called "Hash" in Couvreur's paper) 376 hash_type h; 377 378 // * num: the number of visited nodes. Used to set the order of each 379 // visited node, 380 381 trace 382 << "PASS 2" << std::endl; 383 384 int num = 0; 385 386 // * todo: the depth-first search stack. This holds pairs of the 387 // form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator 388 // over the successors of STATE. In our use, ITERATOR should 389 // always be freed when TODO is popped, but STATE should not because 390 // it is also used as a key in H. 391 std::stack<pair_state_iter> todo; 392 393 // * init: the set of the depth-first search initial states 394 std::queue<const spot::state*> ta_init_it_; 395 396 auto init_states_set = a_->get_initial_states_set(); 397 for (auto init_state: init_states_set) 398 ta_init_it_.push(init_state); 399 400 while (!ta_init_it_.empty()) 401 { 402 // Setup depth-first search from initial states. 403 { 404 auto init = ta_init_it_.front(); 405 ta_init_it_.pop(); 406 407 if (!h.emplace(init, num + 1).second) 408 { 409 init->destroy(); 410 continue; 411 } 412 413 sscc.push(num); 414 sscc.top().is_accepting = t->is_livelock_accepting_state(init); 415 ta_succ_iterator_product* iter = t->succ_iter(init); 416 iter->first(); 417 todo.emplace(init, iter); 418 inc_depth(); 419 } 420 421 while (!todo.empty()) 422 { 423 auto curr = todo.top().first; 424 425 // We are looking at the next successor in SUCC. 426 ta_succ_iterator_product* succ = todo.top().second; 427 428 // If there is no more successor, backtrack. 429 if (succ->done()) 430 { 431 // We have explored all successors of state CURR. 432 433 // Backtrack TODO. 434 todo.pop(); 435 dec_depth(); 436 trace << "PASS 2 : backtrack\n"; 437 438 // fill rem with any component removed, 439 auto i = h.find(curr); 440 assert(i != h.end()); 441 442 sscc.rem().push_front(curr); 443 inc_depth(); 444 445 // When backtracking the root of an SSCC, we must also 446 // remove that SSCC from the ROOT stacks. We must 447 // discard from H all reachable states from this SSCC. 448 assert(!sscc.empty()); 449 if (sscc.top().index == i->second) 450 { 451 // removing states 452 for (auto j: sscc.rem()) 453 h[j] = -1; 454 dec_depth(sscc.rem().size()); 455 sscc.pop(); 456 } 457 458 delete succ; 459 // Do not delete CURR: it is a key in H. 460 461 continue; 462 } 463 464 // We have a successor to look at. 465 inc_transitions(); 466 trace << "PASS 2 : transition\n"; 467 // Fetch the values destination state we are interested in... 468 state* dest = succ->dst(); 469 470 bool is_stuttering_transition = succ->is_stuttering_transition(); 471 // ... and point the iterator to the next successor, for 472 // the next iteration. 473 succ->next(); 474 // We do not need SUCC from now on. 475 476 auto i = h.find(dest); 477 478 // Is this a new state? 479 if (i == h.end()) 480 { 481 482 // Are we going to a new state through a stuttering transition? 483 484 if (!is_stuttering_transition) 485 { 486 ta_init_it_.push(dest); 487 continue; 488 } 489 490 // Number it, stack it, and register its successors 491 // for later processing. 492 h[dest] = ++num; 493 sscc.push(num); 494 sscc.top().is_accepting = t->is_livelock_accepting_state(dest); 495 496 ta_succ_iterator_product* iter = t->succ_iter(dest); 497 iter->first(); 498 todo.emplace(dest, iter); 499 inc_depth(); 500 continue; 501 } 502 else 503 { 504 dest->destroy(); 505 } 506 507 // If we have reached a dead component, ignore it. 508 if (i->second == -1) 509 continue; 510 511 //self loop state 512 if (!curr->compare(i->first)) 513 if (t->is_livelock_accepting_state(curr)) 514 { 515 clear(h, todo, ta_init_it_); 516 trace << "PASS 2: SUCCESS\n"; 517 return true; 518 } 519 520 // Now this is the most interesting case. We have reached a 521 // state S1 which is already part of a non-dead SSCC. Any such 522 // non-dead SSCC has necessarily been crossed by our path to 523 // this state: there is a state S2 in our path which belongs 524 // to this SSCC too. We are going to merge all states between 525 // this S1 and S2 into this SSCC. 526 // 527 // This merge is easy to do because the order of the SSCC in 528 // ROOT is ascending: we just have to merge all SSCCs from the 529 // top of ROOT that have an index greater to the one of 530 // the SSCC of S2 (called the "threshold"). 531 int threshold = i->second; 532 std::list<const state*> rem; 533 bool acc = false; 534 535 while (threshold < sscc.top().index) 536 { 537 assert(!sscc.empty()); 538 539 acc |= sscc.top().is_accepting; 540 541 rem.splice(rem.end(), sscc.rem()); 542 sscc.pop(); 543 544 } 545 // Note that we do not always have 546 // threshold == sscc.top().index 547 // after this loop, the SSCC whose index is threshold might have 548 // been merged with a lower SSCC. 549 550 // Accumulate all acceptance conditions into the merged SSCC. 551 sscc.top().is_accepting |= acc; 552 553 sscc.rem().splice(sscc.rem().end(), rem); 554 if (sscc.top().is_accepting) 555 { 556 clear(h, todo, ta_init_it_); 557 trace 558 << "PASS 2: SUCCESS" << std::endl; 559 return true; 560 } 561 } 562 563 } 564 clear(h, todo, ta_init_it_); 565 return false; 566 } 567 568 void clear(hash_type & h,std::stack<pair_state_iter> todo,std::queue<const spot::state * > init_states)569 ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo, 570 std::queue<const spot::state*> init_states) 571 { 572 573 set_states(states() + h.size()); 574 575 while (!init_states.empty()) 576 { 577 a_->free_state(init_states.front()); 578 init_states.pop(); 579 } 580 581 // Release all iterators in TODO. 582 while (!todo.empty()) 583 { 584 delete todo.top().second; 585 todo.pop(); 586 dec_depth(); 587 } 588 } 589 590 void clear(hash_type & h,std::stack<pair_state_iter> todo,spot::ta_succ_iterator * init_states_it)591 ta_check::clear(hash_type& h, std::stack<pair_state_iter> todo, 592 spot::ta_succ_iterator* init_states_it) 593 { 594 595 set_states(states() + h.size()); 596 597 delete init_states_it; 598 599 // Release all iterators in TODO. 600 while (!todo.empty()) 601 { 602 delete todo.top().second; 603 todo.pop(); 604 dec_depth(); 605 } 606 } 607 608 std::ostream& print_stats(std::ostream & os) const609 ta_check::print_stats(std::ostream& os) const 610 { 611 // ecs_->print_stats(os); 612 os << states() << " unique states visited" << std::endl; 613 614 //TODO sscc; 615 os << scc.size() << " strongly connected components in search stack" 616 << std::endl; 617 os << transitions() << " transitions explored" << std::endl; 618 os << max_depth() << " items max in DFS search stack" << std::endl; 619 return os; 620 } 621 622 ////////////////////////////////////////////////////////////////////// 623 624 625 } 626