* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search):

Record the acceptance conditions in the accepting run.
* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic.

ChangeLog

 2004-10-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search):
+	Record the acceptance conditions in the accepting run.
+	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic.
+
 	* src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files.
 	Cannot test them because the run returned by the emptiness checks
 	are currently incomplete (they lack the acceptance conditions, and

src/tgbaalgos/magic.cc

@@ -45,8 +45,7 @@ namespace spot
 	if (i->first.s->compare(ms_.x) == 0)
 	  l = &run->cycle;
 
-	// FIXME: We need to keep track of the acceptance condition.
-	tgba_run::step s = { i->first.s->clone(), *ti, bddfalse };
+	tgba_run::step s = { i->first.s->clone(), ti->first, ti->second };
 	l->push_back(s);
       }
 
@@ -140,18 +139,19 @@ namespace spot
 	  {
 	    const state* s_prime = i->current_state();
 	    bdd c = i->current_condition();
+	    bdd acc = i->current_acceptance_conditions();
 	    i->next();
 	    if (magic && 0 == s_prime->compare(x))
 	      {
 		delete s_prime;
-		tstack.push_front(c);
+		tstack.push_front (tstack_item(c, acc));
 		assert(stack.size() == tstack.size());
 		return new result(*this);
 	      }
 	    if (!has(s_prime, magic))
 	      {
 		push(s_prime, magic);
-		tstack.push_front(c);
+		tstack.push_front (tstack_item(c, acc));
 		goto recurse;
 	      }
 	    delete s_prime;

src/tgbaalgos/magic.hh

@@ -92,7 +92,8 @@ namespace spot
     typedef std::list<state_iter_pair> stack_type;
     stack_type stack;		///< Stack of visited states on the path.
 
-    typedef std::list<bdd> tstack_type;
+    typedef std::pair<bdd, bdd> tstack_item;
+    typedef std::list<tstack_item> tstack_type;
     /// \brief Stack of transitions.
     ///
     /// This is an addition to the data from the paper.

src/tgbaalgos/replayrun.cc

@@ -22,6 +22,7 @@
 #include "replayrun.hh"
 #include "tgba/tgba.hh"
 #include "emptiness.hh"
+#include "tgba/bddprint.hh"
 
 namespace spot
 {
@@ -56,69 +57,73 @@ namespace spot
 	return false;
       }
 
-    for (;;) // process the prefix then the cycle
+    for (; i != l->end(); ++serial)
       {
-	for (; i != l->end(); ++serial)
-	  {
-	    os << "state " << serial << " in " << in << ": "
-	       << a->format_state(s) << std::endl;
+	os << "state " << serial << " in " << in << ": "
+	   << a->format_state(s) << std::endl;
 
-	    // expected outgoing transition
-	    bdd label = i->label;
-	    bdd acc = i->acc;
+	// expected outgoing transition
+	bdd label = i->label;
+	bdd acc = i->acc;
 
-	    // compute the next expected state
-	    const state* next;
-	    ++i;
-	    if (i != l->end())
-	      next = i->s;
-	    else
-	      next = l->begin()->s;
-
-	    // browse the actual outgoing transition
-	    tgba_succ_iterator* j = a->succ_iter(s);
-	    delete s;
-	    for (j->first(); !j->done(); j->next())
+	// compute the next expected state
+	const state* next;
+	++i;
+	if (i != l->end())
+	  {
+	    next = i->s;
+	  }
+	else
+	  {
+	    if (l == &run->prefix)
 	      {
-		if (j->current_condition() != label
-		    || j->current_acceptance_conditions() != acc)
-		  continue;
+		l = &run->cycle;
+		in = "cycle";
+		i = l->begin();
+	      }
+	    next = l->begin()->s;
+	  }
 
-		const state* s2 = j->current_state();
-		if (s2->compare(next))
-		  {
-		    delete s2;
-		    continue;
-		  }
-		else
-		  {
-		    delete s;
-		    s = s2;
-		    break;
-		  }
+	// browse the actual outgoing transitions
+	tgba_succ_iterator* j = a->succ_iter(s);
+	delete s;
+	for (j->first(); !j->done(); j->next())
+	  {
+	    if (j->current_condition() != label
+		|| j->current_acceptance_conditions() != acc)
+	      continue;
+
+	    const state* s2 = j->current_state();
+	    if (s2->compare(next))
+	      {
+		delete s2;
+		continue;
 	      }
-	    if (j->done())
+	    else
 	      {
-		os << "ERROR: no transition with label=" << label
-		   << " and acc=" << acc << " leaving state " << serial
-		   << std::endl;
-		delete j;
-		return false;
+		s = s2;
+		break;
 	      }
-	    os << "transition with label=" << label
-	       << " and acc=" << acc << " found" << std::endl;
-	    delete j;
 	  }
-	if (l == &run->prefix)
+	if (j->done())
 	  {
-	    l = &run->cycle;
-	    in = "cycle";
-	  }
-	else
-	  {
-	    break;
+	    os << "ERROR: no transition with label="
+	       << bdd_format_formula(a->get_dict(), label)
+	       << " and acc=" << bdd_format_accset(a->get_dict(), acc)
+	       << " leaving state " << serial
+	       << " and going to state "
+	       << a->format_state(next)
+	       << std::endl;
+	    delete j;
+	    return false;
 	  }
+	os << "transition with label="
+	   << bdd_format_formula(a->get_dict(), label)
+	   << " and acc=" << bdd_format_accset(a->get_dict(), acc)
+	   << std::endl;
+	delete j;
       }
+    delete s;
     return true;
   }
 }