1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2015-2018 Laboratoire de Recherche et Développement 3 // de l'Epita. 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/totgba.hh> 22 #include <spot/twaalgos/remfin.hh> 23 #include <spot/twaalgos/cleanacc.hh> 24 #include <spot/twaalgos/sccinfo.hh> 25 #include <spot/twa/twagraph.hh> 26 #include <deque> 27 #include <tuple> 28 29 #define TRACE 0 30 #if TRACE 31 #define trace std::cerr 32 #else 33 #define trace while (0) std::cerr 34 #endif 35 36 namespace spot 37 { 38 namespace 39 { 40 class dnf_to_streett_converter 41 { 42 private: 43 typedef std::pair<acc_cond::mark_t, acc_cond::mark_t> mark_pair; 44 45 const const_twa_graph_ptr& in_; // The given aut. 46 scc_info si_; // SCC information. 47 unsigned nb_scc_; // Number of SCC. 48 unsigned max_set_in_; // Max acc. set nb of in_. 49 bool state_based_; // Is in_ state_based ? 50 unsigned init_st_in_; // Initial state of in_. 51 bool init_reachable_; // Init reach from itself? 52 twa_graph_ptr res_; // Resulting automaton. 53 acc_cond::mark_t all_fin_; // All acc. set marked as 54 // Fin. 55 acc_cond::mark_t all_inf_; // All acc. set marked as 56 // Inf. 57 unsigned num_sets_res_; // Future nb of acc. set. 58 std::vector<mark_pair> all_clauses_; // All clauses. 59 std::vector<acc_cond::mark_t> set_to_keep_; // Set to keep for each clause 60 std::vector<acc_cond::mark_t> set_to_add_; // New set for each clause. 61 acc_cond::mark_t all_set_to_add_; // All new set to add. 62 std::vector<unsigned> assigned_sets_; // Set that will be add. 63 std::vector<std::vector<unsigned>> acc_clauses_; // Acc. clauses. 64 unsigned res_init_; // Future initial st. 65 66 // A state can be copied at most as many times as their are clauses for 67 // which it is not rejecting and must be copied one time (to remain 68 // consistent with the recognized language). This vector records each 69 // created state following this format: 70 // st_repr_[orig_st_nb] gives a vector<pair<clause, state>>. 71 std::vector<std::vector<std::pair<unsigned, unsigned>>> st_repr_; 72 73 // Split the DNF acceptance condition and get all the sets used in each 74 // clause. It separates those that must be seen finitely often from 75 // those that must be seen infinitely often. 76 void split_dnf_clauses(const acc_cond::acc_code & code)77 split_dnf_clauses(const acc_cond::acc_code& code) 78 { 79 auto pos = &code.back(); 80 if (pos->sub.op == acc_cond::acc_op::Or) 81 --pos; 82 auto start = &code.front(); 83 while (pos > start) 84 { 85 const unsigned short size = pos[0].sub.size; 86 if (pos[0].sub.op == acc_cond::acc_op::And) 87 { 88 acc_cond::mark_t fin = {}; 89 acc_cond::mark_t inf = {}; 90 for (int i = 1; i <= (int)size; i += 2) 91 { 92 if (pos[-i].sub.op == acc_cond::acc_op::Fin) 93 fin |= pos[-i - 1].mark; 94 else if (pos[-i].sub.op == acc_cond::acc_op::Inf) 95 inf |= pos[-i - 1].mark; 96 else 97 SPOT_UNREACHABLE(); 98 } 99 all_clauses_.emplace_back(fin, inf); 100 set_to_keep_.emplace_back(fin | inf); 101 } 102 else if (pos[0].sub.op == acc_cond::acc_op::Fin) // Fin 103 { 104 auto m1 = pos[-1].mark; 105 for (unsigned int s : m1.sets()) 106 { 107 all_clauses_.emplace_back(acc_cond::mark_t({s}), 108 acc_cond::mark_t({})); 109 set_to_keep_.emplace_back(acc_cond::mark_t({s})); 110 } 111 } 112 else if (pos[0].sub.op == acc_cond::acc_op::Inf) // Inf 113 { 114 auto m2 = pos[-1].mark; 115 all_clauses_.emplace_back(acc_cond::mark_t({}), m2); 116 set_to_keep_.emplace_back(m2); 117 } 118 else 119 { 120 SPOT_UNREACHABLE(); 121 } 122 pos -= size + 1; 123 } 124 #if TRACE 125 trace << "\nPrinting all clauses\n"; 126 for (unsigned i = 0; i < all_clauses_.size(); ++i) 127 { 128 trace << i << " Fin:" << all_clauses_[i].first << " Inf:" 129 << all_clauses_[i].second << '\n'; 130 } 131 #endif 132 } 133 134 // Compute all the acceptance sets that will be needed: 135 // -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing 136 // on every edge of the associated clone. 137 // -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing 138 // nowhere. 139 // In the second form, Inf(y) with no occurrence of y, can be 140 // reused multiple times. It's called "missing_set" below. 141 void assign_new_sets()142 assign_new_sets() 143 { 144 unsigned int next_set = 0; 145 unsigned int missing_set = -1U; 146 assigned_sets_.resize(max_set_in_, -1U); 147 148 acc_cond::mark_t all_m = all_fin_ | all_inf_; 149 for (unsigned set = 0; set < max_set_in_; ++set) 150 if (all_fin_.has(set)) 151 { 152 if ((int)missing_set < 0) 153 { 154 while (all_m.has(next_set)) 155 ++next_set; 156 missing_set = next_set++; 157 } 158 159 assigned_sets_[set] = missing_set; 160 } 161 else if (all_inf_.has(set)) 162 { 163 while (all_m.has(next_set)) 164 ++next_set; 165 166 assigned_sets_[set] = next_set++; 167 } 168 169 num_sets_res_ = std::max(next_set, max_set_in_); 170 } 171 172 // Precompute: 173 // -the sets to add for each clause, 174 // -all sets to add. 175 void find_set_to_add()176 find_set_to_add() 177 { 178 assign_new_sets(); 179 180 unsigned nb_clause = all_clauses_.size(); 181 for (unsigned clause = 0; clause < nb_clause; ++clause) 182 { 183 if (all_clauses_[clause].second) 184 { 185 acc_cond::mark_t m = {}; 186 for (unsigned set = 0; set < max_set_in_; ++set) 187 if (all_clauses_[clause].second.has(set)) 188 { 189 assert((int)assigned_sets_[set] >= 0); 190 m |= acc_cond::mark_t({assigned_sets_[set]}); 191 } 192 set_to_add_.push_back(m); 193 } 194 else 195 { 196 set_to_add_.emplace_back(acc_cond::mark_t({})); 197 } 198 } 199 200 all_set_to_add_ = {}; 201 for (unsigned s = 0; s < max_set_in_; ++s) 202 if (all_inf_.has(s)) 203 { 204 assert((int)assigned_sets_[s] >= 0); 205 all_set_to_add_.set(assigned_sets_[s]); 206 } 207 } 208 209 // Check whether the initial state is reachable from itself. 210 bool is_init_reachable()211 is_init_reachable() 212 { 213 for (const auto& e : in_->edges()) 214 for (unsigned d : in_->univ_dests(e)) 215 if (d == init_st_in_) 216 return true; 217 return false; 218 } 219 220 // Get all non rejecting scc for each clause of the acceptance 221 // condition. Actually, for each clause, an scc will be kept if it 222 // contains all the 'Inf' acc. sets of the clause. 223 void find_probably_accepting_scc(std::vector<std::vector<unsigned>> & res)224 find_probably_accepting_scc(std::vector<std::vector<unsigned>>& res) 225 { 226 res.resize(nb_scc_); 227 unsigned nb_clause = all_clauses_.size(); 228 for (unsigned scc = 0; scc < nb_scc_; ++scc) 229 { 230 if (si_.is_rejecting_scc(scc)) 231 continue; 232 233 acc_cond::mark_t acc = si_.acc_sets_of(scc); 234 for (unsigned clause = 0; clause < nb_clause; ++clause) 235 { 236 if ((acc & all_clauses_[clause].second) 237 == all_clauses_[clause].second) 238 res[scc].push_back(clause); 239 } 240 } 241 #if TRACE 242 trace << "accepting clauses\n"; 243 for (unsigned i = 0; i < res.size(); ++i) 244 { 245 trace << "scc(" << i << ") -->"; 246 for (auto elt : res[i]) 247 trace << ' ' << elt; 248 if (si_.is_rejecting_scc(i)) 249 trace << " rej"; 250 trace << '\n'; 251 } 252 trace << '\n'; 253 #endif 254 } 255 256 // Add all possible representatives of the original state provided. 257 // Actually, this state will be copied as many times as there are clauses 258 // for which its SCC is not rejecting. 259 void add_state(unsigned st)260 add_state(unsigned st) 261 { 262 trace << "add_state(" << st << ")\n"; 263 if (st_repr_[st].empty()) 264 { 265 unsigned st_scc = si_.scc_of(st); 266 if (st == init_st_in_ && !init_reachable_) 267 st_repr_[st].emplace_back(-1U, res_init_); 268 269 else if (!acc_clauses_[st_scc].empty()) 270 for (const auto& clause : acc_clauses_[st_scc]) 271 st_repr_[st].emplace_back(clause, res_->new_state()); 272 273 else 274 st_repr_[st].emplace_back(-1U, res_->new_state()); 275 trace << "added\n"; 276 } 277 } 278 279 // Compute the mark that will be set (instead of the provided e_acc) 280 // according to the current clause in process. This function is only 281 // called for accepting SCC. 282 acc_cond::mark_t get_edge_mark(const acc_cond::mark_t & e_acc,unsigned clause)283 get_edge_mark(const acc_cond::mark_t& e_acc, 284 unsigned clause) 285 { 286 assert((int)clause >= 0); 287 return (e_acc & set_to_keep_[clause]) | set_to_add_[clause]; 288 } 289 290 // Set the acceptance condition once the resulting automaton is ready. 291 void set_acc_condition()292 set_acc_condition() 293 { 294 acc_cond::acc_code p_code; 295 for (unsigned set = 0; set < max_set_in_; ++set) 296 { 297 if (all_fin_.has(set)) 298 p_code &= 299 acc_cond::acc_code::inf(acc_cond::mark_t({assigned_sets_[set]})) 300 | acc_cond::acc_code::fin(acc_cond::mark_t({set})); 301 else if (all_inf_.has(set)) 302 p_code &= 303 acc_cond::acc_code::inf(acc_cond::mark_t({set})) 304 | acc_cond::acc_code::fin( 305 acc_cond::mark_t({assigned_sets_[set]})); 306 } 307 res_->set_acceptance(num_sets_res_, p_code); 308 } 309 310 public: dnf_to_streett_converter(const const_twa_graph_ptr & in,const acc_cond::acc_code & code)311 dnf_to_streett_converter(const const_twa_graph_ptr& in, 312 const acc_cond::acc_code& code) 313 : in_(in), 314 si_(scc_info(in, scc_info_options::TRACK_STATES 315 | scc_info_options::TRACK_SUCCS)), 316 nb_scc_(si_.scc_count()), 317 max_set_in_(code.used_sets().max_set()), 318 state_based_(in->prop_state_acc() == true), 319 init_st_in_(in->get_init_state_number()), 320 init_reachable_(is_init_reachable()) 321 { 322 trace << "State based ? " << state_based_ << '\n'; 323 std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets(); 324 split_dnf_clauses(code); 325 find_set_to_add(); 326 find_probably_accepting_scc(acc_clauses_); 327 } 328 ~dnf_to_streett_converter()329 ~dnf_to_streett_converter() 330 {} 331 run(bool original_states)332 twa_graph_ptr run(bool original_states) 333 { 334 res_ = make_twa_graph(in_->get_dict()); 335 res_->copy_ap_of(in_); 336 st_repr_.resize(in_->num_states()); 337 res_init_ = res_->new_state(); 338 res_->set_init_state(res_init_); 339 340 for (unsigned scc = 0; scc < nb_scc_; ++scc) 341 { 342 if (!si_.is_useful_scc(scc)) 343 continue; 344 trace << "scc #" << scc << '\n'; 345 346 bool rej_scc = acc_clauses_[scc].empty(); 347 for (auto st : si_.states_of(scc)) 348 { 349 add_state(st); 350 for (const auto& e : in_->out(st)) 351 { 352 trace << "working_on_edge(" << st << ',' << e.dst << ")\n"; 353 354 unsigned dst_scc = si_.scc_of(e.dst); 355 if (!si_.is_useful_scc(dst_scc)) 356 continue; 357 add_state(e.dst); 358 bool same_scc = scc == dst_scc; 359 360 if (st == init_st_in_) 361 { 362 for (const auto& p_dst : st_repr_[e.dst]) 363 res_->new_edge(res_init_, p_dst.second, e.cond, {}); 364 if (!init_reachable_) 365 continue; 366 } 367 368 if (!rej_scc) 369 for (const auto& p_src : st_repr_[st]) 370 for (const auto& p_dst : st_repr_[e.dst]) 371 { 372 trace << "repr(" << p_src.second << ',' 373 << p_dst.second << ")\n"; 374 375 if (same_scc && p_src.first == p_dst.first) 376 res_->new_edge(p_src.second, p_dst.second, e.cond, 377 get_edge_mark(e.acc, p_src.first)); 378 379 else if (!same_scc) 380 res_->new_edge(p_src.second, p_dst.second, e.cond, 381 state_based_ ? 382 get_edge_mark(e.acc, p_src.first) 383 : acc_cond::mark_t({})); 384 } 385 else 386 { 387 assert(st_repr_[st].size() == 1); 388 unsigned src = st_repr_[st][0].second; 389 390 acc_cond::mark_t m = {}; 391 if (same_scc || state_based_) 392 m = e.acc | all_set_to_add_; 393 394 for (const auto& p_dst : st_repr_[e.dst]) 395 res_->new_edge(src, p_dst.second, e.cond, m); 396 } 397 } 398 } 399 } 400 401 // Mapping between each state of the resulting automaton and the 402 // original state of the input automaton. 403 if (original_states) 404 { 405 auto orig_states = new std::vector<unsigned>(); 406 orig_states->resize(res_->num_states(), -1U); 407 res_->set_named_prop("original-states", orig_states); 408 409 auto orig_clauses = new std::vector<unsigned>(); 410 orig_clauses->resize(res_->num_states(), -1U); 411 res_->set_named_prop("original-clauses", orig_clauses); 412 413 unsigned orig_num_states = in_->num_states(); 414 for (unsigned orig = 0; orig < orig_num_states; ++orig) 415 { 416 if (!si_.is_useful_scc(si_.scc_of(orig))) 417 continue; 418 for (const auto& p : st_repr_[orig]) 419 { 420 (*orig_states)[p.second] = orig; 421 (*orig_clauses)[p.second] = p.first; 422 } 423 } 424 } 425 426 set_acc_condition(); 427 res_->prop_state_acc(state_based_); 428 return res_; 429 } 430 }; 431 } 432 433 434 twa_graph_ptr dnf_to_streett(const const_twa_graph_ptr & in,bool original_states)435 dnf_to_streett(const const_twa_graph_ptr& in, bool original_states) 436 { 437 const acc_cond::acc_code& code = in->get_acceptance(); 438 if (!code.is_dnf()) 439 throw std::runtime_error("dnf_to_streett() should only be" 440 " called on automata with DNF acceptance"); 441 if (code.is_t() || code.is_f() || in->acc().is_streett() > 0) 442 return make_twa_graph(in, twa::prop_set::all()); 443 444 dnf_to_streett_converter dnf_to_streett(in, code); 445 return dnf_to_streett.run(original_states); 446 } 447 448 449 namespace 450 { 451 struct st2gba_state 452 { 453 acc_cond::mark_t pend; 454 unsigned s; 455 st2gba_statespot::__anon715d698c0211::st2gba_state456 st2gba_state(unsigned st, acc_cond::mark_t bv = acc_cond::mark_t::all()): 457 pend(bv), s(st) 458 { 459 } 460 }; 461 462 struct st2gba_state_hash 463 { 464 size_t operator ()spot::__anon715d698c0211::st2gba_state_hash465 operator()(const st2gba_state& s) const noexcept 466 { 467 std::hash<acc_cond::mark_t> h; 468 return s.s ^ h(s.pend); 469 } 470 }; 471 472 struct st2gba_state_equal 473 { 474 bool operator ()spot::__anon715d698c0211::st2gba_state_equal475 operator()(const st2gba_state& left, 476 const st2gba_state& right) const 477 { 478 if (left.s != right.s) 479 return false; 480 return left.pend == right.pend; 481 } 482 }; 483 484 typedef std::vector<acc_cond::mark_t> terms_t; 485 cnf_terms(const acc_cond::acc_code & code)486 terms_t cnf_terms(const acc_cond::acc_code& code) 487 { 488 assert(!code.empty()); 489 terms_t res; 490 auto pos = &code.back(); 491 auto end = &code.front(); 492 if (pos->sub.op == acc_cond::acc_op::And) 493 --pos; 494 while (pos >= end) 495 { 496 auto term_end = pos - 1 - pos->sub.size; 497 bool inor = pos->sub.op == acc_cond::acc_op::Or; 498 if (inor) 499 --pos; 500 acc_cond::mark_t m = {}; 501 while (pos > term_end) 502 { 503 assert(pos->sub.op == acc_cond::acc_op::Inf); 504 m |= pos[-1].mark; 505 pos -= 2; 506 } 507 if (inor) 508 res.emplace_back(m); 509 else 510 for (unsigned i: m.sets()) 511 res.emplace_back(acc_cond::mark_t({i})); 512 } 513 return res; 514 } 515 } 516 517 518 // Specialized conversion for Streett -> TGBA 519 // ============================================ 520 // 521 // Christof Löding's Diploma Thesis: Methods for the 522 // Transformation of ω-Automata: Complexity and Connection to 523 // Second Order Logic. Section 3.4.3, gives a transition 524 // from Streett with |Q| states to BA with |Q|*(4^n-3^n+2) 525 // states, if n is the number of acceptance pairs. 526 // 527 // Duret-Lutz et al. (ATVA'2009): On-the-fly Emptiness Check of 528 // Transition-based Streett Automata. Section 3.3 contains a 529 // conversion from transition-based Streett Automata to TGBA using 530 // the generalized Büchi acceptance to limit the explosion. It goes 531 // from Streett with |Q| states to (T)GBA with |Q|*(2^n+1) states. 532 // However the definition of the number of acceptance sets in that 533 // paper is suboptimal: only n are needed, not 2^n. 534 // 535 // This implements this second version. 536 twa_graph_ptr streett_to_generalized_buchi(const const_twa_graph_ptr & in)537 streett_to_generalized_buchi(const const_twa_graph_ptr& in) 538 { 539 // While "t" is Streett, it is also generalized Büchi, so 540 // do not do anything. 541 if (in->acc().is_generalized_buchi()) 542 return std::const_pointer_cast<twa_graph>(in); 543 544 std::vector<acc_cond::rs_pair> pairs; 545 bool res = in->acc().is_streett_like(pairs); 546 if (!res) 547 throw std::runtime_error("streett_to_generalized_buchi() should only be" 548 " called on automata with Streett-like" 549 " acceptance"); 550 551 // In Streett acceptance, inf sets are odd, while fin sets are 552 // even. 553 acc_cond::mark_t inf; 554 acc_cond::mark_t fin; 555 std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); 556 unsigned p = inf.count(); 557 // At some point we will remove anything that is not used as Inf. 558 acc_cond::mark_t to_strip = in->acc().all_sets() - inf; 559 acc_cond::mark_t inf_alone = {}; 560 acc_cond::mark_t fin_alone = {}; 561 562 if (!p) 563 return remove_fin(in); 564 565 unsigned numsets = in->acc().num_sets(); 566 std::vector<acc_cond::mark_t> fin_to_infpairs(numsets, 567 acc_cond::mark_t({})); 568 std::vector<acc_cond::mark_t> inf_to_finpairs(numsets, 569 acc_cond::mark_t({})); 570 for (auto pair: pairs) 571 { 572 if (pair.fin) 573 for (unsigned mark: pair.fin.sets()) 574 fin_to_infpairs[mark] |= pair.inf; 575 else 576 inf_alone |= pair.inf; 577 578 if (pair.inf) 579 for (unsigned mark: pair.inf.sets()) 580 inf_to_finpairs[mark] |= pair.fin; 581 else 582 fin_alone |= pair.fin; 583 } 584 // If we have something like (Fin(0)|Inf(1))&Fin(0), then 0 is in 585 // fin_alone, but we also have fin_to_infpair[0] = {1}. This should 586 // really be simplified to Fin(0). 587 for (auto mark: fin_alone.sets()) 588 fin_to_infpairs[mark] = {}; 589 590 scc_info si(in, scc_info_options::NONE); 591 592 // Compute the acceptance sets present in each SCC 593 unsigned nscc = si.scc_count(); 594 std::vector<std::tuple<acc_cond::mark_t, acc_cond::mark_t, 595 bool, bool>> sccfi; 596 sccfi.reserve(nscc); 597 for (unsigned s = 0; s < nscc; ++s) 598 { 599 auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9} 600 auto acc_fin = acc & fin; // {0, 2, 4,6} 601 auto acc_inf = acc & inf; // { 1, 3, 7,9} 602 // Fin sets that are alone either because the acceptance 603 // condition has no matching Inf, or because the SCC does not 604 // intersect the matching Inf. 605 acc_cond::mark_t fin_wo_inf = {}; 606 for (unsigned mark: acc_fin.sets()) 607 if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf)) 608 fin_wo_inf.set(mark); 609 610 // Inf sets that *do* have a matching Fin in the acceptance 611 // condition but without matching Fin in the SCC: they can be 612 // considered as always present in the SCC. 613 acc_cond::mark_t inf_wo_fin = {}; 614 for (unsigned mark: inf.sets()) 615 if (inf_to_finpairs[mark] && (inf_to_finpairs[mark] - acc_fin)) 616 inf_wo_fin.set(mark); 617 618 sccfi.emplace_back(fin_wo_inf, inf_wo_fin, 619 !acc_fin, !acc_inf); 620 } 621 622 auto out = make_twa_graph(in->get_dict()); 623 out->copy_ap_of(in); 624 out->prop_copy(in, {false, false, false, false, false, true}); 625 out->set_generalized_buchi(p); 626 627 // Map st2gba pairs to the state numbers used in out. 628 typedef std::unordered_map<st2gba_state, unsigned, 629 st2gba_state_hash, 630 st2gba_state_equal> bs2num_map; 631 bs2num_map bs2num; 632 633 // Queue of states to be processed. 634 typedef std::deque<st2gba_state> queue_t; 635 queue_t todo; 636 637 st2gba_state s(in->get_init_state_number()); 638 bs2num[s] = out->new_state(); 639 todo.emplace_back(s); 640 641 bool sbacc = in->prop_state_acc().is_true(); 642 643 // States of the original automaton are marked with s.pend == -1U. 644 const acc_cond::mark_t orig_copy = acc_cond::mark_t::all(); 645 646 while (!todo.empty()) 647 { 648 s = todo.front(); 649 todo.pop_front(); 650 unsigned src = bs2num[s]; 651 652 unsigned scc_src = si.scc_of(s.s); 653 bool maybe_acc_scc = !si.is_rejecting_scc(scc_src); 654 655 acc_cond::mark_t scc_fin_wo_inf; 656 acc_cond::mark_t scc_inf_wo_fin; 657 bool no_fin; 658 bool no_inf; 659 std::tie(scc_fin_wo_inf, scc_inf_wo_fin, no_fin, no_inf) 660 = sccfi[scc_src]; 661 662 for (auto& t: in->out(s.s)) 663 { 664 acc_cond::mark_t pend = s.pend; 665 acc_cond::mark_t acc = {}; 666 667 bool maybe_acc = maybe_acc_scc && (scc_src == si.scc_of(t.dst)); 668 if (pend != orig_copy) 669 { 670 if (!maybe_acc) 671 continue; 672 // No point going to some place we will never leave 673 if (t.acc & scc_fin_wo_inf) 674 continue; 675 // For any Fin set we see, we want to see the 676 // corresponding Inf set. 677 for (unsigned mark: (t.acc & fin).sets()) 678 pend |= fin_to_infpairs[mark]; 679 680 // If we see some Inf set immediately, they are not 681 // pending anymore. 682 pend -= t.acc & inf; 683 684 // Label this transition with all non-pending 685 // inf sets. The strip will shift everything 686 // to the correct numbers in the targets. 687 acc = (inf - pend).strip(to_strip); 688 // Adjust the pending sets to what will be necessary 689 // required on the destination state. 690 if (sbacc) 691 { 692 auto a = in->state_acc_sets(t.dst); 693 if (a & scc_fin_wo_inf) 694 continue; 695 for (unsigned m: (a & fin).sets()) 696 pend |= fin_to_infpairs[m]; 697 698 pend -= a & inf; 699 } 700 pend |= inf_alone; 701 } 702 else if (no_fin && maybe_acc) 703 { 704 // If the acceptance is (Fin(0) | Inf(1)) & Inf(2) 705 // but we do not see any Fin set in this SCC, a 706 // mark {2} should become {1,2} before striping. 707 acc = (t.acc | scc_inf_wo_fin).strip(to_strip); 708 } 709 assert((acc & out->acc().all_sets()) == acc); 710 711 st2gba_state d(t.dst, pend); 712 // Have we already seen this destination? 713 unsigned dest; 714 auto dres = bs2num.emplace(d, 0); 715 if (!dres.second) 716 { 717 dest = dres.first->second; 718 } 719 else // No, this is a new state 720 { 721 dest = dres.first->second = out->new_state(); 722 todo.emplace_back(d); 723 } 724 out->new_edge(src, dest, t.cond, acc); 725 726 // Nondeterministically jump to level ∅. We need to do 727 // that only once per cycle. As an approximation, we 728 // only do that for transitions where t.src >= t.dst as 729 // this has to occur at least once per cycle. 730 if (pend == orig_copy && (t.src >= t.dst) && maybe_acc && !no_fin) 731 { 732 acc_cond::mark_t stpend = {}; 733 if (sbacc) 734 { 735 auto a = in->state_acc_sets(t.dst); 736 if (a & scc_fin_wo_inf) 737 continue; 738 for (unsigned m: (a & fin).sets()) 739 stpend |= fin_to_infpairs[m]; 740 741 stpend -= a & inf; 742 } 743 st2gba_state d(t.dst, stpend | inf_alone); 744 // Have we already seen this destination? 745 unsigned dest; 746 auto dres = bs2num.emplace(d, 0); 747 if (!dres.second) 748 { 749 dest = dres.first->second; 750 } 751 else // No, this is a new state 752 { 753 dest = dres.first->second = out->new_state(); 754 todo.emplace_back(d); 755 } 756 out->new_edge(src, dest, t.cond); 757 } 758 } 759 } 760 simplify_acceptance_here(out); 761 if (out->acc().is_f()) 762 { 763 // "f" is not generalized-Büchi. Just return an 764 // empty automaton instead. 765 auto res = make_twa_graph(out->get_dict()); 766 res->set_generalized_buchi(0); 767 res->set_init_state(res->new_state()); 768 res->prop_stutter_invariant(true); 769 res->prop_weak(true); 770 res->prop_complete(false); 771 return res; 772 } 773 return out; 774 } 775 776 twa_graph_ptr streett_to_generalized_buchi_maybe(const const_twa_graph_ptr & in)777 streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in) 778 { 779 static unsigned min = [&]() { 780 const char* c = getenv("SPOT_STREETT_CONV_MIN"); 781 if (!c) 782 return 3; 783 errno = 0; 784 int val = strtol(c, nullptr, 10); 785 if (val < 0 || errno != 0) 786 throw std::runtime_error("unexpected value for SPOT_STREETT_CONV_MIN"); 787 return val; 788 }(); 789 790 std::vector<acc_cond::rs_pair> pairs; 791 bool res = in->acc().is_streett_like(pairs); 792 if (!res || min == 0 || min > pairs.size()) 793 return nullptr; 794 else 795 return streett_to_generalized_buchi(in); 796 } 797 798 799 /// \brief Take an automaton with any acceptance condition and return 800 /// an equivalent Generalized Büchi automaton. 801 twa_graph_ptr to_generalized_buchi(const const_twa_graph_ptr & aut)802 to_generalized_buchi(const const_twa_graph_ptr& aut) 803 { 804 auto maybe = streett_to_generalized_buchi_maybe(aut); 805 if (maybe) 806 return maybe; 807 808 auto res = remove_fin(cleanup_acceptance(aut)); 809 if (res->acc().is_generalized_buchi()) 810 return res; 811 812 auto cnf = res->get_acceptance().to_cnf(); 813 // If we are very lucky, building a CNF actually gave us a GBA... 814 if (cnf.empty() || 815 (cnf.size() == 2 && cnf.back().sub.op == acc_cond::acc_op::Inf)) 816 { 817 res->set_acceptance(res->num_sets(), cnf); 818 cleanup_acceptance_here(res); 819 return res; 820 } 821 822 // Handle false specifically. We want the output 823 // an automaton with Acceptance: t, that has a single 824 // state without successor. 825 if (cnf.is_f()) 826 { 827 assert(!cnf.front().mark); 828 res = make_twa_graph(aut->get_dict()); 829 res->set_init_state(res->new_state()); 830 res->prop_state_acc(true); 831 res->prop_weak(true); 832 res->prop_universal(true); 833 res->prop_stutter_invariant(true); 834 return res; 835 } 836 837 auto terms = cnf_terms(cnf); 838 unsigned nterms = terms.size(); 839 assert(nterms > 0); 840 res->set_generalized_buchi(nterms); 841 842 for (auto& t: res->edges()) 843 { 844 acc_cond::mark_t cur_m = t.acc; 845 acc_cond::mark_t new_m = {}; 846 for (unsigned n = 0; n < nterms; ++n) 847 if (cur_m & terms[n]) 848 new_m.set(n); 849 t.acc = new_m; 850 } 851 return res; 852 } 853 854 namespace 855 { 856 // If the DNF is 857 // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | 858 // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) 859 // this returns the following vector of pairs: 860 // [({1}, {2,4}) 861 // ({2,3}, {1}), 862 // ({}, {1,3}), 863 // ({}, {2}), 864 // ({4}, t)] 865 static std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> split_dnf_acc(const acc_cond::acc_code & acc)866 split_dnf_acc(const acc_cond::acc_code& acc) 867 { 868 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> res; 869 if (acc.empty()) 870 { 871 res.emplace_back(acc_cond::mark_t({}), acc_cond::mark_t({})); 872 return res; 873 } 874 auto pos = &acc.back(); 875 if (pos->sub.op == acc_cond::acc_op::Or) 876 --pos; 877 auto start = &acc.front(); 878 while (pos > start) 879 { 880 if (pos->sub.op == acc_cond::acc_op::Fin) 881 { 882 // We have only a Fin term, without Inf. In this case 883 // only, the Fin() may encode a disjunction of sets. 884 for (auto s: pos[-1].mark.sets()) 885 res.emplace_back(acc_cond::mark_t({s}), acc_cond::mark_t({})); 886 pos -= pos->sub.size + 1; 887 } 888 else 889 { 890 // We have a conjunction of Fin and Inf sets. 891 auto end = pos - pos->sub.size - 1; 892 acc_cond::mark_t fin = {}; 893 acc_cond::mark_t inf = {}; 894 while (pos > end) 895 { 896 switch (pos->sub.op) 897 { 898 case acc_cond::acc_op::And: 899 --pos; 900 break; 901 case acc_cond::acc_op::Fin: 902 fin |= pos[-1].mark; 903 assert(pos[-1].mark.count() == 1); 904 pos -= 2; 905 break; 906 case acc_cond::acc_op::Inf: 907 inf |= pos[-1].mark; 908 pos -= 2; 909 break; 910 case acc_cond::acc_op::FinNeg: 911 case acc_cond::acc_op::InfNeg: 912 case acc_cond::acc_op::Or: 913 SPOT_UNREACHABLE(); 914 break; 915 } 916 } 917 assert(pos == end); 918 res.emplace_back(fin, inf); 919 } 920 } 921 return res; 922 } 923 924 925 static twa_graph_ptr to_generalized_rabin_aux(const const_twa_graph_ptr & aut,bool share_inf,bool complement)926 to_generalized_rabin_aux(const const_twa_graph_ptr& aut, 927 bool share_inf, bool complement) 928 { 929 auto res = cleanup_acceptance(aut); 930 auto oldacc = res->get_acceptance(); 931 if (complement) 932 res->set_acceptance(res->acc().num_sets(), oldacc.complement()); 933 934 { 935 std::vector<unsigned> pairs; 936 if (res->acc().is_generalized_rabin(pairs)) 937 { 938 if (complement) 939 res->set_acceptance(res->acc().num_sets(), oldacc); 940 return res; 941 } 942 } 943 auto dnf = res->get_acceptance().to_dnf(); 944 if (dnf.is_f()) 945 { 946 if (complement) 947 res->set_acceptance(0, acc_cond::acc_code::t()); 948 return res; 949 } 950 951 auto v = split_dnf_acc(dnf); 952 953 // Decide how we will rename each input set. 954 // 955 // inf_rename is only used if hoa_style=false, to 956 // reuse previously used Inf sets. 957 958 unsigned ns = res->num_sets(); 959 std::vector<acc_cond::mark_t> rename(ns); 960 std::vector<unsigned> inf_rename(ns); 961 962 unsigned next_set = 0; 963 // The output acceptance conditions. 964 acc_cond::acc_code code = 965 complement ? acc_cond::acc_code::t() : acc_cond::acc_code::f(); 966 for (auto& i: v) 967 { 968 unsigned fin_set = 0U; 969 970 if (!complement) 971 { 972 for (auto s: i.first.sets()) 973 rename[s].set(next_set); 974 fin_set = next_set++; 975 } 976 977 acc_cond::mark_t infsets = {}; 978 979 if (share_inf) 980 for (auto s: i.second.sets()) 981 { 982 unsigned n = inf_rename[s]; 983 if (n == 0) 984 n = inf_rename[s] = next_set++; 985 rename[s].set(n); 986 infsets.set(n); 987 } 988 else // HOA style 989 { 990 for (auto s: i.second.sets()) 991 { 992 unsigned n = next_set++; 993 rename[s].set(n); 994 infsets.set(n); 995 } 996 } 997 998 // The definition of Streett wants the Fin first in clauses, 999 // so we do the same for generalized Streett since HOA does 1000 // not specify anything. See 1001 // https://github.com/adl/hoaf/issues/62 1002 if (complement) 1003 { 1004 for (auto s: i.first.sets()) 1005 rename[s].set(next_set); 1006 fin_set = next_set++; 1007 1008 auto pair = acc_cond::inf({fin_set}); 1009 pair |= acc_cond::acc_code::fin(infsets); 1010 pair &= std::move(code); 1011 code = std::move(pair); 1012 } 1013 else 1014 { 1015 auto pair = acc_cond::acc_code::inf(infsets); 1016 pair &= acc_cond::fin({fin_set}); 1017 pair |= std::move(code); 1018 code = std::move(pair); 1019 } 1020 } 1021 1022 // Fix the automaton 1023 res->set_acceptance(next_set, code); 1024 for (auto& e: res->edges()) 1025 { 1026 acc_cond::mark_t m = {}; 1027 for (auto s: e.acc.sets()) 1028 m |= rename[s]; 1029 e.acc = m; 1030 } 1031 return res; 1032 } 1033 1034 1035 } 1036 1037 1038 1039 twa_graph_ptr to_generalized_rabin(const const_twa_graph_ptr & aut,bool share_inf)1040 to_generalized_rabin(const const_twa_graph_ptr& aut, 1041 bool share_inf) 1042 { 1043 return to_generalized_rabin_aux(aut, share_inf, false); 1044 } 1045 1046 twa_graph_ptr to_generalized_streett(const const_twa_graph_ptr & aut,bool share_fin)1047 to_generalized_streett(const const_twa_graph_ptr& aut, 1048 bool share_fin) 1049 { 1050 return to_generalized_rabin_aux(aut, share_fin, true); 1051 } 1052 } 1053