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

ltlcross --save-inclusion-products: name the saved automata

Browse source 
* bin/ltlcross.cc: Name saved automata for easier tracking.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-11 23:06:19 +01:00
parent 124de77925
commit f9f4fd1c89
1 changed files with 21 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

25
bin/ltlcross.cc
View file

@ -772,7 +772,8 @@ namespace
static bool static bool
check_empty_prod(const spot::const_twa_graph_ptr& aut_i, check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
const spot::const_twa_graph_ptr& aut_j, const spot::const_twa_graph_ptr& aut_j,
size_t i, size_t j, bool icomp, bool jcomp) size_t i, size_t j, bool icomp, bool jcomp,
const std::string& formula)
{ {
if (aut_i->num_sets() + aut_j->num_sets() > if (aut_i->num_sets() + aut_j->num_sets() >
spot::acc_cond::mark_t::max_accsets()) spot::acc_cond::mark_t::max_accsets())
@ -800,7 +801,20 @@ namespace
auto prod = spot::product(aut_i, aut_j); auto prod = spot::product(aut_i, aut_j);
if (saved_inclusion_products) if (saved_inclusion_products)
{
std::ostringstream os;
if (icomp)
os << "Comp(N" << i << ')';
else
os << 'P' << i;
if (jcomp)
os << "*Comp(P" << j << ')';
else
os << "*N" << j;
os << ", " << formula;
prod->set_named_prop("automaton-name", new std::string(os.str()));
spot::print_hoa(saved_inclusion_products->ostream(), prod) << std::endl; spot::print_hoa(saved_inclusion_products->ostream(), prod) << std::endl;
}
if (verbose) if (verbose)
{ {
@ -1384,7 +1398,8 @@ namespace
smallest_pos_ref >= 0 && smallest_pos_ref >= 0 &&
(size_t)smallest_pos_ref != i))) (size_t)smallest_pos_ref != i)))
problems += problems +=
check_empty_prod(pos[i], neg[j], i, j, false, false); check_empty_prod(pos[i], neg[j], i, j, false, false,
fstr);
// Deal with the extra complemented automata if we // Deal with the extra complemented automata if we
// have some. // have some.
@ -1405,17 +1420,17 @@ namespace
if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref) if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref)
problems += problems +=
check_empty_prod(pos[i], comp_pos[j], check_empty_prod(pos[i], comp_pos[j],
i, j, false, true); i, j, false, true, fstr);
if (i != j && comp_neg[i] && !comp_pos[i]) if (i != j && comp_neg[i] && !comp_pos[i])
if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref) if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref)
problems += problems +=
check_empty_prod(comp_neg[i], neg[j], check_empty_prod(comp_neg[i], neg[j],
i, j, true, false); i, j, true, false, fstr);
if (comp_pos[i] && comp_neg[j] && if (comp_pos[i] && comp_neg[j] &&
(i == j || (!comp_neg[i] && !comp_pos[j]))) (i == j || (!comp_neg[i] && !comp_pos[j])))
problems += problems +=
check_empty_prod(comp_neg[j], comp_pos[i], check_empty_prod(comp_neg[j], comp_pos[i],
j, i, true, true); j, i, true, true, fstr);
} }
} }
else else