From 249a114f29de34dc2c1ee75ccca467e36b11fb26 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 Mar 2004 17:24:17 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) : Do not blindly enumerate all combinations of atomic properties; initially set all_props to the set of all possibly satisfiable combinations. --- ChangeLog | 6 ++++++ src/tgbaalgos/ltl2tgba_fm.cc | 14 ++++++++++++-- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5cecd9a3b..f79ce6276 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2004-03-08 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) : Do not + blindly enumerate all combinations of atomic properties; initially + set all_props to the set of all possibly satisfiable combinations. + 2004-02-21 Alexandre Duret-Lutz * lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index e469e64e2..d1afe23b8 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -497,7 +497,7 @@ namespace spot // with same source/destination and acceptance conditions. This // is the goal of the `dests' hash. // - // Note that this is still not optimal. For instance it us + // Note that this is still not optimal. For instance it is // better to encode `f U g' as // r(f U g) = g + a(g).r(X(f U g)).f.!g // because that leads to a deterministic automaton. In order @@ -512,9 +512,19 @@ namespace spot typedef Sgi::hash_map > dest_map; dest_map dests; + // Compute all outgoing arcs. - bdd all_props = bddtrue; + + // If EXPROP is set, we will refine the symbolic + // representation of the successors for all combinations of + // the atomic properties involved in the formula. + // VAR_SET is the set of these properties. bdd var_set = bdd_existcomp(bdd_support(res), d.var_set); + // ALL_PROPS is the combinations we have yet to consider. + // We used to start with `all_props = bddtrue', but it is + // more efficient to start with the set of all satisfiable + // variables combinations. + bdd all_props = bdd_existcomp(res, d.var_set); while (all_props != bddfalse) { bdd one_prop_set =