* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make

sure to compute the status of the most Now variables possible.
This helps to identify equivalant states.
(tgba_bdd_concrete): Call set_init_state.

ChangeLog

+2003-06-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make
+	sure to compute the status of the most Now variables possible.
+	This helps to identify equivalant states.
+	(tgba_bdd_concrete): Call set_init_state.
+
 2003-06-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G.

src/tgba/tgbabddconcrete.cc

@@ -10,8 +10,9 @@ namespace spot
   }
 
   tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
-    : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init)
+    : data_(fact.get_core_data()), dict_(fact.get_dict())
   {
+    set_init_state(init);
   }
 
   tgba_bdd_concrete::~tgba_bdd_concrete()
@@ -21,6 +22,40 @@ namespace spot
   void
   tgba_bdd_concrete::set_init_state(bdd s)
   {
+    // Usually, the ltl2tgba translator will return an
+    // initial state which does not include all true Now variables,
+    // even though the truth of some Now variables is garanteed.
+    //
+    // For instance, when building the automata for the formula GFa,
+    // the translator will define the following two equivalences
+    //    Now[Fa] <=> a | (Prom[a] & Next[Fa])
+    //    Now[GFa] <=> Now[Fa] & Next[GFa]
+    // and return Now[GFa] as initial state.
+    //
+    // Starting for state Now[GFa], we could then build
+    // the following automaton:
+    //    In state Now[GFa]:
+    //        if `a', go to state Now[GFa]
+    //        if True, go to state Now[GFa] & Now[Fa] with Prom[a]
+    //    In state Now[GFa] & Now[Fa]:
+    //        if `a', go to state Now[GFa]
+    //        if True, go to state Now[GFa] & Now[Fa] with Prom[a]
+    //
+    // As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share
+    // the same actions.  This is no surprise, because
+    // Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences
+    // defined by the translator.
+    //
+    // What sounds bogus is that we dissociated the two states:
+    // there should be only one, so that the automaton become
+    //
+    //    In state Now[GFa] & Now[Fa]:
+    //        if `a', go to state Now[GFa] & Now[GFa]
+    //        if True, go to state Now[GFa] & Now[Fa] with Prom[a]
+    //
+    // To achieve this, we immerse the state into the relation
+    // to collect the status of other Now variables.
+    s &= bdd_relprod(s, data_.relation, data_.notnow_set);
     init_ = s;
   }
 
@@ -44,6 +79,21 @@ namespace spot
     bdd succ_set = bdd_replace(bdd_exist(data_.relation & s->as_bdd(),
 					 data_.now_set),
 			       data_.next_to_now);
+
+    // Immerse known Now variables into the relation to compute the
+    // status of any other Now variables.  See the comment in
+    // set_init_state for the rational.  Note that unlike
+    // set_init_state, we work only from the Now variables, not from
+    // any other atomic propositions around.  This is because the Now
+    // variables and the atomic propositions do not correspond to the
+    // same instant: atomic propositions describe what we must verify
+    // now while Now variables describe the state where we go (and
+    // where something else we have to be checked) -- actually these
+    // Now variables are really Next variables renammed for
+    // convenience.
+    succ_set &= bdd_relprod(bdd_exist(succ_set, data_.notnow_set),
+			    data_.relation, data_.notnow_set);
+
     return new tgba_succ_iterator_concrete(data_, succ_set);
   }