From 1aa10e139597c38505c004b54f24a0e7c1539711 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Fri, 18 Dec 2009 12:19:07 +0100 Subject: [PATCH] * src/tgba/tgbabddcoredata.cc (delete_unaccepting_scc): Fix a bug. * src/tgbatest/spotlbtt.test: Use the above function with LaCIM for ELTL which greatly reduce the size of the automata! --- ChangeLog | 6 ++++++ src/tgba/tgbabddcoredata.cc | 2 +- src/tgbatest/spotlbtt.test | 2 +- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 032334e5b..ba3172a58 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2009-11-10 Damien Lefortier + + * src/tgba/tgbabddcoredata.cc (delete_unaccepting_scc): Fix a bug. + * src/tgbatest/spotlbtt.test: Use the above function with LaCIM + for ELTL which greatly reduce the size of the automata! + 2009-12-11 Alexandre Duret-Lutz * src/misc/timer.hh (timer::timer): Initialize running... diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 7a633b120..a24a63ee4 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -162,7 +162,7 @@ namespace spot } } - relation = s0 & (relation & bdd_replace(s0, dict->now_to_next)); + relation = (relation & bdd_replace(s0, dict->now_to_next)); } bdd diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 9769a09fc..ae7a85211 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -73,7 +73,7 @@ Algorithm Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc" Path = "${LBTT_TRANSLATE}" Parameters = "--spot '../eltl2tgba -L'" - Enabled = no + Enabled = yes } Algorithm