1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2013-2015, 2017-2021 Laboratoire de Recherche et 3 // Développement 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 <deque> 22 #include <map> 23 #include <spot/twaalgos/complement.hh> 24 #include <spot/twaalgos/dualize.hh> 25 #include <spot/twaalgos/isdet.hh> 26 #include <spot/twaalgos/alternation.hh> 27 #include <spot/twaalgos/postproc.hh> 28 #include <spot/twaalgos/strength.hh> 29 #include <spot/twaalgos/sccinfo.hh> 30 31 namespace spot 32 { 33 twa_graph_ptr dtwa_complement(const const_twa_graph_ptr & aut)34 dtwa_complement(const const_twa_graph_ptr& aut) 35 { 36 if (!is_deterministic(aut)) 37 throw 38 std::runtime_error("dtwa_complement() requires a deterministic input"); 39 40 return dualize(aut); 41 } 42 43 namespace 44 { 45 enum ncsb 46 { 47 ncsb_n = 0, // non deterministic 48 ncsb_c = 2, // needs check 49 ncsb_cb = 3, // needs check AND in breakpoint 50 ncsb_s = 4, // safe 51 ncsb_m = 1, // missing 52 }; 53 54 typedef std::vector<ncsb> mstate; 55 typedef std::vector<std::pair<unsigned, ncsb>> small_mstate; 56 57 struct small_mstate_hash 58 { 59 size_t operator ()spot::__anonbc804fff0111::small_mstate_hash60 operator()(small_mstate s) const noexcept 61 { 62 size_t hash = 0; 63 for (const auto& p: s) 64 { 65 hash = wang32_hash(hash ^ ((p.first<<2) | p.second)); 66 } 67 return hash; 68 } 69 }; 70 71 class ncsb_complementation 72 { 73 private: 74 // The source automaton. 75 const const_twa_graph_ptr aut_; 76 77 // SCCs information of the source automaton. 78 scc_info si_; 79 80 // Number of states in the input automaton. 81 unsigned nb_states_; 82 83 // The complement being built. 84 twa_graph_ptr res_; 85 86 // Association between NCSB states and state numbers of the 87 // complement. 88 std::unordered_map<small_mstate, unsigned, small_mstate_hash> ncsb2n_; 89 90 // States to process. 91 std::deque<std::pair<mstate, unsigned>> todo_; 92 93 // Support for each state of the source automaton. 94 std::vector<bdd> support_; 95 96 // Propositions compatible with all transitions of a state. 97 std::vector<bdd> compat_; 98 99 // Whether a SCC is deterministic or not 100 std::vector<bool> is_deter_; 101 102 // Whether a state only has accepting transitions 103 std::vector<bool> is_accepting_; 104 105 // State names for graphviz display 106 std::vector<std::string>* names_; 107 108 // Show NCSB states in state name to help debug 109 bool show_names_; 110 111 std::string get_name(const small_mstate & ms)112 get_name(const small_mstate& ms) 113 { 114 std::string res = "{"; 115 116 bool first_state = true; 117 for (const auto& p: ms) 118 if (p.second == ncsb_n) 119 { 120 if (!first_state) 121 res += ","; 122 first_state = false; 123 res += std::to_string(p.first); 124 } 125 126 res += "},{"; 127 128 first_state = true; 129 for (const auto& p: ms) 130 if (p.second & ncsb_c) 131 { 132 if (!first_state) 133 res += ","; 134 first_state = false; 135 res += std::to_string(p.first); 136 } 137 138 res += "},{"; 139 140 first_state = true; 141 for (const auto& p: ms) 142 if (p.second == ncsb_s) 143 { 144 if (!first_state) 145 res += ","; 146 first_state = false; 147 res += std::to_string(p.first); 148 } 149 150 res += "},{"; 151 152 first_state = true; 153 for (const auto& p: ms) 154 if (p.second == ncsb_cb) 155 { 156 if (!first_state) 157 res += ","; 158 first_state = false; 159 res += std::to_string(p.first); 160 } 161 162 return res + "}"; 163 } 164 165 small_mstate to_small_mstate(const mstate & ms)166 to_small_mstate(const mstate& ms) 167 { 168 unsigned count = 0; 169 for (unsigned i = 0; i < nb_states_; ++i) 170 count+= (ms[i] != ncsb_m); 171 small_mstate small; 172 small.reserve(count); 173 for (unsigned i = 0; i < nb_states_; ++i) 174 if (ms[i] != ncsb_m) 175 small.emplace_back(i, ms[i]); 176 return small; 177 } 178 179 // From a NCSB state, looks for a duplicate in the map before 180 // creating a new state if needed. 181 unsigned new_state(mstate && s)182 new_state(mstate&& s) 183 { 184 auto p = ncsb2n_.emplace(to_small_mstate(s), 0); 185 if (p.second) // This is a new state 186 { 187 p.first->second = res_->new_state(); 188 if (show_names_) 189 names_->push_back(get_name(p.first->first)); 190 todo_.emplace_back(std::move(s), p.first->second); 191 } 192 return p.first->second; 193 } 194 195 void ncsb_successors(mstate && ms,unsigned origin,bdd letter)196 ncsb_successors(mstate&& ms, unsigned origin, bdd letter) 197 { 198 std::vector<mstate> succs; 199 succs.emplace_back(nb_states_, ncsb_m); 200 201 // Handle S states. 202 // 203 // Treated first because we can escape early if the letter 204 // leads to an accepting transition for a Safe state. 205 for (unsigned i = 0; i < nb_states_; ++i) 206 { 207 if (ms[i] != ncsb_s) 208 continue; 209 210 for (const auto& t: aut_->out(i)) 211 { 212 if (!bdd_implies(letter, t.cond)) 213 continue; 214 if (t.acc || is_accepting_[t.dst]) 215 // Exit early; transition is forbidden for safe 216 // state. 217 return; 218 219 succs[0][t.dst] = ncsb_s; 220 221 // No need to look for other compatible transitions 222 // for this state; it's in the deterministic part of 223 // the automaton 224 break; 225 } 226 } 227 228 // Handle C states. 229 for (unsigned i = 0; i < nb_states_; ++i) 230 { 231 if (!(ms[i] & ncsb_c)) 232 continue; 233 234 bool has_succ = false; 235 for (const auto& t: aut_->out(i)) 236 { 237 if (!bdd_implies(letter, t.cond)) 238 continue; 239 240 has_succ = true; 241 242 // state can become safe, if transition is accepting 243 // and destination isn't an accepting state 244 if (t.acc) 245 { 246 // double all the current possible states 247 unsigned length = succs.size(); 248 for (unsigned j = 0; j < length; ++j) 249 { 250 if (succs[j][t.dst] == ncsb_m) 251 { 252 if (!is_accepting_[t.dst]) 253 { 254 succs.push_back(succs[j]); 255 succs.back()[t.dst] = ncsb_s; 256 } 257 succs[j][t.dst] = ncsb_c; 258 } 259 } 260 } 261 else // state stays in check 262 { 263 // remove states that should stay in s (ncsb_s), 264 // and mark the other as ncsb_c. 265 // The first two loops form a kind of remove_if() 266 // that set the non-removed states to ncsb_c. 267 auto it = succs.begin(); 268 auto end = succs.end(); 269 for (; it != end; ++it) 270 if ((*it)[t.dst] != ncsb_s) 271 (*it)[t.dst] = ncsb_c; 272 else 273 break; 274 if (it != end) 275 for (auto it2 = it; ++it2 != end;) 276 if ((*it2)[t.dst] != ncsb_s) 277 *it++ = std::move(*it2); 278 succs.erase(it, end); 279 } 280 // No need to look for other compatible transitions 281 // for this state; it's in the deterministic part of 282 // the automaton 283 break; 284 } 285 if (!has_succ && !is_accepting_[i]) 286 return; 287 } 288 289 // Handle N states. 290 for (unsigned i = 0; i < nb_states_; ++i) 291 { 292 if (ms[i] != ncsb_n) 293 continue; 294 for (const auto& t: aut_->out(i)) 295 { 296 if (!bdd_implies(letter, t.cond)) 297 continue; 298 299 if (is_deter_[si_.scc_of(t.dst)]) 300 { 301 // double all the current possible states 302 unsigned length = succs.size(); 303 for (unsigned j = 0; j < length; ++j) 304 { 305 if (succs[j][t.dst] == ncsb_m) 306 { 307 // Can become safe if the destination is 308 // not an accepting state. 309 if (!is_accepting_[t.dst]) 310 { 311 succs.push_back(succs[j]); 312 succs.back()[t.dst] = ncsb_s; 313 } 314 succs[j][t.dst] = ncsb_c; 315 } 316 } 317 } 318 else 319 for (auto& succ: succs) 320 succ[t.dst] = ncsb_n; 321 } 322 } 323 324 // Revisit B states to see if they still exist in successors. 325 // This is done at the end because we need to know all of the 326 // states present in C before this stage 327 bool b_empty = true; 328 for (unsigned i = 0; i < nb_states_; ++i) 329 { 330 if (ms[i] != ncsb_cb) 331 continue; 332 333 // The original B set wasn't empty 334 b_empty = false; 335 336 for (const auto& t: aut_->out(i)) 337 { 338 if (!bdd_implies(letter, t.cond)) 339 continue; 340 341 for (auto& succ: succs) 342 { 343 if (succ[t.dst] == ncsb_c) 344 succ[t.dst] = ncsb_cb; 345 } 346 347 // No need to look for other compatible transitions 348 // for this state; it's in the deterministic part of 349 // the automaton 350 break; 351 } 352 } 353 354 // If B was empty, then set every c_not_b to cb in successors 355 if (b_empty) 356 for (auto& succ: succs) 357 for (unsigned i = 0; i < succ.size(); ++i) 358 if (succ[i] == ncsb_c) 359 succ[i] = ncsb_cb; 360 361 // create the automaton states 362 for (auto& succ: succs) 363 { 364 bool b_empty = true; 365 for (const auto& state: succ) 366 if (state == ncsb_cb) 367 { 368 b_empty = false; 369 break; 370 } 371 if (b_empty) // becomes accepting 372 { 373 for (unsigned i = 0; i < succ.size(); ++i) 374 if (succ[i] == ncsb_c) 375 succ[i] = ncsb_cb; 376 unsigned dst = new_state(std::move(succ)); 377 res_->new_edge(origin, dst, letter, {0}); 378 } 379 else 380 { 381 unsigned dst = new_state(std::move(succ)); 382 res_->new_edge(origin, dst, letter); 383 } 384 } 385 } 386 387 public: ncsb_complementation(const const_twa_graph_ptr & aut,bool show_names)388 ncsb_complementation(const const_twa_graph_ptr& aut, bool show_names) 389 : aut_(aut), 390 si_(aut), 391 nb_states_(aut->num_states()), 392 support_(nb_states_), 393 compat_(nb_states_), 394 is_accepting_(nb_states_), 395 show_names_(show_names) 396 { 397 res_ = make_twa_graph(aut->get_dict()); 398 res_->copy_ap_of(aut); 399 res_->set_buchi(); 400 401 // Generate bdd supports and compatible options for each state. 402 // Also check if all its transitions are accepting. 403 for (unsigned i = 0; i < nb_states_; ++i) 404 { 405 bdd res_support = bddtrue; 406 bdd res_compat = bddfalse; 407 bool accepting = true; 408 bool has_transitions = false; 409 for (const auto& out: aut->out(i)) 410 { 411 has_transitions = true; 412 res_support &= bdd_support(out.cond); 413 res_compat |= out.cond; 414 if (!out.acc) 415 accepting = false; 416 } 417 support_[i] = res_support; 418 compat_[i] = res_compat; 419 is_accepting_[i] = accepting && has_transitions; 420 } 421 422 423 424 // Compute which SCCs are part of the deterministic set. 425 is_deter_ = semidet_sccs(si_); 426 427 if (show_names_) 428 { 429 names_ = new std::vector<std::string>(); 430 res_->set_named_prop("state-names", names_); 431 } 432 433 // Because we only handle one initial state, we assume it 434 // belongs to the N set. (otherwise the automaton would be 435 // deterministic) 436 unsigned init_state = aut->get_init_state_number(); 437 mstate new_init_state(nb_states_, ncsb_m); 438 new_init_state[init_state] = ncsb_n; 439 res_->set_init_state(new_state(std::move(new_init_state))); 440 } 441 442 twa_graph_ptr run()443 run() 444 { 445 // Main stuff happens here 446 447 while (!todo_.empty()) 448 { 449 auto top = todo_.front(); 450 todo_.pop_front(); 451 452 mstate ms = top.first; 453 454 // Compute support of all available states. 455 bdd msupport = bddtrue; 456 bdd n_s_compat = bddfalse; 457 bdd c_compat = bddtrue; 458 bool c_empty = true; 459 for (unsigned i = 0; i < nb_states_; ++i) 460 if (ms[i] != ncsb_m) 461 { 462 msupport &= support_[i]; 463 if (ms[i] == ncsb_n || ms[i] == ncsb_s || is_accepting_[i]) 464 n_s_compat |= compat_[i]; 465 else 466 { 467 c_empty = false; 468 c_compat &= compat_[i]; 469 } 470 } 471 472 bdd all; 473 if (!c_empty) 474 all = c_compat; 475 else 476 { 477 all = n_s_compat; 478 if (all != bddtrue) 479 { 480 mstate empty_state(nb_states_, ncsb_m); 481 res_->new_edge(top.second, 482 new_state(std::move(empty_state)), 483 !all, 484 {0}); 485 } 486 } 487 for (bdd one: minterms_of(all, msupport)) 488 // Compute all new states available from the generated 489 // letter. 490 ncsb_successors(std::move(ms), top.second, one); 491 } 492 493 res_->merge_edges(); 494 return res_; 495 } 496 }; 497 498 } 499 500 twa_graph_ptr complement_semidet(const const_twa_graph_ptr & aut,bool show_names)501 complement_semidet(const const_twa_graph_ptr& aut, bool show_names) 502 { 503 if (!is_semi_deterministic(aut)) 504 throw std::runtime_error 505 ("complement_semidet() requires a semi-deterministic input"); 506 507 auto ncsb = ncsb_complementation(aut, show_names); 508 return ncsb.run(); 509 } 510 511 twa_graph_ptr complement(const const_twa_graph_ptr & aut,const output_aborter * aborter)512 complement(const const_twa_graph_ptr& aut, const output_aborter* aborter) 513 { 514 if (!aut->is_existential() || is_universal(aut)) 515 return dualize(aut); 516 if (is_very_weak_automaton(aut)) 517 return remove_alternation(dualize(aut), aborter); 518 // Determinize 519 spot::option_map m; 520 if (aborter) 521 { 522 m.set("det-max-states", aborter->max_states()); 523 m.set("det-max-edges", aborter->max_edges()); 524 } 525 if (aut->num_states() > 32) 526 { 527 m.set("ba-simul", 0); 528 m.set("simul", 0); 529 } 530 spot::postprocessor p(&m); 531 p.set_type(spot::postprocessor::Generic); 532 p.set_pref(spot::postprocessor::Deterministic); 533 p.set_level(spot::postprocessor::Low); 534 auto det = p.run(std::const_pointer_cast<twa_graph>(aut)); 535 if (!det || !is_universal(det)) 536 return nullptr; 537 return dualize(det); 538 } 539 } 540