simplify: fix 3 incorrect simplification rules

* src/ltlvisit/simplify.cc: Remove two incorrect rules, and
partially disable another one.
* doc/tl/tl.tex: Reflect the change.
* src/ltltest/reduccmp.test: Likewise.
* src/ltltest/equals.cc: Add safety checks to catch such errors in the
future.
* NEWS: Mention the bug.

NEWS

@@ -14,6 +14,9 @@ New in spot 1.2.3a (not yet released)
     - "ltl2tgta --ta" could crash in certain conditions due to the
       introduction of a simulation-based reduction after
       degeneralization.
+    - Fix three incorrect simplifications rules, all related to the
+      factorization of Boolean subformulas in operands of the
+      non-length-matching "&" SERE operator.
 
 New in spot 1.2.3 (2014-02-11)
 

doc/tl/tl.tex

@@ -1460,13 +1460,11 @@ SERE.
     \0 &\text{else}\\
   \end{cases}\\
   \sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} &
-  \sere{b_1\CONCAT r_1}\AND   \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND    r_2} \\
+  \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} \\
   \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} &
-  \sere{b_1\FUSION r_1}\AND   \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND    r_2} \\
+  \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\
-  \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} &
+  \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
-  \sere{r_1\CONCAT b_1}\AND   \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND    b_2} \\
+  \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}\\
-  \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} &
-  \sere{r_1\FUSION b_1}\AND   \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND    b_2} \\
 \end{align*}
 
 Starred subformul\ae{} are rewritten in Star Normal

src/ltltest/equals.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
-// et Développement de l'Epita (LRDE).
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -68,7 +68,7 @@ main(int argc, char** argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
 
-  int exit_code;
+  int exit_code = 0;
 
   {
 #if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
@@ -112,6 +112,14 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
@@ -124,6 +132,14 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
@@ -136,13 +152,21 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
     std::cout << std::endl;
 #endif
 
-    exit_code = f1 != f2;
+    exit_code |= f1 != f2;
 
 #if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
     spot::ltl::ltl_simplifier simp;
@@ -150,8 +174,11 @@ main(int argc, char** argv)
 
     if (!simp.are_equivalent(f1, f2))
       {
-	std::cerr << "Source and destination formulae are not equivalent!"
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
-		  << std::endl;
+	std::cerr << "Source and destination formulae are not equivalent!\n";
+#else
+	std::cerr << "Simpl. and destination formulae are not equivalent!\n";
+#endif
 	exit_code = 1;
       }
 

src/ltltest/reduccmp.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
-# et Developpement de l'Epita (LRDE).
+# Recherche et Developpement de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -317,9 +317,10 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
               '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
      run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
-     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
+     run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
-     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
+     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
-     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
+     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced
+     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced
      run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
               '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
      run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'

src/ltlvisit/simplify.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -3456,22 +3456,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail1->push_back(f->all_but(0));
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail1->push_back(multop::instance(op, tail));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
 				head2->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail2->push_back(f->all_but(0));
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail2->push_back(multop::instance(op, tail));
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -3535,20 +3527,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				tail3->push_back(t->clone());
-				multop::vec* head = new multop::vec;
+				head3->push_back(f->all_but(s));
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head3->push_back(multop::instance(op, head));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
 				tail4->push_back(t->clone());
-				multop::vec* head = new multop::vec;
+				head4->push_back(f->all_but(s));
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head4->push_back(multop::instance(op, head));
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -4155,6 +4141,8 @@ namespace spot
 			//                    head1   tail1
 			// {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2}
 			//                    head2   tail2
+			// BEWARE: The second rule is correct only when
+			// both r1 and r2 do not accept [*0].
 
 			multop::vec* head1 = new multop::vec;
 			multop::vec* tail1 = new multop::vec;
@@ -4175,22 +4163,20 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail1->push_back(f->all_but(0));
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail1->push_back(multop::instance(op, tail));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
+				const formula* t = f->all_but(0);
+				if (t->accepts_eword())
+				  {
+				    t->destroy();
+				    continue;
+				  }
 				head2->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail2->push_back(t);
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail2->push_back(multop::instance(op, tail));
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -4230,83 +4216,6 @@ namespace spot
 			    delete tail2;
 			  }
 
-			// {r1;b1}&{r2;b2} = {r1&r2};{b1∧b2}
-			//                    head3   tail3
-			// {r1:b1}&{r2:b2} = {r1&r2}:{b1∧b2}
-			//                    head4   tail4
-			multop::vec* head3 = new multop::vec;
-			multop::vec* tail3 = new multop::vec;
-			multop::vec* head4 = new multop::vec;
-			multop::vec* tail4 = new multop::vec;
-			for (multop::vec::iterator i = s.res_other->begin();
-			     i != s.res_other->end(); ++i)
-			  {
-			    if (!*i)
-			      continue;
-			    if ((*i)->kind() != formula::MultOp)
-			      continue;
-			    const multop* f = down_cast<const multop*>(*i);
-			    unsigned s = f->size() - 1;
-			    const formula* t = f->nth(s);
-			    if (!t->is_boolean())
-			      continue;
-			    multop::type op = f->op();
-			    if (op == multop::Concat)
-			      {
-				tail3->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head3->push_back(multop::instance(op, head));
-				(*i)->destroy();
-				*i = 0;
-			      }
-			    else if (op == multop::Fusion)
-			      {
-				tail4->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head4->push_back(multop::instance(op, head));
-				(*i)->destroy();
-				*i = 0;
-			      }
-			    else
-			      {
-				continue;
-			      }
-			  }
-			if (!head3->empty())
-			  {
-			    const formula* h =
-			      multop::instance(multop::AndNLM, head3);
-			    const formula* t =
-			      multop::instance(multop::And, tail3);
-			    const formula* f =
-			      multop::instance(multop::Concat, h, t);
-			    s.res_other->push_back(f);
-			  }
-			else
-			  {
-			    delete head3;
-			    delete tail3;
-			  }
-			if (!head4->empty())
-			  {
-			    const formula* h =
-			      multop::instance(multop::AndNLM, head4);
-			    const formula* t =
-			      multop::instance(multop::And, tail4);
-			    const formula* f =
-			      multop::instance(multop::Fusion, h, t);
-			    s.res_other->push_back(f);
-			  }
-			else
-			  {
-			    delete head4;
-			    delete tail4;
-			  }
-
 			result_ = multop::instance(multop::AndNLM, s.res_other);
 			// If we altered the formula in some way, process
 			// it another time.