* src/ltlvisit/basereduc.cc (spot): Correct some mistakes.

* src/ltlvisit/lunabbrev.cc (spot): Nothing change.
* src/tgbatest/ltl2tgba.cc (main): More option to reduce
formula.
* src/tgbatest/spotlbtt.test: One more test.

ChangeLog

@@ -1,3 +1,11 @@
+2004-05-14  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/ltlvisit/basereduc.cc (spot): Correct some mistakes.
+	* src/ltlvisit/lunabbrev.cc (spot): Nothing change.
+	* src/tgbatest/ltl2tgba.cc (main): More option to reduce
+	formula.
+	* src/tgbatest/spotlbtt.test: One more test.
+
 2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltlvisit/tostring.cc (to_spin_string_visitor,

src/ltlvisit/basereduc.cc

@@ -89,8 +89,8 @@ namespace spot
 	    /* X(f1 | GF(f2)) = X(f1) | GF(F2) */
 	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
 	      if (dynamic_cast<multop*>(result_)->size() == 2) {
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
+		if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
+		  //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
@@ -99,8 +99,8 @@ namespace spot
 		    spot::ltl::destroy(f);
 		    return;
 		  }
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
+		if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
+		  //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
@@ -137,8 +137,8 @@ namespace spot
 	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
 	      if (dynamic_cast<multop*>(result_)->op() == multop::And) {
 		if (dynamic_cast<multop*>(result_)->size() == 2) {
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
+		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
+		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
@@ -146,8 +146,8 @@ namespace spot
 		    result_ = multop::instance(multop::And, res);
 		    return;
 		  }
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
+		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
+		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
@@ -193,8 +193,8 @@ namespace spot
 	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
 	      if (dynamic_cast<multop*>(f)->op() == multop::Or) {
 		if (dynamic_cast<multop*>(result_)->size() == 2) {
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
+		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
+		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
@@ -202,8 +202,8 @@ namespace spot
 		    result_ = multop::instance(multop::Or, res);
 		    return;
 		  }
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
+		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		      is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
+		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
 		    multop::vec* res = new multop::vec;
 		    res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
 		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
@@ -450,7 +450,7 @@ namespace spot
 		  break;
 		}
 
-		/* GF(a) & GF(b) = GF(a & b)*/
+		/* GF(a) | GF(b) = GF(a | b)*/
 		if (is_GF(*i)) {
 		  tmpGF->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
 		  break;
@@ -553,8 +553,8 @@ namespace spot
 							      multop::instance(mo->op(),tmpGF))));
 	if (tmpFG != NULL)
 	  if (tmpFG->size())
-	    tmpOther->push_back(unop::instance(unop::G,
+	    tmpOther->push_back(unop::instance(unop::F,
-					       unop::instance(unop::F,
+					       unop::instance(unop::G,
 							      multop::instance(mo->op(),tmpFG))));
 
 	result_ = multop::instance(op, tmpOther);

src/ltlvisit/lunabbrev.cc

@@ -22,7 +22,7 @@
 #include "ltlast/allnodes.hh"
 #include "ltlvisit/clone.hh"
 #include "lunabbrev.hh"
-//#include "reducform.hh"
+#include "reducform.hh"
 #include <cassert>
 
 namespace spot
@@ -30,50 +30,6 @@ namespace spot
   namespace ltl
   {
 
-    class node_type_form_visitor : public const_visitor
-    {
-    public:
-      enum type { Atom, Const, Unop, Binop, Multop };
-      
-      node_type_form_visitor(){}
-      
-      type
-      result() const { return result_;}
-      
-      void
-      visit(const atomic_prop* ap){ 
-	if (ap == NULL);
-	result_ = node_type_form_visitor::Atom;
-      }
-      
-      void
-      visit(const constant* c){ 
-	if (c == NULL);
-	result_ = node_type_form_visitor::Const;
-      }
-      
-      void
-      visit(const unop* uo){
-	if (uo == NULL); 
-	result_ = node_type_form_visitor::Unop;
-      }
-      
-      void
-      visit(const binop* bo){ 
-	if (bo == NULL);
-	result_ = node_type_form_visitor::Binop;
-      }
-      
-      void
-      visit(const multop* mo){ 
-	if (mo == NULL);
-	result_ = node_type_form_visitor::Multop;
-      }
-      
-    protected:
-      type result_;
-    };
-    
     unabbreviate_logic_visitor::unabbreviate_logic_visitor()
     {
     }
@@ -82,38 +38,12 @@ namespace spot
     {
     }
 
-    /*
-    void
-    unabbreviate_logic_visitor::visit(unop* uo)
-    {
-      formula* f = uo->child();
-      switch (uo->op())
-	{
-	case unop::Not:
-	case unop::X:
-	  result_ = unop::instance(uo->op(),recurse(f));
-	  return;
-	case unop::F:
-	  result_ = binop::instance(binop::U,constant::true_instance(),recurse(f));
-	  return;
-	case unop::G:
-	  result_ = binop::instance(binop::R,constant::false_instance(),recurse(f));
-	  return;
-	}
-      // Unreachable code.
-      assert(0);
-    }
-    */
-
     void
     unabbreviate_logic_visitor::visit(binop* bo)
     {
       formula* f1 = recurse(bo->first());
       formula* f2 = recurse(bo->second());
 
-      node_type_form_visitor v;
-      const_cast<formula*>(f1)->accept(v);
-
       switch (bo->op())
 	{
 	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
@@ -145,7 +75,7 @@ namespace spot
 
 	  /* true U f2 == F(f2) */
 	case binop::U:
-	  if ( v.result() == node_type_form_visitor::Const )
+	  if ( node_type(f1) == node_type_form_visitor::Const )
 	    if ( ((constant*)f1)->val() == constant::True ) {
 	      result_ = unop::instance(unop::F,f2);
 	      return;
@@ -155,7 +85,7 @@ namespace spot
 
 	  /* false R f2 == G(f2) */
 	case binop::R:
-	  if ( v.result() == node_type_form_visitor::Const )
+	  if ( node_type(f1) == node_type_form_visitor::Const )
 	    if ( ((constant*)f1)->val() == constant::False ) {
 	      result_ = unop::instance(unop::G,f2);
 	      return;

src/tgbatest/ltl2tgba.cc

@@ -93,7 +93,15 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -y   do not merge states with same symbolic representation "
 	    << "(implies -f)" << std::endl
-	    << "  -z   to reduce formula "
+	    << "  -r1  to reduce formula using basic rewriting"
+	    << std::endl
+	    << "  -r2  to reduce formula using class of eventuality and "
+	    << "and universality"
+	    << std::endl
+	    << "  -r3  to reduce formula using implication between "
+	    << "two formula"
+	    << std::endl
+	    << "  -r4  to reduce formula using all rules"
 	    << std::endl;
   exit(2);
 }
@@ -116,7 +124,10 @@ main(int argc, char** argv)
   bool magic_many = false;
   bool expect_counter_example = false;
   bool from_file = false;
-  bool reduc = false;
+  bool reduc_r1 = false;
+  bool reduc_r2 = false;
+  bool reduc_r3 = false;
+  bool reduc_r4 = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
 
@@ -254,9 +265,25 @@ main(int argc, char** argv)
 	  fm_opt = true;
 	  fm_symb_merge_opt = false;
 	}
-      else if (!strcmp(argv[formula_index], "-z"))
+      else if (!strcmp(argv[formula_index], "-r1"))
 	{
-	  reduc = true;
+	  reduc_r1 = true;
+	}
+      else if (!strcmp(argv[formula_index], "-r2"))
+	{
+	  reduc_r2 = true;
+	}
+      else if (!strcmp(argv[formula_index], "-r3"))
+	{
+	  reduc_r3 = true;
+	}
+      else if (!strcmp(argv[formula_index], "-r4"))
+	{
+	  reduc_r4 = true;
+	}
+      else if (!strcmp(argv[formula_index], "-rd"))
+	{
+	  reduc_rd = true;
 	}
       else
 	{
@@ -322,8 +349,20 @@ main(int argc, char** argv)
 	{
 
 	  spot::ltl::formula* ftmp = f;
-	  if (reduc)
+	  if (reduc_r4)
 	    f = spot::ltl::reduce(f);
+	  else {
+	    if (reduc_r1 | reduc_r2 | reduc_r3) {
+	      spot::ltl::option o = spot::ltl::BRI;
+	      if (reduc_r1)
+		o = spot::ltl::Base;
+	      if (reduc_r2)
+		o = spot::ltl::EventualUniversal;
+	      if (reduc_r3)
+		o = spot::ltl::Inf;
+	      f = spot::ltl::reduce(f, o);
+	    }
+	  }
 
 	  if (fm_opt)
 	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
@@ -333,8 +372,9 @@ main(int argc, char** argv)
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 
-	  if (reduc)
+	  if (reduc_r1 || reduc_r2 || reduc_r3 || reduc_r4) {
 	    spot::ltl::destroy(ftmp);
+	  }
 	}
 
       spot::tgba_tba_proxy* degeneralized = 0;

src/tgbatest/spotlbtt.test

@@ -28,6 +28,13 @@ echo 'This test can take as long as 15 minutes on a 2GHz Pentium 4.'
 set -e
 
 cat > config <<EOF
+Algorithm
+{
+   Name = "Spot (Couvreur -- LaCIM), reduction of formula"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -r4 -F -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM)"