1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2021 Laboratoire de Recherche et 3 // Developpement 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 #include "config.h" 21 #include <ostream> 22 #include <sstream> 23 #include <cstring> 24 #include <map> 25 #include <spot/twa/twa.hh> 26 #include <spot/twa/twagraph.hh> 27 #include <spot/twaalgos/hoa.hh> 28 #include <spot/misc/escape.hh> 29 #include <spot/misc/bddlt.hh> 30 #include <spot/misc/minato.hh> 31 #include <spot/twa/formula2bdd.hh> 32 #include <spot/tl/formula.hh> 33 #include <spot/kripke/fairkripke.hh> 34 35 using namespace std::string_literals; 36 37 namespace spot 38 { 39 namespace 40 { 41 struct metadata final 42 { 43 // Assign a number to each atomic proposition. 44 typedef std::map<int, unsigned> ap_map; 45 ap_map ap; 46 typedef std::vector<int> vap_t; 47 vap_t vap; 48 49 std::vector<bool> common_acc; 50 bool has_state_acc; 51 bool is_complete; 52 bool is_universal; 53 bool is_colored; 54 bool use_implicit_labels; 55 bool use_state_labels = true; 56 bdd all_ap; 57 58 // Label support: the set of all conditions occurring in the 59 // automaton. 60 typedef std::map<bdd, std::string, bdd_less_than> sup_map; 61 sup_map sup; 62 metadataspot::__anon81d34ea30111::metadata63 metadata(const const_twa_graph_ptr& aut, bool implicit, 64 bool state_labels) 65 { 66 check_det_and_comp(aut); 67 use_implicit_labels = implicit && is_universal && is_complete; 68 use_state_labels &= state_labels; 69 number_all_ap(aut); 70 } 71 72 std::ostream& emit_accspot::__anon81d34ea30111::metadata73 emit_acc(std::ostream& os, acc_cond::mark_t b) 74 { 75 // FIXME: We could use a cache for this. 76 if (!b) 77 return os; 78 os << " {"; 79 bool notfirst = false; 80 for (auto v: b.sets()) 81 { 82 if (notfirst) 83 os << ' '; 84 else 85 notfirst = true; 86 os << v; 87 } 88 os << '}'; 89 return os; 90 } 91 check_det_and_compspot::__anon81d34ea30111::metadata92 void check_det_and_comp(const const_twa_graph_ptr& aut) 93 { 94 std::string empty; 95 96 unsigned ns = aut->num_states(); 97 bool universal = true; 98 bool complete = true; 99 bool state_acc = true; 100 bool nodeadend = true; 101 bool colored = aut->num_sets() >= 1; 102 for (unsigned src = 0; src < ns; ++src) 103 { 104 bdd sum = bddfalse; 105 bdd available = bddtrue; 106 bool st_acc = true; 107 bool notfirst = false; 108 acc_cond::mark_t prev = {}; 109 bool has_succ = false; 110 bdd lastcond = bddfalse; 111 for (auto& t: aut->out(src)) 112 { 113 if (has_succ) 114 use_state_labels &= lastcond == t.cond; 115 else 116 lastcond = t.cond; 117 if (complete) 118 sum |= t.cond; 119 if (universal) 120 { 121 if (!bdd_implies(t.cond, available)) 122 universal = false; 123 else 124 available -= t.cond; 125 } 126 sup.insert(std::make_pair(t.cond, empty)); 127 if (st_acc) 128 { 129 if (notfirst && prev != t.acc) 130 { 131 st_acc = false; 132 } 133 else 134 { 135 notfirst = true; 136 prev = t.acc; 137 } 138 } 139 if (colored) 140 { 141 auto a = t.acc; 142 if (!a || a.remove_some(1)) 143 colored = false; 144 } 145 has_succ = true; 146 } 147 nodeadend &= has_succ; 148 if (complete) 149 complete &= sum == bddtrue; 150 common_acc.push_back(st_acc); 151 state_acc &= st_acc; 152 } 153 is_universal = universal; 154 is_complete = complete; 155 has_state_acc = state_acc; 156 // If the automaton has state-based acceptance and contain 157 // some states without successors do not declare it as 158 // colored. 159 is_colored = colored && (!has_state_acc || nodeadend); 160 // If the automaton declares that it is universal or 161 // state-based, make sure that it really is. 162 if (aut->prop_universal().is_true() && !universal) 163 throw std::runtime_error("print_hoa(): automaton is not universal" 164 " but prop_universal()==true"); 165 if (aut->prop_universal().is_false() && universal) 166 throw std::runtime_error("print_hoa(): automaton is universal" 167 " despite prop_universal()==false"); 168 if (aut->prop_complete().is_true() && !complete) 169 throw std::runtime_error("print_hoa(): automaton is not complete" 170 " but prop_complete()==true"); 171 if (aut->prop_complete().is_false() && complete) 172 throw std::runtime_error("print_hoa(): automaton is complete" 173 " but prop_complete()==false"); 174 if (aut->prop_state_acc() && !state_acc) 175 throw std::runtime_error("print_hoa(): automaton has " 176 "transition-based acceptance despite" 177 " prop_state_acc()==true"); 178 } 179 number_all_apspot::__anon81d34ea30111::metadata180 void number_all_ap(const const_twa_graph_ptr& aut) 181 { 182 // Make sure that the automaton uses only atomic propositions 183 // that have been registered via twa::register_ap() or some 184 // variant. If that is not the case, it is a bug that should 185 // be fixed in the function creating the automaton. Since 186 // that function could be written by the user, throw an 187 // exception rather than using an assert(). 188 bdd all = bddtrue; 189 for (auto& i: sup) 190 all &= bdd_support(i.first); 191 all_ap = aut->ap_vars(); 192 if (bdd_exist(all, all_ap) != bddtrue) 193 throw std::runtime_error("print_hoa(): automaton uses " 194 "unregistered atomic propositions"); 195 all = all_ap; 196 197 while (all != bddtrue) 198 { 199 int v = bdd_var(all); 200 all = bdd_high(all); 201 ap.insert(std::make_pair(v, vap.size())); 202 vap.emplace_back(v); 203 } 204 205 if (use_implicit_labels) 206 return; 207 208 for (auto& i: sup) 209 { 210 bdd cond = i.first; 211 if (cond == bddtrue) 212 { 213 i.second = "t"; 214 continue; 215 } 216 if (cond == bddfalse) 217 { 218 i.second = "f"; 219 continue; 220 } 221 std::ostringstream s; 222 bool notfirstor = false; 223 224 minato_isop isop(cond); 225 bdd cube; 226 while ((cube = isop.next()) != bddfalse) 227 { 228 if (notfirstor) 229 s << " | "; 230 bool notfirstand = false; 231 while (cube != bddtrue) 232 { 233 if (notfirstand) 234 s << '&'; 235 else 236 notfirstand = true; 237 bdd h = bdd_high(cube); 238 if (h == bddfalse) 239 { 240 s << '!' << ap[bdd_var(cube)]; 241 cube = bdd_low(cube); 242 } 243 else 244 { 245 s << ap[bdd_var(cube)]; 246 cube = h; 247 } 248 } 249 notfirstor = true; 250 } 251 i.second = s.str(); 252 } 253 } 254 }; 255 256 } 257 258 enum hoa_acceptance 259 { 260 Hoa_Acceptance_States, /// state-based acceptance if 261 /// (globally) possible 262 /// transition-based acceptance 263 /// otherwise. 264 Hoa_Acceptance_Transitions, /// transition-based acceptance globally 265 Hoa_Acceptance_Mixed /// mix state-based and transition-based 266 }; 267 268 static std::ostream& print_hoa(std::ostream & os,const const_twa_graph_ptr & aut,const char * opt)269 print_hoa(std::ostream& os, 270 const const_twa_graph_ptr& aut, 271 const char* opt) 272 { 273 bool newline = true; 274 hoa_acceptance acceptance = Hoa_Acceptance_States; 275 bool implicit_labels = false; 276 bool verbose = false; 277 bool state_labels = false; 278 bool v1_1 = false; 279 280 if (opt) 281 while (*opt) 282 { 283 switch (char c = *opt++) 284 { 285 case '1': 286 if (opt[0] == '.' && opt[1] == '1') 287 { 288 v1_1 = true; 289 opt += 2; 290 } 291 else if (opt[0] == '.' && opt[1] == '0') 292 { 293 v1_1 = false; 294 opt += 2; 295 } 296 else 297 { 298 v1_1 = false; 299 } 300 break; 301 case 'i': 302 implicit_labels = true; 303 break; 304 case 'k': 305 state_labels = true; 306 break; 307 case 'K': 308 state_labels = false; 309 break; 310 case 'l': 311 newline = false; 312 break; 313 case 'm': 314 acceptance = Hoa_Acceptance_Mixed; 315 break; 316 case 's': 317 acceptance = Hoa_Acceptance_States; 318 break; 319 case 't': 320 acceptance = Hoa_Acceptance_Transitions; 321 break; 322 case 'v': 323 verbose = true; 324 break; 325 default: 326 throw std::runtime_error("unknown option for print_hoa(): "s + c); 327 } 328 } 329 330 metadata md(aut, implicit_labels, state_labels); 331 332 if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) 333 acceptance = Hoa_Acceptance_Transitions; 334 335 auto print_dst = [&os, &aut](unsigned dst) 336 { 337 bool notfirst = false; 338 for (unsigned d: aut->univ_dests(dst)) 339 { 340 if (notfirst) 341 os << '&'; 342 else 343 notfirst = true; 344 os << d; 345 } 346 }; 347 348 unsigned num_states = aut->num_states(); 349 unsigned init = aut->get_init_state_number(); 350 351 const char nl = newline ? '\n' : ' '; 352 os << (v1_1 ? "HOA: v1.1" : "HOA: v1") << nl; 353 auto n = aut->get_named_prop<std::string>("automaton-name"); 354 if (n) 355 escape_str(os << "name: \"", *n) << '"' << nl; 356 unsigned nap = md.vap.size(); 357 os << "States: " << num_states << nl 358 << "Start: "; 359 print_dst(init); 360 os << nl 361 << "AP: " << nap; 362 auto d = aut->get_dict(); 363 for (auto& i: md.vap) 364 escape_str(os << " \"", d->bdd_map[i].f.ap_name()) << '"'; 365 os << nl; 366 367 unsigned num_acc = aut->num_sets(); 368 acc_cond::acc_code acc_c = aut->acc().get_acceptance(); 369 if (aut->acc().is_generalized_buchi()) 370 { 371 if (aut->acc().is_all()) 372 os << "acc-name: all"; 373 else if (aut->acc().is_buchi()) 374 os << "acc-name: Buchi"; 375 else 376 os << "acc-name: generalized-Buchi " << num_acc; 377 os << nl; 378 } 379 else if (aut->acc().is_generalized_co_buchi()) 380 { 381 if (aut->acc().is_none()) 382 os << "acc-name: none"; 383 else if (aut->acc().is_co_buchi()) 384 os << "acc-name: co-Buchi"; 385 else 386 os << "acc-name: generalized-co-Buchi " << num_acc; 387 os << nl; 388 } 389 else 390 { 391 int r = aut->acc().is_rabin(); 392 assert(r != 0); 393 if (r > 0) 394 { 395 os << "acc-name: Rabin " << r << nl; 396 // Force the acceptance to remove any duplicate sets, and 397 // make sure it is correctly ordered. 398 acc_c = acc_cond::acc_code::rabin(r); 399 } 400 else 401 { 402 r = aut->acc().is_streett(); 403 assert(r != 0); 404 if (r > 0) 405 { 406 os << "acc-name: Streett " << r << nl; 407 // Force the acceptance to remove any duplicate sets, and 408 // make sure it is correctly ordered. 409 acc_c = acc_cond::acc_code::streett(r); 410 } 411 else 412 { 413 std::vector<unsigned> pairs; 414 if (aut->acc().is_generalized_rabin(pairs)) 415 { 416 os << "acc-name: generalized-Rabin " << pairs.size(); 417 for (auto p: pairs) 418 os << ' ' << p; 419 os << nl; 420 // Force the acceptance to remove any duplicate 421 // sets, and make sure it is correctly ordered. 422 acc_c = acc_cond::acc_code::generalized_rabin(pairs.begin(), 423 pairs.end()); 424 } 425 else 426 { 427 bool max = false; 428 bool odd = false; 429 if (aut->acc().is_parity(max, odd)) 430 os << "acc-name: parity " 431 << (max ? "max " : "min ") 432 << (odd ? "odd " : "even ") 433 << num_acc << nl; 434 } 435 } 436 } 437 } 438 os << "Acceptance: " << num_acc << ' '; 439 os << acc_c; 440 os << nl; 441 os << "properties:"; 442 // Make sure the property line is not too large, 443 // otherwise our test cases do not fit in 80 columns... 444 unsigned prop_len = 60; 445 auto prop = [&](const char* str) 446 { 447 if (newline) 448 { 449 auto l = strlen(str); 450 if (prop_len < l) 451 { 452 prop_len = 60; 453 os << "\nproperties:"; 454 } 455 prop_len -= l; 456 } 457 os << str; 458 }; 459 implicit_labels = md.use_implicit_labels; 460 state_labels = md.use_state_labels; 461 if (implicit_labels) 462 prop(" implicit-labels"); 463 else if (state_labels) 464 prop(" state-labels explicit-labels"); 465 else 466 prop(" trans-labels explicit-labels"); 467 if (acceptance == Hoa_Acceptance_States) 468 prop(" state-acc"); 469 else if (acceptance == Hoa_Acceptance_Transitions) 470 prop(" trans-acc"); 471 if (md.is_colored) 472 prop(" colored"); 473 else if (verbose && v1_1) 474 prop(" !colored"); 475 if (md.is_complete) 476 prop(" complete"); 477 else if (v1_1) 478 prop(" !complete"); 479 // The definition of "deterministic" was changed between HOA v1 480 // (were it meant "universal") and HOA v1.1 were it means 481 // ("universal" and "existential"). 482 if (!v1_1) 483 { 484 if (md.is_universal) 485 prop(" deterministic"); 486 // It's probable that nobody cares about the "no-univ-branch" 487 // property. The "univ-branch" property seems more important to 488 // announce that the automaton might not be parsable by tools that 489 // do not support alternating automata. 490 if (!aut->is_existential()) 491 { 492 prop(" univ-branch"); 493 } 494 else if (verbose) 495 { 496 if (v1_1) 497 prop(" !univ-branch"); 498 else 499 prop(" no-univ-branch"); 500 } 501 } 502 else 503 { 504 if (md.is_universal && aut->is_existential()) 505 { 506 prop(" deterministic"); 507 if (verbose) 508 prop(" !univ-branch !exist-branch"); 509 } 510 else 511 { 512 prop(" !deterministic"); 513 if (!aut->is_existential()) 514 prop(" univ-branch"); 515 else if (verbose) 516 prop(" !univ-branch"); 517 if (!md.is_universal) 518 prop(" exist-branch"); 519 else if (verbose) 520 prop(" !exist-branch"); 521 } 522 } 523 // Deterministic automata are also unambiguous, so writing both 524 // properties seems redundant. People working on unambiguous 525 // automata are usually concerned about non-deterministic 526 // unambiguous automata. So do not mention "unambiguous" 527 // in the case of deterministic automata. 528 if (aut->prop_unambiguous() && (verbose || !md.is_universal)) 529 prop(" unambiguous"); 530 else if (v1_1 && !aut->prop_unambiguous()) 531 prop(" !unambiguous"); 532 if (aut->prop_semi_deterministic() && (verbose || !md.is_universal)) 533 prop(" semi-deterministic"); 534 else if (v1_1 && !aut->prop_semi_deterministic()) 535 prop(" !semi-deterministic"); 536 if (aut->prop_stutter_invariant()) 537 prop(" stutter-invariant"); 538 if (!aut->prop_stutter_invariant()) 539 { 540 if (v1_1) 541 prop(" !stutter-invariant"); 542 else 543 prop(" stutter-sensitive"); 544 } 545 if (aut->prop_terminal()) 546 prop(" terminal"); 547 if (aut->prop_very_weak() && (verbose || aut->prop_terminal() != true)) 548 prop(" very-weak"); 549 if (aut->prop_weak() && (verbose || (aut->prop_terminal() != true && 550 aut->prop_very_weak() != true))) 551 prop(" weak"); 552 if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true)) 553 prop(" inherently-weak"); 554 if (v1_1 && !aut->prop_terminal() && (verbose || aut->prop_weak() != false)) 555 prop(" !terminal"); 556 if (v1_1 && !aut->prop_very_weak() && (verbose 557 || aut->prop_weak() != false)) 558 prop(" !very-weak"); 559 if (v1_1 && !aut->prop_weak() && (verbose || 560 aut->prop_inherently_weak() != false)) 561 prop(" !weak"); 562 if (v1_1 && !aut->prop_inherently_weak()) 563 prop(" !inherently-weak"); 564 os << nl; 565 566 // highlighted states and edges are only output in the 1.1 format, 567 // because we use a dot in the header name. 568 if (v1_1) 569 { 570 if (auto hstates = aut->get_named_prop 571 <std::map<unsigned, unsigned>>("highlight-states")) 572 { 573 os << "spot.highlight.states:"; 574 for (auto& p: *hstates) 575 os << ' ' << p.first << ' ' << p.second; 576 os << nl; 577 } 578 if (auto hedges = aut->get_named_prop 579 <std::map<unsigned, unsigned>>("highlight-edges")) 580 { 581 // Numbering edges is a delicate process. The 582 // "highlight-edges" property uses edges numbers that are 583 // indices in the "edges" vector. However these edges 584 // need not be sorted. When edges are output in HOA, they 585 // are output with increasing source state number, and the 586 // edges number expected in the HOA file should use that 587 // order. So we need to make a first pass on the 588 // automaton to number all edges as they will be output. 589 unsigned maxedge = aut->edge_vector().size(); 590 std::vector<unsigned> renum(maxedge); 591 unsigned edge = 0; 592 for (unsigned i = 0; i < num_states; ++i) 593 for (auto& t: aut->out(i)) 594 renum[aut->get_graph().index_of_edge(t)] = ++edge; 595 os << "spot.highlight.edges:"; 596 for (auto& p: *hedges) 597 if (p.first < maxedge) // highlighted edges could come from user 598 os << ' ' << renum[p.first] << ' ' << p.second; 599 os << nl; 600 } 601 } 602 if (auto word = aut->get_named_prop<std::string>("accepted-word")) 603 { 604 os << (v1_1 ? "spot." : "spot-") << "accepted-word: \""; 605 escape_str(os, *word) << '"' << nl; 606 } 607 if (auto word = aut->get_named_prop<std::string>("rejected-word")) 608 { 609 os << (v1_1 ? "spot." : "spot-") << "rejected-word: \""; 610 escape_str(os, *word) << '"' << nl; 611 } 612 if (auto player = aut->get_named_prop<std::vector<bool>>("state-player")) 613 { 614 os << (v1_1 ? "spot." : "spot-") << "state-player:"; 615 if (player->size() != num_states) 616 throw std::runtime_error("print_hoa(): state-player property has" 617 " (" + std::to_string(player->size()) + 618 " states but automaton has " + 619 std::to_string(num_states)); 620 unsigned n = 0; 621 while (n < num_states) 622 { 623 os << ' ' << (*player)[n]; 624 ++n; 625 if (newline && n < num_states && (n % 30 == 0)) 626 os << "\n "; 627 } 628 os << nl; 629 } 630 631 // If we want to output implicit labels, we have to 632 // fill a vector with all destinations in order. 633 std::vector<unsigned> out; 634 std::vector<acc_cond::mark_t> outm; 635 if (implicit_labels) 636 { 637 out.resize(1UL << nap); 638 if (acceptance != Hoa_Acceptance_States) 639 outm.resize(1UL << nap); 640 } 641 642 os << "--BODY--" << nl; 643 644 auto sn = aut->get_named_prop<std::vector<std::string>>("state-names"); 645 for (unsigned i = 0; i < num_states; ++i) 646 { 647 hoa_acceptance this_acc = acceptance; 648 if (this_acc == Hoa_Acceptance_Mixed) 649 this_acc = (md.common_acc[i] ? 650 Hoa_Acceptance_States : Hoa_Acceptance_Transitions); 651 652 os << "State: "; 653 if (state_labels) 654 { 655 bool output = false; 656 for (auto& t: aut->out(i)) 657 { 658 os << '[' << md.sup[t.cond] << "] "; 659 output = true; 660 break; 661 } 662 if (!output) 663 os << "[f] "; 664 } 665 os << i; 666 if (sn && i < sn->size() && !(*sn)[i].empty()) 667 os << " \"" << (*sn)[i] << '"'; 668 if (this_acc == Hoa_Acceptance_States) 669 { 670 acc_cond::mark_t acc = {}; 671 for (auto& t: aut->out(i)) 672 { 673 acc = t.acc; 674 break; 675 } 676 md.emit_acc(os, acc); 677 } 678 os << nl; 679 680 if (!implicit_labels && !state_labels) 681 { 682 683 for (auto& t: aut->out(i)) 684 { 685 os << '[' << md.sup[t.cond] << "] "; 686 print_dst(t.dst); 687 if (this_acc == Hoa_Acceptance_Transitions) 688 md.emit_acc(os, t.acc); 689 os << nl; 690 } 691 } 692 else if (state_labels) 693 { 694 unsigned n = 0; 695 for (auto& t: aut->out(i)) 696 { 697 print_dst(t.dst); 698 if (this_acc == Hoa_Acceptance_Transitions) 699 { 700 md.emit_acc(os, t.acc); 701 os << nl; 702 } 703 else 704 { 705 ++n; 706 os << (((n & 15) && t.next_succ) ? ' ' : nl); 707 } 708 } 709 } 710 else 711 { 712 for (auto& t: aut->out(i)) 713 for (bdd one: minterms_of(t.cond, md.all_ap)) 714 { 715 unsigned level = 1; 716 unsigned pos = 0U; 717 while (one != bddtrue) 718 { 719 bdd h = bdd_high(one); 720 if (h == bddfalse) 721 { 722 one = bdd_low(one); 723 } 724 else 725 { 726 pos |= level; 727 one = h; 728 } 729 level <<= 1; 730 } 731 out[pos] = t.dst; 732 if (this_acc != Hoa_Acceptance_States) 733 outm[pos] = t.acc; 734 } 735 unsigned n = out.size(); 736 for (unsigned i = 0; i < n;) 737 { 738 print_dst(out[i]); 739 if (this_acc != Hoa_Acceptance_States) 740 { 741 md.emit_acc(os, outm[i]) << nl; 742 ++i; 743 } 744 else 745 { 746 ++i; 747 os << (((i & 15) && i < n) ? ' ' : nl); 748 } 749 } 750 } 751 } 752 os << "--END--"; // No newline. Let the caller decide. 753 return os; 754 } 755 756 std::ostream& print_hoa(std::ostream & os,const const_twa_ptr & aut,const char * opt)757 print_hoa(std::ostream& os, 758 const const_twa_ptr& aut, 759 const char* opt) 760 { 761 bool preserve_names = false; 762 // for Kripke structures, automatically append "k" to the options. 763 // (Unless "K" was given.) 764 char* tmpopt = nullptr; 765 if (std::dynamic_pointer_cast<const fair_kripke>(aut) && 766 (!opt || (strchr(opt, 'K') == nullptr))) 767 { 768 unsigned n = opt ? strlen(opt) : 0; 769 tmpopt = new char[n + 2]; 770 if (opt) 771 strcpy(tmpopt, opt); 772 tmpopt[n] = 'k'; 773 tmpopt[n + 1] = 0; 774 preserve_names = true; 775 } 776 777 auto a = std::dynamic_pointer_cast<const twa_graph>(aut); 778 if (!a) 779 a = make_twa_graph(aut, twa::prop_set::all(), preserve_names); 780 781 print_hoa(os, a, tmpopt ? tmpopt : opt); 782 delete[] tmpopt; 783 return os; 784 } 785 786 } 787