From f2f10852c6aacb72df63ca15d5e76ca8682f1b0b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 14 May 2004 14:09:01 +0000
Subject: [PATCH] * ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc:
 Fix style. * sanity/style.test: More tests.

---
 ChangeLog                 |   3 +
 src/ltltest/inf.cc        |  27 +--
 src/ltltest/reduc.cc      | 130 +++++++------
 src/ltlvisit/reducform.cc | 378 +++++++++++++++++++-------------------
 src/sanity/style.test     |  15 ++
 5 files changed, 292 insertions(+), 261 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 3273c660e..bfd13f923 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
+	* sanity/style.test: More tests.
+
 	* src/tgbatest/ltl2tgba.cc (main): Fix style.
 	* HACKING: Mention `else if'.
 
diff --git a/src/ltltest/inf.cc b/src/ltltest/inf.cc
index e9200d5a9..375d249f3 100644
--- a/src/ltltest/inf.cc
+++ b/src/ltltest/inf.cc
@@ -64,23 +64,26 @@ main(int argc, char** argv)
   int exit_return = 0;
 
   std::cout << "Test f1 < f2" << std::endl;
-  if (spot::ltl::inf_form(f1,f2)) {
-    std::cout << f1s << " < " << f2s << std::endl;
-    exit_return = 1;
-  }
+  if (spot::ltl::inf_form(f1, f2))
+    {
+      std::cout << f1s << " < " << f2s << std::endl;
+      exit_return = 1;
+    }
 
   /*
   std::cout << "Test !f1 < f2" << std::endl;
-  if (spot::ltl::infneg_form(f1,f2,0)) {
-    std::cout << "!(" << f1s << ") < " << f2s << std::endl;
-    exit_return = 2;
-  }
+  if (spot::ltl::infneg_form(f1, f2, 0))
+    {
+      std::cout << "!(" << f1s << ") < " << f2s << std::endl;
+      exit_return = 2;
+    }
 
   std::cout << "Test f1 < !f2" << std::endl;
-  if (spot::ltl::infneg_form(f1,f2,1)) {
-    std::cout << f1s << " < !(" << f2s << ")" << std::endl;
-    exit_return = 3;
-  }
+  if (spot::ltl::infneg_form(f1, f2, 1))
+    {
+      std::cout << f1s << " < !(" << f2s << ")" << std::endl;
+      exit_return = 3;
+    }
   */
 
   spot::ltl::dump(std::cout, f1); std::cout << std::endl;
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
index 665c31763..582581ad4 100644
--- a/src/ltltest/reduc.cc
+++ b/src/ltltest/reduc.cc
@@ -45,20 +45,22 @@ main(int argc, char** argv)
     syntax(argv[0]);
 
   spot::ltl::option o;
-  switch(atoi(argv[1])){
-  case 0:
-    o = spot::ltl::Base;
-    break;
-  case 1:
-    o = spot::ltl::Inf;
-    break;
-  case 2:
-    o = spot::ltl::EventualUniversal;
-    break;
-  case 3:
-    o = spot::ltl::BRI;
-    break;
-  default: return 2;
+  switch (atoi(argv[1]))
+    {
+    case 0:
+      o = spot::ltl::Base;
+      break;
+    case 1:
+      o = spot::ltl::Inf;
+      break;
+    case 2:
+      o = spot::ltl::EventualUniversal;
+      break;
+    case 3:
+      o = spot::ltl::BRI;
+      break;
+    default:
+      return 2;
   }
 
   spot::ltl::parse_error_list p1;
@@ -69,12 +71,13 @@ main(int argc, char** argv)
     return 2;
 
 
-  if (argc == 4){
-    spot::ltl::parse_error_list p2;
-    f2 = spot::ltl::parse(argv[3], p2);
-    if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
-      return 2;
-  }
+  if (argc == 4)
+    {
+      spot::ltl::parse_error_list p2;
+      f2 = spot::ltl::parse(argv[3], p2);
+      if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
+	return 2;
+    }
 
   int exit_code = 0;
 
@@ -93,7 +96,7 @@ main(int argc, char** argv)
   std::string f1s_before = spot::ltl::to_string(f1);
 
   ftmp1 = f1;
-  f1 = spot::ltl::reduce(f1,o);
+  f1 = spot::ltl::reduce(f1, o);
   ftmp2 = f1;
   f1 = spot::ltl::unabbreviate_logic(f1);
   spot::ltl::destroy(ftmp1);
@@ -103,51 +106,56 @@ main(int argc, char** argv)
   std::string f1s_after = spot::ltl::to_string(f1);
 
   bool red = (length_f1_after < length_f1_before);
-  if (red);
   std::string f2s = "";
-  if (f2 != NULL) {
-    ftmp1 = f2;
-    f2 = unabbreviate_logic(f2);
-    ftmp2 = f2;
-    f2 = negative_normal_form(f2);
-    spot::ltl::destroy(ftmp1);
-    spot::ltl::destroy(ftmp2);
-    ftmp1 = f2;
-    f2 = unabbreviate_logic(f2);
-    spot::ltl::destroy(ftmp1);
-    f2s = spot::ltl::to_string(f2);
-  }
+  if (f2 != NULL)
+    {
+      ftmp1 = f2;
+      f2 = unabbreviate_logic(f2);
+      ftmp2 = f2;
+      f2 = negative_normal_form(f2);
+      spot::ltl::destroy(ftmp1);
+      spot::ltl::destroy(ftmp2);
+      ftmp1 = f2;
+      f2 = unabbreviate_logic(f2);
+      spot::ltl::destroy(ftmp1);
+      f2s = spot::ltl::to_string(f2);
+    }
 
+  if (red && !f2)
+    {
+      std::cout << length_f1_before << " " << length_f1_after
+		<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
+		<< std::endl;
+    }
 
-  if (red && (f2 == NULL)) {
-    std::cout << length_f1_before << " " << length_f1_after
-	      << " '" << f1s_before << "' reduce to '" << f1s_after << "'"
-	      << std::endl;
-  }
-
-  if (f2 != NULL){
-    if (f1 != f2) {
+  if (f2)
+    {
+      if (f1 != f2)
+	{
+	  if (length_f1_after < length_f1_before)
+	    std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
+		      << " KOREDUC " << std::endl;
+	  else
+	    std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
+		      << " KOIDEM " << std::endl;
+	  exit_code = 1;
+	}
+      else
+	{
+	  if (f1s_before != f1s_after)
+	    std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
+		      << " OKREDUC " << std::endl;
+	  else
+	    std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
+		      << " OKIDEM" << std::endl;
+	  exit_code = 0;
+	}
+    }
+  else
+    {
       if (length_f1_after < length_f1_before)
-	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
-		  << " KOREDUC " << std::endl;
-      else
-	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
-		  << " KOIDEM " << std::endl;
-      exit_code = 1;
+	exit_code = 0;
     }
-    else {
-      if (f1s_before != f1s_after)
-	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
-		  << " OKREDUC " << std::endl;
-      else
-	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
-		  << " OKIDEM" << std::endl;
-      exit_code = 0;
-    }
-  }
-  else{
-    if (length_f1_after < length_f1_before) exit_code = 0;
-  }
 
   spot::ltl::destroy(f1);
   if (f2 != NULL)
diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc
index bed16b20c..aefd51fb1 100644
--- a/src/ltlvisit/reducform.cc
+++ b/src/ltlvisit/reducform.cc
@@ -90,17 +90,15 @@ namespace spot
 	    return;
 
 	  case unop::F:
-	    /* if f is class of eventuality then F(f)=f */
-	    if (!is_eventual(result_) || (o == Inf)) {
+	    /* If f is class of eventuality then F(f)=f.  */
+	    if (!is_eventual(result_) || (o == Inf))
 	      result_ = unop::instance(unop::F, result_);
-	    }
 	    return;
 
 	  case unop::G:
-	    /* if f is class of universality then G(f)=f */
-	    if (!is_universal(result_) || (o == Inf)) {
+	    /* If f is class of universality then G(f)=f.  */
+	    if (!is_universal(result_) || (o == Inf))
 	      result_ = unop::instance(unop::G, result_);
-	    }
 	    return;
 	  }
 	/* Unreachable code.  */
@@ -112,86 +110,86 @@ namespace spot
       {
 	formula* f2 = recurse(bo->second());
 
-	/* if b is of class eventuality then a U b = b
-	   if b is of class universality then a R b = b */
-	if (o != Inf) {
-	  if ((is_eventual(f2) && ((bo->op()) == binop::U)) ||
-	      (is_universal(f2) && ((bo->op()) == binop::R)))
-	    {
-	      result_ = f2;
-	      return;
-	    }
-	}
+	/* If b is of class eventuality then a U b = b.
+	   If b is of class universality then a R b = b. */
+	if ((o != Inf)
+	    && ((is_eventual(f2) && ((bo->op()) == binop::U))
+		|| (is_universal(f2) && ((bo->op()) == binop::R))))
+	  {
+	    result_ = f2;
+	    return;
+	  }
 	/* case of implies */
 	formula* f1 = recurse(bo->first());
 
-	if (o != EventualUniversal) {
-	  bool inf = inf_form(f1,f2);
-	  bool infinv = inf_form(f2,f1);
-	  bool infnegleft = infneg_form(f2,f1,0);
-	  bool infnegright = infneg_form(f2,f1,1);
+	if (o != EventualUniversal)
+	  {
+	    bool inf = inf_form(f1, f2);
+	    bool infinv = inf_form(f2, f1);
+	    bool infnegleft = infneg_form(f2, f1, 0);
+	    bool infnegright = infneg_form(f2, f1, 1);
 
-	  switch (bo->op())
-	    {
-	    case binop::Xor:
-	    case binop::Equiv:
-	    case binop::Implies:
-	      break;;
+	    switch (bo->op())
+	      {
+	      case binop::Xor:
+	      case binop::Equiv:
+	      case binop::Implies:
+		break;;
 
-	    case binop::U:
-	      /* a < b => a U b = b */
-	      if (inf)
-		{
-		  result_ = f2;
-		  spot::ltl::destroy(f1);
-		  return;
-		}
-	      /* !b < a => a U b = Fb */
-	      if (infnegleft)
-		{
-		  result_ = unop::instance(unop::F, f2);
-		  spot::ltl::destroy(f1);
-		  return;
-		}
-	      /* a < b => a U (b U c) = (b U c) */
-	      if (node_type(f2) == node_type_form_visitor::Binop)
-		if (dynamic_cast<binop*>(f2)->op() == binop::U)
-		  if (inf_form(f1,dynamic_cast<binop*>(f2)->first()))
-		    {
-		      result_ = f2;
-		      spot::ltl::destroy(f1);
-		      return;
-		    }
-	      break;
+	      case binop::U:
+		/* a < b => a U b = b */
+		if (inf)
+		  {
+		    result_ = f2;
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		/* !b < a => a U b = Fb */
+		if (infnegleft)
+		  {
+		    result_ = unop::instance(unop::F, f2);
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		/* a < b => a U (b U c) = (b U c) */
+		if (node_type(f2) == node_type_form_visitor::Binop
+		    && dynamic_cast<binop*>(f2)->op() == binop::U
+		    && inf_form(f1, dynamic_cast<binop*>(f2)->first()))
+		  {
+		    result_ = f2;
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		break;
 
-	    case binop::R:
-	      /* b < a => a R b = b */
-	      if (infinv)
-		{
-		  result_ = f2;
-		  spot::ltl::destroy(f1);
-		  return;
-		}
-	      /* b < !a => a R b = Gb */
-	      if (infnegright)
-		{
-		  result_ = unop::instance(unop::G, f2);
-		  spot::ltl::destroy(f1);
-		  return;
-		}
-	      /* b < a => a R (b R c) = b R c */
-	      if (node_type(f2) == node_type_form_visitor::Binop)
-		if (dynamic_cast<binop*>(f2)->op() == binop::R)
-		  if (inf_form(dynamic_cast<binop*>(f2)->first(),f1))
-		    {
-		      result_ = f2;
-		      spot::ltl::destroy(f1);
-		      return;
-		    }
-	      break;
+	      case binop::R:
+		/* b < a => a R b = b */
+		if (infinv)
+		  {
+		    result_ = f2;
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		/* b < !a => a R b = Gb */
+		if (infnegright)
+		  {
+		    result_ = unop::instance(unop::G, f2);
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		/* b < a => a R (b R c) = b R c */
+		if (node_type(f2) == node_type_form_visitor::Binop
+		    && dynamic_cast<binop*>(f2)->op() == binop::R
+		    && inf_form(dynamic_cast<binop*>(f2)->first(), f1))
+		  {
+		    result_ = f2;
+		    spot::ltl::destroy(f1);
+		    return;
+		  }
+		break;
 
-	    }
-	}
+	      }
+	  }
 	result_ = binop::instance(bo->op(), f1, f2);
       }
 
@@ -208,97 +206,98 @@ namespace spot
 	for (unsigned i = 0; i < mos; ++i)
 	  res->push_back(recurse(mo->nth(i)));
 
-	if (o != EventualUniversal){
-	  switch (mo->op())
-	    {
+	if (o != EventualUniversal)
+	  {
+	    switch (mo->op())
+	      {
 
-	    case multop::Or:
-	      index = indextmp = res->begin();
-	      if (index != res->end())
-		{
-		  f1 = *index;
-		  index++;
-		}
-	      for (; index != res->end();index++)
-		{
-		  f2 = *index;
-		  /* a < b => a + b = b */
-		  if (inf_form(f1,f2)) // f1 < f2
-		    {
-		      f1 = f2;
-		      spot::ltl::destroy(*indextmp);
-		      res->erase(indextmp);
-		      indextmp = index;
-		      index--;
-		    }
-		  else if (inf_form(f2,f1)) // f2 < f1
-		    {
-		      spot::ltl::destroy(*index);
-		      res->erase(index);
-		      index--;
-		    }
-		}
-	      break;
-
-	    case multop::And:
-	      index = indextmp = res->begin();
-	      if (mos)
-		{
-		  f1 = mo->nth(0);
-		  index++;
-		}
-	      for (; index != res->end(); index++)
-		{
-		  f2 = *index;
-		  /* a < b => a & b = a */
-		  if (inf_form(f1,f2)) // f1 < f2
-		    {
-		      spot::ltl::destroy(*index);
-		      res->erase(index);
-		      index--;
-		    }
-		  else if (inf_form(f2,f1)) // f2 < f1
-		    {
-		      f1 = f2;
-		      spot::ltl::destroy(*indextmp);
-		      res->erase(indextmp);
-		      indextmp = index;
-		      index--;
-		    }
-		}
-	      break;
-	    }
-
-	  /* f1 < !f2 => f1 & f2 = false
-	     !f1 < f2 => f1 | f2 = true */
-	  for (index = res->begin(); index != res->end(); index++) {
-	    for (indextmp = res->begin(); indextmp != res->end(); indextmp++) {
-	      if (index != indextmp){
-		if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) {
-		  for (multop::vec::iterator j = res->begin(); j != res->end(); j++) {
-		    spot::ltl::destroy(*j);
+	      case multop::Or:
+		index = indextmp = res->begin();
+		if (index != res->end())
+		  {
+		    f1 = *index;
+		    index++;
 		  }
-		  if (mo->op() == multop::Or)
-		    result_ = constant::true_instance();
-		  else
-		    result_ = constant::false_instance();
-		  return;
-		}
+		for (; index != res->end();index++)
+		  {
+		    f2 = *index;
+		    /* a < b => a + b = b */
+		    if (inf_form(f1, f2)) // f1 < f2
+		      {
+			f1 = f2;
+			spot::ltl::destroy(*indextmp);
+			res->erase(indextmp);
+			indextmp = index;
+			index--;
+		      }
+		    else if (inf_form(f2, f1)) // f2 < f1
+		      {
+			spot::ltl::destroy(*index);
+			res->erase(index);
+			index--;
+		      }
+		  }
+		break;
+
+	      case multop::And:
+		index = indextmp = res->begin();
+		if (mos)
+		  {
+		    f1 = mo->nth(0);
+		    index++;
+		  }
+		for (; index != res->end(); index++)
+		  {
+		    f2 = *index;
+		    /* a < b => a & b = a */
+		    if (inf_form(f1, f2)) // f1 < f2
+		      {
+			spot::ltl::destroy(*index);
+			res->erase(index);
+			index--;
+		      }
+		    else if (inf_form(f2, f1)) // f2 < f1
+		      {
+			f1 = f2;
+			spot::ltl::destroy(*indextmp);
+			res->erase(indextmp);
+			indextmp = index;
+			index--;
+		      }
+		  }
+		break;
 	      }
-	    }
+
+	    /* f1 < !f2 => f1 & f2 = false
+	       !f1 < f2 => f1 | f2 = true */
+	    for (index = res->begin(); index != res->end(); index++)
+	      for (indextmp = res->begin(); indextmp != res->end(); indextmp++)
+		if (index != indextmp
+		    && infneg_form(*index,*indextmp,
+				   (mo->op() == multop::Or) ? 0 : 1))
+		  {
+		    for (multop::vec::iterator j = res->begin();
+			 j != res->end(); j++)
+		      spot::ltl::destroy(*j);
+		    if (mo->op() == multop::Or)
+		      result_ = constant::true_instance();
+		    else
+		      result_ = constant::false_instance();
+		    return;
+		  }
+	  }
+	if (res->size())
+	  {
+	    result_ = multop::instance(mo->op(), res);
+	    return;
 	  }
-	}
-	if (res->size()) {
-	  result_ = multop::instance(mo->op(),res);
-	  return;
-	}
 	assert(0);
       }
 
       formula*
       recurse(formula* f)
       {
-	return reduce_form(f,o);
+	return reduce_form(f, o);
       }
 
     protected:
@@ -313,19 +312,21 @@ namespace spot
       spot::ltl::formula* ftmp2 = NULL;
       reduce_form_visitor v(o);
 
-      if (o == BRI) {
-	ftmp1 = spot::ltl::basic_reduce_form(f);
-	const_cast<formula*>(ftmp1)->accept(v);
-	ftmp2 = spot::ltl::basic_reduce_form(v.result());
-	spot::ltl::destroy(ftmp1);
-	spot::ltl::destroy(v.result());
+      if (o == BRI)
+	{
+	  ftmp1 = spot::ltl::basic_reduce_form(f);
+	  const_cast<formula*>(ftmp1)->accept(v);
+	  ftmp2 = spot::ltl::basic_reduce_form(v.result());
+	  spot::ltl::destroy(ftmp1);
+	  spot::ltl::destroy(v.result());
 
-	return ftmp2;
-      }
-      else {
-	const_cast<formula*>(f)->accept(v);
-	return v.result();
-      }
+	  return ftmp2;
+	}
+      else
+	{
+	  const_cast<formula*>(f)->accept(v);
+	  return v.result();
+	}
 
       /* unreachable code */
       assert(0);
@@ -341,22 +342,23 @@ namespace spot
       ftmp1 = spot::ltl::unabbreviate_logic(f);
       ftmp2 = spot::ltl::negative_normal_form(ftmp1);
 
-      switch (o) {
-      case Base:
-	ftmp3 = spot::ltl::basic_reduce_form(ftmp2);
-	break;
-      case Inf:
-	ftmp3 = spot::ltl::reduce_form(ftmp2,o);
-	break;
-      case EventualUniversal:
-	ftmp3 = spot::ltl::reduce_form(ftmp2,o);
-	break;
-      case BRI:
-	ftmp3 = spot::ltl::reduce_form(ftmp2);
-	break;
-      default:
-	assert(0);
-      }
+      switch (o)
+	{
+	case Base:
+	  ftmp3 = spot::ltl::basic_reduce_form(ftmp2);
+	  break;
+	case Inf:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
+	  break;
+	case EventualUniversal:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
+	  break;
+	case BRI:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2);
+	  break;
+	default:
+	  assert(0);
+	}
       spot::ltl::destroy(ftmp1);
       spot::ltl::destroy(ftmp2);
 
diff --git a/src/sanity/style.test b/src/sanity/style.test
index d0450e416..e36995b05 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -39,18 +39,27 @@ while read file; do
    grep '[	 ]if (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
+   grep '[	 ]if (.*).*;' $tmp &&
+     diag 'if body should be on another line.'
+
    grep '[	 ]while(' $tmp &&
      diag 'Missing space after "while"'
 
    grep '[	 ]while (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
+   grep '[	 ]while (.*).*[^)];' $tmp &&
+     diag 'while body should be on another line.'
+
    grep '[	 ]for(' $tmp &&
      diag 'Missing space after "for"'
 
    grep '[	 ]for (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
+   grep '[	 ]for (.*;.*;.*).*;' $tmp &&
+     diag 'for body should be on another line.'
+
    grep '[	 ]switch(' $tmp &&
      diag 'Missing space after "switch"'
 
@@ -75,6 +84,12 @@ while read file; do
    grep '[^	 ]||[^	 ]' $tmp &&
      diag 'Space arround binary operators.'
 
+   grep '[	 ]default:[^:].*;' $tmp &&
+     diag 'Label should be on their own line.'
+
+   grep '[	 ]case.*:[^:].*;' $tmp &&
+     diag 'Label should be on their own line.'
+
    $fail && echo "$file" >>failures
 done