1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2021 Laboratoire de Recherche et Développement de 3 // 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 #include "config.h" 21 #include <spot/twaalgos/stutter.hh> 22 #include <spot/twa/twa.hh> 23 #include <spot/misc/hash.hh> 24 #include <spot/misc/hashfunc.hh> 25 #include <spot/tl/apcollect.hh> 26 #include <spot/twaalgos/translate.hh> 27 #include <spot/tl/remove_x.hh> 28 #include <spot/twaalgos/product.hh> 29 #include <spot/twaalgos/ltl2tgba_fm.hh> 30 #include <spot/twaalgos/isdet.hh> 31 #include <spot/twaalgos/complement.hh> 32 #include <spot/twaalgos/remfin.hh> 33 #include <spot/twaalgos/sccinfo.hh> 34 #include <spot/twaalgos/word.hh> 35 #include <spot/twa/twaproduct.hh> 36 #include <spot/twa/bddprint.hh> 37 #include <deque> 38 #include <unordered_map> 39 #include <unordered_set> 40 #include <vector> 41 #include <numeric> 42 43 namespace spot 44 { 45 namespace 46 { 47 class state_tgbasl final: public state 48 { 49 public: state_tgbasl(const state * s,bdd cond)50 state_tgbasl(const state* s, bdd cond) : s_(s), cond_(cond) 51 { 52 } 53 54 virtual ~state_tgbasl()55 ~state_tgbasl() 56 { 57 s_->destroy(); 58 } 59 60 virtual int compare(const state * other) const61 compare(const state* other) const override 62 { 63 const state_tgbasl* o = 64 down_cast<const state_tgbasl*>(other); 65 int res = s_->compare(o->real_state()); 66 if (res != 0) 67 return res; 68 return cond_.id() - o->cond_.id(); 69 } 70 71 virtual size_t hash() const72 hash() const override 73 { 74 return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id()); 75 } 76 77 virtual clone() const78 state_tgbasl* clone() const override 79 { 80 return new state_tgbasl(s_, cond_); 81 } 82 83 const state* real_state() const84 real_state() const 85 { 86 return s_; 87 } 88 89 bdd cond() const90 cond() const 91 { 92 return cond_; 93 } 94 95 private: 96 const state* s_; 97 bdd cond_; 98 }; 99 100 class twasl_succ_iterator final : public twa_succ_iterator 101 { 102 public: twasl_succ_iterator(twa_succ_iterator * it,const state_tgbasl * state,bdd_dict_ptr d,bdd atomic_propositions)103 twasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state, 104 bdd_dict_ptr d, bdd atomic_propositions) 105 : it_(it), state_(state), aps_(atomic_propositions), d_(d) 106 { 107 } 108 109 virtual ~twasl_succ_iterator()110 ~twasl_succ_iterator() 111 { 112 delete it_; 113 } 114 115 // iteration 116 117 virtual bool first()118 first() override 119 { 120 loop_ = false; 121 done_ = false; 122 need_loop_ = true; 123 if (it_->first()) 124 { 125 cond_ = it_->cond(); 126 next_edge(); 127 } 128 return true; 129 } 130 131 virtual bool next()132 next() override 133 { 134 if (cond_ != bddfalse) 135 { 136 next_edge(); 137 return true; 138 } 139 if (!it_->next()) 140 { 141 if (loop_ || !need_loop_) 142 done_ = true; 143 loop_ = true; 144 return !done_; 145 } 146 else 147 { 148 cond_ = it_->cond(); 149 next_edge(); 150 return true; 151 } 152 } 153 154 virtual bool done() const155 done() const override 156 { 157 return it_->done() && done_; 158 } 159 160 // inspection 161 162 virtual state_tgbasl* dst() const163 dst() const override 164 { 165 if (loop_) 166 return new state_tgbasl(state_->real_state(), state_->cond()); 167 return new state_tgbasl(it_->dst(), one_); 168 } 169 170 virtual bdd cond() const171 cond() const override 172 { 173 if (loop_) 174 return state_->cond(); 175 return one_; 176 } 177 178 virtual acc_cond::mark_t acc() const179 acc() const override 180 { 181 if (loop_) 182 return {}; 183 return it_->acc(); 184 } 185 186 private: 187 void next_edge()188 next_edge() 189 { 190 one_ = bdd_satoneset(cond_, aps_, bddfalse); 191 cond_ -= one_; 192 if (need_loop_ && (state_->cond() == one_) 193 && (state_ == it_->dst())) 194 need_loop_ = false; 195 } 196 197 twa_succ_iterator* it_; 198 const state_tgbasl* state_; 199 bdd cond_; 200 bdd one_; 201 bdd aps_; 202 bdd_dict_ptr d_; 203 bool loop_; 204 bool need_loop_; 205 bool done_; 206 }; 207 208 209 class tgbasl final : public twa 210 { 211 public: tgbasl(const_twa_ptr a)212 tgbasl(const_twa_ptr a) 213 : twa(a->get_dict()), a_(a) 214 { 215 copy_ap_of(a); 216 copy_acceptance_of(a_); 217 } 218 get_init_state() const219 virtual const state* get_init_state() const override 220 { 221 return new state_tgbasl(a_->get_init_state(), bddfalse); 222 } 223 succ_iter(const state * state) const224 virtual twa_succ_iterator* succ_iter(const state* state) const override 225 { 226 const state_tgbasl* s = down_cast<const state_tgbasl*>(state); 227 return new twasl_succ_iterator(a_->succ_iter(s->real_state()), s, 228 a_->get_dict(), ap_vars()); 229 } 230 format_state(const state * state) const231 virtual std::string format_state(const state* state) const override 232 { 233 const state_tgbasl* s = down_cast<const state_tgbasl*>(state); 234 return (a_->format_state(s->real_state()) 235 + ", " 236 + bdd_format_formula(a_->get_dict(), s->cond())); 237 } 238 239 private: 240 const_twa_ptr a_; 241 }; 242 243 typedef std::shared_ptr<tgbasl> tgbasl_ptr; 244 make_tgbasl(const const_twa_ptr & aut)245 inline tgbasl_ptr make_tgbasl(const const_twa_ptr& aut) 246 { 247 return std::make_shared<tgbasl>(aut); 248 } 249 250 251 252 typedef std::pair<unsigned, bdd> stutter_state; 253 254 struct stutter_state_hash 255 { 256 size_t operator ()spot::__anondececfa60111::stutter_state_hash257 operator()(const stutter_state& s) const noexcept 258 { 259 return wang32_hash(s.first) ^ wang32_hash(s.second.id()); 260 } 261 }; 262 263 // Associate the stutter state to its number. 264 typedef std::unordered_map<stutter_state, unsigned, 265 stutter_state_hash> ss2num_map; 266 267 // Queue of state to be processed. 268 typedef std::deque<stutter_state> queue_t; 269 } 270 271 twa_graph_ptr sl(const_twa_graph_ptr a)272 sl(const_twa_graph_ptr a) 273 { 274 // The result automaton uses numbered states. 275 twa_graph_ptr res = make_twa_graph(a->get_dict()); 276 bdd atomic_propositions = a->ap_vars(); 277 // We use the same BDD variables as the input. 278 res->copy_ap_of(a); 279 res->copy_acceptance_of(a); 280 281 // We are going to create self-loop labeled by {}, 282 // and those should not be accepting. If they are, 283 // we need to upgrade the acceptance condition. 284 acc_cond::mark_t toadd = {}; 285 if (res->acc().accepting({})) 286 { 287 unsigned ns = res->num_sets(); 288 auto na = res->get_acceptance() & acc_cond::acc_code::inf({ns}); 289 res->set_acceptance(ns + 1, na); 290 toadd = {ns}; 291 } 292 293 // These maps make it possible to convert stutter_state to number 294 // and vice-versa. 295 ss2num_map ss2num; 296 297 queue_t todo; 298 299 unsigned s0 = a->get_init_state_number(); 300 stutter_state s(s0, bddfalse); 301 ss2num[s] = 0; 302 res->new_state(); 303 todo.emplace_back(s); 304 305 while (!todo.empty()) 306 { 307 s = todo.front(); 308 todo.pop_front(); 309 unsigned src = ss2num[s]; 310 311 bool self_loop_needed = true; 312 313 for (auto& t : a->out(s.first)) 314 { 315 bdd all = t.cond; 316 for (bdd one: minterms_of(t.cond, atomic_propositions)) 317 { 318 stutter_state d(t.dst, one); 319 320 auto r = ss2num.emplace(d, ss2num.size()); 321 unsigned dest = r.first->second; 322 323 if (r.second) 324 { 325 todo.emplace_back(d); 326 unsigned u = res->new_state(); 327 assert(u == dest); 328 (void)u; 329 } 330 331 // Create the edge. 332 res->new_edge(src, dest, one, t.acc | toadd); 333 334 if (src == dest) 335 self_loop_needed = false; 336 } 337 } 338 339 if (self_loop_needed && s.second != bddfalse) 340 res->new_edge(src, src, s.second, {}); 341 } 342 res->merge_edges(); 343 return res; 344 } 345 346 twa_graph_ptr sl2_inplace(twa_graph_ptr a)347 sl2_inplace(twa_graph_ptr a) 348 { 349 // We are going to create self-loop labeled by {}, 350 // and those should not be accepting. If they are, 351 // we need to upgrade the acceptance condition. 352 if (a->acc().accepting({})) 353 { 354 unsigned ns = a->num_sets(); 355 auto na = a->get_acceptance() & acc_cond::acc_code::inf({ns}); 356 a->set_acceptance(ns + 1, na); 357 acc_cond::mark_t toadd = {ns}; 358 for (auto& e: a->edges()) 359 e.acc |= toadd; 360 } 361 362 // The self-loops we add should not be accepting, so try to find 363 // an unsat mark, and upgrade the acceptance condition if 364 // necessary. 365 // 366 // UM is a pair (bool, mark). If the Boolean is false, the 367 // acceptance is always satisfiable. Otherwise, MARK is an 368 // example of unsatisfiable mark. 369 auto um = a->acc().unsat_mark(); 370 if (!um.first) 371 { 372 auto m = a->set_buchi(); 373 for (auto& e: a->edges()) 374 e.acc = m; 375 um.second = {}; 376 } 377 acc_cond::mark_t unsat = um.second; 378 379 bdd atomic_propositions = a->ap_vars(); 380 unsigned num_states = a->num_states(); 381 unsigned num_edges = a->num_edges(); 382 std::vector<bdd> selfloops(num_states, bddfalse); 383 std::map<std::pair<unsigned, int>, unsigned> newstates; 384 // Record all the conditions for which we can selfloop on each 385 // state. 386 for (auto& t: a->edges()) 387 if (t.src == t.dst) 388 selfloops[t.src] |= t.cond; 389 for (unsigned t = 1; t <= num_edges; ++t) 390 { 391 auto& td = a->edge_storage(t); 392 if (a->is_dead_edge(td)) 393 continue; 394 395 unsigned src = td.src; 396 unsigned dst = td.dst; 397 if (src != dst) 398 { 399 bdd all = td.cond; 400 // If there is a self-loop with the whole condition on 401 // either end of the edge, do not bother with it. 402 if (bdd_implies(all, selfloops[src]) 403 || bdd_implies(all, selfloops[dst])) 404 continue; 405 // Do not use td in the loop because the new_edge() 406 // might invalidate it. 407 auto acc = td.acc; 408 for (bdd one: minterms_of(all, atomic_propositions)) 409 { 410 // Skip if there is a loop for this particular letter. 411 if (bdd_implies(one, selfloops[src]) 412 || bdd_implies(one, selfloops[dst])) 413 continue; 414 auto p = newstates.emplace(std::make_pair(dst, one.id()), 0); 415 if (p.second) 416 p.first->second = a->new_state(); 417 unsigned tmp = p.first->second; // intermediate state 418 unsigned i = a->new_edge(src, tmp, one, acc); 419 assert(i > num_edges); 420 i = a->new_edge(tmp, tmp, one, unsat); 421 assert(i > num_edges); 422 // unsat acceptance here to preserve the state-based property. 423 i = a->new_edge(tmp, dst, one, unsat); 424 assert(i > num_edges); 425 (void)i; 426 } 427 } 428 } 429 if (num_states != a->num_states()) 430 a->prop_keep({true, // state_based 431 false, // inherently_weak 432 false, false, // deterministic 433 true, // complete 434 false, // stutter inv. 435 }); 436 a->merge_edges(); 437 return a; 438 } 439 440 twa_graph_ptr sl2(const_twa_graph_ptr a)441 sl2(const_twa_graph_ptr a) 442 { 443 return sl2_inplace(make_twa_graph(a, twa::prop_set::all())); 444 } 445 446 twa_graph_ptr closure_inplace(twa_graph_ptr a)447 closure_inplace(twa_graph_ptr a) 448 { 449 // In the fin-less version of the closure, we can merge edges that 450 // have the same src, letter, and destination by taking the union 451 // of their marks. If some Fin() is used, we cannot do that. 452 bool fin_less = !a->acc().uses_fin_acceptance(); 453 454 a->prop_keep({false, // state_based 455 false, // inherently_weak 456 false, false, // deterministic 457 true, // complete 458 false, // stutter inv. 459 }); 460 461 unsigned n = a->num_states(); 462 std::vector<unsigned> todo; 463 std::vector<std::vector<unsigned> > dst2trans(n); 464 465 for (unsigned state = 0; state < n; ++state) 466 { 467 auto trans = a->out(state); 468 469 for (auto it = trans.begin(); it != trans.end(); ++it) 470 { 471 todo.emplace_back(it.trans()); 472 dst2trans[it->dst].emplace_back(it.trans()); 473 } 474 475 while (!todo.empty()) 476 { 477 auto t1 = a->edge_storage(todo.back()); 478 todo.pop_back(); 479 480 for (auto& t2 : a->out(t1.dst)) 481 { 482 bdd cond = t1.cond & t2.cond; 483 if (cond != bddfalse) 484 { 485 bool need_new_trans = true; 486 acc_cond::mark_t acc = t1.acc | t2.acc; 487 for (auto& t: dst2trans[t2.dst]) 488 { 489 auto& ts = a->edge_storage(t); 490 if (acc == ts.acc) 491 { 492 if (!bdd_implies(cond, ts.cond)) 493 { 494 ts.cond |= cond; 495 if (std::find(todo.begin(), todo.end(), t) 496 == todo.end()) 497 todo.emplace_back(t); 498 } 499 need_new_trans = false; 500 break; 501 } 502 else if (fin_less && cond == ts.cond) 503 { 504 acc |= ts.acc; 505 if (ts.acc != acc) 506 { 507 ts.acc = acc; 508 if (std::find(todo.begin(), todo.end(), t) 509 == todo.end()) 510 todo.emplace_back(t); 511 } 512 need_new_trans = false; 513 break; 514 } 515 } 516 if (need_new_trans) 517 { 518 // Load t2.dst first, because t2 can be 519 // invalidated by new_edge(). 520 auto dst = t2.dst; 521 auto i = a->new_edge(state, dst, cond, acc); 522 dst2trans[dst].emplace_back(i); 523 todo.emplace_back(i); 524 } 525 } 526 } 527 } 528 for (auto& it: dst2trans) 529 it.clear(); 530 } 531 return a; 532 } 533 534 twa_graph_ptr closure(const_twa_graph_ptr a)535 closure(const_twa_graph_ptr a) 536 { 537 return closure_inplace(make_twa_graph(a, twa::prop_set::all())); 538 } 539 540 namespace 541 { 542 // The stutter check algorithm to use can be overridden via an 543 // environment variable. default_stutter_check_algorithm()544 static int default_stutter_check_algorithm() 545 { 546 static const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); 547 if (stutter_check) 548 { 549 char* endptr; 550 long res = strtol(stutter_check, &endptr, 10); 551 if (*endptr || res < 0 || res > 9) 552 throw 553 std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); 554 return res; 555 } 556 else 557 { 558 return 8; // The best variant, according to our benchmarks. 559 } 560 } 561 } 562 563 namespace 564 { 565 // The own_f and own_nf tell us whether we can modify the aut_f 566 // and aut_nf automata inplace. do_si_check(const_twa_graph_ptr aut_f,bool own_f,const_twa_graph_ptr aut_nf,bool own_nf,int algo)567 static bool do_si_check(const_twa_graph_ptr aut_f, bool own_f, 568 const_twa_graph_ptr aut_nf, bool own_nf, 569 int algo) 570 { 571 auto cl = [](const_twa_graph_ptr a, bool own) { 572 if (own) 573 return closure_inplace(std::const_pointer_cast<twa_graph> 574 (std::move(a))); 575 return closure(std::move(a)); 576 }; 577 auto sl_2 = [](const_twa_graph_ptr a, bool own) { 578 if (own) 579 return sl2_inplace(std::const_pointer_cast<twa_graph>(std::move(a))); 580 return sl2(std::move(a)); 581 }; 582 583 switch (algo) 584 { 585 case 1: // sl(aut_f) x sl(aut_nf) 586 return product(sl(std::move(aut_f)), 587 sl(std::move(aut_nf)))->is_empty(); 588 case 2: // sl(cl(aut_f)) x aut_nf 589 return product(sl(cl(std::move(aut_f), own_f)), 590 std::move(aut_nf))->is_empty(); 591 case 3: // (cl(sl(aut_f)) x aut_nf 592 return product(closure_inplace(sl(std::move(aut_f))), 593 std::move(aut_nf))->is_empty(); 594 case 4: // sl2(aut_f) x sl2(aut_nf) 595 return product(sl_2(std::move(aut_f), own_f), 596 sl_2(std::move(aut_nf), own_nf)) 597 ->is_empty(); 598 case 5: // sl2(cl(aut_f)) x aut_nf 599 return product(sl2_inplace(cl(std::move(aut_f), own_f)), 600 std::move(aut_nf))->is_empty(); 601 case 6: // (cl(sl2(aut_f)) x aut_nf 602 return product(closure_inplace(sl_2(std::move(aut_f), own_f)), 603 std::move(aut_nf))->is_empty(); 604 case 7: // on-the-fly sl(aut_f) x sl(aut_nf) 605 return otf_product(make_tgbasl(std::move(aut_f)), 606 make_tgbasl(std::move(aut_nf)))->is_empty(); 607 case 8: // cl(aut_f) x cl(aut_nf) 608 return product(cl(std::move(aut_f), own_f), 609 cl(std::move(aut_nf), own_nf))->is_empty(); 610 default: 611 throw std::runtime_error("is_stutter_invariant(): " 612 "invalid algorithm number"); 613 SPOT_UNREACHABLE(); 614 } 615 } 616 617 bool is_stutter_invariant_aux(twa_graph_ptr aut_f,bool own_f,const_twa_graph_ptr aut_nf=nullptr,int algo=0)618 is_stutter_invariant_aux(twa_graph_ptr aut_f, 619 bool own_f, 620 const_twa_graph_ptr aut_nf = nullptr, 621 int algo = 0) 622 { 623 trival si = aut_f->prop_stutter_invariant(); 624 if (si.is_known()) 625 return si.is_true(); 626 if (aut_nf) 627 { 628 trival si_n = aut_nf->prop_stutter_invariant(); 629 if (si_n.is_known()) 630 { 631 bool res = si_n.is_true(); 632 aut_f->prop_stutter_invariant(res); 633 return res; 634 } 635 } 636 637 if (algo == 0) 638 algo = default_stutter_check_algorithm(); 639 640 bool own_nf = false; 641 if (!aut_nf) 642 { 643 aut_nf = complement(aut_f); 644 own_nf = true; 645 } 646 bool res = do_si_check(aut_f, own_f, 647 std::move(aut_nf), own_nf, 648 algo); 649 aut_f->prop_stutter_invariant(res); 650 return res; 651 } 652 653 } 654 655 bool is_stutter_invariant(twa_graph_ptr aut_f,const_twa_graph_ptr aut_nf,int algo)656 is_stutter_invariant(twa_graph_ptr aut_f, 657 const_twa_graph_ptr aut_nf, 658 int algo) 659 { 660 return is_stutter_invariant_aux(aut_f, false, aut_nf, algo); 661 } 662 663 bool is_stutter_invariant(formula f,twa_graph_ptr aut_f)664 is_stutter_invariant(formula f, twa_graph_ptr aut_f) 665 { 666 if (f.is_ltl_formula() && f.is_syntactic_stutter_invariant()) 667 return true; 668 669 int algo = default_stutter_check_algorithm(); 670 671 if (algo == 0 || algo == 9) 672 // Etessami's check via syntactic transformation. 673 { 674 if (!f.is_ltl_formula()) 675 throw std::runtime_error("Cannot use the syntactic " 676 "stutter-invariance check " 677 "for non-LTL formulas"); 678 formula g = remove_x(f); 679 bool res; 680 if (algo == 0) // Equivalence check 681 { 682 tl_simplifier ls; 683 res = ls.are_equivalent(f, g); 684 } 685 else 686 { 687 formula h = formula::Xor(f, g); 688 res = ltl_to_tgba_fm(h, make_bdd_dict())->is_empty(); 689 } 690 return res; 691 } 692 693 // Prepare for an automata-based check. 694 translator trans(aut_f ? aut_f->get_dict() : make_bdd_dict()); 695 bool own_f = false; 696 if (!aut_f) 697 { 698 aut_f = trans.run(f); 699 own_f = true; 700 } 701 return is_stutter_invariant_aux(aut_f, own_f, trans.run(formula::Not(f))); 702 } 703 704 trival check_stutter_invariance(twa_graph_ptr aut,formula f,bool do_not_determinize,bool find_counterexamples)705 check_stutter_invariance(twa_graph_ptr aut, formula f, 706 bool do_not_determinize, 707 bool find_counterexamples) 708 { 709 trival is_stut = aut->prop_stutter_invariant(); 710 if (!find_counterexamples && is_stut.is_known()) 711 return is_stut.is_true(); 712 713 twa_graph_ptr neg = nullptr; 714 if (f) 715 neg = translator(aut->get_dict()).run(formula::Not(f)); 716 else if (!is_deterministic(aut) && do_not_determinize) 717 return trival::maybe(); 718 719 if (!find_counterexamples) 720 return is_stutter_invariant(aut, std::move(neg)); 721 722 // Procedure that may find a counterexample. 723 724 if (!neg) 725 neg = complement(aut); 726 727 auto aword = product(closure(aut), closure(neg))->accepting_word(); 728 if (!aword) 729 { 730 aut->prop_stutter_invariant(true); 731 return true; 732 } 733 aword->simplify(); 734 aword->use_all_aps(aut->ap_vars()); 735 auto aaut = aword->as_automaton(); 736 twa_word_ptr rword; 737 if (aaut->intersects(aut)) 738 { 739 rword = sl2(aaut)->intersecting_word(neg); 740 rword->simplify(); 741 } 742 else 743 { 744 rword = aword; 745 aword = sl2(aaut)->intersecting_word(aut); 746 aword->simplify(); 747 } 748 std::ostringstream os; 749 os << *aword; 750 aut->set_named_prop<std::string>("accepted-word", 751 new std::string(os.str())); 752 os.str(""); 753 os << *rword; 754 aut->set_named_prop<std::string>("rejected-word", 755 new std::string(os.str())); 756 aut->prop_stutter_invariant(false); 757 return false; 758 } 759 760 std::vector<bool> stutter_invariant_states(const_twa_graph_ptr pos,formula f)761 stutter_invariant_states(const_twa_graph_ptr pos, formula f) 762 { 763 if (f.is_syntactic_stutter_invariant() 764 || pos->prop_stutter_invariant().is_true()) 765 return std::vector<bool>(pos->num_states(), true); 766 auto neg = translator(pos->get_dict()).run(formula::Not(f)); 767 return stutter_invariant_states(pos, neg); 768 } 769 770 // Based on an idea by Joachim Klein. 771 std::vector<bool> stutter_invariant_states(const_twa_graph_ptr pos,const_twa_graph_ptr neg)772 stutter_invariant_states(const_twa_graph_ptr pos, 773 const_twa_graph_ptr neg) 774 { 775 std::vector<bool> res(pos->num_states(), true); 776 if (pos->prop_stutter_invariant().is_true()) 777 return res; 778 779 if (neg == nullptr) 780 neg = complement(pos); 781 782 auto product_states = [](const const_twa_graph_ptr& a) 783 { 784 return (a->get_named_prop<std::vector<std::pair<unsigned, unsigned>>> 785 ("product-states")); 786 }; 787 788 // Get the set of states (x,y) that appear in the product P1=pos*neg. 789 std::set<std::pair<unsigned, unsigned>> pairs = [&]() 790 { 791 twa_graph_ptr prod = spot::product(pos, neg); 792 auto goodstates = product_states(prod); 793 std::set<std::pair<unsigned, unsigned>> pairs(goodstates->begin(), 794 goodstates->end()); 795 return pairs; 796 }(); 797 798 // Compute P2=cl(pos)*cl(neg). A state x of pos is stutter-sensitive 799 // if there exists a state (x,y) in both P1 and P2 that as a successor 800 // in the useful part of P2 and that is not in P1. 801 twa_graph_ptr prod = spot::product(closure(pos), closure(neg)); 802 auto prod_pairs = product_states(prod); 803 scc_info si(prod, scc_info_options::TRACK_SUCCS 804 | scc_info_options::TRACK_STATES_IF_FIN_USED); 805 si.determine_unknown_acceptance(); 806 unsigned n = prod->num_states(); 807 bool sinv = true; 808 809 for (unsigned s = 0; s < n; ++s) 810 { 811 if (!si.is_useful_scc(si.scc_of(s))) 812 continue; 813 if (pairs.find((*prod_pairs)[s]) == pairs.end()) 814 continue; 815 for (auto& e: prod->out(s)) 816 if (si.is_useful_scc(si.scc_of(e.dst))) 817 res[(*prod_pairs)[s].first] = sinv = false; 818 } 819 std::const_pointer_cast<twa_graph>(pos)->prop_stutter_invariant(sinv); 820 std::const_pointer_cast<twa_graph>(neg)->prop_stutter_invariant(sinv); 821 return res; 822 } 823 824 std::vector<bdd> stutter_invariant_letters(const_twa_graph_ptr pos,formula f)825 stutter_invariant_letters(const_twa_graph_ptr pos, formula f) 826 { 827 if (f.is_syntactic_stutter_invariant() 828 || pos->prop_stutter_invariant().is_true()) 829 { 830 std::const_pointer_cast<twa_graph>(pos)->prop_stutter_invariant(true); 831 return stutter_invariant_letters(pos); 832 } 833 auto neg = translator(pos->get_dict()).run(formula::Not(f)); 834 return stutter_invariant_letters(pos, neg); 835 } 836 837 std::vector<bdd> stutter_invariant_letters(const_twa_graph_ptr pos,const_twa_graph_ptr neg)838 stutter_invariant_letters(const_twa_graph_ptr pos, 839 const_twa_graph_ptr neg) 840 { 841 unsigned ns = pos->num_states(); 842 std::vector<bdd> res(ns, bddtrue); 843 if (pos->prop_stutter_invariant().is_true()) 844 return res; 845 846 if (neg == nullptr) 847 neg = complement(pos); 848 849 auto product_states = [](const const_twa_graph_ptr& a) 850 { 851 return (a->get_named_prop<std::vector<std::pair<unsigned, unsigned>>> 852 ("product-states")); 853 }; 854 855 // Get the set of states (x,y) that appear in the product P1=pos*neg. 856 std::set<std::pair<unsigned, unsigned>> pairs = [&]() 857 { 858 twa_graph_ptr prod = spot::product(pos, neg); 859 auto goodstates = product_states(prod); 860 std::set<std::pair<unsigned, unsigned>> pairs(goodstates->begin(), 861 goodstates->end()); 862 return pairs; 863 }(); 864 865 // Compute P2=cl(pos)*cl(neg). A state x of pos is stutter-sensitive 866 // if there exists a state (x,y) in both P1 and P2 that as a successor 867 // in the useful part of P2 and that is not in P1. 868 twa_graph_ptr prod = spot::product(closure(pos), closure(neg)); 869 auto prod_pairs = product_states(prod); 870 scc_info si(prod, scc_info_options::TRACK_SUCCS 871 | scc_info_options::TRACK_STATES_IF_FIN_USED); 872 si.determine_unknown_acceptance(); 873 unsigned n = prod->num_states(); 874 bool sinv = true; 875 876 for (unsigned s = 0; s < n; ++s) 877 { 878 if (!si.is_useful_scc(si.scc_of(s))) 879 continue; 880 if (pairs.find((*prod_pairs)[s]) == pairs.end()) 881 continue; 882 for (auto& e: prod->out(s)) 883 if (si.is_useful_scc(si.scc_of(e.dst))) 884 { 885 sinv = false; 886 res[(*prod_pairs)[s].first] -= e.cond; 887 } 888 } 889 std::const_pointer_cast<twa_graph>(pos)->prop_stutter_invariant(sinv); 890 std::const_pointer_cast<twa_graph>(neg)->prop_stutter_invariant(sinv); 891 return res; 892 } 893 894 namespace 895 { 896 static highlight_vector(twa_graph_ptr aut,const std::vector<bool> & v,unsigned color)897 void highlight_vector(twa_graph_ptr aut, 898 const std::vector<bool>& v, 899 unsigned color) 900 { 901 // Create the highlight-states property only if it does not 902 // exist already. 903 auto hs = 904 aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states"); 905 if (!hs) 906 { 907 hs = new std::map<unsigned, unsigned>; 908 aut->set_named_prop("highlight-states", hs); 909 } 910 911 unsigned n = v.size(); 912 for (unsigned i = 0; i < n; ++i) 913 if (v[i]) 914 (*hs)[i] = color; 915 } 916 } 917 918 void highlight_stutter_invariant_states(twa_graph_ptr pos,formula f,unsigned color)919 highlight_stutter_invariant_states(twa_graph_ptr pos, 920 formula f, unsigned color) 921 { 922 highlight_vector(pos, stutter_invariant_states(pos, f), color); 923 } 924 925 void highlight_stutter_invariant_states(twa_graph_ptr pos,const_twa_graph_ptr neg,unsigned color)926 highlight_stutter_invariant_states(twa_graph_ptr pos, 927 const_twa_graph_ptr neg, 928 unsigned color) 929 { 930 highlight_vector(pos, stutter_invariant_states(pos, neg), color); 931 } 932 933 934 namespace 935 { sistates_has_wrong_size(const char * fun)936 [[noreturn]] static void sistates_has_wrong_size(const char* fun) 937 { 938 throw std::runtime_error(std::string(fun) + 939 "(): vector size should match " 940 "the number of states"); 941 } 942 } 943 944 int is_stutter_invariant_forward_closed(twa_graph_ptr aut,const std::vector<bool> & sistates)945 is_stutter_invariant_forward_closed(twa_graph_ptr aut, 946 const std::vector<bool>& sistates) 947 { 948 unsigned ns = aut->num_states(); 949 if (SPOT_UNLIKELY(sistates.size() != ns)) 950 sistates_has_wrong_size("is_stutter_invariant_forward_closed"); 951 for (unsigned s = 0; s < ns; ++s) 952 { 953 if (!sistates[s]) 954 continue; 955 for (auto& e : aut->out(s)) 956 { 957 if (!sistates[e.dst]) 958 return e.dst; 959 } 960 } 961 return -1; 962 } 963 964 std::vector<bool> make_stutter_invariant_forward_closed_inplace(twa_graph_ptr aut,const std::vector<bool> & sistates)965 make_stutter_invariant_forward_closed_inplace 966 (twa_graph_ptr aut, const std::vector<bool>& sistates) 967 { 968 unsigned ns = aut->num_states(); 969 if (SPOT_UNLIKELY(sistates.size() != ns)) 970 sistates_has_wrong_size("make_stutter_invariant_forward_closed_inplace"); 971 // Find the set of SI states that can jump into non-SI states. 972 std::vector<unsigned> seed_states; 973 bool pb = false; 974 for (unsigned s = 0; s < ns; ++s) 975 { 976 if (!sistates[s]) 977 continue; 978 for (auto& e : aut->out(s)) 979 if (!sistates[e.dst]) 980 { 981 seed_states.push_back(s); 982 pb = true; 983 break; 984 } 985 } 986 if (!pb) // Nothing to change 987 return sistates; 988 989 // Find the set of non-SI states that are reachable from a seed 990 // state, and give each of them a new number. 991 std::vector<unsigned> new_number(ns, 0); 992 std::vector<unsigned> prob_states; 993 prob_states.reserve(ns); 994 unsigned base = ns; 995 std::vector<unsigned> dfs; 996 dfs.reserve(ns); 997 for (unsigned pb: seed_states) 998 { 999 dfs.push_back(pb); 1000 while (!dfs.empty()) 1001 { 1002 unsigned src = dfs.back(); 1003 dfs.pop_back(); 1004 for (auto& e: aut->out(src)) 1005 { 1006 unsigned dst = e.dst; 1007 if (sistates[dst] || new_number[dst]) 1008 continue; 1009 new_number[dst] = base++; 1010 dfs.push_back(dst); 1011 prob_states.push_back(dst); 1012 } 1013 } 1014 } 1015 1016 // Actually duplicate the problematic states 1017 assert(base > ns); 1018 aut->new_states(base - ns); 1019 assert(aut->num_states() == base); 1020 for (unsigned ds: prob_states) 1021 { 1022 unsigned new_src = new_number[ds]; 1023 assert(new_src > 0); 1024 for (auto& e: aut->out(ds)) 1025 { 1026 unsigned dst = new_number[e.dst]; 1027 if (!dst) 1028 dst = e.dst; 1029 aut->new_edge(new_src, dst, e.cond, e.acc); 1030 } 1031 } 1032 1033 // Redirect the transition coming out of the seed states 1034 // to the duplicate state. 1035 for (unsigned pb: seed_states) 1036 for (auto& e: aut->out(pb)) 1037 { 1038 unsigned ndst = new_number[e.dst]; 1039 if (ndst) 1040 e.dst = ndst; 1041 } 1042 1043 // Create a new SI-state vector. 1044 std::vector<bool> new_sistates; 1045 new_sistates.reserve(base); 1046 new_sistates.insert(new_sistates.end(), sistates.begin(), sistates.end()); 1047 new_sistates.insert(new_sistates.end(), base - ns, true); 1048 return new_sistates; 1049 } 1050 1051 } 1052