From 1ef3e5f3ff2cefce29716fdfb7818187ca3eb951 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 May 2015 20:09:39 +0200
Subject: [PATCH] translate: remove arbitrary restriction on -U and -D

* src/twaalgos/translate.cc, src/bin/ltl2tgba.cc: Do not assume that
unambiguous is incompatible with deterministic.
---
 src/bin/ltl2tgba.cc       | 18 ------------------
 src/twaalgos/translate.cc | 19 ++++++-------------
 2 files changed, 6 insertions(+), 31 deletions(-)

diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc
index d7b14b303..829b450a0 100644
--- a/src/bin/ltl2tgba.cc
+++ b/src/bin/ltl2tgba.cc
@@ -181,24 +181,6 @@ main(int argc, char** argv)
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
     exit(err);
 
-  // Using both --unambiguous --deterministic do not really make
-  // sense.
-  if (unambiguous)
-    {
-      if (type == spot::postprocessor::Monitor)
-	{
-	  // We do not now how to make unambiguous monitors, other
-	  // than deterministic monitors.
-	  unambiguous = false;
-	  pref = spot::postprocessor::Deterministic;
-	}
-      else if (pref == spot::postprocessor::Deterministic)
-	{
-	  error(2, 0,
-		"--unambiguous and --deterministic are incompatible options");
-	}
-    }
-
   if (jobs.empty())
     error(2, 0, "No formula to translate?  Run '%s --help' for usage.",
 	  program_name);
diff --git a/src/twaalgos/translate.cc b/src/twaalgos/translate.cc
index d6ff47ae2..496b8ca3c 100644
--- a/src/twaalgos/translate.cc
+++ b/src/twaalgos/translate.cc
@@ -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 (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -64,19 +64,12 @@ namespace spot
 
   twa_graph_ptr translator::run(const ltl::formula** f)
   {
-    if (unambiguous_)
+    if (unambiguous_ && type_ == postprocessor::Monitor)
       {
-	if (type_ == postprocessor::Monitor)
-	  {
-	    // Deterministic monitor are unambiguous, so the
-	    // unambiguous option is not really relevant for monitors.
-	    unambiguous_ = false;
-	    set_pref(postprocessor::Deterministic);
-	  }
-	else if (pref_ == postprocessor::Deterministic)
-	  {
-	    unambiguous_ = false;
-	  }
+	// Deterministic monitor are unambiguous, so the unambiguous
+	// option is not really relevant for monitors.
+	unambiguous_ = false;
+	set_pref(postprocessor::Deterministic);
       }
 
     const ltl::formula* r = simpl_->simplify(*f);