From 5d310940292bc74b23ca6ef31623b033e1fa3937 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 10 Feb 2015 16:58:08 +0100
Subject: [PATCH] dtgba_complement: take a tgba_digraph_ptr as input

* src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh: Here.
* src/tgbatest/ltl2tgba.cc: Adjust.
---
 src/tgbaalgos/dtgbacomp.cc | 10 +++++-----
 src/tgbaalgos/dtgbacomp.hh |  4 ++--
 src/tgbatest/ltl2tgba.cc   |  2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc
index 2cfbd3523..a0b6e49de 100644
--- a/src/tgbaalgos/dtgbacomp.cc
+++ b/src/tgbaalgos/dtgbacomp.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
-// de l'Epita.
+// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -22,7 +22,7 @@
 
 namespace spot
 {
-  tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut)
+  tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_digraph_ptr& aut)
   {
     // Clone the original automaton.
     auto res = make_tgba_digraph(aut,
@@ -110,7 +110,7 @@ namespace spot
     return res;
   }
 
-  tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut)
+  tgba_digraph_ptr dtgba_complement_weak(const const_tgba_digraph_ptr& aut)
   {
     // Clone the original automaton.
     auto res = make_tgba_digraph(aut,
@@ -158,7 +158,7 @@ namespace spot
     return res;
   }
 
-  tgba_digraph_ptr dtgba_complement(const const_tgba_ptr& aut)
+  tgba_digraph_ptr dtgba_complement(const const_tgba_digraph_ptr& aut)
   {
     if (aut->is_inherently_weak())
       return dtgba_complement_weak(aut);
diff --git a/src/tgbaalgos/dtgbacomp.hh b/src/tgbaalgos/dtgbacomp.hh
index 6cad13e54..964a76d31 100644
--- a/src/tgbaalgos/dtgbacomp.hh
+++ b/src/tgbaalgos/dtgbacomp.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -32,7 +32,7 @@ namespace spot
   /// which case the output will also be weak and deterministic) the
   /// resulting automaton is very unlikely to be deterministic.
   SPOT_API tgba_digraph_ptr
-  dtgba_complement(const const_tgba_ptr& aut);
+  dtgba_complement(const const_tgba_digraph_ptr& aut);
 }
 
 #endif // SPOT_TGBAALGOS_DTGBACOMP_HH
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 1ec323794..1c8fc23bf 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -1279,7 +1279,7 @@ checked_main(int argc, char** argv)
       if (opt_dtgbacomp)
 	{
 	  tm.start("DTGBA complement");
-	  a = dtgba_complement(a);
+	  a = dtgba_complement(ensure_digraph(a));
 	  tm.stop("DTGBA complement");
 	}