alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

degen: small fixups and interface with ltl2tgba

Browse source 
* src/tgbaalgos/degen.cc: Fixups.
* src/tgbatest/ltl2tgba.cc: Add switches to enable/disable
the options Tomáš added to degeneralize().
This commit is contained in:
Alexandre Duret-Lutz 2012-12-06 00:34:00 +01:00
parent bb1aa0ca13
commit c04951c444
2 changed files with 64 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/tgbaalgos/degen.cc
View file

@ -239,6 +239,8 @@ namespace spot
degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
bool use_lvl_cache) bool use_lvl_cache)
{ {
bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
bdd_dict* dict = a->get_dict(); bdd_dict* dict = a->get_dict();
// The result (degeneralized) automaton uses numbered state. // The result (degeneralized) automaton uses numbered state.
@ -295,15 +297,13 @@ namespace spot
typedef std::map<int, state_explicit_number::transition*> tr_cache_t; typedef std::map<int, state_explicit_number::transition*> tr_cache_t;
tr_cache_t tr_cache; tr_cache_t tr_cache;
// State level cache
// State level cash
typedef std::map<const state*, int> lvl_cache_t; typedef std::map<const state*, int> lvl_cache_t;
lvl_cache_t lvl_cache; lvl_cache_t lvl_cache;
// Compute SCCs in order to use custom acc order for each SCC // Compute SCCs in order to use any optimization.
// or lvl_cache
scc_map m(a); 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(); m.build_map();
queue_t todo; queue_t todo;
@ -337,15 +337,15 @@ namespace spot
std::map<const state*, int>names; std::map<const state*, int>names;
names[s.first] = 1; 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 #else
ds2num[s] = 0; ds2num[s] = 0;
#endif #endif
todo.push_back(s); todo.push_back(s);
// If use_lvl_cache is on insert initial state to level cash // If use_lvl_cache is on insert initial state to level cache
// Level cash stores first encountered level for each state. // Level cache stores first encountered level for each state.
// When entering an SCC first the lvl_cache is checked. // When entering an SCC first the lvl_cache is checked.
// If such state exists level from chache is used. // If such state exists level from chache is used.
// If not, a new level (starting with 0) is computed. // If not, a new level (starting with 0) is computed.
@ -367,7 +367,7 @@ namespace spot
// Check SCC for state s // Check SCC for state s
int s_scc = -1; int s_scc = -1;
if (use_lvl_cache || use_cust_acc_orders) if (use_scc)
s_scc = m.scc_of_state(s.first); s_scc = m.scc_of_state(s.first);
tgba_succ_iterator* i = a->succ_iter(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 // Check whether the target's SCC is accepting
bool is_scc_acc = false; bool is_scc_acc = false;
int scc = m.scc_of_state(i->current_state()); int scc = use_scc ? m.scc_of_state(i->current_state()) : -1;
if (m.accepting(scc)) if (!use_scc || m.accepting(scc))
is_scc_acc = true; is_scc_acc = true;
// The old level is slevel. What should be the new one? // The old level is slevel. What should be the new one?
@ -460,10 +460,11 @@ namespace spot
{ {
acc |= otheracc; acc |= otheracc;
// If use_z_lvl is on, start with level zero 0 when swhitching SCCs // 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 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()) if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end())
{ {
d.second = lvl_cache[d.first]; d.second = lvl_cache[d.first];
} }
@ -497,13 +498,13 @@ namespace spot
else else
{ {
#ifdef DEGEN_DEBUG #ifdef DEGEN_DEBUG
dest = 10000*names[d.first] + 100*d.second + scc; dest = 10000 * names[d.first] + 100 * d.second + scc;
#else #else
dest = ds2num.size(); dest = ds2num.size();
#endif #endif
ds2num[d] = dest; ds2num[d] = dest;
todo.push_back(d); 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()) if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end())
lvl_cache[d.first] = d.second; lvl_cache[d.first] = d.second;
} }

51
src/tgbatest/ltl2tgba.cc
View file

@ -197,6 +197,10 @@ syntax(char* prog)
<< "(SGBA)" << std::endl << "(SGBA)" << std::endl
<< " -D degeneralize the automaton as a TBA" << std::endl << " -D degeneralize the automaton as a TBA" << std::endl
<< " -DS degeneralize the automaton as an SBA" << 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 << std::endl
<< "Automaton simplifications (after translation):" << "Automaton simplifications (after translation):"
@ -326,6 +330,9 @@ main(int argc, char** argv)
bool fm_exprop_opt = false; bool fm_exprop_opt = false;
bool fm_symb_merge_opt = true; bool fm_symb_merge_opt = true;
bool file_opt = false; bool file_opt = false;
bool degen_reset = true;
bool degen_order = true;
bool degen_cache = true;
int output = 0; int output = 0;
int formula_index = 0; int formula_index = 0;
const char* echeck_algo = 0; const char* echeck_algo = 0;
@ -427,9 +434,34 @@ main(int argc, char** argv)
{ {
degeneralize_opt = DegenTBA; degeneralize_opt = DegenTBA;
} }
else if (!strcmp(argv[formula_index], "-DS")) else if (!strncmp(argv[formula_index], "-DS", 3))
{ {
degeneralize_opt = DegenSBA; 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)) else if (!strncmp(argv[formula_index], "-e", 2))
{ {
@ -1157,7 +1189,10 @@ main(int argc, char** argv)
else if (degeneralize_opt == DegenSBA) else if (degeneralize_opt == DegenSBA)
{ {
tm.start("degeneralization"); tm.start("degeneralization");
degeneralized = a = spot::degeneralize(a); degeneralized = a = spot::degeneralize(a,
degen_reset,
degen_order,
degen_cache);
tm.stop("degeneralization"); tm.stop("degeneralization");
assume_sba = true; assume_sba = true;
} }
@ -1301,7 +1336,11 @@ main(int argc, char** argv)
else if (degeneralize_opt == DegenSBA) else if (degeneralize_opt == DegenSBA)
{ {
tm.start("degeneralize product"); 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"); tm.stop("degeneralize product");
assume_sba = true; assume_sba = true;
} }
@ -1390,7 +1429,11 @@ main(int argc, char** argv)
// It is possible that we have applied other // It is possible that we have applied other
// operations to the automaton since its initial // operations to the automaton since its initial
// degeneralization. Let's degeneralize again! // degeneralization. Let's degeneralize again!
spot::unique_ptr<spot::tgba> s(spot::degeneralize(a)); spot::unique_ptr<spot::tgba>
s(spot::degeneralize(a,
degen_reset,
degen_order,
degen_cache));
spot::never_claim_reachable(std::cout, s, f, spin_comments); spot::never_claim_reachable(std::cout, s, f, spin_comments);
} }
break; break;