diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 3b3522bec..b5d877f7d 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -25,7 +25,6 @@ #include #include #include "scc.hh" -#include "isweakscc.hh" #include "tgba/bddprint.hh" #include "ltlast/constant.hh" #include "stats.hh" @@ -206,10 +205,8 @@ namespace spot typedef std::map rev_map; rev_map revtransid; rev_map revtransacc; - std::set weak_scc; std::map prodid; - std::map pathcand; std::map pathid_ref; std::map pathid_cand; int nvars; @@ -245,10 +242,6 @@ namespace spot state_based_(state_based), sm_(sm) { d.nvars = 0; - unsigned count = sm.scc_count(); - for (unsigned i = 0; i < count; ++i) - if (!sm_.trivial(i) && is_weak_scc(sm, i)) - d.weak_scc.insert(i); } int size() @@ -272,15 +265,14 @@ namespace spot { unsigned i_scc = sm_.scc_of_state(d.int_to_state[i]); - bool is_weak = sm_.trivial(i_scc) - || (d.weak_scc.find(i_scc) != d.weak_scc.end()); + bool is_trivial = sm_.trivial(i_scc); for (int j = 1; j <= d.cand_size; ++j) { d.prodid[state_pair(j, i)] = ++d.nvars; - // skip weak or trivial SCCs - if (is_weak) + // skip trivial SCCs + if (is_trivial) continue; for (int k = 1; k <= size_; ++k) @@ -325,17 +317,6 @@ namespace spot } } } - - - if (!d.weak_scc.empty()) - { - for (int i = 1; i <= d.cand_size; ++i) - for (int j = 1; j <= d.cand_size; ++j) - { - state_pair pc(i, j); - d.pathcand[pc] = ++d.nvars; - } - } } }; @@ -487,49 +468,6 @@ namespace spot delete it; } - if (!d.weak_scc.empty()) - { - dout << "Rules for tracking paths in the candidate\n"; - - for (int q1 = 1; q1 <= d.cand_size; q1++) - { - state_pair q1q1(q1, q1); - int q1q1id = d.pathcand[q1q1]; - dout << q1q1 << "C\n"; - out << q1q1id << " 0\n"; - ++nclauses; - for (int q2 = 1; q2 <= d.cand_size; q2++) - { - state_pair q1q2(q1, q2); - int q1q2id = d.pathcand[q1q2]; - - for (int q3 = 1; q3 <= d.cand_size; q3++) - { - if (q3 == q1) - continue; - state_pair q1q3(q1, q3); - int q1q3id = d.pathcand[q1q3]; - - bdd all = bddtrue; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - - transition t(q2, s, q3); - int ti = d.transid[t]; - - dout << q1q2 << "C ∧ " << t << "δ → " - << q1q3 << "C\n"; - out << -q1q2id << ' ' << -ti << ' ' << q1q3id - << " 0\n"; - ++nclauses; - } - } - } - } - } - bdd all_acc = ref->all_acceptance_conditions(); // construction of contraints (4,5) : all loops in the product @@ -546,163 +484,87 @@ namespace spot // cycle, so they must belong to the same SCC. if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc) continue; - if (d.weak_scc.find(q1p_scc) == d.weak_scc.end()) - { - // The SCC is not weak. - for (int q1 = 1; q1 <= d.cand_size; ++q1) - for (int q2 = 1; q2 <= d.cand_size; ++q2) + for (int q1 = 1; q1 <= d.cand_size; ++q1) + for (int q2 = 1; q2 <= d.cand_size; ++q2) + { + path p1(q1, q1p, q2, q2p); + + dout << "(4&5) matching paths from reference based on " + << p1 << "\n"; + + int pid1; + if (q1 == q2 && q1p == q2p) + pid1 = d.prodid[state_pair(q1, q1p)]; + else + pid1 = d.pathid_ref[p1]; + + tgba_succ_iterator* it = + ref->succ_iter(d.int_to_state[q2p]); + for (it->first(); !it->done(); it->next()) { - path p1(q1, q1p, q2, q2p); - - dout << "(4&5) matching paths from reference based on " - << p1 << "\n"; - - int pid1; - if (q1 == q2 && q1p == q2p) - pid1 = d.prodid[state_pair(q1, q1p)]; - else - pid1 = d.pathid_ref[p1]; - - tgba_succ_iterator* it = - ref->succ_iter(d.int_to_state[q2p]); - for (it->first(); !it->done(); it->next()) + const state* dps = it->current_state(); + // Skip destinations not in the SCC. + if (sm.scc_of_state(dps) != q1p_scc) { - const state* dps = it->current_state(); - // Skip destinations not in the SCC. - if (sm.scc_of_state(dps) != q1p_scc) - { - dps->destroy(); - continue; - } - int dp = d.state_to_int[dps]; dps->destroy(); + continue; + } + int dp = d.state_to_int[dps]; + dps->destroy(); - if (it->current_acceptance_conditions() == all_acc) - continue; - for (int q3 = 1; q3 <= d.cand_size; ++q3) + if (it->current_acceptance_conditions() == all_acc) + continue; + for (int q3 = 1; q3 <= d.cand_size; ++q3) + { + if (dp == q1p && q3 == q1) // (4) looping { - if (dp == q1p && q3 == q1) // (4) looping + bdd all = it->current_condition(); + while (all != bddfalse) { - bdd all = it->current_condition(); - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, - bddfalse); - all -= s; - - transition t(q2, s, q1); - int ti = d.transid[t]; - int ta = d.transacc[t]; - - dout << p1 << "R ∧ " << t << "δ → ¬" - << t << "F\n"; - out << -pid1 << " " << -ti << " " - << -ta << " 0\n"; - ++nclauses; - } + bdd s = bdd_satoneset(all, ap, bddfalse); + all -= s; + transition t(q2, s, q1); + int ti = d.transid[t]; + int ta = d.transacc[t]; + dout << p1 << "R ∧ " << t << "δ → ¬" << t + << "F\n"; + out << -pid1 << " " << -ti << " " + << -ta << " 0\n"; + ++nclauses; } - else // (5) not looping + + + } + else // (5) not looping + { + path p2 = path(q1, q1p, q3, dp); + int pid2 = d.pathid_ref[p2]; + + if (pid1 == pid2) + continue; + + bdd all = it->current_condition(); + while (all != bddfalse) { - path p2 = path(q1, q1p, q3, dp); - int pid2 = d.pathid_ref[p2]; + bdd s = bdd_satoneset(all, ap, bddfalse); + all -= s; - if (pid1 == pid2) - continue; + transition t(q2, s, q3); + int ti = d.transid[t]; - bdd all = it->current_condition(); - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, - bddfalse); - all -= s; - - transition t(q2, s, q3); - int ti = d.transid[t]; - - dout << p1 << "R ∧ " << t << "δ → " - << p2 << "R\n"; - out << -pid1 << " " << -ti << " " - << pid2 << " 0\n"; - ++nclauses; - } + dout << p1 << "R ∧ " << t << "δ → " << p2 + << "R\n"; + out << -pid1 << " " << -ti << " " + << pid2 << " 0\n"; + ++nclauses; } } } - delete it; } - } - else // The SCC is weak. - { - for (int q1 = 1; q1 <= d.cand_size; ++q1) - { - state_pair q1q1p(q1, q1p); - int q1q1pid = d.prodid[q1q1p]; - - for (int q2 = 1; q2 <= d.cand_size; ++q2) - { - state_pair q2q2p(q2, q2p); - int q2q2pid = d.prodid[q2q2p]; - - state_pair q1q2(q1, q2); - int q1q2id = d.pathcand[q1q2]; - - tgba_succ_iterator* it = - ref->succ_iter(d.int_to_state[q2p]); - - - for (it->first(); !it->done(); it->next()) - { - const state* dps = it->current_state(); - int dp = d.state_to_int[dps]; - dps->destroy(); - // Skip destinations different from q1. - if (dp != q1p) - continue; - - bdd all = it->current_condition(); - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, - bddfalse); - all -= s; - - transition t(q2, s, q1); - int tid = d.transid[t]; - int tacc = d.transacc[t]; - - if (sm.accepting(q1p_scc)) - { - dout << q1q1p << " ∧ " - << q2q2p << " ∧ " - << q1q2 << "C ∧ " - << t << "δ → " << t << "F \n"; - out << -q1q1pid << ' ' - << -q2q2pid << ' ' - << -q1q2id << ' ' - << -tid << ' ' - << tacc << " 0\n"; - } - else - { - dout << q1q1p << " ∧ " - << q2q2p << " ∧ " - << q1q2 << "C ∧ " - << t << "δ → ¬" << t << "F \n"; - out << -q1q1pid << ' ' - << -q2q2pid << ' ' - << -q1q2id << ' ' - << -tid << ' ' - << -tacc << " 0\n"; - } - ++nclauses; - } - } - delete it; - } - } - } + delete it; + } } } // construction of contraints (6,7): all loops in the product @@ -719,9 +581,6 @@ namespace spot // cycle, so they must belong to the same SCC. if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc) continue; - // Weak SCCs have already be dealt with. - if (d.weak_scc.find(q1p_scc) != d.weak_scc.end()) - continue; for (int q1 = 1; q1 <= d.cand_size; ++q1) for (int q2 = 1; q2 <= d.cand_size; ++q2) {