From d13c9c179baa50b8a03a36a56793dfaed89b0126 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 Feb 2004 16:26:15 +0000
Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify
 states with identical successors.  This optimizes the translation of `a R (b
 R c)', for instance. * src/tgbatest/ltl2tgba.test: Add two new tests.

---
 src/tgbaalgos/ltl2tgba_fm.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index c47906c27..0fd6cbd0f 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -476,6 +476,7 @@ namespace spot
 	// Translate it into a BDD to simplify it.
 	f->accept(v);
 	bdd res = v.result();
+	canonical_succ[res] = f;
 
 	std::string now = to_string(f);