1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2009-2011, 2013-2019, 2021 Laboratoire de Recherche et 3 // Développement de l'Epita (LRDE). 4 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), 5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre 6 // et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 #include "config.h" 24 #include <set> 25 #include <iterator> 26 #include <vector> 27 #include <spot/twaalgos/powerset.hh> 28 #include <spot/misc/hash.hh> 29 #include <spot/twaalgos/sccinfo.hh> 30 #include <spot/twaalgos/cycles.hh> 31 #include <spot/twaalgos/gtec/gtec.hh> 32 #include <spot/twaalgos/product.hh> 33 #include <spot/twa/bddprint.hh> 34 #include <spot/twaalgos/sccfilter.hh> 35 #include <spot/twaalgos/ltl2tgba_fm.hh> 36 #include <spot/twaalgos/dualize.hh> 37 #include <spot/twaalgos/remfin.hh> 38 #include <spot/misc/bitvect.hh> 39 #include <spot/misc/bddlt.hh> 40 41 namespace spot 42 { 43 namespace 44 { 45 static power_map::power_state bv_to_ps(const bitvect * in)46 bv_to_ps(const bitvect* in) 47 { 48 power_map::power_state ps; 49 unsigned ns = in->size(); 50 for (unsigned pos = 0; pos < ns; ++pos) 51 if (in->get(pos)) 52 ps.insert(pos); 53 return ps; 54 } 55 56 struct bv_hash 57 { operator ()spot::__anonab693a040111::bv_hash58 size_t operator()(const bitvect* bv) const noexcept 59 { 60 return bv->hash(); 61 } 62 }; 63 64 struct bv_equal 65 { operator ()spot::__anonab693a040111::bv_equal66 bool operator()(const bitvect* bvl, const bitvect* bvr) const 67 { 68 return *bvl == *bvr; 69 } 70 }; 71 } 72 print_reason(std::ostream & os) const73 std::ostream& output_aborter::print_reason(std::ostream& os) const 74 { 75 os << "more than "; 76 if (reason_is_states_) 77 os << max_states_ << " states required"; 78 else 79 os << max_edges_ << " edges required"; 80 return os; 81 } 82 83 twa_graph_ptr tgba_powerset(const const_twa_graph_ptr & aut,power_map & pm,bool merge,const output_aborter * aborter,std::vector<unsigned> * accepting_sinks)84 tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge, 85 const output_aborter* aborter, 86 std::vector<unsigned>* accepting_sinks) 87 { 88 unsigned ns = aut->num_states(); 89 unsigned nap = aut->ap().size(); 90 91 if ((-1UL / ns) >> nap == 0) 92 throw std::runtime_error("too many atomic propositions (or states)"); 93 94 // Build a correspondence between conjunctions of APs and unsigned 95 // indexes. 96 std::vector<bdd> num2bdd; 97 num2bdd.reserve(1UL << nap); 98 std::map<bdd, unsigned, bdd_less_than> bdd2num; 99 bdd allap = aut->ap_vars(); 100 for (bdd one: minterms_of(bddtrue, allap)) 101 { 102 bdd2num.emplace(one, num2bdd.size()); 103 num2bdd.emplace_back(one); 104 } 105 106 size_t nc = num2bdd.size(); // number of conditions 107 assert(nc == (1UL << nap)); 108 109 // Conceptually, we represent the automaton as an array 'bv' of 110 // ns*nc bit vectors of size 'ns'. Each original state is 111 // represented by 'nc' consecutive bitvectors representing the 112 // possible destinations for each condition. 113 // 114 // src cond 115 // 0 !a&!b [...bit vector of size ns...] 116 // !a&b [...bit vector of size ns...] 117 // a&!b [...bit vector of size ns...] 118 // a&b [...bit vector of size ns...] 119 // 1 !a&!b [...bit vector of size ns...] 120 // !a&b [...bit vector of size ns...] 121 // a&!b [...bit vector of size ns...] 122 // a&b [...bit vector of size ns...] 123 // 2 !a&!b [...bit vector of size ns...] 124 // !a&b [...bit vector of size ns...] 125 // a&!b [...bit vector of size ns...] 126 // a&b [...bit vector of size ns...] 127 // ... 128 // 129 // Since there are nc possible "cond" value, and ns sources, the 130 // ns*nc bitvectors of ns bits each can take a lot of space. In 131 // issue #302, we had the case of an automaton with ns=8777 132 // states, and 8 atomic propositions (nc=256): this large array 133 // would require 2.3GB, causing out-of-memory error on small 134 // systems. 135 // 136 // To work around this, we reduce the number of states we store in 137 // this array to reduced_ns, which we currently limit to 512 138 // (chosen arbitrarily), and use it as a least-recently-used 139 // cache. A separate vector of size ns, contains pointers 140 // (i.e. iterators) to a list cell that gives an index in this 141 // cache. The purpose of the list is to maintain the 142 // least-recently-used order. 143 typedef std::list<std::pair<unsigned, unsigned>>::const_iterator iter; 144 std::list<std::pair<unsigned, unsigned>> lru; // list of (idx in bv, state#) 145 std::vector<iter> iters(ns, lru.end()); 146 const unsigned reduced_ns = std::min(512U, ns); 147 auto bv = 148 std::unique_ptr<bitvect_array>(make_bitvect_array(ns, reduced_ns * nc)); 149 150 // Get the index of src in bv, filling bv in an LRU-fashion if needed. 151 auto index = [&](unsigned src) { 152 iter i = iters[src]; 153 if (i != lru.end()) 154 { 155 // bv has already been filled for this state. Just move it 156 // to the front of the LRU list. 157 lru.splice(lru.begin(), lru, i); 158 return i->first; 159 } 160 161 unsigned idx = lru.size(); 162 bool reused = false; 163 if (idx < reduced_ns) 164 { 165 lru.emplace_front(idx, src); 166 } 167 else 168 { 169 unsigned state; 170 std::tie(idx, state) = lru.back(); 171 iters[state] = lru.end(); 172 lru.pop_back(); 173 lru.emplace_front(idx, src); 174 reused = true; 175 } 176 iters[src] = lru.begin(); 177 178 size_t base = idx * nc; 179 if (reused) 180 for (unsigned i = 0; i < nc; ++i) 181 bv->at(base + i).clear_all(); 182 for (auto& t: aut->out(src)) 183 for (bdd one: minterms_of(t.cond, allap)) 184 { 185 unsigned num = bdd2num[one]; 186 bv->at(base + num).set(t.dst); 187 } 188 189 assert(idx == lru.begin()->first); 190 return idx; 191 }; 192 193 typedef power_map::power_state power_state; 194 195 typedef std::unordered_map<bitvect*, int, bv_hash, bv_equal> power_set; 196 power_set seen; 197 198 std::vector<const bitvect*> toclean; 199 200 auto res = make_twa_graph(aut->get_dict()); 201 res->copy_ap_of(aut); 202 203 bitvect* acc_sinks = nullptr; 204 if (accepting_sinks) 205 { 206 acc_sinks = make_bitvect(ns); 207 for (unsigned s: *accepting_sinks) 208 acc_sinks->set(s); 209 toclean.emplace_back(acc_sinks); 210 211 // The accepting sink is the first registered state by 212 // convention. 213 power_state ps = bv_to_ps(acc_sinks); 214 unsigned num = res->new_state(); 215 seen[acc_sinks] = num; 216 assert(pm.map_.size() == num); 217 pm.map_.emplace_back(std::move(ps)); 218 } 219 220 { 221 unsigned init_num = aut->get_init_state_number(); 222 auto bvi = make_bitvect(ns); 223 bvi->set(init_num); 224 power_state ps{init_num}; 225 unsigned num = res->new_state(); 226 res->set_init_state(num); 227 seen[bvi] = num; 228 assert(pm.map_.size() == num); 229 pm.map_.emplace_back(std::move(ps)); 230 toclean.emplace_back(bvi); 231 } 232 233 // outgoing map 234 auto om = std::unique_ptr<bitvect_array>(make_bitvect_array(ns, nc)); 235 236 for (unsigned src_num = 0; src_num < res->num_states(); ++src_num) 237 { 238 om->clear_all(); 239 240 const power_state& src = pm.states_of(src_num); 241 for (auto s: src) 242 { 243 size_t base = index(s) * nc; 244 for (unsigned c = 0; c < nc; ++c) 245 om->at(c) |= bv->at(base + c); 246 } 247 for (unsigned c = 0; c < nc; ++c) 248 { 249 auto dst = &om->at(c); 250 if (dst->is_fully_clear()) 251 continue; 252 if (acc_sinks && dst->intersects(*acc_sinks)) 253 *dst = *acc_sinks; 254 auto i = seen.find(dst); 255 unsigned dst_num; 256 if (i != seen.end()) 257 { 258 dst_num = i->second; 259 } 260 else 261 { 262 dst_num = res->new_state(); 263 auto dst2 = dst->clone(); 264 seen[dst2] = dst_num; 265 toclean.emplace_back(dst2); 266 auto ps = bv_to_ps(dst); 267 assert(pm.map_.size() == dst_num); 268 pm.map_.emplace_back(std::move(ps)); 269 } 270 res->new_edge(src_num, dst_num, num2bdd[c]); 271 if (aborter && aborter->too_large(res)) 272 { 273 for (auto v: toclean) 274 delete v; 275 return nullptr; 276 } 277 } 278 } 279 280 for (auto v: toclean) 281 delete v; 282 if (merge) 283 res->merge_edges(); 284 return res; 285 } 286 287 twa_graph_ptr tgba_powerset(const const_twa_graph_ptr & aut,const output_aborter * aborter,std::vector<unsigned> * accepting_sinks)288 tgba_powerset(const const_twa_graph_ptr& aut, 289 const output_aborter* aborter, 290 std::vector<unsigned>* accepting_sinks) 291 { 292 power_map pm; 293 return tgba_powerset(aut, pm, true, aborter, accepting_sinks); 294 } 295 296 297 namespace 298 { 299 300 class fix_scc_acceptance final: protected enumerate_cycles 301 { 302 public: 303 typedef dfs_stack::const_iterator cycle_iter; 304 typedef twa_graph_edge_data trans; 305 typedef std::set<trans*> edge_set; 306 typedef std::vector<edge_set> set_set; 307 protected: 308 const_twa_graph_ptr ref_; 309 power_map& refmap_; 310 edge_set reject_; // set of rejecting edges 311 set_set accept_; // set of cycles that are accepting 312 edge_set all_; // all non rejecting edges 313 unsigned threshold_; // maximum count of enumerated cycles 314 unsigned cycles_left_; // count of cycles left to explore 315 316 public: fix_scc_acceptance(const scc_info & sm,const_twa_graph_ptr ref,power_map & refmap,unsigned threshold)317 fix_scc_acceptance(const scc_info& sm, const_twa_graph_ptr ref, 318 power_map& refmap, unsigned threshold) 319 : enumerate_cycles(sm), ref_(ref), refmap_(refmap), 320 threshold_(threshold) 321 { 322 } 323 fix_scc(const int m)324 bool fix_scc(const int m) 325 { 326 reject_.clear(); 327 accept_.clear(); 328 cycles_left_ = threshold_; 329 run(m); 330 331 // std::cerr << "SCC #" << m << '\n'; 332 // std::cerr << "REJECT: "; 333 // print_set(std::cerr, reject_) << '\n'; 334 // std::cerr << "ALL: "; 335 // print_set(std::cerr, all_) << '\n'; 336 // for (set_set::const_iterator j = accept_.begin(); 337 // j != accept_.end(); ++j) 338 // { 339 // std::cerr << "ACCEPT: "; 340 // print_set(std::cerr, *j) << '\n'; 341 // } 342 343 auto acc = aut_->acc().all_sets(); 344 for (auto i: all_) 345 i->acc = acc; 346 return threshold_ != 0 && cycles_left_ == 0; 347 } 348 is_cycle_accepting(cycle_iter begin,edge_set & ts) const349 bool is_cycle_accepting(cycle_iter begin, edge_set& ts) const 350 { 351 auto a = std::const_pointer_cast<twa_graph>(aut_); 352 353 // Build an automaton representing this loop. 354 auto loop_a = make_twa_graph(aut_->get_dict()); 355 int loop_size = std::distance(begin, dfs_.end()); 356 loop_a->new_states(loop_size); 357 int n; 358 cycle_iter i; 359 for (n = 1, i = begin; n <= loop_size; ++n, ++i) 360 { 361 trans* t = &a->edge_data(i->succ); 362 loop_a->new_edge(n - 1, n % loop_size, t->cond); 363 if (reject_.find(t) == reject_.end()) 364 ts.insert(t); 365 } 366 assert(i == dfs_.end()); 367 368 unsigned loop_a_init = loop_a->get_init_state_number(); 369 assert(loop_a_init == 0); 370 371 // Check if the loop is accepting in the original automaton. 372 bool accepting = false; 373 374 // Iterate on each original state corresponding to the 375 // start of the loop in the determinized automaton. 376 for (auto s: refmap_.states_of(begin->s)) 377 { 378 // Check the product between LOOP_A, and ORIG_A starting 379 // in S. 380 if (!product(loop_a, ref_, loop_a_init, s)->is_empty()) 381 { 382 accepting = true; 383 break; 384 } 385 } 386 return accepting; 387 } 388 389 // std::ostream& 390 // print_set(std::ostream& o, const edge_set& s) const 391 // { 392 // o << "{ "; 393 // for (auto i: s) 394 // o << i << ' '; 395 // o << '}'; 396 // return o; 397 // } 398 399 virtual bool cycle_found(unsigned start)400 cycle_found(unsigned start) override 401 { 402 cycle_iter i = dfs_.begin(); 403 while (i->s != start) 404 ++i; 405 edge_set ts; 406 bool is_acc = is_cycle_accepting(i, ts); 407 do 408 ++i; 409 while (i != dfs_.end()); 410 if (is_acc) 411 { 412 accept_.emplace_back(ts); 413 all_.insert(ts.begin(), ts.end()); 414 } 415 else 416 { 417 for (auto t: ts) 418 { 419 reject_.insert(t); 420 for (auto& j: accept_) 421 j.erase(t); 422 all_.erase(t); 423 } 424 } 425 426 // Abort this algorithm if we have seen too many cycles, i.e., 427 // when cycle_left_ *reaches* 0. (If cycle_left_ == 0, that 428 // means we had no limit.) 429 return (cycles_left_ == 0) || --cycles_left_; 430 } 431 }; 432 433 static bool fix_dba_acceptance(twa_graph_ptr det,const_twa_graph_ptr ref,power_map & refmap,unsigned threshold)434 fix_dba_acceptance(twa_graph_ptr det, 435 const_twa_graph_ptr ref, power_map& refmap, 436 unsigned threshold) 437 { 438 det->copy_acceptance_of(ref); 439 440 scc_info sm(det, scc_info_options::NONE); 441 442 unsigned scc_count = sm.scc_count(); 443 444 fix_scc_acceptance fsa(sm, ref, refmap, threshold); 445 446 for (unsigned m = 0; m < scc_count; ++m) 447 if (!sm.is_trivial(m)) 448 if (fsa.fix_scc(m)) 449 return true; 450 return false; 451 } 452 } 453 454 twa_graph_ptr tba_determinize(const const_twa_graph_ptr & aut,unsigned threshold_states,unsigned threshold_cycles)455 tba_determinize(const const_twa_graph_ptr& aut, 456 unsigned threshold_states, unsigned threshold_cycles) 457 { 458 power_map pm; 459 // Do not merge edges in the deterministic automaton. If we 460 // add two self-loops labeled by "a" and "!a", we do not want 461 // these to be merged as "1" before the acceptance has been fixed. 462 463 unsigned max_states = aut->num_states() * threshold_states; 464 if (max_states == 0) 465 max_states = ~0U; 466 output_aborter aborter(max_states); 467 auto det = tgba_powerset(aut, pm, false, &aborter); 468 if (!det) 469 return nullptr; 470 if (fix_dba_acceptance(det, aut, pm, threshold_cycles)) 471 return nullptr; 472 det->merge_edges(); 473 return det; 474 } 475 476 twa_graph_ptr tba_determinize_check(const twa_graph_ptr & aut,unsigned threshold_states,unsigned threshold_cycles,formula f,const_twa_graph_ptr neg_aut)477 tba_determinize_check(const twa_graph_ptr& aut, 478 unsigned threshold_states, 479 unsigned threshold_cycles, 480 formula f, 481 const_twa_graph_ptr neg_aut) 482 { 483 if (f == nullptr && neg_aut == nullptr) 484 return nullptr; 485 if (aut->num_sets() > 1) 486 return nullptr; 487 488 auto det = tba_determinize(aut, threshold_states, threshold_cycles); 489 490 if (!det) 491 return nullptr; 492 493 if (neg_aut == nullptr) 494 { 495 neg_aut = ltl_to_tgba_fm(formula::Not(f), aut->get_dict()); 496 // Remove useless SCCs. 497 neg_aut = scc_filter(neg_aut, true); 498 } 499 500 if (!det->intersects(neg_aut) && !aut->intersects(dualize(det))) 501 // Determinization was safe. 502 return det; 503 504 return aut; 505 } 506 } 507