From 03d9a7512ac41fe8ca2d4c63899f0bde008fa23b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Feb 2016 12:10:53 +0100 Subject: [PATCH] determinize: do not work on deterministic automata * spot/twaalgos/determinize.cc: Here. --- spot/twaalgos/determinize.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index d3a3c66e2..cbaad7d63 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -611,6 +611,9 @@ namespace spot bool pretty_print, bool use_scc, bool use_simulation, bool use_stutter) { + if (a->prop_deterministic()) + return std::const_pointer_cast(a); + // Degeneralize twa_graph_ptr aut = spot::degeneralize_tba(a); std::map implications;