From 6489d6c091d23f47d8b0474ac68be483c9d19a4c Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Sun, 22 Mar 2020 16:04:44 +0100 Subject: [PATCH] ltlsynt: Correct segfault with ds algorithm and verbose * bin/ltlsynt.cc: Use initialized DPA when printing when we use DET_SPLIT and verbose. --- bin/ltlsynt.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index e92d36f2d..1e4225d52 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -318,8 +318,8 @@ namespace auto tmp = to_dpa(aut); if (verbose) std::cerr << "determinization done\nDPA has " - << dpa->num_states() << " states, " - << dpa->num_sets() << " colors\n"; + << tmp->num_states() << " states, " + << tmp->num_sets() << " colors\n"; tmp->merge_states(); if (verbose) std::cerr << "simplification done\nDPA has " @@ -327,7 +327,7 @@ namespace dpa = split_2step(tmp, all_inputs); if (verbose) 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); break; }