dbacomp: connect only back-links and generalize to tgba

* src/tgbaalgos/dbacomp.cc: Here.
* src/tgbaalgos/dbacomp.hh: Adjust documentation.
* src/tgbatest/dbacomp.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* src/tgbatest/det.test: Update.

src/tgbaalgos/dbacomp.cc

@@ -26,38 +26,33 @@ namespace spot
 
   namespace
   {
-    class dbacomp_iter: public tgba_reachable_iterator_depth_first
+    class dbacomp_iter: public tgba_reachable_iterator_depth_first_stack
     {
       bdd orig_acc_;
+      bdd all_neg_;
       bdd acc_;
       bdd_dict* dict_;
       tgba_explicit_number* out_;
+      int num_acc_;
+
       typedef state_explicit_number::transition trans;
     public:
       dbacomp_iter(const tgba* a)
-	: tgba_reachable_iterator_depth_first(a),
+	: tgba_reachable_iterator_depth_first_stack(a),
 	  dict_(a->get_dict()),
 	  out_(new tgba_explicit_number(dict_))
       {
 	dict_->register_all_variables_of(a, out_);
-	unsigned c = a->number_of_acceptance_conditions();
 	orig_acc_ = a->all_acceptance_conditions();
-	if (c == 1)
+	all_neg_ = a->neg_acceptance_conditions();
-	  {
+	num_acc_ =  a->number_of_acceptance_conditions();
-	    out_->copy_acceptance_conditions_of(a);
+
-	    acc_ = orig_acc_;
+	// Register one acceptance condition for the result.
-	  }
-	else
-	  {
-	    // If there is no acceptance conditions in the original
-	    // automaton, add one.
-	    assert(c == 0);
 	int accvar = dict_->register_acceptance_variable
 	  (ltl::constant::true_instance(), out_);
 	acc_ = bdd_ithvar(accvar);
 	out_->set_acceptance_conditions(acc_);
       }
-      }
 
       tgba_explicit_number*
       result()
@@ -106,20 +101,62 @@ namespace spot
 	trans* t1 = out_->create_transition(in, out);
 	t1->condition = si->current_condition();
 
-	// Negative states encode a copy of the automaton in which all
+	// Negative states encode NUM_ACC_ copies of the automaton.
-	// accepting transitions have been removed, and all the
+	// In each copy transitions labeled by one of the acceptance
-	// remaining transitions are now accepting.
+	// set have been removed, and all the remaining transitions
+	// are now accepting.
+	// For each state S, we have NUM_ACC_ additional copies
+	// labeled S*-NUM_ACC, S*-NUM_ACC+1, ... S*-NUM_ACC+(NUM_ACC-1),
 	if (a != orig_acc_)
 	  {
-	    trans* t2 = out_->create_transition(-in, -out);
+	    bool backlink = on_stack(out);
+	    int add = 0;
+	    if (a == bddfalse)
+	      a = all_neg_;
+	    // Iterate over all the acceptance conditions in 'a'.
+	    bdd ac = a;
+	    while (ac != bddtrue)
+	      {
+		bdd h = bdd_high(ac);
+		if (h == bddfalse)
+		  {
+		    trans* t2 = out_->create_transition(in * -num_acc_ + add,
+							out * -num_acc_ + add);
 		    t2->condition = si->current_condition();
 		    t2->acceptance_conditions = acc_;
-	  }
 
-	// A non-deterministic transition between the two copies.
+		    if (backlink)
-	trans* t3 = out_->create_transition(in, -out);
+		      {
+			// Since we are closing a cycle, add
+			// a non-deterministic transition from
+			// the original automaton to this copy.
+			trans* t3 =
+			  out_->create_transition(in, out * -num_acc_ + add);
 			t3->condition = si->current_condition();
 		      }
+		    ac = bdd_low(ac);
+		  }
+		else
+		  {
+		    // We know that only one variable can be positive
+		    // on any branch, so since we have just seen such
+		    // a variable, we want to go to explore its LOW
+		    // branch for more positive variables.  The only
+		    // case where we will not do that is if the LOW
+		    // branch is false.  In that case we take the HIGH
+		    // branch to enumerate all the remaining negated
+		    // variables.
+		    bdd tmp = bdd_low(ac);
+		    if (tmp != bddfalse)
+		      ac = tmp;
+		    else
+		      ac = h;
+		  }
+		++add;
+	      }
+	    assert(add == num_acc_);
+	  }
+      }
 
     };
 

src/tgbaalgos/dbacomp.hh

@@ -24,13 +24,11 @@
 
 namespace spot
 {
-
+  /// \brief Complement a deterministic Büchi automaton
-
-  /// Complement a deterministic Büchi automaton
   ///
-  /// The automaton \a aut should be deterministic and should have at
+  /// The automaton \a aut should be deterministic.  It does no need
-  /// most a single acceptance condition.  It can be transition-based,
+  /// to be complete.  Acceptance can be transition-based, or
-  /// or state-based.  The resulting automaton is very unlikely to be
+  /// state-based.  The resulting automaton is very unlikely to be
   /// deterministic.
   SPOT_API tgba_explicit_number*
   dba_complement(const tgba* aut);

src/tgbatest/Makefile.am

@@ -107,6 +107,7 @@ TESTS = \
   lbttparse.test \
   scc.test \
   sccsimpl.test \
+  dbacomp.test \
   obligation.test \
   wdba.test \
   wdba2.test \

src/tgbatest/dbacomp.test

@@ -0,0 +1,46 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
+#
+# 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+# This automaton used to trigger a bug in the complementation: its
+# intersection with the complement was not empty!
+cat >input.tgba <<EOF
+acc = "a" "b" "c";
+"1", "1", "(a & d) | (a & b)", "b" "c";
+"1", "2", "a & !d & !c & !b",;
+"1", "1", "(d & !a) | (b & !a)", "a" "b" "c";
+"1", "2", "!a & !d & !c & !b", "a";
+"2", "1", "a & c & b", "b" "c";
+"2", "3", "a & b & !c", "b";
+"2", "2", "a & !c & !b",;
+"2", "1", "c & b & !a", "a" "b" "c";
+"2", "3", "b & !a & !c", "a" "b";
+"2", "2", "!a & !c & !b", "a";
+"3", "1", "(a & d & c) | (a & c & b)", "b" "c";
+"3", "3", "(a & d & !c) | (a & b & !c)", "b";
+"3", "2", "a & !d & !c & !b",;
+"3", "1", "(d & c & !a) | (c & b & !a)", "a" "b" "c";
+"3", "3", "(d & !a & !c) | (b & !a & !c)", "a" "b";
+"3", "2", "!a & !d & !c & !b", "a";
+EOF
+
+# Check emptiness of product with complement.
+run 0 ../ltl2tgba -Pinput.tgba -DC -E -C -X input.tgba

src/tgbatest/det.test

@@ -69,6 +69,7 @@ acc = "1";
 "3", "1", "!a",;
 EOF
 
+# FIXME: we should improve this output
 cat >ex.tgba <<'EOF'
 acc = "1";
 "1", "2", "a",;
@@ -76,13 +77,35 @@ acc = "1";
 "1", "-1", "!a",;
 "2", "3", "a",;
 "2", "1", "!a",;
+"2", "-1", "!a",;
 "-1", "-1", "!a", "1";
 "3", "3", "a",;
 "3", "-3", "a",;
 "3", "1", "!a",;
+"3", "-1", "!a",;
 "-3", "-3", "a", "1";
 "-3", "-1", "!a", "1";
 EOF
 
 run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba
-cmp out.tgba ex.tgba
+diff out.tgba ex.tgba
+
+
+run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba
+cat >ex.tgba <<EOF
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="1"]
+  1 -> 2 [label="1\n"]
+  2 [label="2"]
+  2 -> 2 [label="1\n"]
+  2 -> 3 [label="!a\n"]
+  2 -> 4 [label="!b\n"]
+  3 [label="-4"]
+  3 -> 3 [label="!a\n{Acc[1]}"]
+  4 [label="-3"]
+  4 -> 4 [label="!b\n{Acc[1]}"]
+}
+EOF
+diff out.tgba ex.tgba