* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc

(set_init_state): Return a pointer to the initial state.

(tgba_run_to_tgba): New function.

ChangeLog

@@ -1,3 +1,12 @@
+2004-12-07  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
+
+	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
+	(set_init_state): Return a pointer to the initial state.
+
+        * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc
+	(tgba_run_to_tgba): New function.
+        * src/tgbatest/ltl2tgba.cc: Add option -G.
+
 2004-12-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaalgos/replayrun.cc (replay_tgba_run): More comments.

src/tgba/tgbaexplicit.cc

@@ -152,11 +152,12 @@ namespace spot
     return i->second;
   }
 
-  void
+  tgba_explicit::state*
   tgba_explicit::set_init_state(const std::string& state)
   {
     tgba_explicit::state* s = add_state(state);
     init_ = s;
+    return s;
   }
 
   tgba_explicit::transition*

src/tgba/tgbaexplicit.hh

@@ -51,7 +51,7 @@ namespace spot
       const state* dest;
     };
 
-    void set_init_state(const std::string& state);
+    state* set_init_state(const std::string& state);
 
     transition*
     create_transition(const std::string& source, const std::string& dest);

src/tgbaalgos/emptiness.cc

@@ -19,9 +19,11 @@
 // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 // 02111-1307, USA.
 
+#include <sstream>
 #include "emptiness.hh"
 #include "tgba/tgba.hh"
 #include "tgba/bddprint.hh"
+#include "tgba/tgbaexplicit.hh"
 
 namespace spot
 {
@@ -80,7 +82,6 @@ namespace spot
     return os;
   }
 
-
   tgba_run&
   tgba_run::operator=(const tgba_run& run)
   {
@@ -108,4 +109,118 @@ namespace spot
   {
     return os;
   }
+
+  namespace
+  {
+    std::string format_state(const tgba* a, const state* s, int n)
+    {
+      std::ostringstream os;
+      os << a->format_state(s) << " (" << n << ")";
+      return os.str();
+    }
+  }
+
+  tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run)
+  {
+    tgba_explicit* res = new tgba_explicit(a->get_dict());
+    res->copy_acceptance_conditions_of(a);
+
+    const state* s = a->get_init_state();
+    int number = 1;
+    tgba_explicit::state* source;
+    tgba_explicit::state* dest;
+    const tgba_run::steps* l;
+    bdd seen_acc = bddfalse;
+
+    typedef Sgi::hash_map<const state*, tgba_explicit::state*,
+                          state_ptr_hash, state_ptr_equal> state_map;
+    state_map seen;
+
+    if (run->prefix.empty())
+        l = &run->cycle;
+    else
+        l = &run->prefix;
+
+    tgba_run::steps::const_iterator i = l->begin();
+
+    assert(s->compare(i->s) == 0);
+    source = res->set_init_state(format_state(a, i->s, number));
+    ++number;
+    seen.insert(std::make_pair(i->s, source));
+
+    for (; i != l->end(); )
+      {
+        // 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
+          {
+            if (l == &run->prefix)
+              {
+                l = &run->cycle;
+                i = l->begin();
+              }
+            next = l->begin()->s;
+          }
+
+        // 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) != 0)
+              {
+                delete s2;
+                continue;
+              }
+            else
+              {
+                s = s2;
+                break;
+              }
+          }
+        assert(!j->done());
+        delete j;
+
+        state_map::const_iterator its = seen.find(next);
+        if (its == seen.end())
+          {
+            dest = res->add_state(format_state(a, next, number));
+            ++number;
+            seen.insert(std::make_pair(next, dest));
+          }
+        else
+          dest = its->second;
+
+        tgba_explicit::transition* t = res->create_transition(source, dest);
+        res->add_conditions(t, label);
+        res->add_acceptance_conditions(t, acc);
+        source = dest;
+
+        // Sum acceptance conditions.
+        if (l == &run->cycle && i != l->begin())
+            seen_acc |= acc;
+      }
+    delete s;
+
+    assert(seen_acc == a->all_acceptance_conditions());
+
+    res->merge_transitions();
+
+    return res;
+  }
+
 }

src/tgbaalgos/emptiness.hh

@@ -179,12 +179,23 @@ namespace spot
   /// annotation).
   ///
   /// (\a a is used here only to format states and transitions.)
+  ///
+  /// Output the prefix and cycle of the tgba_run \a run, even if it
+  /// does not corresponds to an actual run of the automaton \a a.
+  /// This is unlike replay_tgba_run(), which will ensure the run
+  /// actually exist in the automaton (and will display any transition
+  /// annotation).
   std::ostream& print_tgba_run(std::ostream& os,
-			       const tgba* a,
-			       const tgba_run* run);
+                               const tgba* a,
+                               const tgba_run* run);
+
+  /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable
+  /// states are merged).
+  ///
+  /// \pre \a run must correspond to an actual run of the automaton \a a.
+  tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run);
+
   /// @}
-
-
 }
 
 #endif // SPOT_TGBAALGOS_EMPTINESS_HH

src/tgbatest/ltl2tgba.cc

@@ -74,6 +74,8 @@ syntax(char* prog)
             << "  -F    read the formula from the file" << std::endl
 	    << "  -g    graph the accepting run on the automaton (requires -e)"
 	    << std::endl
+	    << "  -G    graph the accepting run seen as an automaton "
+	    << " (requires -e)" << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
 	    << "  -m    try to reduce accepting runs, in a second pass"
 	    << std::endl
@@ -170,6 +172,7 @@ main(int argc, char** argv)
   bool post_branching = false;
   bool fair_loop_approx = false;
   bool graph_run_opt = false;
+  bool graph_run_tgba_opt = false;
   bool opt_reduce = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
@@ -241,6 +244,10 @@ main(int argc, char** argv)
 	{
 	  graph_run_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-G"))
+	{
+	  graph_run_tgba_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-L"))
 	{
 	  fair_loop_approx = true;
@@ -443,9 +450,10 @@ main(int argc, char** argv)
 	}
     }
 
-  if (graph_run_opt && (echeck_algo == "" || !expect_counter_example))
+  if ((graph_run_opt || graph_run_tgba_opt) &&
+              (echeck_algo == "" || !expect_counter_example))
     {
-      std::cerr << argv[0] << ": error: -g requires -e." << std::endl;
+      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
       exit(1);
     }
 
@@ -690,7 +698,7 @@ main(int argc, char** argv)
             {
               ec = spot::explicit_tau03_search(a);
             }
-
+          break;
 	case Tau03OptSearch:
           ec = spot::explicit_tau03_opt_search(a);
 	  break;
@@ -704,7 +712,7 @@ main(int argc, char** argv)
 	  do
 	    {
 	      spot::emptiness_check_result* res = ec->check();
-	      if (!graph_run_opt)
+	      if (!graph_run_opt && !graph_run_tgba_opt)
 		ec->print_stats(std::cout);
 	      if (expect_counter_example != !!res &&
                       (!bit_state_hashing || !expect_counter_example))
@@ -746,6 +754,12 @@ main(int argc, char** argv)
 			  spot::tgba_run_dotty_decorator deco(run);
 			  spot::dotty_reachable(std::cout, a, &deco);
 			}
+		      else if (graph_run_tgba_opt)
+			{
+			  spot::tgba* ar = spot::tgba_run_to_tgba(a, run);
+			  spot::dotty_reachable(std::cout, ar);
+			  delete ar;
+			}
 		      else
 			{
 			  spot::print_tgba_run(std::cout, a, run);