From 97237384042b63d7f1f789449fac0a63d8cc31a5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 26 Mar 2013 17:00:44 +0100
Subject: [PATCH] dve2: use the new translator class

* iface/dve2/dve2check.cc: Adjust.
* iface/dve2/README: Some (unrelated) typos.
---
 iface/dve2/README       |  8 +++++---
 iface/dve2/dve2check.cc | 32 ++++++++++----------------------
 2 files changed, 15 insertions(+), 25 deletions(-)

diff --git a/iface/dve2/README b/iface/dve2/README
index dbc6fb51b..9469940cf 100644
--- a/iface/dve2/README
+++ b/iface/dve2/README
@@ -53,8 +53,8 @@ Usage with Spot
   The function load_dve2() defined in dve2.hh in this directory
   will accept "model.dve" or "model.dve2C" as file argument.
   In the former case, it will call "divine compile --ltsmin"
-  if "model.dve2C" does not exist or is older.  Then load
-  "model.dve2C" dynamically.
+  if "model.dve2C" does not exist or is older.  Then it will
+  load "model.dve2C" dynamically.
 
   load_dve2() also requires a set of atomic propositions that should
   be observed in the model.  These are usually the atomic propositions
@@ -100,7 +100,9 @@ Usage with Spot
   be enclosed in double quote.
 
   Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are
-  considered to be two atomic propositions with the same semantics.
+  considered to be two distinct atomic propositions with the same
+  semantics.
+
 
 Examples
 ========
diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc
index a0306ee06..04ae7de62 100644
--- a/iface/dve2/dve2check.cc
+++ b/iface/dve2/dve2check.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE)
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -21,7 +21,7 @@
 #include "ltlenv/defaultenv.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
-#include "tgbaalgos/ltl2tgba_fm.hh"
+#include "tgbaalgos/translate.hh"
 #include "tgbaalgos/emptiness.hh"
 #include "tgbaalgos/reducerun.hh"
 #include "tgbaalgos/postproc.hh"
@@ -203,15 +203,15 @@ main(int argc, char **argv)
   if (exit_code)
     goto safe_exit;
 
-  tm.start("reducing formula");
+  tm.start("translating formula");
   {
-    spot::ltl::ltl_simplifier_options opt(true, true, true, true, true);
-    spot::ltl::ltl_simplifier simp(opt);
-    const spot::ltl::formula* r = simp.simplify(f);
-    f->destroy();
-    f = r;
+    spot::translator trans(dict);
+    if (deterministic)
+      trans.set_pref(spot::postprocessor::Deterministic);
+
+    prop = trans.run(&f);
   }
-  tm.stop("reducing formula");
+  tm.stop("translating formula");
 
   atomic_prop_collect(f, &ap);
 
@@ -243,18 +243,6 @@ main(int argc, char **argv)
       }
     }
 
-
-  tm.start("translating formula");
-  prop = spot::ltl_to_tgba_fm(f, dict);
-  tm.stop("translating formula");
-
-  if (deterministic)
-    post.set_pref(spot::postprocessor::Deterministic);
-
-  tm.start("postprocessing A_f");
-  prop = post.run(prop, f);
-  tm.stop("postprocessing A_f");
-
   if (output == DotFormula)
     {
       tm.start("dotty output");