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

ltlsynt: Correct segfault with ds algorithm and verbose

Browse source 
* bin/ltlsynt.cc: Use initialized DPA when printing when
 we use DET_SPLIT and verbose.
This commit is contained in:
Florian Renkin 2020-03-22 16:04:44 +01:00
parent e827d3a634
commit 6489d6c091
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
bin/ltlsynt.cc
View file

@ -318,8 +318,8 @@ namespace
auto tmp = to_dpa(aut); auto tmp = to_dpa(aut);
if (verbose) if (verbose)
std::cerr << "determinization done\nDPA has " std::cerr << "determinization done\nDPA has "
<< dpa->num_states() << " states, " << tmp->num_states() << " states, "
<< dpa->num_sets() << " colors\n"; << tmp->num_sets() << " colors\n";
tmp->merge_states(); tmp->merge_states();
if (verbose) if (verbose)
std::cerr << "simplification done\nDPA has " std::cerr << "simplification done\nDPA has "
@ -327,7 +327,7 @@ namespace
dpa = split_2step(tmp, all_inputs); dpa = split_2step(tmp, all_inputs);
if (verbose) if (verbose)
std::cerr << "split inputs and outputs done\nautomaton has " std::cerr << "split inputs and outputs done\nautomaton has "
<< dpa->num_states() << " states\n"; << tmp->num_states() << " states\n";
spot::colorize_parity_here(dpa, true); spot::colorize_parity_here(dpa, true);
break; break;
} }