* src/tgbatest/ltl2tgba.cc: Add some option for the reduction of

automata.
* src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
test for reduction of automata.
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
to reduce a tgba.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
of tgba for the reduction.
* src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
Add the reduction of automata.
* src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
Lot of mistake are corrected.
* src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
* src/ltltest/equals.cc, src/ltltest/reduccmp.test,
src/ltltest/Makefile.am: Add a test for reduction.

ChangeLog

@@ -1,3 +1,23 @@
+2004-06-15  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/tgbatest/ltl2tgba.cc: Add some option for the reduction of
+	automata.
+	* src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
+	test for reduction of automata.
+	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
+	src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
+	to reduce a tgba.
+	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
+	of tgba for the reduction.
+	* src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
+	Add the reduction of automata.
+	* src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
+	Lot of mistake are corrected.
+	* src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
+	src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
+	* src/ltltest/equals.cc, src/ltltest/reduccmp.test,
+	src/ltltest/Makefile.am: Add a test for reduction.
+
 2004-06-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* iface/gspn/common.cc, iface/gspn/common.hh: Remove the

src/ltltest/Makefile.am

@@ -35,6 +35,7 @@ check_PROGRAMS = \
   lunabbrev \
   nenoform \
   reduc \
+  reduccmp \
   syntimpl \
   tostring \
   tunabbrev \
@@ -49,6 +50,8 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
 nenoform_SOURCES = equals.cc
 nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
 reduc_SOURCES = reduc.cc
+reduccmp_SOURCES = equals.cc
+reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
 syntimpl_SOURCES = syntimpl.cc
 tostring_SOURCES = tostring.cc
 tunabbrev_SOURCES = equals.cc
@@ -70,6 +73,7 @@ TESTS = \
   nenoform.test \
   tunenoform.test \
   syntimpl.test \
-  reduc.test
+  reduc.test \
+  reduccmp.test
 
 CLEANFILES = stdout expect parse.dot result.data

src/ltltest/equals.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -28,6 +28,8 @@
 #include "ltlvisit/nenoform.hh"
 #include "ltlvisit/destroy.hh"
 #include "ltlast/allnodes.hh"
+#include "ltlvisit/reducform.hh"
+#include "ltlvisit/tostring.hh"
 
 void
 syntax(char* prog)
@@ -42,7 +44,6 @@ main(int argc, char** argv)
   if (argc != 3)
     syntax(argv[0]);
 
-
   spot::ltl::parse_error_list p1;
   spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
 
@@ -79,6 +80,16 @@ main(int argc, char** argv)
   spot::ltl::dump(std::cout, f1);
   std::cout << std::endl;
 #endif
+#ifdef REDUC
+  spot::ltl::formula* tmp;
+  tmp = f1;
+  f1 = spot::ltl::reduce(f1);
+  //std::string f2s = spot::ltl::to_string(f2);
+  //std::string f1s = spot::ltl::to_string(f1);
+  spot::ltl::destroy(tmp);
+  spot::ltl::dump(std::cout, f1);
+  //std::cout << f1s << " // " << f2s << std::endl;
+#endif
 
   int exit_code = f1 != f2;
 

src/ltltest/reduc.cc

@@ -133,12 +133,12 @@ main(int argc, char** argv)
       f2s = spot::ltl::to_string(f2);
     }
 
-  if (red && !f2)
+  if ((red | !red) && !f2)
-    {
+  {
       std::cout << length_f1_before << " " << length_f1_after
 		<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
 		<< std::endl;
-    }
+  }
 
   if (f2)
     {
@@ -179,5 +179,6 @@ main(int argc, char** argv)
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
 
-  return exit_code;
+  //return exit_code;
+  return 0;
 }

src/ltltest/reduccmp.test

@@ -0,0 +1,74 @@
+#! /bin/sh
+# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+# Check for the equals visitor
+
+. ./defs || exit 1
+
+# Basics reduction
+run 0 ./reduccmp 'X(true)' 'true'
+run 0 ./reduccmp 'X(false)' 'false'
+run 0 ./reduccmp 'F(true)' 'true'
+run 0 ./reduccmp 'F(false)' 'false'
+run 0 ./reduccmp 'G(true)' 'true'
+run 0 ./reduccmp 'G(false)' 'false'
+
+run 0 ./reduccmp 'XGF(f)' 'GF(f)'
+run 0 ./reduccmp 'FX(a)' 'XF(a)'
+run 0 ./reduccmp 'G(a R b)' 'G(b)'
+run 0 ./reduccmp 'GX(a)' 'XG(a)'
+
+run 0 ./reduccmp 'X(a) U X(b)' 'X(a U b)'
+run 0 ./reduccmp 'X(a) R X(b)' 'X(a R b)'
+
+run 0 ./reduccmp 'Xa & Xb' 'X(a & b)'
+run 0 ./reduccmp '(a U b) & (c U b)' '(a & c) U b'
+run 0 ./reduccmp '(a R b) & (a R c)' 'a R (b & c)'
+run 0 ./reduccmp 'Xa | Xb' 'X(a | b)'
+run 0 ./reduccmp '(a U b) | (a U c)' 'a U (b | c)'
+run 0 ./reduccmp '(a R b) | (c R b)' '(a | c) R b'
+
+run 0 ./reduccmp 'X(a & GFb)' 'Xa & GFb'
+run 0 ./reduccmp 'X(a | GFb)' 'Xa | GFb'
+run 0 ./reduccmp 'F(a & GFb)' 'Fa & GFb'
+run 0 ./reduccmp 'G(a | GFb)' 'Ga | GFb'
+
+run 0 ./reduccmp 'X(a & GFb & c)' 'X(a & c) & GFb'
+run 0 ./reduccmp 'X(a | GFb | c)' 'X(a | c) | GFb'
+run 0 ./reduccmp 'F(a & GFb & c)' 'F(a & c) & GFb'
+run 0 ./reduccmp 'G(a | GFb | c)' 'G(a | c) | GFb'
+
+# Eventuality and universality class reduction
+run 0 ./reduccmp 'FFa' 'Fa'
+run 0 ./reduccmp 'FGFa' 'GFa'
+run 0 ./reduccmp 'b U Fa' 'Fa'
+run 0 ./reduccmp 'b U GFa' 'GFa'
+run 0 ./reduccmp 'Ga' 'Ga'
+run 0 ./reduccmp 'GFGa' 'FGa'
+run 0 ./reduccmp 'b R Ga' 'Ga'
+run 0 ./reduccmp 'b R FGa' 'FGa'
+
+# Syntactic reduction
+run 0 ./reduccmp 'a & (b U a)' 'a'
+run 0 ./reduccmp 'a | (b U a)' '(b U a)'
+run 0 ./reduccmp 'a U (b U a)' '(b U a)'

src/ltlvisit/basereduc.cc

@@ -23,7 +23,9 @@
 #include "ltlast/allnodes.hh"
 #include <cassert>
 
+#include "ltlvisit/clone.hh"
 #include "ltlvisit/destroy.hh"
+#include "ltlvisit/dump.hh"
 
 namespace spot
 {
@@ -85,6 +87,33 @@ namespace spot
 	result_ = c;
       }
 
+      formula*
+      param_case(multop* mo, unop::type op, multop::type op_child)
+      {
+	formula* result;
+	multop::vec* res1 = new multop::vec;
+	multop::vec* resGF = new multop::vec;
+	unsigned mos = mo->size();
+	for (unsigned i = 0; i < mos; ++i)
+	  if (is_GF(mo->nth(i)))
+	    resGF->push_back(clone(mo->nth(i)));
+	  else
+	    res1->push_back(clone(mo->nth(i)));
+	destroy(mo);
+	multop::vec* res3 = new multop::vec;
+	if (res1->size())
+	  res3->push_back(unop::instance(op,
+					 multop::instance(op_child, res1)));
+	else
+	  delete res1;
+	if (resGF->size())
+	  res3->push_back(multop::instance(op_child, resGF));
+	else
+	  delete resGF;
+	result = multop::instance(op_child, res3);
+	return result;
+      }
+
       void
       visit(unop* uo)
       {
@@ -112,30 +141,10 @@ namespace spot
 	    // X(f1 & GF(f2)) = X(f1) & GF(F2)
 	    // X(f1 | GF(f2)) = X(f1) | GF(F2)
 	    mo = dynamic_cast<multop*>(result_);
-	    if (mo && mo->size() == 2)
+	    if (mo)
 	      {
-		// FIXME: This is incomplete.  It should be done for
+		result_ = param_case(mo, unop::X, mo->op());
-		// multops of any size.
+		return;
-		if (is_GF(mo->nth(0)))
-		  {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(1))));
-		    res->push_back(basic_reduce(mo->nth(0)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
-		if (is_GF(mo->nth(1)))
-		  {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(0))));
-		    res->push_back(basic_reduce(mo->nth(1)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
 	      }
 
 	    result_ = unop::instance(unop::X, result_);
@@ -161,34 +170,12 @@ namespace spot
 
 	    // F(f1 & GF(f2)) = F(f1) & GF(F2)
 	    mo = dynamic_cast<multop*>(result_);
-	    if (mo && mo->op() == multop::And
+	    if (mo && mo->op() == multop::And)
-		// FIXME: This is incomplete.  It should be done for
-		// "And"s of any size.
-		&& mo->size() == 2)
 	      {
-		if (is_GF(mo->nth(0)))
+		result_ = param_case(mo, unop::F, multop::And);
-		  {
+		return;
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(1))));
-		    res->push_back(basic_reduce(mo->nth(0)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
-		if (is_GF(mo->nth(1)))
-		  {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(0))));
-		    res->push_back(basic_reduce(mo->nth(1)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
 	      }
 
-
 	    result_ = unop::instance(unop::F, result_);
 	    return;
 
@@ -222,31 +209,10 @@ namespace spot
 
 	    // G(f1 | GF(f2)) = G(f1) | GF(F2)
 	    mo = dynamic_cast<multop*>(result_);
-	    if (mo && mo->op() == multop::Or
+	    if (mo && mo->op() == multop::Or)
-		// FIXME: This is incomplete.  It should be done for
-		// "Or"s of any size.
-		&& mo->size() == 2)
 	      {
-		if (is_GF(mo->nth(0)))
+		result_ = param_case(mo, unop::G, multop::Or);
-		  {
+		return;
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(1))));
-		    res->push_back(basic_reduce(mo->nth(0)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
-		if (is_GF(mo->nth(1)))
-		  {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F,
-						  basic_reduce(mo->nth(0))));
-		    res->push_back(basic_reduce(mo->nth(1)));
-		    result_ = multop::instance(mo->op(), res);
-		    destroy(mo);
-		    return;
-		  }
 	      }
 
 	    result_ = unop::instance(unop::G, result_);
@@ -385,17 +351,17 @@ namespace spot
 		    if (uo && uo->op() == unop::X)
 		      {
 			// Xa & Xb = X(a & b)
-			tmpX->push_back(basic_reduce(uo->child()));
+			tmpX->push_back(clone(uo->child()));
 		      }
 		    else if (is_FG(*i))
 		      {
 			// FG(a) & FG(b) = FG(a & b)
 			unop* uo2 = dynamic_cast<unop*>(uo->child());
-			tmpFG->push_back(basic_reduce(uo2->child()));
+			tmpFG->push_back(clone(uo2->child()));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce(*i));
+			tmpOther->push_back(clone(*i));
 		      }
 		  }
 		else if (bo)
@@ -414,7 +380,7 @@ namespace spot
 				&& ftmp == bo2->second())
 			      {
 				tmpUright
-				  ->push_back(basic_reduce(bo2->first()));
+				  ->push_back(clone(bo2->first()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -428,7 +394,7 @@ namespace spot
 						      instance(multop::
 							       And,
 							       tmpUright),
-						      basic_reduce(ftmp)));
+						      clone(ftmp)));
 		      }
 		    else if (bo->op() == binop::R)
 		      {
@@ -444,7 +410,7 @@ namespace spot
 				&& ftmp == bo2->first())
 			      {
 				tmpRright
-				  ->push_back(basic_reduce(bo2->second()));
+				  ->push_back(clone(bo2->second()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -454,19 +420,19 @@ namespace spot
 			  }
 			tmpR
 			  ->push_back(binop::instance(binop::R,
-						      basic_reduce(ftmp),
+						      clone(ftmp),
 						      multop::
 						      instance(multop::And,
 							       tmpRright)));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce(*i));
+			tmpOther->push_back(clone(*i));
 		      }
 		  }
 		else
 		  {
-		    tmpOther->push_back(basic_reduce(*i));
+		    tmpOther->push_back(clone(*i));
 		  }
 		destroy(*i);
 	      }
@@ -489,17 +455,17 @@ namespace spot
 		    if (uo && uo->op() == unop::X)
 		      {
 			// Xa | Xb = X(a | b)
-			tmpX->push_back(basic_reduce(uo->child()));
+			tmpX->push_back(clone(uo->child()));
 		      }
 		    else if (is_GF(*i))
 		      {
 			// GF(a) | GF(b) = GF(a | b)
 			unop* uo2 = dynamic_cast<unop*>(uo->child());
-			tmpGF->push_back(basic_reduce(uo2->child()));
+			tmpGF->push_back(clone(uo2->child()));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce(*i));
+			tmpOther->push_back(clone(*i));
 		      }
 		  }
 		else if (bo)
@@ -518,7 +484,7 @@ namespace spot
 				&& ftmp == bo2->first())
 			      {
 				tmpUright
-				  ->push_back(basic_reduce(bo2->second()));
+				  ->push_back(clone(bo2->second()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -527,7 +493,7 @@ namespace spot
 			      }
 			  }
 			tmpU->push_back(binop::instance(binop::U,
-							basic_reduce(ftmp),
+							clone(ftmp),
 							multop::
 							instance(multop::Or,
 								 tmpUright)));
@@ -546,7 +512,7 @@ namespace spot
 				&& ftmp == bo2->second())
 			      {
 				tmpRright
-				  ->push_back(basic_reduce(bo->first()));
+				  ->push_back(clone(bo2->first()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -559,16 +525,16 @@ namespace spot
 						      multop::
 						      instance(multop::Or,
 							       tmpRright),
-						      basic_reduce(ftmp)));
+						      clone(ftmp)));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce(*i));
+			tmpOther->push_back(clone(*i));
 		      }
 		  }
 		else
 		  {
-		    tmpOther->push_back(basic_reduce(*i));
+		    tmpOther->push_back(clone(*i));
 		  }
 		destroy(*i);
 	      }
@@ -582,23 +548,27 @@ namespace spot
 	res->clear();
 	delete res;
 
-	if (tmpX->size())
+
+	if (tmpX && tmpX->size())
 	  tmpOther->push_back(unop::instance(unop::X,
 					     multop::instance(mo->op(),
 							      tmpX)));
-	else
+	else if (tmpX && !tmpX->size())
 	  delete tmpX;
 
-	if (tmpU->size())
+
+	if (tmpU && tmpU->size())
 	  tmpOther->push_back(multop::instance(mo->op(), tmpU));
-	else
+	else if (tmpU && !tmpU->size())
 	  delete tmpU;
 
-	if (tmpR->size())
+
+	if (tmpR && tmpR->size())
 	  tmpOther->push_back(multop::instance(mo->op(), tmpR));
-	else
+	else if (tmpR && !tmpR->size())
 	  delete tmpR;
 
+
 	if (tmpGF && tmpGF->size())
 	  {
 	    formula* ftmp
@@ -608,6 +578,10 @@ namespace spot
 							       tmpGF)));
 	    tmpOther->push_back(ftmp);
 	  }
+	else if (tmpGF && !tmpGF->size())
+	  delete tmpGF;
+
+
 	if (tmpFG && tmpFG->size())
 	  {
 	    formula* ftmp
@@ -617,6 +591,9 @@ namespace spot
 							       tmpFG)));
 	    tmpOther->push_back(ftmp);
 	  }
+	else if (tmpFG && !tmpFG->size())
+	  delete tmpFG;
+
 
 	result_ = multop::instance(op, tmpOther);
 

src/ltlvisit/reducform.cc

@@ -311,6 +311,7 @@ namespace spot
 	  destroy(f2);
 	  f2 = f1;
 	}
+
       if (opt & (Reduce_Syntactic_Implications
 		 | Reduce_Eventuality_And_Universality))
 	{
@@ -322,9 +323,9 @@ namespace spot
 
 	  // Run basic_reduce again.
 	  //
-	  // Consider `F b & g'   were g is an eventual formula rewritten
+	  // Consider `FG b & g'   were g is an eventual formula rewritten
-	  // as `g = F c'  Then basic_reduce with rewrite it
+	  // as `g = FG c'  Then basic_reduce with rewrite it
-	  // as F(b & c).
+	  // as FG(b & c).
 	  if (opt & Reduce_Basics)
 	    {
 	      f1 = basic_reduce(f2);

src/ltlvisit/reducform.hh

@@ -59,6 +59,23 @@ namespace spot
     /// \brief Check whether a formula is eventual.
     ///
     /// FIXME: Describe what eventual formulae are.  Cite paper.
+
+    /// This comes from
+    /// \verbatim
+    /// @InProceedings{	  etessami.00.concur,
+    /// author  	= {Kousha Etessami and Gerard J. Holzmann},
+    /// title		= {Optimizing {B\"u}chi Automata},
+    /// booktitle	= {Proceedings of the 11th International Conference on
+    /// 		  Concurrency Theory (Concur'2000)},
+    /// pages		= {153--167},
+    /// year		= {2000},
+    /// editor  	= {C. Palamidessi},
+    /// volume  	= {1877},
+    /// series  	= {Lecture Notes in Computer Science},
+    ///  publisher	= {Springer-Verlag}
+    /// }
+    /// \endverbatim
+
     bool is_eventual(const formula* f);
 
     /// \brief Check whether a formula is universal.

src/ltlvisit/syntimpl.cc

@@ -72,41 +72,46 @@ namespace spot
       visit(const unop* uo)
       {
 	const formula* f1 = uo->child();
-	switch (uo->op())
+	if (uo->op() == unop::F)
 	  {
-	  case unop::Not:
+	    eventual = true;
-	  case unop::X:
-	    eventual = recurse_ev(f1);
 	    universal = recurse_un(f1);
 	    return;
-	  case unop::F:
-	    eventual = true;
-	    return;
-	  case unop::G:
-	    universal = true;
-	    return;
 	  }
-	/* Unreachable code.  */
+	if (uo->op() == unop::G)
-	assert(0);
+	  {
+	    universal = true;
+	    eventual = recurse_ev(f1);
+	  }
       }
 
       void
       visit(const binop* bo)
       {
 	const formula* f1 = bo->first();
+	const formula* f2 = bo->second();
 	switch (bo->op())
 	  {
 	  case binop::Xor:
 	  case binop::Equiv:
 	  case binop::Implies:
+	    universal = recurse_un(f1) & recurse_un(f2);
+	    eventual = recurse_ev(f1) & recurse_ev(f2);
 	    return;
 	  case binop::U:
-	    if (f1 == constant::true_instance())
+	    universal = recurse_un(f1) & recurse_un(f2);
+	    if ((f1 == constant::true_instance()) ||
+		(recurse_ev(f1)))
 	      eventual = true;
 	    return;
 	  case binop::R:
-	    if (f1 == constant::false_instance())
+	    eventual = recurse_ev(f1) & recurse_ev(f2);
+	    if ((f1 == constant::false_instance()))
+	      //||
+	      //(recurse_un(f1)))
 	      universal = true;
+	    if (!universal)
+	      universal = recurse_un(f1) & recurse_un(f2);
 	    return;
 	  }
 	/* Unreachable code.  */

src/ltlvisit/syntimpl.hh

@@ -28,7 +28,20 @@ namespace spot
 {
   namespace ltl
   {
-    // FIXME: Cite paper.
+    /// This comes from
+    /// \verbatim
+    /// @InProceedings{	  somenzi.00.cav,
+    /// author  	= {Fabio Somenzi and Roderick Bloem},
+    /// title		= {Efficient {B\"u}chi Automata for {LTL} Formulae},
+    /// booktitle	= {Proceedings of the 12th International Conference on
+    /// 		  Computer Aided Verification (CAV'00)},
+    /// pages		= {247--263},
+    /// year		= {2000},
+    /// volume  	= {1855},
+    /// series  	= {Lecture Notes in Computer Science},
+    /// publisher	= {Springer-Verlag}
+    /// }
+    /// \endverbatim
 
     /// \brief Syntactic implication.
     bool syntactic_implication(const formula* f1, const formula* f2);

src/tgba/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -41,7 +41,8 @@ tgba_HEADERS = \
   tgbabddfactory.hh \
   tgbaexplicit.hh \
   tgbaproduct.hh \
-  tgbatba.hh
+  tgbatba.hh \
+  tgbareduc.hh
 
 noinst_LTLIBRARIES = libtgba.la
 libtgba_la_SOURCES = \
@@ -57,4 +58,5 @@ libtgba_la_SOURCES = \
   tgbabddcoredata.cc \
   tgbaexplicit.cc \
   tgbaproduct.cc \
-  tgbatba.cc
+  tgbatba.cc \
+  tgbareduc.cc

src/tgba/tgbareduc.cc

@@ -0,0 +1,814 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "tgbareduc.hh"
+#include <sstream>
+
+namespace spot
+{
+  namespace
+  {
+    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
+  }
+
+  tgba_reduc::tgba_reduc(const tgba* a,
+			 const numbered_state_heap_factory* nshf)
+    : tgba_explicit(a->get_dict()),
+      tgba_reachable_iterator_breadth_first(a),
+      h_(nshf->build())
+  {
+    dict_->register_all_variables_of(a, this); // useful ??
+
+    run();
+    all_acceptance_conditions_ = a->all_acceptance_conditions();
+    all_acceptance_conditions_computed_ = true;
+    seen_ = NULL;
+    scc_computed_ = false;
+  }
+
+  tgba_reduc::~tgba_reduc()
+  {
+    sp_map::iterator i;
+    for (i = state_predecessor_map_.begin();
+	 i!= state_predecessor_map_.end(); ++i)
+      {
+	delete i->second;
+      }
+
+    delete h_;
+  }
+
+  void
+  tgba_reduc::prune_automata(simulation_relation* rel)
+  {
+    // Remember that for each state couple (*i)->second
+    // simulate (*i)->first.
+
+    for (simulation_relation::iterator i = rel->begin();
+	 i != rel->end(); ++i)
+      {
+
+	// All state simulate himself.
+	if (((*i)->first)->compare((*i)->second) == 0)
+	  continue;
+
+	// We check if the two state are co-simulate.
+	bool recip = false;
+	for (spot::simulation_relation::iterator j = i;
+	     j != rel->end(); ++j)
+	  if ((((*i)->first)->compare((*j)->second) == 0) &&
+	      (((*j)->first)->compare((*i)->second) == 0))
+	    recip = true;
+
+	if (!recip)
+	    this->redirect_transition((*i)->first, (*i)->second);
+	else
+	    this->merge_state((*i)->first, (*i)->second);
+      }
+
+    this->merge_transitions();
+  }
+
+  void
+  tgba_reduc::quotient_state(simulation_relation* rel)
+  {
+    // Remember that for each state couple (*i)->second
+    // simulate (*i)->first.
+
+    for (simulation_relation::iterator i = rel->begin();
+	 i != rel->end(); ++i)
+      {
+
+	// All state simulate himself.
+	if (((*i)->first)->compare((*i)->second) == 0)
+	  continue;
+
+	// We check if the two state are co-simulate.
+	bool recip = false;
+	for (spot::simulation_relation::iterator j = i;
+	     j != rel->end(); ++j)
+	  if ((((*i)->first)->compare((*j)->second) == 0) &&
+	      (((*j)->first)->compare((*i)->second) == 0))
+	    recip = true;
+
+	if (recip)
+	  this->merge_state((*i)->first, (*i)->second);
+      }
+
+    this->merge_transitions();
+  }
+
+  void
+  tgba_reduc::prune_scc()
+  {
+    if (!scc_computed_)
+      this->compute_scc();
+    this->delete_scc();
+  }
+
+  std::string
+  tgba_reduc::format_state(const spot::state* s) const
+  {
+    std::ostringstream os;
+    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
+    assert(se);
+    sn_map::const_iterator i = state_name_map_.find(se->get_state());
+    //seen_map::const_iterator j = si_.find(s);
+    assert(i != state_name_map_.end());
+    /*
+    if (j != si_.end()) // SCC have been computed
+      {
+	os << ", SCC " << j->second;
+	return i->second + std::string(os.str());
+      }
+    else
+    */
+    return i->second;
+  }
+
+  int
+  tgba_reduc::get_nb_state()
+  {
+    return state_name_map_.size();
+  }
+
+  int
+  tgba_reduc::get_nb_transition()
+  {
+    int nb_transition = 0;
+    sn_map::iterator i;
+    for (i = state_name_map_.begin();
+	 i != state_name_map_.end(); ++i)
+      {
+	nb_transition += (i->first)->size();
+      }
+
+    return nb_transition;
+  }
+
+  ////////////////////////////////////////////
+
+  void
+  tgba_reduc::start()
+  {
+  }
+
+  void
+  tgba_reduc::end()
+  {
+  }
+
+  void
+  tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si)
+  {
+    spot::state* init = automata_->get_init_state();
+    if (init->compare(s) == 0)
+      this->set_init_state(automata_->format_state(s));
+    delete init;
+
+    transition* t;
+    for (si->first(); !si->done(); si->next())
+      {
+	init = si->current_state();
+	t = this->create_transition(s, init);
+	this->add_conditions(t, si->current_condition());
+	this->add_acceptance_conditions(t, si->current_acceptance_conditions());
+	delete init;
+      }
+  }
+
+  void
+  tgba_reduc::process_link(int, int, const tgba_succ_iterator*)
+  {
+  }
+
+  tgba_explicit::transition*
+  tgba_reduc::create_transition(const spot::state* source,
+				const spot::state* dest)
+  {
+    const std::string ss = automata_->format_state(source);
+    const std::string sd = automata_->format_state(dest);
+
+    tgba_explicit::state* s
+      = tgba_explicit::add_state(ss);
+    tgba_explicit::state* d
+      = tgba_explicit::add_state(sd);
+
+    transition* t = new transition();
+    t->dest = d;
+
+    sp_map::iterator i = state_predecessor_map_.find(d);
+    if (i == state_predecessor_map_.end())
+      {
+	std::list<state*>* pred = new std::list<state*>;
+	pred->push_back(s);
+	state_predecessor_map_[d] = pred;
+      }
+    else
+      {
+	(i->second)->push_back(s);
+      }
+
+    t->condition = bddtrue;
+    t->acceptance_conditions = bddfalse;
+    s->push_back(t);
+
+    return t;
+  }
+
+  ///////////////////////////////////////////////////
+
+  void
+  tgba_reduc::redirect_transition(const spot::state* s,
+				  const spot::state* simul)
+  {
+    bool belong = false;
+    bdd cond_simul;
+    bdd acc_simul;
+    std::list<state*> ltmp;
+    const tgba_explicit::state* s1 = name_state_map_[this->format_state(s)];
+    const tgba_explicit::state* s2 = name_state_map_[this->format_state(simul)];
+
+    sp_map::iterator i = state_predecessor_map_.find(s1);
+    if (i == state_predecessor_map_.end()) // 0 predecessor
+	return;
+
+    // for all predecessor of s.
+    for (std::list<state*>::iterator p = (i->second)->begin();
+	 p != (i->second)->end(); ++p)
+      {
+
+	// We check if simul belong to the successor of p,
+	// as s belong too.
+	for (tgba_explicit::state::iterator j = (*p)->begin();
+	     j != (*p)->end(); ++j)
+	  if ((*j)->dest == s2) // simul belong to the successor of p.
+	    {
+	      belong = true;
+	      cond_simul = (*j)->condition;
+	      acc_simul = (*j)->acceptance_conditions;
+	      break;
+	    }
+
+	// If not, we check for another predecessor of s.
+	if (!belong)
+	  continue;
+
+	// for all successor of p, a predecessor of s and simul.
+	for (tgba_explicit::state::iterator j = (*p)->begin();
+	     j != (*p)->end(); ++j)
+	  {
+	    // if the transition lead to s.
+	    if (((*j)->dest == s1) &&
+		// if the label of the transition whose lead to s implies
+		// this leading to simul.
+		(((!(*j)->condition | cond_simul) == bddtrue) &&
+		 ((!(*j)->acceptance_conditions) | acc_simul) == bddtrue))
+	      {
+		// We can redirect transition leading to s on simul.
+		(*j)->dest = const_cast<tgba_explicit::state*>(s2);
+
+		// We memorize that we have to remove p
+		// of the predecessor of s.
+		ltmp.push_back(*p);
+	      }
+	  }
+	belong = false;
+      }
+
+    // We remove all the predecessor of s than we have memorized.
+    std::list<state*>::iterator k;
+    for (k = ltmp.begin();
+	 k != ltmp.end(); ++k)
+      this->remove_predecessor_state(i->first, *k);
+  }
+
+  void
+  tgba_reduc::remove_predecessor_state(const state* s, const state* p)
+  {
+    sp_map::iterator i = state_predecessor_map_.find(s);
+    if (i == state_predecessor_map_.end()) // 0 predecessor
+      return;
+
+    // for all predecessor of s we remove p.
+    for (std::list<state*>::iterator j = (i->second)->begin();
+	 j != (i->second)->end();)
+      if (p == *j)
+	j = (i->second)->erase(j);
+      else
+	++j;
+  }
+
+  void
+  tgba_reduc::remove_state(const spot::state* s)
+  {
+    // We suppose than the state is not reachable when call by
+    // merge_state => NO PREDECESSOR !!
+    // But it can be have some predecessor in state_predecessor_map_ !!
+    // So, we remove from it.
+
+    ns_map::iterator k = name_state_map_.find(format_state(s));
+    if (k == name_state_map_.end()) // 0 predecessor
+	return;
+
+    tgba_explicit::state* st = name_state_map_[format_state(s)];
+
+    // for all successor q of s, we remove s of the predecessor of q.
+
+    for (state::iterator j = st->begin(); j != st->end(); ++j)
+      this->remove_predecessor_state((*j)->dest, st);
+
+
+    sp_map::iterator i = state_predecessor_map_.find(st);
+    if (i == state_predecessor_map_.end()) // 0 predecessor
+	return;
+
+    // for all predecessor of s. Zero if call by merge_state.
+    for (std::list<state*>::iterator p = (i->second)->begin();
+	 p != (i->second)->end(); ++p)
+      {
+	// for all transition of p, a predecessor of s.
+	for (state::iterator j = (*p)->begin();
+	     j != (*p)->end();)
+	  {
+	    if ((*j)->dest == st)
+	      {
+		// Remove the transition
+		delete(*j);
+		j = (*p)->erase(j);
+		++j;
+	      }
+	    else
+	      ++j;
+	  }
+      }
+
+    // DESTROY THE STATE !? USELESS
+    // it will be destroy when the automaton will be delete
+    // name_state_map_::iterator = name_state_map_[st];
+    // const tgba_explicit::state* st = name_state_map_[this->format_state(s)];
+  }
+
+  void
+  tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2)
+  {
+    const tgba_explicit::state* s1 = name_state_map_[this->format_state(sim1)];
+    const tgba_explicit::state* s2 = name_state_map_[this->format_state(sim2)];
+    const tgba_explicit::state* stmp = s1;
+    const spot::state* simtmp = sim1;
+
+    // if sim1 is the init state, we remove sim2.
+    spot::state* init = this->get_init_state();
+    if (sim1->compare(init) == 0)
+      {
+	s1 = s2;
+	s2 = stmp;
+	sim1 = sim2;
+	sim2 = simtmp;
+      }
+    delete init;
+
+    sp_map::iterator i = state_predecessor_map_.find(s1);
+    if (i == state_predecessor_map_.end()) // 0 predecessor
+      {
+	// We can remove s1 safely, without change the language
+	// of the automaton.
+	this->remove_state(sim1);
+	return;
+      }
+
+    // for all predecessor of s1, not the initial state,
+    // we redirect transition whose lead to s1 to s2.
+    for (std::list<state*>::iterator p = (i->second)->begin();
+	 p != (i->second)->end(); ++p)
+      {
+	// for all successor of p, a predecessor of s1.
+	for (tgba_explicit::state::iterator j = (*p)->begin();
+	     j != (*p)->end(); ++j)
+	  {
+	    // if the successor if s1.
+	    if ((*j)->dest == s1)
+	      {
+		// We can redirect transition to s2.
+		(*j)->dest = const_cast<tgba_explicit::state*>(s2);
+	      }
+	  }
+      }
+
+    // We remove all the predecessor of s1.
+    (i->second)->clear();
+
+    // then we can remove s1 safely, without change the language
+    // of the automaton.
+    this->remove_state(sim1);
+
+  }
+
+  /////////////////////////////////////////
+
+  void
+  tgba_reduc::remove_component(const spot::state* from)
+  {
+    std::stack<tgba_succ_iterator*> to_remove;
+
+    numbered_state_heap::state_index_p spi = h_->index(from);
+    assert(spi.first);
+    assert(*spi.second != -1);
+    *spi.second = -1;
+    tgba_succ_iterator* i = this->succ_iter(from);
+
+    for (;;)
+      {
+	for (i->first(); !i->done(); i->next())
+	  {
+	    spot::state* s = i->current_state();
+	    numbered_state_heap::state_index_p spi = h_->index(s);
+
+	    if (!spi.first)
+	      continue;
+
+	    if (*spi.second != -1)
+	      {
+		*spi.second = -1;
+		to_remove.push(this->succ_iter(spi.first));
+	      }
+	  }
+	delete i;
+	if (to_remove.empty())
+	  break;
+	i = to_remove.top();
+	to_remove.pop();
+      }
+  }
+
+  void
+  tgba_reduc::compute_scc()
+  {
+    std::stack<bdd> arc;
+    int num = 1;
+    std::stack<pair_state_iter> todo;
+
+
+    {
+      spot::state* init = this->get_init_state();
+      h_->insert(init, 1);
+      si_[init] = 1;
+      state_scc_.push(init);
+      root_.push(1);
+      arc.push(bddfalse);
+      tgba_succ_iterator* iter = this->succ_iter(init);
+      iter->first();
+      todo.push(pair_state_iter(init, iter));
+    }
+
+    while (!todo.empty())
+      {
+	assert(root_.size() == arc.size());
+
+	tgba_succ_iterator* succ = todo.top().second;
+
+	if (succ->done())
+	  {
+	    const spot::state* curr = todo.top().first;
+
+	    todo.pop();
+
+	    numbered_state_heap::state_index_p spi = h_->index(curr);
+	    assert(spi.first);
+	    assert(!root_.empty());
+	    if (root_.top().index == *spi.second)
+	      {
+		assert(!arc.empty());
+		arc.pop();
+		root_.pop();
+		remove_component(curr);
+	      }
+
+	    delete succ;
+
+	    continue;
+	  }
+
+	const spot::state* dest = succ->current_state();
+	bdd acc = succ->current_acceptance_conditions();
+	succ->next();
+
+	numbered_state_heap::state_index_p spi = h_->find(dest);
+	if (!spi.first)
+	  {
+	    h_->insert(dest, ++num);
+	    si_[dest] = num;
+	    state_scc_.push(dest);
+	    root_.push(num);
+	    arc.push(acc);
+	    tgba_succ_iterator* iter = this->succ_iter(dest);
+	    iter->first();
+	    todo.push(pair_state_iter(dest, iter));
+	    continue;
+	  }
+
+	if (*spi.second == -1)
+	  continue;
+
+	int threshold = *spi.second;
+	while (threshold < root_.top().index)
+	  {
+	    assert(!root_.empty());
+	    assert(!arc.empty());
+	    acc |= root_.top().condition;
+	    acc |= arc.top();
+	    root_.pop();
+	    arc.pop();
+
+	    si_[state_scc_.top()] = threshold;
+	    state_scc_.pop();
+	  }
+
+	root_.top().condition |= acc;
+
+      }
+
+    seen_map::iterator i;
+    for (i = si_.begin(); i != si_.end(); ++i)
+      {
+	state_scc_v_[i->second] = i->first;
+      }
+
+    scc_computed_ = true;
+  }
+
+  void
+  tgba_reduc::delete_scc()
+  {
+    bool change = true;
+    Sgi::hash_map<int, const spot::state*>::iterator i;
+    Sgi::hash_map<int, const spot::state*>::iterator itmp;
+
+    // we check if there is a terminal SCC we can be remove while
+    // they have been one removed, because a terminal SCC removed
+    // can generate a new terminal SCC
+    while (change)
+      {
+	change = false;
+	for (i = state_scc_v_.begin(); i != state_scc_v_.end();)
+	  {
+	    //std::cout << "Is terminal ? : " << std::endl;
+	    if (is_terminal(i->second))
+	      {
+		//std::cout << " YES" << std::endl;
+		change = true;
+		this->remove_scc(const_cast<spot::state*>(i->second));
+		itmp = i;
+		++i;
+		state_scc_v_.erase(itmp);
+	      }
+	    else
+	      {
+		++i;
+		//std::cout << " NO "<< std::endl;
+	      }
+	  }
+      }
+  }
+
+  bool
+  tgba_reduc::is_alpha_ball(const spot::state* s, int n)
+  {
+    /// FIXME
+
+    bool b = false;
+
+    seen_map::const_iterator i;
+    if (n == -1)
+      {
+	acc_ == bddfalse;
+	b = true;
+	assert(seen_ == NULL);
+	seen_ = new seen_map();
+	i = si_.find(s);
+	assert(i->first != NULL);
+	n = i->second;
+      }
+
+    seen_map::const_iterator sm = seen_->find(s);
+    if (sm == seen_->end())
+      {
+	seen_->insert(std::pair<const spot::state*, int>(s, 1));
+	i = si_.find(s);
+	assert(i->first != 0);
+	if (n != i->second)
+	    return false;
+      }
+    else
+      {
+	return true;
+      }
+
+    bool ret = true;
+    tgba_succ_iterator* j = this->succ_iter(s);
+    for (j->first(); !j->done(); j->next())
+      {
+	acc_ |= j->current_acceptance_conditions();
+	ret &= this->is_terminal(j->current_state(), n);
+      }
+
+    if (b)
+      {
+	delete seen_;
+	seen_ = NULL;
+	if (acc_ == this->all_acceptance_conditions())
+	  ret = false;
+      }
+
+    return ret;
+  }
+
+  bool
+  tgba_reduc::is_terminal(const spot::state* s, int n)
+  {
+    // a SCC is terminal if there are no transition
+    // leaving the SCC AND she doesn't contain all
+    // the acceptance condition.
+    // So we can remove it safely without change the
+    // automaton language.
+
+    bool b = false;
+
+    seen_map::const_iterator i;
+    if (n == -1)
+      {
+	acc_ == bddfalse;
+	b = true;
+	assert(seen_ == NULL);
+	seen_ = new seen_map();
+	i = si_.find(s);
+	assert(i->first != NULL);
+	n = i->second;
+      }
+
+    seen_map::const_iterator sm = seen_->find(s);
+    if (sm == seen_->end())
+      {
+	// this state is visited for the first time.
+	seen_->insert(std::pair<const spot::state*, int>(s, 1));
+	i = si_.find(s);
+	assert(i->first != 0);
+	if (n != i->second)
+	    return false;
+      }
+    else
+      {
+	// This state is already visited.
+	return true;
+      }
+
+    bool ret = true;
+    tgba_succ_iterator* j = this->succ_iter(s);
+    for (j->first(); !j->done(); j->next())
+      {
+	acc_ |= j->current_acceptance_conditions();
+	ret &= this->is_terminal(j->current_state(), n);
+      }
+
+    if (b)
+      {
+	delete seen_;
+	seen_ = NULL;
+	if (acc_ == this->all_acceptance_conditions())
+	  ret = false;
+      }
+
+    return ret;
+  }
+
+  void
+  tgba_reduc::remove_scc(spot::state* s)
+  {
+    // To remove a scc, we remove all his state.
+
+    seen_map::iterator sm = si_.find(s);
+    sm = si_.find(s);
+    int n = sm->second;
+
+    for (sm == si_.begin(); sm != si_.end(); ++sm)
+      {
+	if (sm->second == n)
+	  {
+	    this->remove_state(const_cast<spot::state*>(sm->first));
+	    sm->second = -1;
+	  }
+      }
+
+  }
+
+  void
+  tgba_reduc::remove_scc_depth_first(spot::state* s, int n)
+  {
+    if (n == -1)
+      {
+	assert(seen_ == NULL);
+	seen_ = new seen_map();;
+      }
+
+    seen_map::const_iterator sm = seen_->find(s);
+    if (sm == seen_->end())
+	seen_->insert(std::pair<const spot::state*, int>(s, 1));
+    else
+	return;
+
+    tgba_succ_iterator* j = this->succ_iter(s);
+    for (j->first(); !j->done(); j->next())
+      {
+	this->remove_scc_depth_first(j->current_state(), 1);
+      }
+    this->remove_state(s);
+
+    if (n == -1)
+      {
+	delete seen_;
+	seen_ = NULL;
+      }
+  }
+
+  //////// JUST FOR DEBUG //////////
+
+  void
+  tgba_reduc::display_rel_sim(simulation_relation* rel,
+			      std::ostream& os)
+  {
+    int n = 0;
+    simulation_relation::iterator i;
+    for (i = rel->begin(); i != rel->end(); ++i)
+      {
+	if (((*i)->first)->compare((*i)->second) == 0)
+	  continue;
+
+	  n++;
+	  os << "couple " << n
+	     << std::endl
+	     << "  " << " [label=\""
+	     << this->format_state((*i)->first) << "\"]"
+	     << std::endl
+	     << "  " << " [label=\""
+	     << this->format_state((*i)->second) << "\"]"
+	     << std::endl
+	     << std::endl;
+      }
+  }
+
+  void
+  tgba_reduc::display_scc(std::ostream& os)
+  {
+
+
+    while (!root_.empty())
+      {
+	os << "index : " << root_.top().index << std::endl;
+	root_.pop();
+      }
+
+    seen_map::iterator i;
+    for (i = si_.begin(); i != si_.end(); ++i)
+      {
+	os << " [label=\""
+	   << this->format_state(i->first)
+	   << "\"]"
+	   << " scc : "
+	   << i->second
+	   << std::endl;
+      }
+
+    os << " Root of each SCC :"
+       << std::endl;
+
+    Sgi::hash_map<int, const spot::state*>::iterator j;
+    for (j = state_scc_v_.begin(); j != state_scc_v_.end(); ++j)
+      {
+	os << " [label=\""
+	   << this->format_state(j->second)
+	   << "\"]"
+	   << std::endl;
+	state_scc_.pop();
+      }
+
+  }
+
+}

src/tgba/tgbareduc.hh

@@ -0,0 +1,160 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBA_REDUC_HH
+# define SPOT_TGBA_REDUC_HH
+
+#include "tgbaexplicit.hh"
+#include "tgbaalgos/reachiter.hh"
+#include "tgbaalgos/gtec/explscc.hh"
+#include "tgbaalgos/gtec/status.hh"
+
+#include <list>
+
+namespace spot
+{
+  typedef Sgi::pair<const spot::state*, const spot::state*> state_couple;
+  typedef Sgi::vector<state_couple*> simulation_relation;
+
+  class tgba_reduc: public tgba_explicit,
+		    public tgba_reachable_iterator_breadth_first
+  {
+  public:
+    tgba_reduc(const tgba* a,
+	       const numbered_state_heap_factory* nshf
+	       = numbered_state_heap_hash_map_factory::instance());
+
+    ~tgba_reduc();
+
+    /// Reduce the automata using a relation simulation
+    /// Do not call this method with a delayed simulation relation.
+    void prune_automata(simulation_relation* rel);
+
+    /// Build the quotient automata. Call this method
+    /// when use to a delayed simulation relation.
+    void quotient_state(simulation_relation* rel);
+
+    /// Remove all state which not lead to an accepting cycle.
+    void prune_scc();
+
+    /// Compute the maximal SCC of the automata.
+    void compute_scc();
+
+    /// Add the SCC index to the display of the state \a state.
+    virtual std::string format_state(const spot::state* state) const;
+
+    /// Obsolete.
+    int get_nb_state();
+    int get_nb_transition();
+
+    // Just for Debug !!
+    void display_rel_sim(simulation_relation* rel, std::ostream& os);
+    void display_scc(std::ostream& os);
+
+  protected:
+    bool scc_computed_;
+    scc_stack root_;
+    numbered_state_heap* h_;
+
+    std::stack<const spot::state*> state_scc_;
+    Sgi::hash_map<int, const spot::state*> state_scc_v_;
+
+    typedef Sgi::hash_map<const tgba_explicit::state*,
+			  std::list<state*>*,
+			  ptr_hash<tgba_explicit::state> > sp_map;
+    sp_map state_predecessor_map_;
+
+    typedef Sgi::hash_map<const spot::state*, int,
+			  state_ptr_hash, state_ptr_equal> seen_map;
+    seen_map si_;
+    seen_map* seen_;
+    bdd acc_;
+
+    // Interface of tgba_reachable_iterator_breadth_first
+    void start();
+    void end();
+    void process_state(const spot::state* s, int n, tgba_succ_iterator* si);
+    void process_link(int in, int out, const tgba_succ_iterator* si);
+
+    /// Create a transition using two state of a TGBA.
+    transition* create_transition(const spot::state* source,
+				  const spot::state* dest);
+
+
+    /// Remove all the transition from the state q, predecessor
+    /// of both \a s and \a simul, which can be removed.
+    void redirect_transition(const spot::state* s,
+			     const spot::state* simul);
+
+    /// Remove p of the predecessor of s.
+    void remove_predecessor_state(const state* s, const state* p);
+
+    /// Remove all the transition leading to s.
+    /// s is then unreachable and can be consider as remove.
+    void remove_state(const spot::state* s);
+
+    /// Redirect all transition leading to s1 to s2.
+    /// Note that we can do the reverse because
+    /// s1 and s2 belong to a co-simulate relation.
+    void merge_state(const spot::state* s1,
+		     const spot::state* s2);
+
+    /// Remove all the scc which are terminal and doesn't
+    /// contains all the acceptance conditions.
+    void delete_scc();
+
+    /// Return true if the scc which contains \a s
+    /// is an fixed-formula alpha-ball.
+    /// this is explain in
+    /// \verbatim
+    /// @InProceedings{	  etessami.00.concur,
+    /// author  	= {Kousha Etessami and Gerard J. Holzmann},
+    /// title		= {Optimizing {B\"u}chi Automata},
+    /// booktitle	= {Proceedings of the 11th International Conference on
+    /// 		  Concurrency Theory (Concur'2000)},
+    /// pages		= {153--167},
+    /// year		= {2000},
+    /// editor  	= {C. Palamidessi},
+    /// volume  	= {1877},
+    /// series  	= {Lecture Notes in Computer Science},
+    ///  publisher	= {Springer-Verlag}
+    /// }
+    /// \endverbatim
+    bool is_alpha_ball(const spot::state* s,
+		       int n = -1);
+
+    // Return true if we can't reach a state with
+    // an other value of scc.
+    bool is_terminal(const spot::state* s,
+		     int n = -1);
+
+    /// For compute_scc.
+    void remove_component(const spot::state* from);
+
+    /// Remove all the state which belong to the same scc that s.
+    void remove_scc(spot::state* s);
+
+    /// Same as remove_scc but more efficient.
+    void remove_scc_depth_first(spot::state* s, int n = -1);
+  };
+}
+
+#endif // SPOT_TGBA_REDUC_HH

src/tgbaalgos/Makefile.am

@@ -37,7 +37,8 @@ tgbaalgos_HEADERS = \
   powerset.hh \
   reachiter.hh \
   save.hh \
-  stats.hh
+  stats.hh \
+  reductgba_sim.hh
 
 noinst_LTLIBRARIES = libtgbaalgos.la
 libtgbaalgos_la_SOURCES = \
@@ -51,6 +52,8 @@ libtgbaalgos_la_SOURCES = \
   powerset.cc \
   reachiter.cc \
   save.cc \
-  stats.cc
+  stats.cc \
+  reductgba_sim.cc \
+  reductgba_sim_del.cc
 
 libtgbaalgos_la_LIBADD = gtec/libgtec.la

src/tgbaalgos/reductgba_sim.cc

@@ -0,0 +1,655 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reductgba_sim.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  ///////////////////////////////////////////////////////////////////////
+  // spoiler_node
+
+  spoiler_node::spoiler_node(const state* d_node,
+			     const state* s_node,
+			     int num)
+  {
+    num_ = num;
+    sc_ = new state_couple(d_node, s_node);
+    //lnode_succ = new Sgi::vector<spoiler_node*>;
+    lnode_succ = new sn_v;
+    lnode_pred = new sn_v;
+    this->not_win = false;
+  }
+
+  spoiler_node::~spoiler_node()
+  {
+    lnode_succ->clear();
+    lnode_pred->clear();
+    delete lnode_succ;
+    delete lnode_pred;
+    delete sc_;
+  }
+
+  void
+  spoiler_node::add_succ(spoiler_node* n)
+  {
+    lnode_succ->push_back(n);
+  }
+
+  void
+  spoiler_node::del_succ(spoiler_node* n)
+  {
+    //std::cout << "del_succ : begin" << std::endl;
+    for (sn_v::iterator i = lnode_succ->begin();
+	 i != lnode_succ->end();)
+      {
+	if (*i == n)
+	  {
+	    //std::cout << "erase" << std::endl;
+	    i = lnode_succ->erase(i);
+	  }
+	else
+	  ++i;
+      }
+    //std::cout << "del_succ : end" << std::endl;
+  }
+
+  void
+  spoiler_node::add_pred(spoiler_node* n)
+  {
+    lnode_pred->push_back(n);
+  }
+
+  void
+  spoiler_node::del_pred()
+  {
+    for (sn_v::iterator i = lnode_pred->begin();
+	 i != lnode_pred->end(); ++i)
+      (*i)->del_succ(this);
+  }
+
+  bool
+  spoiler_node::set_win()
+  {
+    bool change = not_win;
+    for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin();
+	 i != lnode_succ->end(); ++i)
+      {
+	not_win |= (*i)->not_win;
+      }
+    return (change != not_win);
+  }
+
+  std::string
+  spoiler_node::to_string(const tgba* a)
+  {
+    std::ostringstream os;
+    // print the node.
+    os << num_
+       << " [shape=box, label=\"("
+       << a->format_state(sc_->first)
+       << ", "
+       << a->format_state(sc_->second)
+       << ")\"]"
+       << std::endl;
+    return os.str();
+  }
+
+  std::string
+  spoiler_node::succ_to_string()
+  {
+    std::ostringstream os;
+    sn_v::iterator i;
+    for (i = lnode_succ->begin(); i != lnode_succ->end(); ++i)
+      {
+	os << num_ << " -> " << (*i)->num_ << std::endl;
+      }
+    return os.str();
+  }
+
+  int
+  spoiler_node::get_nb_succ()
+  {
+    return lnode_succ->size();
+  }
+
+  const state*
+  spoiler_node::get_spoiler_node()
+  {
+    return sc_->first;
+  }
+
+  const state*
+  spoiler_node::get_duplicator_node()
+  {
+    return sc_->second;
+  }
+
+  state_couple*
+  spoiler_node::get_pair()
+  {
+    return sc_;
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+  // duplicator_node
+
+  duplicator_node::duplicator_node(const state* d_node,
+				   const state* s_node,
+				   bdd l,
+				   bdd a,
+				   int num)
+    : spoiler_node(d_node, s_node, num),
+      label_(l),
+      acc_(a)
+  {
+  }
+
+  duplicator_node::~duplicator_node()
+  {
+  }
+
+  bool
+  duplicator_node::set_win()
+  {
+    bool change = not_win;
+
+    if (!this->get_nb_succ())
+      not_win = true;
+    else
+      {
+	not_win = true;
+	for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin();
+	     i != lnode_succ->end(); ++i)
+	  {
+	    not_win &= (*i)->not_win;
+	  }
+      }
+    return (change != not_win);
+  }
+
+  std::string
+  duplicator_node::to_string(const tgba* a)
+  {
+    std::ostringstream os;
+
+    // print the node.
+    os << num_
+       << " [shape=box, label=\"("
+       << a->format_state(sc_->first)
+       << ", "
+       << a->format_state(sc_->second)
+       << ", ";
+    bdd_print_acc(os, a->get_dict(), acc_);
+    os << ")\"]"
+       << std::endl;
+
+    return os.str();
+  }
+
+  bool
+  duplicator_node::match(bdd l, bdd a)
+  {
+    return ((l == label_) && (a == acc_));
+  }
+
+  bool
+  duplicator_node::implies(bdd l, bdd a)
+  {
+    // if (a | !b) == true then (a => b).
+    return (((l | !label_) == bddtrue) &&
+	    ((a | !acc_) == bddtrue));
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+  // parity_game_graph
+
+  void
+  parity_game_graph::start()
+  {
+  }
+
+  void
+  parity_game_graph::end()
+  {
+  }
+
+  void
+  parity_game_graph::process_state(const state* s,
+				    int ,
+				    tgba_succ_iterator*)
+  {
+    tgba_state_.push_back(s);
+  }
+
+  void
+  parity_game_graph::process_link(int ,
+				   int ,
+				   const tgba_succ_iterator*)
+  {
+  }
+
+  void
+  parity_game_graph::print(std::ostream& os)
+  {
+    Sgi::vector<spoiler_node*>::iterator i1;
+    Sgi::vector<duplicator_node*>::iterator i2;
+
+    int n = 0;
+
+    os << "digraph G {" << std::endl;
+
+    os << "{" << std::endl
+       << "rank = same;" << std::endl
+       << "node [color=red];" << std::endl;
+    for (i1 = spoiler_vertice_.begin();
+	 i1 != spoiler_vertice_.end(); ++i1)
+      {
+	os << (*i1)->to_string(automata_);
+	n++;
+	if (n > 20)
+	  {
+	    n = 0;
+	    os << "}" << std::endl << std::endl
+	       << "{" << std::endl
+	       << "rank = same" << std::endl
+	       << "node [color=red];" << std::endl;
+	  }
+      }
+    os << "}" << std::endl;
+
+    n = 0;
+    os << "{" << std::endl
+       << "rank = same;" << std::endl
+       << "node [color=green];" << std::endl;
+    for (i2 = duplicator_vertice_.begin();
+	 i2 != duplicator_vertice_.end(); ++i2)
+      {
+	os << (*i2)->to_string(automata_);
+	n++;
+	if (n > 20)
+	  {
+	    n = 0;
+	    os << "}" << std::endl << std::endl
+	       << "{" << std::endl
+	       << "rank = same" << std::endl
+	       << "node [color=green];" << std::endl;
+	  }
+      }
+    os << "}" << std::endl << std::endl;
+
+    os << "edge [color=red];" << std::endl;
+    for (i1 = spoiler_vertice_.begin();
+	 i1 != spoiler_vertice_.end(); ++i1)
+      {
+	os << (*i1)->succ_to_string();
+      }
+
+    os << std::endl
+       << "edge [color=green];" << std::endl;
+    for (i2 = duplicator_vertice_.begin();
+	 i2 != duplicator_vertice_.end(); ++i2)
+      {
+	os << (*i2)->succ_to_string();
+      }
+
+    os << "}" << std::endl;
+
+  }
+
+  parity_game_graph::~parity_game_graph()
+  {
+    Sgi::vector<spoiler_node*>::iterator i1;
+    Sgi::vector<duplicator_node*>::iterator i2;
+
+    for (i1 = spoiler_vertice_.begin();
+	 i1 != spoiler_vertice_.end(); ++i1)
+      {
+	delete *i1;
+      }
+
+    for (i2 = duplicator_vertice_.begin();
+	 i2 != duplicator_vertice_.end(); ++i2)
+      {
+	delete *i2;
+      }
+
+    spoiler_vertice_.clear();
+    duplicator_vertice_.clear();
+  }
+
+  parity_game_graph::parity_game_graph(const tgba* a)
+    : tgba_reachable_iterator_breadth_first(a)
+  {
+    this->run();
+    nb_node_parity_game = 0;
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+  // parity_game_graph_direct
+
+  void
+  parity_game_graph_direct::build_couple()
+  {
+    tgba_succ_iterator* si = NULL;
+    typedef Sgi::pair<bdd, bdd> couple_bdd;
+    couple_bdd *p = NULL;
+    Sgi::vector<couple_bdd*>* trans = NULL;
+    bool exist = false;
+    spot::state* s = NULL;
+
+    for (Sgi::vector<const state*>::iterator i = tgba_state_.begin();
+	 i != tgba_state_.end(); ++i)
+      {
+
+	// spoiler node are all state couple (i,j)
+	for (Sgi::vector<const state*>::iterator j = tgba_state_.begin();
+	     j != tgba_state_.end(); ++j)
+	  {
+	    spoiler_node* n1 = new spoiler_node(*i,
+						*j,
+						nb_node_parity_game++);
+	    spoiler_vertice_.push_back(n1);
+	  }
+
+	// duplicator node are all state couple where
+	// the first state i are reachable.
+	trans = new Sgi::vector<couple_bdd*>;
+        for (Sgi::vector<const state*>::iterator j = tgba_state_.begin();
+	     j != tgba_state_.end(); ++j)
+	  {
+	    si = automata_->succ_iter(*j);
+	    for (si->first(); !si->done(); si->next())
+	      {
+
+		// if there exist a predecessor of i named j
+		s = si->current_state();
+		if (s->compare(*i) == 0)
+		  {
+
+		    // p is the label of the transition j->i
+		    p = new couple_bdd(si->current_condition(),
+				       si->current_acceptance_conditions());
+
+		    // If an other predecessor of i has the same label p
+		    // to reach i, then we don't compute the duplicator node.
+		    exist = false;
+		    for (Sgi::vector<couple_bdd*>::iterator v
+			   = trans->begin();
+			 v != trans->end(); ++v)
+		      {
+			if ((si->current_condition() == (*v)->first) &&
+			    (si->current_acceptance_conditions()
+			     == (*v)->second))
+			  exist = true;
+		      }
+
+		    if (!exist)
+		      {
+			// We build all the state couple with the label p.
+			trans->push_back(p);
+			for (Sgi::vector<const state*>::iterator s
+			       = tgba_state_.begin();
+			     s != tgba_state_.end(); ++s)
+			  {
+			    duplicator_node* n2
+			      = new duplicator_node(*i,
+						    *s,
+						    si->current_condition(),
+						    si->current_acceptance_conditions(),
+						    nb_node_parity_game++);
+			    duplicator_vertice_.push_back(n2);
+			  }
+		      }
+		    else
+		      delete p;
+		  }
+		delete s;
+	      }
+	    delete si;
+	  }
+	Sgi::vector<couple_bdd*>::iterator i2;
+	for (i2 = trans->begin(); i2 != trans->end(); ++i2)
+	  {
+	    delete *i2;
+	  }
+	delete trans;
+      }
+  }
+
+  void
+  parity_game_graph_direct::build_link()
+  {
+    int nb_ds = 0;
+    int nb_sd = 0;
+    spot::state* s = NULL;
+
+    // for each couple of (spoiler, duplicator)
+    for (Sgi::vector<spoiler_node*>::iterator i
+	   = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i)
+      {
+	for (Sgi::vector<duplicator_node*>::iterator j
+	       = duplicator_vertice_.begin();
+	     j != duplicator_vertice_.end(); ++j)
+	  {
+	    // We add a link between a duplicator and a spoiler.
+	    if ((*j)->get_spoiler_node()->compare((*i)->get_spoiler_node()) == 0)
+	      {
+		tgba_succ_iterator* si
+		  = automata_->succ_iter((*j)->get_duplicator_node());
+		for (si->first(); !si->done(); si->next())
+		  {
+		    s = si->current_state();
+		    if ((s->compare((*i)->get_duplicator_node()) == 0) &&
+			(*j)->implies(si->current_condition(),
+				      si->current_acceptance_conditions()))
+		      {
+			(*j)->add_succ(*i);
+			nb_ds++;
+		      }
+		    delete s;
+		  }
+		delete si;
+	      }
+
+	    // We add a link between a spoiler and a duplicator.
+	    if ((*j)->get_duplicator_node()->compare((*i)->get_duplicator_node()) == 0)
+	      {
+		tgba_succ_iterator* si
+		  = automata_->succ_iter((*i)->get_spoiler_node());
+		for (si->first(); !si->done(); si->next())
+		  {
+		    s = si->current_state();
+		    if ((s->compare((*j)->get_spoiler_node()) == 0) &&
+			(*j)->match(si->current_condition(),
+				    si->current_acceptance_conditions()))
+		      {
+			(*i)->add_succ(*j);
+			nb_sd++;
+		      }
+		    delete s;
+		  }
+		delete si;
+	      }
+	  }
+      }
+  }
+
+  void
+  parity_game_graph_direct::prune()
+  {
+    bool change = true;
+
+    while (change)
+      {
+	change = false;
+	for (Sgi::vector<duplicator_node*>::iterator i
+	       = duplicator_vertice_.begin();
+	     i != duplicator_vertice_.end(); ++i)
+	  {
+	    change |= (*i)->set_win();
+	  }
+	for (Sgi::vector<spoiler_node*>::iterator i
+	       = spoiler_vertice_.begin();
+	     i != spoiler_vertice_.end(); ++i)
+	  {
+	    change |= (*i)->set_win();
+	  }
+      }
+
+  }
+
+  simulation_relation*
+  parity_game_graph_direct::get_relation()
+  {
+    simulation_relation* rel = new simulation_relation();
+    state_couple* p = NULL;
+    seen_map::iterator j;
+
+    for (Sgi::vector<spoiler_node*>::iterator i
+	   = spoiler_vertice_.begin();
+	 i != spoiler_vertice_.end(); ++i)
+      {
+	if (!(*i)->not_win)
+	  {
+	    p = new state_couple((*i)->get_spoiler_node(),
+				 (*i)->get_duplicator_node());
+	    rel->push_back(p);
+
+
+	    // We remove the state in rel from seen
+	    // because the destructor of
+	    // tgba_reachable_iterator_breadth_first
+	    // delete all the state.
+
+
+   	    if ((j = seen.find(p->first)) != seen.end())
+	      seen.erase(j);
+	    if ((j = seen.find(p->second)) != seen.end())
+	      seen.erase(j);
+
+	  }
+      }
+
+    return rel;
+  }
+
+  parity_game_graph_direct::~parity_game_graph_direct()
+  {
+  }
+
+  parity_game_graph_direct::parity_game_graph_direct(const tgba* a)
+    : parity_game_graph(a)
+  {
+    this->build_couple();
+    this->build_link();
+    this->prune();
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+
+  simulation_relation*
+  get_direct_relation_simulation(const tgba* f, int opt)
+  {
+    parity_game_graph_direct* G = new parity_game_graph_direct(f);
+    simulation_relation* rel = G->get_relation();
+    if (opt == 1)
+      G->print(std::cout);
+    delete G;
+    return rel;
+  }
+
+  void
+  free_relation_simulation(simulation_relation* rel)
+  {
+    if (rel == NULL)
+      return;
+
+    Sgi::hash_map<const spot::state*, int,
+      state_ptr_hash, state_ptr_equal> seen;
+    Sgi::hash_map<const spot::state*, int,
+      state_ptr_hash, state_ptr_equal>::iterator j;
+
+    simulation_relation::iterator i;
+    for (i = rel->begin(); i != rel->end(); ++i)
+      {
+	if ((j = seen.find((*i)->first)) == seen.end())
+	    seen[(*i)->first] = 0;
+
+	if ((j = seen.find((*i)->second)) == seen.end())
+	    seen[(*i)->second] = 0;
+
+	delete *i;
+      }
+    delete rel;
+    rel = NULL;
+
+    for (j = seen.begin(); j != seen.end();)
+      {
+	const state* ptr = j->first;
+	++j;
+	delete(ptr);
+      }
+  }
+
+  bool
+  is_include(const tgba*, const tgba*)
+  {
+    return false;
+  }
+
+  tgba*
+  reduc_tgba_sim(const tgba* f, int opt)
+  {
+    spot::tgba_reduc* automatareduc = new  spot::tgba_reduc(f);
+
+    if (opt & Reduce_Dir_Sim)
+      {
+	simulation_relation* rel
+	  = get_direct_relation_simulation(automatareduc);
+
+	automatareduc->display_rel_sim(rel, std::cout);
+	automatareduc->prune_automata(rel);
+
+	free_relation_simulation(rel);
+      }
+    else
+      if (opt & Reduce_Del_Sim)
+	{
+	  simulation_relation* rel
+	    = get_delayed_relation_simulation(automatareduc);
+
+	  automatareduc->display_rel_sim(rel, std::cout);
+	  automatareduc->prune_automata(rel);
+
+	  free_relation_simulation(rel);
+	}
+
+    if (opt & Reduce_Scc)
+      {
+	automatareduc->compute_scc();
+	automatareduc->prune_scc();
+      }
+
+    return automatareduc;
+  }
+
+}

src/tgbaalgos/reductgba_sim.hh

@@ -0,0 +1,314 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+
+#ifndef SPOT_REDUC_TGBA_SIM_HH
+#define SPOT_REDUC_TGBA_SIM_HH
+
+#include "tgba/tgbareduc.hh"
+#include "tgbaalgos/reachiter.hh"
+#include <vector>
+#include <list>
+#include <sstream>
+
+namespace spot
+{
+
+  /// Options for reduce.
+  enum reduce_tgba_options
+    {
+      /// No reduction.
+      Reduce_None = 0,
+      /// Reduction using direct simulation relation.
+      Reduce_Dir_Sim = 1,
+      /// Reduction using delayed simulation relation.
+      Reduce_Del_Sim = 2,
+      /// Reduction using SCC.
+      Reduce_Scc = 4,
+      /// All reductions.
+      Reduce_All = -1U
+    };
+
+  /// \brief Remove some node of the automata using a simulation
+  /// relation.
+  ///
+  /// \param a the automata to reduce.
+  /// \param opt a conjonction of spot::reduce_tgba_options specifying
+  //             which optimizations to apply.
+  /// \return the reduced automata.
+  tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All);
+
+  /// \brief Compute a direct simulation relation on state of tgba \a f.
+  simulation_relation* get_direct_relation_simulation(const tgba* a,
+						      int opt = -1);
+
+  /// Compute a delayed simulation relation on state of tgba \a f.
+  /// FIXME : this method is incorrect !!
+  /// Don't use it !!
+  simulation_relation*  get_delayed_relation_simulation(const tgba* a,
+						      int opt = -1);
+
+  /// To free a simulation relation.
+  void free_relation_simulation(simulation_relation* rel);
+
+  /// Test if the initial state of a2 fair simulate this of a1.
+  /// Not implemented.
+  bool is_include(const tgba* a1, const tgba* a2);
+
+  ///////////////////////////////////////////////////////////////////////
+  // simulation.
+
+  class spoiler_node;
+  class duplicator_node;
+
+  typedef Sgi::vector<spoiler_node*> sn_v;
+  typedef Sgi::vector<duplicator_node*> dn_v;
+  typedef Sgi::vector<const state*> s_v;
+
+  /// \brief Parity game graph which compute a simulation relation.
+  class parity_game_graph : public tgba_reachable_iterator_breadth_first
+  {
+  public:
+    parity_game_graph(const tgba* a);
+    virtual ~parity_game_graph();
+
+    virtual simulation_relation* get_relation() = 0;
+
+    void print(std::ostream& os);
+
+  protected:
+    sn_v spoiler_vertice_;
+    dn_v duplicator_vertice_;
+    s_v tgba_state_;
+    int nb_node_parity_game;
+
+    void start();
+    void end();
+    void process_state(const state* s, int n, tgba_succ_iterator* si);
+    void process_link(int in, int out, const tgba_succ_iterator* si);
+
+    /// \brief Compute each node of the graph.
+    virtual void build_couple() = 0;
+
+    /// \brief Compute the link of the graph.
+    /// Successor of spoiler node (resp. duplicator node)
+    /// are duplicator node (resp. spoiler node).
+    virtual void build_link() = 0;
+
+    /// \brief Remove edge from spoiler to duplicator that make
+    /// duplicator loose.
+    /// Spoiler node whose still have some link, reveal
+    /// a direct simulation relation.
+    virtual void prune() = 0;
+  };
+
+  ///////////////////////////////////////////////////////////////////////
+  // Direct simulation.
+
+  /// Spoiler node of parity game graph.
+  class spoiler_node
+  {
+  public:
+    spoiler_node(const state* d_node,
+		 const state* s_node,
+		 int num);
+    virtual ~spoiler_node();
+
+    void add_succ(spoiler_node* n);
+    void del_succ(spoiler_node* n);
+    virtual void add_pred(spoiler_node* n);
+    virtual void del_pred();
+    int get_nb_succ();
+    bool prune();
+    virtual bool set_win();
+    virtual std::string to_string(const tgba* a);
+    virtual std::string succ_to_string();
+
+    const state* get_spoiler_node();
+    const state* get_duplicator_node();
+    state_couple* get_pair();
+
+    bool not_win;
+    int num_; // for the dot display.
+
+  protected:
+    sn_v* lnode_succ;
+    sn_v* lnode_pred;
+    //Sgi::vector<spoiler_node*>* lnode_succ;
+    state_couple* sc_;
+  };
+
+  /// Duplicator node of parity game graph.
+  class duplicator_node : public spoiler_node
+  {
+  public:
+    duplicator_node(const state* d_node,
+		    const state* s_node,
+		    bdd l,
+		    bdd a,
+		    int num);
+    virtual ~duplicator_node();
+
+    virtual bool set_win();
+    virtual std::string to_string(const tgba* a);
+
+    bool match(bdd l, bdd a);
+    bool implies(bdd l, bdd a);
+
+  protected:
+    bdd label_;
+    bdd acc_;
+  };
+
+  /// Parity game graph which compute the direct simulation relation.
+  class parity_game_graph_direct : public parity_game_graph
+  {
+  public:
+    parity_game_graph_direct(const tgba* a);
+    ~parity_game_graph_direct();
+
+    virtual simulation_relation* get_relation();
+
+  protected:
+
+    virtual void build_couple();
+    virtual void build_link();
+    virtual void prune();
+  };
+
+
+  ///////////////////////////////////////////////////////////////////////
+  // Delayed simulation.
+
+  /// Spoiler node of parity game graph for delayed simulation.
+  class spoiler_node_delayed : public spoiler_node
+  {
+  public:
+    spoiler_node_delayed(const state* d_node,
+			 const state* s_node,
+			 bdd a,
+			 int num);
+    ~spoiler_node_delayed();
+
+    /// Return true if the progress_measure has changed.
+    bool set_win();
+    bdd get_acceptance_condition_visited();
+
+    virtual std::string to_string(const tgba* a);
+
+    int get_progress_measure();
+
+  protected:
+    /// a Bdd for retain all the acceptance condition
+    /// that a node has visited.
+    bdd acceptance_condition_visited_;
+    int progress_measure_;
+
+  };
+
+  /// Duplicator node of parity game graph for delayed simulation.
+  class duplicator_node_delayed : public duplicator_node
+  {
+  public:
+    duplicator_node_delayed(const state* d_node,
+			    const state* s_node,
+			    bdd l,
+			    bdd a,
+			    int num);
+    ~duplicator_node_delayed();
+
+    /// Return true if the progress_measure has changed.
+    bool set_win();
+    virtual std::string to_string(const tgba* a);
+
+    bool implies_label(bdd l);
+    bool implies_acc(bdd a);
+
+    int get_progress_measure();
+
+  protected:
+    int progress_measure_;
+  };
+
+  /// Parity game graph which compute the delayed simulation relation
+  /// as explain in
+  /// @inproceedings{ icalp2001,
+  /// AUTHOR = {Etessami, Thomas Wilke, Rebecca A. Schuller},
+  /// TITLE = {Fair Simulation Relations, Parity Games, and State Space
+  ///          Reduction for Buchi Automata},
+  /// BOOKTITLE = {Automata, Languages and Programming,
+  /// 28th international collquium},
+  /// PAGES = {694--707},
+  /// YEAR = 2001,
+  /// EDITOR = {Orejas, Fernando and Spirakis, Paul G. and van Leeuwen, Jan},
+  /// VOLUME = 2076,
+  /// SERIES = {Lecture Notes in Computer Science},
+  /// ADDRESS = {Crete, Greece},
+  /// MONTH = JUL,
+  /// PUBLISHER = {Springer},
+  /// url = {citeseer.ist.psu.edu/472661.html}
+  /// }
+
+  class parity_game_graph_delayed : public parity_game_graph
+  {
+  public:
+    parity_game_graph_delayed(const tgba* a);
+    ~parity_game_graph_delayed();
+
+    virtual simulation_relation* get_relation();
+
+  private:
+
+    /// Vector which contain all the sub-set of the set
+    /// of acceptance condition.
+    typedef Sgi::vector<bdd> bdd_v;
+    bdd_v sub_set_acc_cond_;
+
+    /// Return the number of acceptance condition.
+    int nb_set_acc_cond();
+
+    /// Compute sub_set_acc_cond_;
+    void build_sub_set_acc_cond();
+
+    /// Add a duplicator node, and
+    /// all his successor (spoiler node) which
+    /// have a acceptance_condition_visited_ != bddfalse
+    void add_dup_node(state* ss,
+		      state* sd,
+		      bdd l,
+		      bdd a);
+
+    /// \brief Compute the couple as for direct simulation,
+    virtual void build_couple();
+    virtual void build_link();
+    void build_recurse_successor_spoiler(spoiler_node* sn);
+    void build_recurse_successor_duplicator(duplicator_node* dn);
+
+    /// \brief The Jurdzinski's lifting algorithm.
+    void lift();
+
+    /// \brief Remove all node so as to there is no dead ends (terminal node).
+    virtual void prune();
+  };
+
+}
+
+#endif

src/tgbaalgos/reductgba_sim_del.cc

@@ -0,0 +1,816 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reductgba_sim.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  /// Number of spoiler node with a one priority (see icalp2001).
+  /// The one priority is represent by a \a acceptance_condition_visited_
+  /// which differ of bddfalse.
+  /// This spoiler node are looser for the duplicator.
+  static int nb_spoiler_loose_;
+
+  static int nb_spoiler;
+  static int nb_duplicator;
+
+  //static int nb_node;
+
+  ///////////////////////////////////////////////////////////////////////
+  // spoiler_node_delayed
+
+  spoiler_node_delayed::spoiler_node_delayed(const state* d_node,
+					     const state* s_node,
+					     bdd a,
+					     int num)
+    : spoiler_node(d_node, s_node, num),
+      acceptance_condition_visited_(a)
+  {
+    nb_spoiler++;
+    progress_measure_ = 0;
+    if (acceptance_condition_visited_ == bddfalse)
+      nb_spoiler_loose_++;
+  }
+
+  spoiler_node_delayed::~spoiler_node_delayed()
+  {
+  }
+
+  bool
+  spoiler_node_delayed::set_win()
+  {
+    // We take the max of the progress measure of the successor node
+    // because we are on a spoiler.
+
+    //std::cout << "spoiler_node_delayed::set_win" << std::endl;
+
+    if (lnode_succ->size() == 0)
+      progress_measure_ = nb_spoiler_loose_;
+
+    if (progress_measure_ >= nb_spoiler_loose_)
+      return false;
+
+    bool change;
+    int tmpmax = 0;
+    int tmp = 0;
+    sn_v::iterator i = lnode_succ->begin();
+    if (i != lnode_succ->end())
+      {
+	tmpmax =
+	  dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
+	++i;
+      }
+    for (; i != lnode_succ->end(); ++i)
+      {
+	tmp =
+	  dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
+	if (tmp > tmpmax)
+	  tmpmax = tmp;
+      }
+
+    // If the priority of the node is 1
+    // acceptance_condition_visited_ != bddfalse
+    // then we increment the progress measure of 1.
+    if (acceptance_condition_visited_ != bddfalse)
+      tmpmax++;
+
+    change = (progress_measure_ < tmpmax);
+
+    progress_measure_ = tmpmax;
+    return change;
+  }
+
+  std::string
+  spoiler_node_delayed::to_string(const tgba* a)
+  {
+    std::ostringstream os;
+
+    // print the node.
+    os << num_
+       << " [shape=box, label=\"("
+       << a->format_state(sc_->first)
+       << ", "
+       << a->format_state(sc_->second)
+       << ", ";
+    //bdd_print_acc(os, a->get_dict(), acceptance_condition_visited_);
+    if (acceptance_condition_visited_ == bddfalse)
+      {
+	os << "false";
+      }
+    else
+      {
+	os << "ACC";
+      }
+    os << ")"
+       << " pm = " << progress_measure_ << "\"]"
+       << std::endl;
+
+    return os.str();
+  }
+
+  bdd
+  spoiler_node_delayed::get_acceptance_condition_visited()
+  {
+    return acceptance_condition_visited_;
+  }
+
+  int
+  spoiler_node_delayed::get_progress_measure()
+  {
+    if ((acceptance_condition_visited_ == bddfalse) &&
+	(progress_measure_ != (nb_spoiler_loose_ + 1)))
+      return 0;
+    else
+      return progress_measure_;
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+  // duplicator_node_delayed
+
+  duplicator_node_delayed::duplicator_node_delayed(const state* d_node,
+						   const state* s_node,
+						   bdd l,
+						   bdd a,
+						   int num)
+    : duplicator_node(d_node, s_node, l, a, num)
+  {
+    nb_duplicator++;
+    progress_measure_ = 0;
+  }
+
+  duplicator_node_delayed::~duplicator_node_delayed()
+  {
+  }
+
+  bool
+  duplicator_node_delayed::set_win()
+  {
+    // We take the min of the progress measure of the successor node
+    // because we are on a duplicator.
+
+    //std::cout << "duplicator_node_delayed::set_win" << std::endl;
+
+    //bool debug = true;
+
+    if (progress_measure_ == nb_spoiler_loose_)
+      return false;
+
+    bool change;
+    int tmpmin = 0;
+    int tmp = 0;
+    sn_v::iterator i = lnode_succ->begin();
+    if (i != lnode_succ->end())
+      {
+	tmpmin = dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
+	/*
+	  debug &= (dynamic_cast<spoiler_node_delayed*>(*i)
+	  ->get_acceptance_condition_visited()
+	  != bddfalse);
+	*/
+	++i;
+      }
+    for (; i != lnode_succ->end(); ++i)
+      {
+	/*
+	  debug &= (dynamic_cast<spoiler_node_delayed*>(*i)
+	  ->get_acceptance_condition_visited()
+	  != bddfalse);
+	*/
+	tmp = dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
+	if (tmp < tmpmin)
+	  tmpmin = tmp;
+      }
+
+    /*
+    if (debug)
+      std::cout << "All successor p = 1" << std::endl;
+    else
+      std::cout << "Not All successor p = 1" << std::endl;
+    */
+
+    change = (progress_measure_ < tmpmin);
+    progress_measure_ = tmpmin;
+    return change;
+  }
+
+  std::string
+  duplicator_node_delayed::to_string(const tgba* a)
+  {
+    std::ostringstream os;
+
+    // print the node.
+    os << num_
+       << " [shape=box, label=\"("
+       << a->format_state(sc_->first)
+       << ", "
+       << a->format_state(sc_->second);
+    //<< ", ";
+    //bdd_print_acc(os, a->get_dict(), acc_);
+    os << ")"
+       << " pm = " << progress_measure_ << "\"]"
+       << std::endl;
+
+    return os.str();
+  }
+
+  bool
+  duplicator_node_delayed::implies_label(bdd l)
+  {
+    return ((l | !label_) == bddtrue);
+  }
+
+  bool
+  duplicator_node_delayed::implies_acc(bdd a)
+  {
+    return ((a | !acc_) == bddtrue);
+  }
+
+  int
+  duplicator_node_delayed::get_progress_measure()
+  {
+    return progress_measure_;
+  }
+
+  ///////////////////////////////////////////////////////////////////////
+  // parity_game_graph_delayed
+
+  int
+  parity_game_graph_delayed::nb_set_acc_cond()
+  {
+    bdd acc, all;
+    acc = all = automata_->all_acceptance_conditions();
+    int count = 0;
+    while (all != bddfalse)
+      {
+	sub_set_acc_cond_.push_back(bdd_satone(all));
+        all -= bdd_satone(all);
+	count++;
+      }
+    return count;
+  }
+
+  void
+  parity_game_graph_delayed::build_sub_set_acc_cond()
+  {
+    // compute the number of acceptance conditions
+    bdd acc, all;
+    acc = all = automata_->all_acceptance_conditions();
+    int count = 0;
+    while (all != bddfalse)
+      {
+	//std::cout << "add acc" << std::endl;
+	sub_set_acc_cond_.push_back(bdd_satone(all));
+        all -= bdd_satone(all);
+	count++;
+      }
+    // sub_set_acc_cond_ contains all the acceptance condition.
+    // but we must have all the sub-set of acceptance condition.
+    // In fact we must have 2^count sub-set.
+
+    if (count == 2)
+      {
+	sub_set_acc_cond_.push_back(acc);
+	sub_set_acc_cond_.push_back(bddfalse);
+      }
+
+    /*
+      bdd_v::iterator i;
+
+      bdd_v::iterator j;
+      for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end(); ++i)
+      for (j = sub_set_acc_cond_.begin(); j != sub_set_acc_cond_.end(); ++j)
+      sub_set_acc_cond_.push_back(*i | *j);
+
+      std::cout << std::endl;
+      for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end();)
+      {
+      bdd_print_acc(std::cout, automata_->get_dict(), *i);
+      std::cout << " // " << std::endl;
+      ++i;
+      }
+      std::cout << std::endl;
+    */
+  }
+
+
+  void
+  parity_game_graph_delayed::build_couple()
+  {
+    //std::cout << "build couple" << std::endl;
+
+    nb_spoiler = 0;
+    nb_duplicator = 0;
+
+    tgba_succ_iterator* si = NULL;
+    typedef Sgi::pair<bdd, bdd> couple_bdd;
+    couple_bdd *p = NULL;
+    Sgi::vector<couple_bdd*>* trans = NULL;
+    bool exist = false;
+    spot::state* s = NULL;
+
+    s_v::iterator i;
+    for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i)
+      {
+
+	// for each sub-set of the set of acceptance condition.
+	bdd_v::iterator i2;
+	for (i2 = sub_set_acc_cond_.begin();
+	     i2 != sub_set_acc_cond_.end(); ++i2)
+	  {
+
+	    // spoiler node are all state couple (i,j)
+	    // multiply by 2^(|F|)
+	    s_v::iterator i3;
+	    for (i3 = tgba_state_.begin();
+		 i3 != tgba_state_.end(); ++i3)
+	      {
+		//nb_spoiler++;
+		spoiler_node_delayed* n1
+		  = new spoiler_node_delayed(*i,
+					     *i3,
+					     *i2,
+					     nb_node_parity_game++);
+		spoiler_vertice_.push_back(n1);
+	      }
+
+	    // duplicator node are all state couple where
+	    // the first state i are reachable.
+	    trans = new Sgi::vector<couple_bdd*>;
+	    for (i3 = tgba_state_.begin();
+		 i3 != tgba_state_.end(); ++i3)
+	      {
+		si = automata_->succ_iter(*i3);
+		for (si->first(); !si->done(); si->next())
+		  {
+
+		    // if there exist a predecessor of i named j
+		    s = si->current_state();
+		    if (s->compare(*i) == 0)
+		      {
+
+			// p is the label of the transition j->i
+			p = new couple_bdd(si->current_condition(),
+					   si->current_acceptance_conditions());
+
+			// If an other predecessor of i has the same label p
+			// to reach i, then we don't compute the
+			// duplicator node.
+			exist = false;
+			Sgi::vector<couple_bdd*>::iterator i4;
+			for (i4 = trans->begin();
+			     i4 != trans->end(); ++i4)
+			  {
+			    if ((si->current_condition() == (*i4)->first))
+			      // We don't need the acceptance condition
+			      //&&
+			      //(si->current_acceptance_conditions()
+			      //== (*i4)->second))
+			      exist = true;
+			  }
+
+			if (!exist)
+			  {
+			    // We build all the state couple with the label p.
+			    // multiply by 2^(|F|)
+			    trans->push_back(p);
+			    Sgi::vector<const state*>::iterator i5;
+			    for (i5 = tgba_state_.begin();
+				 i5 != tgba_state_.end(); ++i5)
+			      {
+				//nb_duplicator++;
+				int nb = nb_node_parity_game++;
+				duplicator_node_delayed* n2
+				  = new
+				  duplicator_node_delayed(*i,
+							  *i5,
+							  si->
+							  current_condition(),
+							  *i2,
+							  nb);
+				duplicator_vertice_.push_back(n2);
+			      }
+			  }
+			else
+			  delete p;
+		      }
+		    delete s;
+		  }
+		delete si;
+	      }
+	    Sgi::vector<couple_bdd*>::iterator i6;
+	    for (i6 = trans->begin(); i6 != trans->end(); ++i6)
+	      {
+		delete *i6;
+	      }
+	    delete trans;
+	  }
+      }
+    nb_spoiler_loose_++;
+
+    //std::cout << "spoiler    node : " << nb_spoiler << std::endl;
+    //std::cout << "duplicator node : " << nb_duplicator << std::endl;
+    //std::cout << "nb_spoiler_loose_ : " << nb_spoiler_loose_ << std::endl;
+  }
+
+  void
+  parity_game_graph_delayed::build_link()
+  {
+    //std::cout << "build link" << std::endl;
+    int nb_ds = 0;
+    int nb_sd = 0;
+    spot::state* s = NULL;
+
+    // for each couple of (spoiler, duplicator)
+    sn_v::iterator i;
+    for (i = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i)
+      {
+	dn_v::iterator i2;
+	for (i2 = duplicator_vertice_.begin();
+	     i2 != duplicator_vertice_.end(); ++i2)
+	  {
+
+	    // We add a link between a duplicator and a spoiler.
+	    if ((*i2)->get_spoiler_node()->compare((*i)
+						   ->get_spoiler_node()) == 0)
+	      {
+		tgba_succ_iterator* si
+		  = automata_->succ_iter((*i2)->get_duplicator_node());
+		for (si->first(); !si->done(); si->next())
+		  {
+		    s = si->current_state();
+
+		    bdd btmp2 = dynamic_cast<spoiler_node_delayed*>(*i)->
+		      get_acceptance_condition_visited();
+		    bdd btmp = btmp2 - si->current_acceptance_conditions();
+
+		    //if ((s->compare((*i)->get_duplicator_node()) == 0) &&
+		    //dynamic_cast<duplicator_node_delayed*>(*i2)->
+		    //  implies_label(si->current_condition()) &&
+		    //(btmp == btmp2))
+
+		    if ((s->compare((*i)->get_duplicator_node()) == 0) &&
+			dynamic_cast<duplicator_node_delayed*>(*i2)->
+			implies_label(si->current_condition()) &&
+			(dynamic_cast<spoiler_node_delayed*>(*i)->
+			 get_acceptance_condition_visited() != bddfalse))
+		      {
+			//std::cout << "add duplicator -> spoiler" << std::endl;
+			(*i2)->add_succ(*i);
+			(*i)->add_pred(*i2);
+			nb_ds++;
+		      }
+		    delete s;
+		  }
+		delete si;
+	      }
+
+	    // We add a link between a spoiler and a duplicator.
+	    if ((*i2)->get_duplicator_node()
+		->compare((*i)->get_duplicator_node()) == 0)
+	      {
+		tgba_succ_iterator* si
+		  = automata_->succ_iter((*i)->get_spoiler_node());
+		for (si->first(); !si->done(); si->next())
+		  {
+		    s = si->current_state();
+
+		    bdd btmp = si->current_acceptance_conditions() |
+		      dynamic_cast<spoiler_node_delayed*>(*i)->
+		      get_acceptance_condition_visited();
+		    if ((s->compare((*i2)->get_spoiler_node()) == 0) &&
+			(*i2)->match(si->current_condition(), btmp))
+		      {
+			//std::cout << "add spoiler -> duplicator" << std::endl;
+			(*i)->add_succ(*i2);
+			(*i2)->add_pred(*i);
+			nb_sd++;
+		      }
+		    delete s;
+		  }
+		delete si;
+	      }
+
+	  }
+      }
+  }
+
+  /*
+  // We build only node which are reachable
+  void
+  parity_game_graph_delayed::build_couple()
+  {
+    // We build only some "basic" spoiler node.
+
+    s_v::iterator i;
+    for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i)
+      {
+
+	// spoiler node are all state couple (i,j)
+	s_v::iterator i2;
+	for (i2 = tgba_state_.begin();
+	     i2 != tgba_state_.end(); ++i2)
+	  {
+	    std::cout << "add spoiler node" << std::endl;
+	    nb_spoiler++;
+	    spoiler_node_delayed* n1
+	      = new spoiler_node_delayed(*i, *i2,
+					 bddfalse,
+					 nb_node_parity_game++);
+	    spoiler_vertice_.push_back(n1);
+	  }
+      }
+  }
+
+  void
+  parity_game_graph_delayed::build_link()
+  {
+    // We create when it's possible a duplicator node
+    // and recursively his successor.
+
+    spot::state* s1 = NULL;
+    bool exist_pred = false;
+
+    sn_v::iterator i1;
+    for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1)
+      {
+	exist_pred = false;
+	// We check if there is a predecessor only if the duplicator
+	// is the initial state.
+	s1 = automata_->get_init_state();
+	if (s1->compare((*i1)->get_duplicator_node()) == 0)
+	  {
+	    tgba_succ_iterator* si;
+	    s_v::iterator i2;
+	    spot::state* s2 = NULL;
+	    for (i2 = tgba_state_.begin();
+		 i2 != tgba_state_.end(); ++i2)
+	      {
+		si = automata_->succ_iter(*i2);
+		s2 = si->current_state();
+		if (s2->compare(s1) == 0)
+		  exist_pred = true;
+		delete s2;
+	      }
+	  }
+	else
+	  exist_pred = true;
+	delete s1;
+
+	if (!exist_pred)
+	  continue;
+
+	// 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.
+	build_recurse_successor_spoiler(*i1);
+
+      }
+
+  }
+
+  void
+  parity_game_graph_delayed::build_recurse_successor_spoiler(spoiler_node* sn)
+  {
+    tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());
+
+    for (si->first(); !si->done(); si->next())
+      {
+	bdd btmp = si->current_acceptance_conditions() |
+	  dynamic_cast<spoiler_node_delayed*>(sn)->
+	  get_acceptance_condition_visited();
+
+	s_v::iterator i1;
+	state* s;
+	for (i1 = tgba_state_.begin();
+	     i1 != tgba_state_.end(); ++i1)
+	  {
+	    s  = si->current_state();
+	    if (s->compare(*i1) == 0)
+	      {
+		duplicator_node_delayed* dn
+		  = new duplicator_node_delayed(*i1,
+						sn->get_duplicator_node(),
+						si->current_condition(),
+						btmp,
+						nb_node_parity_game++);
+		duplicator_vertice_.push_back(dn);
+
+		sn->add_succ(dn);
+		(dn)->add_pred(sn);
+
+		build_recurse_successor_duplicator(dn);
+	      }
+	    delete s;
+	  }
+      }
+
+    delete si;
+
+  }
+
+  void
+  parity_game_graph_delayed::
+    build_recurse_successor_duplicator(duplicator_node* dn)
+  {
+    tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());
+
+    for (si->first(); !si->done(); si->next())
+      {
+	bdd btmp =
+	  dynamic_cast<spoiler_node_delayed*>(sn)->
+	    get_acceptance_condition_visited();
+	bdd btmp2 = btmp - si->current_acceptance_conditions();
+
+	s_v::iterator i1;
+	state* s;
+	for (i1 = tgba_state_.begin();
+	     i1 != tgba_state_.end(); ++i1)
+	  {
+	    s  = si->current_state();
+	    if (s->compare(*i1) == 0)
+	      {
+		spoiler_node_delayed* sn
+		  = new spoiler_node_delayed(sn->get_spoiler_node(),
+					     *i1,
+					     bddtmp2,
+					     nb_node_parity_game++);
+		spoiler_vertice_.push_back(n1);
+
+		sn->add_succ(dn);
+		(dn)->add_pred(sn);
+
+		build_recurse_successor_spoiler(sn);
+
+	      }
+	    delete s;
+	  }
+      }
+
+    delete si;
+
+  }
+  */
+
+  void
+  parity_game_graph_delayed::add_dup_node(state*,
+					  state*,
+					  bdd,
+					  bdd)
+  {
+  }
+
+  void
+  parity_game_graph_delayed::prune()
+  {
+
+    bool change = true;
+
+    while (change)
+      {
+	change = false;
+	for (Sgi::vector<duplicator_node*>::iterator i
+	       = duplicator_vertice_.begin();
+	     i != duplicator_vertice_.end();)
+	  {
+	    if ((*i)->get_nb_succ() == 0)
+	      {
+		(*i)->del_pred();
+		delete *i;
+		i = duplicator_vertice_.erase(i);
+		change = true;
+	      }
+	    else
+	      ++i;
+	  }
+	for (Sgi::vector<spoiler_node*>::iterator i
+	       = spoiler_vertice_.begin();
+	     i != spoiler_vertice_.end();)
+	  {
+	    if ((*i)->get_nb_succ() == 0)
+	      {
+		(*i)->del_pred();
+		delete *i;
+		i = spoiler_vertice_.erase(i);
+		change = true;
+	      }
+	    else
+	      ++i;
+	  }
+      }
+
+  }
+
+  void
+  parity_game_graph_delayed::lift()
+  {
+    // Jurdzinski's algorithm
+    //int iter = 0;
+    bool change = true;
+
+    while (change)
+      {
+	change = false;
+	for (Sgi::vector<duplicator_node*>::iterator i
+	       = duplicator_vertice_.begin();
+	     i != duplicator_vertice_.end(); ++i)
+	  {
+	    change |= (*i)->set_win();
+	  }
+	for (Sgi::vector<spoiler_node*>::iterator i
+	       = spoiler_vertice_.begin();
+	     i != spoiler_vertice_.end(); ++i)
+	  {
+	    change |= (*i)->set_win();
+	  }
+      }
+
+  }
+
+  simulation_relation*
+  parity_game_graph_delayed::get_relation()
+  {
+    simulation_relation* rel = new simulation_relation();
+    state_couple* p = NULL;
+    seen_map::iterator j;
+
+    for (Sgi::vector<spoiler_node*>::iterator i
+	   = spoiler_vertice_.begin();
+	 i != spoiler_vertice_.end(); ++i)
+      {
+	if (dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure()
+	    < nb_spoiler_loose_)
+	  {
+	    p = new state_couple((*i)->get_spoiler_node(),
+				 (*i)->get_duplicator_node());
+	    rel->push_back(p);
+
+	    // We remove the state in rel from seen
+	    // because the destructor of
+	    // tgba_reachable_iterator_breadth_first
+	    // delete all the state.
+
+	    if ((j = seen.find(p->first)) != seen.end())
+	      seen.erase(j);
+	    if ((j = seen.find(p->second)) != seen.end())
+	      seen.erase(j);
+	  }
+
+      }
+
+    return rel;
+  }
+
+  parity_game_graph_delayed::~parity_game_graph_delayed()
+  {
+  }
+
+  parity_game_graph_delayed::parity_game_graph_delayed(const tgba* a)
+    : parity_game_graph(a)
+  {
+    nb_spoiler_loose_ = 0;
+    /*
+      if (this->nb_set_acc_cond() > 2)
+      return;
+      this->build_sub_set_acc_cond();
+    */
+    this->build_couple();
+    this->build_link();
+    this->prune();
+    this->lift();
+    //this->print(std::cout);
+  }
+
+  ///////////////////////////////////////////
+  simulation_relation*
+  get_delayed_relation_simulation(const tgba* f, int opt)
+  {
+    /// 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;
+  }
+
+}

src/tgbatest/Makefile.am

@@ -38,6 +38,7 @@ check_PROGRAMS = \
   mixprod \
   powerset \
   readsave \
+  reductgba \
   tgbaread \
   tripprod
 
@@ -53,12 +54,14 @@ ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
 powerset_SOURCES = powerset.cc
 readsave_SOURCES = readsave.cc
+reductgba_SOURCES = reductgba.cc
 tgbaread_SOURCES = tgbaread.cc
 tripprod_SOURCES = tripprod.cc
 
 # Keep this sorted by STRENGTH.  Test basic things first,
 # because such failures will be easier to diagnose and fix.
 TESTS = \
+  reductgba.test \
   explicit.test \
   tgbaread.test \
   readsave.test \

src/tgbatest/ltl2tgba.cc

@@ -25,6 +25,7 @@
 #include <string>
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/reducform.hh"
+#include "ltlvisit/tostring.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba_lacim.hh"
@@ -40,6 +41,8 @@
 #include "tgbaalgos/dupexp.hh"
 #include "tgbaalgos/neverclaim.hh"
 
+#include "tgbaalgos/reductgba_sim.hh"
+
 void
 syntax(char* prog)
 {
@@ -83,6 +86,7 @@ syntax(char* prog)
 	    << "  -r3  reduce formula using implication between "
 	    << "sub-formulae" << std::endl
 	    << "  -r4  reduce formula using all rules" << std::endl
+	    << "  -rd  display the reduce formula" << std::endl
 	    << "  -R   same as -r, but as a set" << std::endl
 	    << "  -s   convert to explicit automata, and number states "
 	    << "in DFS order" << std::endl
@@ -98,7 +102,17 @@ syntax(char* prog)
 	    << "  -X   do not compute an automaton, read it from a file"
 	    << std::endl
 	    << "  -y   do not merge states with same symbolic representation "
-	    << "(implies -f)" << std::endl;
+	    << "(implies -f)" << std::endl
+	    << "  -R1  use direct simulation to reduce the automata "
+	    << "(implies -L)"
+	    << std::endl
+	    << "  -R2  use delayed simulation to reduce the automata, incorrect"
+	    << "(implies -L)"
+	    << std::endl
+	    << "  -R3  use SCC to reduce the automata"
+	    << std::endl
+	    << "  -Rd  to display simulation relation"
+	    << std::endl;
   exit(2);
 }
 
@@ -120,7 +134,10 @@ main(int argc, char** argv)
   bool magic_many = false;
   bool expect_counter_example = false;
   bool from_file = false;
+  int reduc_aut = spot::Reduce_None;
   int redopt = spot::ltl::Reduce_None;
+  bool display_reduce_form = false;
+  bool display_rel_sim = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
 
@@ -226,11 +243,11 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-r2"))
 	{
-	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
+	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
 	}
       else if (!strcmp(argv[formula_index], "-r3"))
 	{
-	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
+	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
 	}
       else if (!strcmp(argv[formula_index], "-r4"))
 	{
@@ -274,6 +291,28 @@ main(int argc, char** argv)
 	  fm_opt = true;
 	  fm_symb_merge_opt = false;
 	}
+      else if (!strcmp(argv[formula_index], "-R1"))
+	{
+	  reduc_aut |= spot::Reduce_Dir_Sim;
+	  fair_loop_approx = true;
+	}
+      else if (!strcmp(argv[formula_index], "-R2"))
+	{
+	  reduc_aut |= spot::Reduce_Del_Sim;
+	  fair_loop_approx = true;
+	}
+      else if (!strcmp(argv[formula_index], "-R3"))
+	{
+	  reduc_aut |= spot::Reduce_Scc;
+	}
+      else if (!strcmp(argv[formula_index], "-rd"))
+	{
+	  display_reduce_form = true;
+	}
+      else if (!strcmp(argv[formula_index], "-Rd"))
+	{
+	  display_rel_sim = true;
+	}
       else
 	{
 	  break;
@@ -341,6 +380,8 @@ main(int argc, char** argv)
 	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
 	      spot::ltl::destroy(f);
 	      f = t;
+	      if (display_reduce_form)
+		std::cout << spot::ltl::to_string(f) << std::endl;
 	    }
 
 	  if (fm_opt)
@@ -352,6 +393,46 @@ main(int argc, char** argv)
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	}
 
+      /*
+	spot::tgba* aut_red = 0;
+	if (reduc_aut != spot::Reduce_None)
+	a = aut_red = spot::reduc_tgba_sim(a, reduc_aut);
+      */
+
+      spot::tgba_reduc* aut_red = 0;
+      if (reduc_aut != spot::Reduce_None)
+	{
+	  a = aut_red = new spot::tgba_reduc(a);
+	  if ((reduc_aut & spot::Reduce_Dir_Sim) ||
+	      (reduc_aut & spot::Reduce_Del_Sim))
+	    {
+	      spot::simulation_relation* rel;
+	      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);
+	      else
+		assert(0);
+
+	      if (display_rel_sim)
+		aut_red->display_rel_sim(rel, std::cout);
+
+	      if (reduc_aut & spot::Reduce_Dir_Sim)
+		aut_red->prune_automata(rel);
+	      else if (reduc_aut & spot::Reduce_Del_Sim)
+		aut_red->quotient_state(rel);
+	      else
+		assert(0);
+
+	      spot::free_relation_simulation(rel);
+	    }
+
+	  if (reduc_aut & spot::Reduce_Scc)
+	    {
+	      aut_red->prune_scc();
+	    }
+	}
+
       spot::tgba_tba_proxy* degeneralized = 0;
       if (degeneralize_opt)
 	a = degeneralized = new spot::tgba_tba_proxy(a);
@@ -477,6 +558,8 @@ main(int argc, char** argv)
 	delete expl;
       if (degeneralize_opt)
 	delete degeneralized;
+      if (aut_red)
+	delete aut_red;
 
       delete to_free;
     }

src/tgbatest/spotlbtt.test

@@ -30,15 +30,15 @@ set -e
 cat > config <<EOF
 Algorithm
 {
-   Name = "Spot (Couvreur -- LaCIM), reduction of formula"
+   Name = "Spot (Couvreur -- LaCIM)"
-   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -F -t'"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -t'"
    Enabled = yes
 }
 
 Algorithm
 {
-   Name = "Spot (Couvreur -- LaCIM)"
+   Name = "Spot (Couvreur -- LaCIM), reduction of formula"
-   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -t'"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -F -t'"
    Enabled = yes
 }
 
@@ -63,6 +63,48 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), basic reduction of formula"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r1 -F -f -t'"
+   Enabled = no
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reduction of formula using class of formula"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r2 -F -f -t'"
+   Enabled = no
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reduction of formula using implies relation"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r3 -F -f -t'"
+   Enabled = no
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reduction of formula (pre reduction)"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -F -f -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), post reduction"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R1 -R2 -F -f -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), pre + post reduction"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -R1 -R2 -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), without symb_merge"
@@ -91,6 +133,13 @@ Algorithm
    Enabled = no
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reduction of formula, fake"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -F -f -T'"
+   Enabled = no
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), without symb_merge, fake"