* src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc,

src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
bug in delayed simulation.

* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
src/tgba/tgbareduc.cc: bug in scc reduction.

ChangeLog

@@ -1,3 +1,12 @@
+2004-06-22  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc,
+	src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
+	bug in delayed simulation.
+
+	* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
+	src/tgba/tgbareduc.cc: bug in scc reduction.
+
 2004-06-21  Thomas Martinez  <martinez@src.lip6.fr>
 
 	* src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc:

src/tgba/tgbareduc.cc

@@ -121,7 +121,8 @@ namespace spot
   {
     if (!scc_computed_)
       this->compute_scc();
-    this->delete_scc();
+    // FIXME
+    // this->delete_scc();
   }
 
   std::string
@@ -334,7 +335,7 @@ namespace spot
       name_state_map_[tgba_explicit::format_state(s)];
 
     // for all successor q of s, we remove s of the predecessor of q.
-
+    // Note that the initial node can't be removed.
     for (state::iterator j = st->begin(); j != st->end(); ++j)
       this->remove_predecessor_state((*j)->dest, st);
 
@@ -591,6 +592,8 @@ namespace spot
 		state_scc_v_.erase(i);
 		break;
 	      }
+	    //else
+	    delete s;
 	    std::cout << "end is_terminal" << std::endl;
 	  }
       }

src/tgbaalgos/reductgba_sim.cc

@@ -35,7 +35,7 @@ namespace spot
     sc_ = new state_couple(d_node, s_node);
     lnode_succ = new sn_v;
     lnode_pred = new sn_v;
-    this->not_win = false;
+    not_win = false;
   }
 
   spoiler_node::~spoiler_node()
@@ -50,15 +50,27 @@ namespace spot
   bool
   spoiler_node::add_succ(spoiler_node* n)
   {
-    /*
+    //std::cout << "spoiler_node::add_succ" << std::endl;
     bool exist = false;
     for (sn_v::iterator i = lnode_succ->begin();
-      i != lnode_succ->end();)
+	 i != lnode_succ->end(); ++i)
+      // Be careful, we have to compare two duplicator node
       if (*i == n)
 	exist = true;
     if (exist)
       return false;
+    // TO TEST FOR THE DIRECT SIMULATION //
+    /*
+    bool exist = false;
+    for (sn_v::iterator i = lnode_succ->begin();
+	 i != lnode_succ->end(); ++i)
+      // Be careful, we have to compare two duplicator node
+      if (dynamic_cast<duplicator_node*>(*i)->compare(n) == 0)
+	exist = true;
+    if (exist)
+      return false;
     */
+    ///////////////
     lnode_succ->push_back(n);
     return true;
   }
@@ -81,14 +93,14 @@ namespace spot
   void
   spoiler_node::add_pred(spoiler_node* n)
   {
-    /*
+    // TO TEST FOR THE DIRECT SIMULATION //
     bool exist = false;
     for (sn_v::iterator i = lnode_pred->begin();
-      i != lnode_pred->end();)
+	 i != lnode_pred->end(); ++i)
-      if (*i == n)
+      if ((*i)->compare(n) == 0)
 	exist = true;
     if (!exist)
-    */
+      ///////////////
       lnode_pred->push_back(n);
   }
 
@@ -139,6 +151,14 @@ namespace spot
     return os.str();
   }
 
+  bool
+  spoiler_node::compare(spoiler_node* n)
+  {
+    //std::cout << "spoiler_node::compare" << std::endl;
+    return (((sc_->first)->compare((n->get_pair())->first) == 0) &&
+	    ((sc_->second)->compare((n->get_pair())->second) == 0));
+  }
+
   int
   spoiler_node::get_nb_succ()
   {
@@ -197,6 +217,7 @@ namespace spot
 	    not_win &= (*i)->not_win;
 	  }
       }
+
     return (change != not_win);
   }
 
@@ -212,6 +233,8 @@ namespace spot
        << ", "
        << a->format_state(sc_->second)
        << ", ";
+    bdd_print_acc(os, a->get_dict(), label_);
+    os << ", ";
     bdd_print_acc(os, a->get_dict(), acc_);
     os << ")\"]"
        << std::endl;
@@ -219,6 +242,27 @@ namespace spot
     return os.str();
   }
 
+  bool
+  duplicator_node::compare(spoiler_node* n)
+  {
+    //std::cout << "duplicator_node::compare" << std::endl;
+    return (this->spoiler_node::compare(n) &&
+	    (label_ == dynamic_cast<duplicator_node*>(n)->get_label()) &&
+	    (acc_ == dynamic_cast<duplicator_node*>(n)->get_acc()));
+  }
+
+  bdd
+  duplicator_node::get_label() const
+  {
+    return label_;
+  }
+
+  bdd
+  duplicator_node::get_acc() const
+  {
+    return acc_;
+  }
+
   bool
   duplicator_node::match(bdd l, bdd a)
   {
@@ -552,7 +596,7 @@ namespace spot
 	    // We remove the state in rel from seen
 	    // because the destructor of
 	    // tgba_reachable_iterator_breadth_first
-	    // delete all the state.
+	    // delete all instance of state.
 
 
    	    if ((j = seen.find(p->first)) != seen.end())

src/tgbaalgos/reductgba_sim.hh

@@ -144,6 +144,7 @@ namespace spot
     virtual bool set_win();
     virtual std::string to_string(const tgba* a);
     virtual std::string succ_to_string();
+    virtual bool compare(spoiler_node* n);
 
     const state* get_spoiler_node();
     const state* get_duplicator_node();
@@ -172,10 +173,14 @@ namespace spot
 
     virtual bool set_win();
     virtual std::string to_string(const tgba* a);
+    virtual bool compare(spoiler_node* n);
 
     bool match(bdd l, bdd a);
     bool implies(bdd l, bdd a);
 
+    bdd get_label() const;
+    bdd get_acc() const;
+
   protected:
     bdd label_;
     bdd acc_;
@@ -213,11 +218,12 @@ namespace spot
 
     /// Return true if the progress_measure has changed.
     bool set_win();
-    bdd get_acceptance_condition_visited();
+    bdd get_acceptance_condition_visited() const;
+    virtual bool compare(spoiler_node* n);
 
     virtual std::string to_string(const tgba* a);
 
-    int get_progress_measure();
+    int get_progress_measure() const;
 
   protected:
     /// a Bdd for retain all the acceptance condition
@@ -291,13 +297,18 @@ namespace spot
     /// Compute sub_set_acc_cond_;
     void build_sub_set_acc_cond();
 
-    /// Add a duplicator node, and
+    ///
-    /// all his successor (spoiler node) which
+    duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn,
-    /// have a acceptance_condition_visited_ != bddfalse
+							 const spot::state* dn,
-    void add_dup_node(state* ss,
+							 bdd acc,
-		      state* sd,
+							 bdd label,
-		      bdd l,
+							 int nb);
-		      bdd a);
+
+    ///
+    spoiler_node_delayed* add_spoiler_node_delayed(const spot::state* sn,
+						   const spot::state* dn,
+						   bdd acc,
+						   int nb);
 
     /// \brief Compute the couple as for direct simulation,
     virtual void build_couple();

src/tgbaalgos/reductgba_sim_del.cc

@@ -99,6 +99,16 @@ namespace spot
     return change;
   }
 
+  bool
+  spoiler_node_delayed::compare(spoiler_node* n)
+  {
+    std::cout << "spoiler_node_delayed::compare" << std::endl;
+    return (this->spoiler_node::compare(n) &&
+	    (acceptance_condition_visited_ ==
+	     dynamic_cast<spoiler_node_delayed*>(n)->
+	     get_acceptance_condition_visited()));
+  }
+
   std::string
   spoiler_node_delayed::to_string(const tgba* a)
   {
@@ -128,13 +138,13 @@ namespace spot
   }
 
   bdd
-  spoiler_node_delayed::get_acceptance_condition_visited()
+  spoiler_node_delayed::get_acceptance_condition_visited() const
   {
     return acceptance_condition_visited_;
   }
 
   int
-  spoiler_node_delayed::get_progress_measure()
+  spoiler_node_delayed::get_progress_measure() const
   {
     if ((acceptance_condition_visited_ == bddfalse) &&
 	(progress_measure_ != (nb_spoiler_loose_ + 1)))
@@ -180,7 +190,8 @@ namespace spot
     sn_v::iterator i = lnode_succ->begin();
     if (i != lnode_succ->end())
       {
-	tmpmin = dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
+	tmpmin =
+	  dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
 	/*
 	  debug &= (dynamic_cast<spoiler_node_delayed*>(*i)
 	  ->get_acceptance_condition_visited()
@@ -550,6 +561,7 @@ namespace spot
     //bool exist_pred = false;
 
     sn_v::iterator i1;
+    int n = 0;
     for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1)
       {
 	/*
@@ -584,6 +596,7 @@ namespace spot
 	// We add a link between a spoiler and a (new) duplicator.
 	// The acc of the duplicator must contains the
 	// acceptance_condition_visited_ of the spoiler.
+	std::cout << "build_link : iter " << ++n << std::endl;
 	build_recurse_successor_spoiler(*i1);
 
       }
@@ -615,16 +628,21 @@ namespace spot
 	    if (s->compare(*i1) == 0)
 	      {
 		duplicator_node_delayed* dn
-		  = new duplicator_node_delayed(*i1,
+		  = add_duplicator_node_delayed(*i1,
 						sn->get_duplicator_node(),
 						si->current_condition(),
 						btmp,
 						nb_node_parity_game++);
-		duplicator_vertice_.push_back(dn);
 
 		// dn is already a successor of sn.
+		std::cout << "spoiler call add_succ" << std::endl;
 		if (!(sn->add_succ(dn)))
+		  {
+		    std::cout << "dn is already a successor of sn."
+			      << std::endl;
 		    continue;
+		  }
+		std::cout << "dn is a new successor of sn." << std::endl;
 		(dn)->add_pred(sn);
 
 		/* TEST
@@ -662,6 +680,11 @@ namespace spot
 	    get_acceptance_condition_visited();
 	bdd btmp2 = btmp - si->current_acceptance_conditions();
 
+	/*
+	if (btmp2 == bddfalse)
+	  continue;
+	*/
+
 	s_v::iterator i1;
 	state* s;
 	for (i1 = tgba_state_.begin();
@@ -671,15 +694,20 @@ namespace spot
 	    if (s->compare(*i1) == 0)
 	      {
 		spoiler_node_delayed* sn_n
-		  = new spoiler_node_delayed(sn->get_spoiler_node(),
+		  = add_spoiler_node_delayed(sn->get_spoiler_node(),
 					     *i1,
 					     btmp2,
 					     nb_node_parity_game++);
-		spoiler_vertice_.push_back(sn_n);
 
-		// dn is already a successor of sn.
+		// sn_n is already a successor of dn.
+		std::cout << "duplicator call add_succ" << std::endl;
 		if (!(dn->add_succ(sn_n)))
+		  {
+		    std::cout << "sn_n is already a successor of dn."
+			      << std::endl;
 		    continue;
+		  }
+		std::cout << "sn_n is a new successor of dn." << std::endl;
 		(sn_n)->add_pred(dn);
 
 		build_recurse_successor_spoiler(sn_n);
@@ -693,13 +721,67 @@ namespace spot
 
   }
 
-
+  duplicator_node_delayed*
-  void
+  parity_game_graph_delayed::add_duplicator_node_delayed(const spot::state* sn,
-  parity_game_graph_delayed::add_dup_node(state*,
+							 const spot::state* dn,
-					  state*,
+							 bdd acc,
-					  bdd,
+							 bdd label,
-					  bdd)
+							 int nb)
   {
+    bool exist = false;
+
+    duplicator_node_delayed* dn_n
+      = new duplicator_node_delayed(sn, dn, acc, label, nb);
+
+    for (Sgi::vector<duplicator_node*>::iterator i
+	       = duplicator_vertice_.begin();
+	     i != duplicator_vertice_.end(); ++i)
+      {
+	std::cout << "COMPARE" << std::endl;
+	if (dn_n->compare(*i))
+	  {
+	    exist = true;
+	    delete dn_n;
+	    dn_n = dynamic_cast<duplicator_node_delayed*>(*i);
+	    break;
+	  }
+      }
+
+    if (!exist)
+      duplicator_vertice_.push_back(dn_n);
+
+    return dn_n;
+  }
+
+  spoiler_node_delayed*
+  parity_game_graph_delayed::add_spoiler_node_delayed(const spot::state* sn,
+						      const spot::state* dn,
+						      bdd acc,
+						      int nb)
+  {
+    bool exist = false;
+
+    spoiler_node_delayed* sn_n
+      = new spoiler_node_delayed(sn, dn, acc, nb);
+
+    for (Sgi::vector<spoiler_node*>::iterator i
+	   = spoiler_vertice_.begin();
+	 i != spoiler_vertice_.end(); ++i)
+      {
+	std::cout << "COMPARE" << std::endl;
+	if (sn_n->compare(*i))
+	  {
+	    exist = true;
+	    delete sn_n;
+	    sn_n = dynamic_cast<spoiler_node_delayed*>(*i);
+	    break;
+	  }
+      }
+
+    if (!exist)
+      spoiler_vertice_.push_back(sn_n);
+
+    return sn_n;
   }
 
   void
@@ -708,6 +790,13 @@ namespace spot
 
     bool change = true;
 
+    std::cout << "prune : nb spoiler : "
+	      << spoiler_vertice_.size()
+	      << std::endl
+	      << "prune : nb duplicator : "
+	      << duplicator_vertice_.size()
+	      << std::endl;
+
     while (change)
       {
 	std::cout << "prune::change = true" << std::endl;
@@ -718,6 +807,7 @@ namespace spot
 	  {
 	    if ((*i)->get_nb_succ() == 0)
 	      {
+		std::cout << "Remove duplicator" << std::endl;
 		(*i)->del_pred();
 		delete *i;
 		i = duplicator_vertice_.erase(i);
@@ -732,6 +822,7 @@ namespace spot
 	  {
 	    if ((*i)->get_nb_succ() == 0)
 	      {
+		std::cout << "Remove spoiler" << std::endl;
 		(*i)->del_pred();
 		delete *i;
 		i = spoiler_vertice_.erase(i);
@@ -742,6 +833,13 @@ namespace spot
 	  }
       }
     std::cout << "prune::change = false" << std::endl;
+
+    std::cout << "prune : nb spoiler : "
+	      << spoiler_vertice_.size()
+	      << std::endl
+	      << "prune : nb duplicator : "
+	      << duplicator_vertice_.size()
+	      << std::endl;
   }
 
   void
@@ -836,12 +934,15 @@ namespace spot
   {
     /// FIXME : this method is incorrect !!
     /// Don't use it !!
+    /*
       parity_game_graph_delayed* G = new parity_game_graph_delayed(f);
       simulation_relation* rel = G->get_relation();
       if (opt == 1)
       G->print(std::cout);
       delete G;
-    return rel;
+    */
+
+    return get_direct_relation_simulation(f, opt);
   }
 
 }

src/tgbatest/ltl2tgba.cc

@@ -404,7 +404,7 @@ main(int argc, char** argv)
 	      if (reduc_aut & spot::Reduce_Dir_Sim)
 		rel = spot::get_direct_relation_simulation(a);
 	      else if (reduc_aut & spot::Reduce_Del_Sim)
-		rel = spot::get_delayed_relation_simulation(a, 1);
+		rel = spot::get_delayed_relation_simulation(a);
 	      else
 		assert(0);
 

src/tgbatest/reduccmp.test

@@ -23,9 +23,6 @@
 
 . ./defs
 
-# FIXME
-exit 0
-
 set -e
 
 cat >input <<EOF
@@ -46,6 +43,9 @@ digraph G {
 }
 EOF
 
+# FIXME
+exit 0
+
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
 sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout

src/tgbatest/reductgba.test

@@ -21,7 +21,7 @@
 # 02111-1307, USA.
 
 
-#. ./defs
+. ./defs
 
 set -e
 
@@ -34,22 +34,22 @@ check()
 # We don't check the output, but just running these might be enough to
 # trigger assertions.
 
-#check 0 'Fa & Xb & GFc & Gd'
+check 0 'Fa & Xb & GFc & Gd'
-#check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
 
-#check 0 a
+check 0 a
-#check 0 'a U b'
+check 0 'a U b'
-#check 0 'a U Fb'
+check 0 'a U Fb'
-#check 0 'X a'
+check 0 'X a'
-#check 0 'a & b & c'
+check 0 'a & b & c'
-#check 0 'a | b | (c U (d & (g U (h ^ i))))'
+check 0 'a | b | (c U (d & (g U (h ^ i))))'
-#check 0 'Xa & (b U !a) & (b U !a)'
+check 0 'Xa & (b U !a) & (b U !a)'
-#check 0 'Fa & Xb & GFc & Gd'
+check 0 'Fa & Xb & GFc & Gd'
-#check 0 'Fa & Xa & GFc & Gc'
+check 0 'Fa & Xa & GFc & Gc'
-#check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
-#check 0 'a R (b R c)'
+check 0 'a R (b R c)'
-#check 0 '(a U b) U (c U d)'
+check 0 '(a U b) U (c U d)'
-#check 0 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
+check 0 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
 
 # No reduction
 check 1 a
@@ -66,22 +66,22 @@ check 1 '(a U b) U (c U d)'
 check 1 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
 
 #reduction
-#check 1 'a U Fb'
+check 1 'a U Fb'
 
-#check 3 a
+check 3 a
-#check 3 'a U b'
+check 3 'a U b'
-#check 3 'a U Fb'
+check 3 'a U Fb'
 
-#check 3 a
+check 3 a
-#check 3 'a U b'
+check 3 'a U b'
-#check 3 'a U Fb'
+check 3 'a U Fb'
-#check 3 'X a'
+check 3 'X a'
-#check 3 'a & b & c'
+check 3 'a & b & c'
-#check 3 'a | b | (c U (d & (g U (h ^ i))))'
+check 3 'a | b | (c U (d & (g U (h ^ i))))'
-#check 3 'Xa & (b U !a) & (b U !a)'
+check 3 'Xa & (b U !a) & (b U !a)'
-#check 3 'Fa & Xb & GFc & Gd'
+check 3 'Fa & Xb & GFc & Gd'
-#check 3 'Fa & Xa & GFc & Gc'
+check 3 'Fa & Xa & GFc & Gc'
-#check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
-#check 3 'a R (b R c)'
+check 3 'a R (b R c)'
-#check 3 '(a U b) U (c U d)'
+check 3 '(a U b) U (c U d)'
-#check 3 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
+check 3 '((Xp2)U(X(1)))*(p1 R(p2 R p0))'