* src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions)

Compute all_accepting_conditions_ from neg_accepting_conditions_,
not by browsing the dictionary.  The dictionary also contains
accepting conditions from other automata...  This bug was a
consequence of the change from 2003-07-14.
* src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not
browse the dictionary to print accepting conditions.  Call
->all_accepting_conditions() instead.
* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo
from 2003-08-22 in the computation of all_accepting_conditions_.
* src/tgbatest/explpro3.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add explpro3.test.
* src/tgbatest/explprod.test, src/tgbatest/explpro2.test,
 src/tgbatest/tripprod.test: Sort the output using Perl.

ChangeLog

@@ -1,3 +1,20 @@
+2003-08-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions)
+	Compute all_accepting_conditions_ from neg_accepting_conditions_,
+	not by browsing the dictionary.  The dictionary also contains
+	accepting conditions from other automata...  This bug was a
+	consequence of the change from 2003-07-14.
+	* src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not
+	browse the dictionary to print accepting conditions.  Call
+	->all_accepting_conditions() instead.
+	* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo
+	from 2003-08-22 in the computation of all_accepting_conditions_.
+	* src/tgbatest/explpro3.test: New file.
+	* src/tgbatest/Makefile.am (TESTS): Add explpro3.test.
+	* src/tgbatest/explprod.test, src/tgbatest/explpro2.test,
+	 src/tgbatest/tripprod.test: Sort the output using Perl.
+
 2003-08-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	Rewrite all std::map<const formula*, ...> as
@@ -413,7 +430,7 @@
 	* iface/gspn/gspn.cc (EVENT_TRUE): Undefine.
 	(tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes.
 	* iface/gspn/dottygspn.cc (main): Destroy the automaton before
-	its dictionnary.
+	its dictionary.
 
 2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 

src/tgba/tgbaexplicit.cc

@@ -307,11 +307,22 @@ namespace spot
     if (!all_accepting_conditions_computed_)
       {
 	bdd all = bddfalse;
-	bdd_dict::fv_map::const_iterator i;
-	for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i)
+
+	// Build all_accepting_conditions_ from neg_accepting_conditions_
+	// I.e., transform !A & !B & !C into
+	//        A & !B & !C
+	//     + !A &  B & !C
+	//     + !A & !B &  C
+	bdd cur = neg_accepting_conditions_;
+	while (cur != bddtrue)
 	  {
-	    bdd v = bdd_ithvar(i->second);
+	    assert(cur != bddfalse);
+
+	    bdd v = bdd_ithvar(bdd_var(cur));
 	    all |= v & bdd_exist(neg_accepting_conditions_, v);
+
+	    assert(bdd_high(cur) != bddtrue);
+	    cur = bdd_low(cur);
 	  }
 	all_accepting_conditions_ = all;
 	all_accepting_conditions_computed_ = true;

src/tgba/tgbaproduct.cc

@@ -154,9 +154,9 @@ namespace spot
     right_acc_complement_ = bdd_exist(rna, bdd_support(lna));
 
     all_accepting_conditions_ = ((left_->all_accepting_conditions()
-				  & left_acc_complement_)
+				  & right_acc_complement_)
 				 | (right_->all_accepting_conditions()
-				    & right_acc_complement_));
+				    & left_acc_complement_));
     neg_accepting_conditions_ = lna & rna;
 
     dict_->register_all_variables_of(&left_, this);

src/tgbaalgos/save.cc

@@ -20,11 +20,29 @@ namespace spot
     {
       const bdd_dict* d = automata_->get_dict();
       os_ << "acc =";
-      for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin();
-	   ai != d->acc_map.end(); ++ai)
+
+      bdd acc = automata_->all_accepting_conditions();
+      while (acc != bddfalse)
 	{
-	  os_ << " \"";
-	  ltl::to_string(ai->first, os_) << "\"";
+	  bdd cube = bdd_satone(acc);
+	  acc -= cube;
+	  while (cube != bddtrue)
+	    {
+	      assert(cube != bddfalse);
+	      // Display the first variable that is positive.
+	      // There should be only one per satisfaction.
+	      if (bdd_high(cube) != bddfalse)
+		{
+		  int v = bdd_var(cube);
+		  bdd_dict::vf_map::const_iterator vi =
+		    d->acc_formula_map.find(v);
+		  assert(vi != d->acc_formula_map.end());
+		  os_ << " \"";
+		  ltl::to_string(vi->second, os_) << "\"";
+		  break;
+		}
+	      cube = bdd_low(cube);
+	    }
 	}
       os_ << ";" << std::endl;
     }
@@ -37,7 +55,7 @@ namespace spot
       for (si->first(); !si->done(); si->next())
 	{
 	  state* dest = si->current_state();
-	  os_ << "\"" << cur << "\", \"" 
+	  os_ << "\"" << cur << "\", \""
 	      << automata_->format_state(dest) << "\", ";
 	  bdd_print_sat(os_, d, si->current_condition()) << ",";
 	  bdd_print_acc(os_, d, si->current_accepting_conditions());

src/tgbatest/Makefile.am

@@ -39,6 +39,7 @@ TESTS = \
   bddprod.test \
   explprod.test \
   explpro2.test \
+  explpro3.test \
   tripprod.test \
   mixprod.test \
   ltlmagic.test \

src/tgbatest/explpro2.test

@@ -18,16 +18,16 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3";
-"s1 * s1", "s2 * s2", ! a b, "p1" "p2";
-"s1 * s1", "s3 * s3", a ! b, "p2" "p3";
+"s1 * s1", "s2 * s2", ! a b,  "p1" "p2";
+"s1 * s1", "s3 * s3", a ! b,  "p2" "p3";
 EOF
 
 ./explprod input1 input2 > stdout
 
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
-sed 's/c a/a c/g;s/b a/a b/g;s/"p3" "p2"/"p2" "p3"/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
-  mv tmp_ stdout
+perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g' \
+  stdout > tmp_ && mv tmp_ stdout
 
 cat stdout
 diff stdout expected

src/tgbatest/explpro3.test

@@ -0,0 +1,33 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+cat >input1 <<EOF
+acc = ;
+s1, s2, !a,;
+s1, s3, !b,;
+EOF
+
+cat >input2 <<EOF
+acc = p2 p3;
+s1, s2, b, p2;
+s1, s3, a, p3;
+EOF
+
+cat >expected <<EOF
+acc = "p2" "p3";
+"s1 * s1", "s2 * s2", ! a b, "p2";
+"s1 * s1", "s3 * s3", a ! b, "p3";
+EOF
+
+./explprod input1 input2 > stdout
+
+# Sort out some possible inversions in the output.
+# (The order is not guaranteed by SPOT.)
+sed 's/"p3" "p2"/"p2" "p3"/g' stdout > tmp_ && mv tmp_ stdout
+
+cat stdout
+diff stdout expected
+rm input1 input2 stdout expected

src/tgbatest/explprod.test

@@ -20,17 +20,16 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3";
-"s1 * s1", "s3 * s2", a b, "p1" "p2";
-"s1 * s1", "s2 * s2", b, "p1" "p2";
-"s2 * s2", "s3 * s1", a c, "p1" "p3";
+"s1 * s1", "s3 * s2", a b,  "p1" "p2";
+"s1 * s1", "s2 * s2", b,  "p1" "p2";
+"s2 * s2", "s3 * s1", a c,  "p1" "p3";
 EOF
 
 ./explprod input1 input2 > stdout
-
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
-sed 's/c a/a c/g;s/b a/a b/g;s/"p3" "p1"/"p1" "p3"/g;s/"p3" "p2"/"p2" "p3"/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
-  mv tmp_ stdout
+perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g' \
+  stdout > tmp_ && mv tmp_ stdout
 
 cat stdout
 diff stdout expected

src/tgbatest/tripprod.test

@@ -28,25 +28,20 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3" "p4";
-"s1 * s1 * s1", "s3 * s2 * s2", a b, "p1" "p2";
-"s1 * s1 * s1", "s2 * s2 * s2", a b, "p1" "p2";
-"s1 * s1 * s1", "s3 * s2 * s3", a b, "p1" "p2";
-"s1 * s1 * s1", "s2 * s2 * s3", b, "p1" "p2";
-"s2 * s2 * s2", "s3 * s1 * s3", a c, "p3" "p4";
-"s2 * s2 * s3", "s3 * s1 * s2", a c, "p3" "p4";
+"s1 * s1 * s1", "s3 * s2 * s2", a b,   "p1" "p2";
+"s1 * s1 * s1", "s2 * s2 * s2", a b,   "p1" "p2";
+"s1 * s1 * s1", "s3 * s2 * s3", a b,   "p1" "p2";
+"s1 * s1 * s1", "s2 * s2 * s3", b,   "p1" "p2";
+"s2 * s2 * s2", "s3 * s1 * s3", a c,   "p3" "p4";
+"s2 * s2 * s3", "s3 * s1 * s2", a c,   "p3" "p4";
 EOF
 
 ./tripprod input1 input2 input3 > stdout
 
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
-sed 's/c a/a c/g;s/b a/a b/g;
-     s/"p4" "p1"/"p1" "p4"/g;
-     s/"p3" "p1"/"p1" "p3"/g;
-     s/"p2" "p1"/"p1" "p2"/g;
-     s/"p4" "p2"/"p2" "p4"/g;
-     s/"p3" "p2"/"p2" "p3"/g;
-     s/"p4" "p3"/"p3" "p4"/g' stdout > tmp_ &&
+perl -pe 's/c a/a c/g;s/b a/a b/g;s/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1, $2, $3, $4]}/g' \
+  stdout > tmp_ &&
   mv tmp_ stdout
 
 cat stdout