alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) <exprop>: Do not

Browse source 
blindly enumerate all combinations of atomic properties; initially
set all_props to the set of all possibly satisfiable combinations.
This commit is contained in:
Alexandre Duret-Lutz 2004-03-08 17:24:17 +00:00
parent 3aec630540
commit 249a114f29
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2004-03-08 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) <exprop>: 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 <adl@src.lip6.fr> 2004-02-21 Alexandre Duret-Lutz <adl@src.lip6.fr>
* lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover * lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover

14
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -497,7 +497,7 @@ namespace spot
// with same source/destination and acceptance conditions. This // with same source/destination and acceptance conditions. This
// is the goal of the `dests' hash. // 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 // better to encode `f U g' as
// r(f U g) = g + a(g).r(X(f U g)).f.!g // r(f U g) = g + a(g).r(X(f U g)).f.!g
// because that leads to a deterministic automaton. In order // because that leads to a deterministic automaton. In order
@ -512,9 +512,19 @@ namespace spot
typedef Sgi::hash_map<const formula*, prom_map, ptr_hash<formula> > typedef Sgi::hash_map<const formula*, prom_map, ptr_hash<formula> >
dest_map; dest_map;
dest_map dests; dest_map dests;
// Compute all outgoing arcs. // 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); 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) while (all_props != bddfalse)
{ {
bdd one_prop_set = bdd one_prop_set =