diff --git a/buchi.c b/buchi.c
index 79df8b7..0baf3a0 100644
--- a/buchi.c
+++ b/buchi.c
@@ -420,6 +420,12 @@ void make_btrans(BState *s) /* creates all the transitions from a state */
   bstate_count++;
 }
 
+/********************************************************************\
+|*                  Export of the Buchi automaton                   *|
+\********************************************************************/
+BState* buchi_bstates() { return bstates; }
+int     buchi_accept() { return accept; }
+
 /********************************************************************\
 |*                  Display of the Buchi automaton                  *|
 \********************************************************************/
@@ -461,6 +467,50 @@ void print_buchi(BState *s) /* dumps the Buchi automaton */
   }
 }
 
+static void
+print_dot_buchi_1(BState *s)
+{
+    BTrans *t;
+    if(s == bstates) return;
+
+    print_dot_buchi_1(s->nxt); /* begins with the last state */
+
+    fprintf(tl_out, "%i[label=\"%i\"%s];\n", s->id, s->id,
+            s->final == accept ? ",shape=doublecircle" : "");
+
+    for(t = s->trans->nxt; t != s->trans; t = t->nxt) {
+        fprintf(tl_out, "%d -> %d [label=\"", s->id, t->to->id);
+
+        /* print label */
+        BTrans *t1;
+        spin_print_set(t->pos, t->neg);
+        for(t1 = t; t1->nxt != s->trans; ) {
+            if (t1->nxt->to->id == t->to->id &&
+                t1->nxt->to->final == t->to->final) {
+                fprintf(tl_out, ") || (");
+                spin_print_set(t1->nxt->pos, t1->nxt->neg);
+                t1->nxt = t1->nxt->nxt;
+            } else {
+                t1 = t1->nxt;
+            }
+        }
+        fprintf(tl_out, "\"];\n");
+    }
+}
+
+void
+print_dot_buchi()
+{
+    fprintf(tl_out,
+            "digraph g {\n"
+            "rankdir=\"LR\";\n"
+            "node [shape=circle];\n"
+            "Init[shape=plaintext,label=\"\"];\n"
+            "Init -> %i;\n", -1);
+    print_dot_buchi_1(bstates->nxt);
+    fprintf(tl_out, "}\n");
+}
+
 void print_spin_buchi() {
   BTrans *t;
   BState *s;
@@ -647,6 +697,4 @@ void mk_buchi()
       fprintf(tl_out, "\n");
     }
   }
-
-  print_spin_buchi();
 }
diff --git a/ltl2ba.h b/ltl2ba.h
index f330149..53997bf 100644
--- a/ltl2ba.h
+++ b/ltl2ba.h
@@ -201,6 +201,13 @@ void    mk_alternating(Node *);
 void    mk_generalized();
 void    mk_buchi();
 
+BState* buchi_bstates();
+int     buchi_accept();
+
+void    print_spin_buchi();
+void    print_dot_buchi();
+
+
 ATrans *dup_trans(ATrans *);
 ATrans *merge_trans(ATrans *, ATrans *);
 void do_merge_trans(ATrans **, ATrans *, ATrans *);
diff --git a/main.c b/main.c
index ee138fa..eb4d7ae 100644
--- a/main.c
+++ b/main.c
@@ -109,6 +109,7 @@ tl_main(int argc, char *argv[])
 	}
 	if (hasuform == 0) usage();
 	tl_parse();
+	print_spin_buchi();
 	if (tl_stats) tl_endstats();
 	return tl_errs;
 }