diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 0287166b1..5b7947221 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -239,6 +239,8 @@ namespace spot degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, bool use_lvl_cache) { + bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; + bdd_dict* dict = a->get_dict(); // The result (degeneralized) automaton uses numbered state. @@ -295,15 +297,13 @@ namespace spot typedef std::map tr_cache_t; tr_cache_t tr_cache; - - // State level cash + // State level cache typedef std::map lvl_cache_t; lvl_cache_t lvl_cache; - // Compute SCCs in order to use custom acc order for each SCC - // or lvl_cache + // Compute SCCs in order to use any optimization. scc_map m(a); - if (use_cust_acc_orders || use_lvl_cache) + if (use_cust_acc_orders || use_lvl_cache || use_z_lvl) m.build_map(); queue_t todo; @@ -337,15 +337,15 @@ namespace spot std::mapnames; names[s.first] = 1; - ds2num[s] = 10000*names[s.first] + 100*s.second + m.scc_of_state(s.first); + ds2num[s] = 10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first); #else ds2num[s] = 0; #endif todo.push_back(s); - // If use_lvl_cache is on insert initial state to level cash - // Level cash stores first encountered level for each state. + // If use_lvl_cache is on insert initial state to level cache + // Level cache stores first encountered level for each state. // When entering an SCC first the lvl_cache is checked. // If such state exists level from chache is used. // If not, a new level (starting with 0) is computed. @@ -367,7 +367,7 @@ namespace spot // Check SCC for state s int s_scc = -1; - if (use_lvl_cache || use_cust_acc_orders) + if (use_scc) s_scc = m.scc_of_state(s.first); tgba_succ_iterator* i = a->succ_iter(s.first); @@ -382,8 +382,8 @@ namespace spot // Check whether the target's SCC is accepting bool is_scc_acc = false; - int scc = m.scc_of_state(i->current_state()); - if (m.accepting(scc)) + int scc = use_scc ? m.scc_of_state(i->current_state()) : -1; + if (!use_scc || m.accepting(scc)) is_scc_acc = true; // The old level is slevel. What should be the new one? @@ -460,10 +460,11 @@ namespace spot { acc |= otheracc; // If use_z_lvl is on, start with level zero 0 when swhitching SCCs - unsigned next = (!use_z_lvl || s_scc == scc)?slevel:0; + unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0; - // If lvl_cache is used and switching SCCs, use level from cahce - if (use_lvl_cache && s_scc != scc && lvl_cache.find(d.first) != lvl_cache.end()) + // If lvl_cache is used and switching SCCs, use level from cache + if (use_lvl_cache && s_scc != scc + && lvl_cache.find(d.first) != lvl_cache.end()) { d.second = lvl_cache[d.first]; } @@ -497,13 +498,13 @@ namespace spot else { #ifdef DEGEN_DEBUG - dest = 10000*names[d.first] + 100*d.second + scc; + dest = 10000 * names[d.first] + 100 * d.second + scc; #else dest = ds2num.size(); #endif ds2num[d] = dest; todo.push_back(d); - // Insert new state to cash + // Insert new state to cache if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end()) lvl_cache[d.first] = d.second; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 742d3403a..1c3871abe 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -197,6 +197,10 @@ syntax(char* prog) << "(SGBA)" << std::endl << " -D degeneralize the automaton as a TBA" << std::endl << " -DS degeneralize the automaton as an SBA" << std::endl + << " (append z/Z, o/O, l/L: to turn on/off options " + << "(default: zol)\n " + << " z: level resetting, o: adaptive order, " + << "l: level cache)\n" << std::endl << "Automaton simplifications (after translation):" @@ -326,6 +330,9 @@ main(int argc, char** argv) bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; bool file_opt = false; + bool degen_reset = true; + bool degen_order = true; + bool degen_cache = true; int output = 0; int formula_index = 0; const char* echeck_algo = 0; @@ -427,9 +434,34 @@ main(int argc, char** argv) { degeneralize_opt = DegenTBA; } - else if (!strcmp(argv[formula_index], "-DS")) + else if (!strncmp(argv[formula_index], "-DS", 3)) { degeneralize_opt = DegenSBA; + const char* p = argv[formula_index] + 3; + while (*p) + { + switch (*p++) + { + case 'o': + degen_order = true; + break; + case 'O': + degen_order = false; + break; + case 'z': + degen_reset = true; + break; + case 'Z': + degen_reset = false; + break; + case 'l': + degen_cache = true; + break; + case 'L': + degen_cache = false; + break; + } + } } else if (!strncmp(argv[formula_index], "-e", 2)) { @@ -1157,7 +1189,10 @@ main(int argc, char** argv) else if (degeneralize_opt == DegenSBA) { tm.start("degeneralization"); - degeneralized = a = spot::degeneralize(a); + degeneralized = a = spot::degeneralize(a, + degen_reset, + degen_order, + degen_cache); tm.stop("degeneralization"); assume_sba = true; } @@ -1301,7 +1336,11 @@ main(int argc, char** argv) else if (degeneralize_opt == DegenSBA) { tm.start("degeneralize product"); - product_degeneralized = a = spot::degeneralize(a); + product_degeneralized = a = + spot::degeneralize(a, + degen_reset, + degen_order, + degen_cache); tm.stop("degeneralize product"); assume_sba = true; } @@ -1390,7 +1429,11 @@ main(int argc, char** argv) // It is possible that we have applied other // operations to the automaton since its initial // degeneralization. Let's degeneralize again! - spot::unique_ptr s(spot::degeneralize(a)); + spot::unique_ptr + s(spot::degeneralize(a, + degen_reset, + degen_order, + degen_cache)); spot::never_claim_reachable(std::cout, s, f, spin_comments); } break;