ltl: remove the useless Finish operator

* src/ltlast/unop.cc, src/ltlast/unop.hh src/ltlvisit/lbt.cc,
src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc: Remove Finish.
* src/tgbaalgos/ltl2taa.cc: Remove Finish, and simply use an empty
destination to code the sink.

src/ltlast/unop.cc

@@ -98,20 +98,6 @@ namespace spot
 	  is.syntactic_persistence = is.syntactic_safety;
 	  is.accepting_eword = false;
 	  break;
-	case Finish:
-	  is.not_marked = true;
-	  is.boolean = false;
-	  is.ltl_formula = false;
-	  is.psl_formula = false;
-	  is.sere_formula = false;
-	  is.finite = false;
-	  is.syntactic_safety = false;
-	  is.syntactic_guarantee = false;
-	  is.syntactic_obligation = false;
-	  is.syntactic_recurrence = false;
-	  is.syntactic_persistence = false;
-	  is.accepting_eword = false;
-	  break;
 	case NegClosure:
 	case NegClosureMarked:
 	  is.not_marked = (op == NegClosure);
@@ -181,8 +167,6 @@ namespace spot
 	  return "F";
 	case G:
 	  return "G";
-	case Finish:
-	  return "Finish";
 	case Closure:
 	  return "Closure";
 	case NegClosure:
@@ -272,10 +256,6 @@ namespace spot
 	  assert(child != constant::empty_word_instance());
 	  break;
 
-	case Finish:
-	  // No simplifications for Finish.
-	  break;
-
 	case Closure:
 	  // {0} = 0, {1} = 1,  {b} = b
 	  if (child->is_boolean())

src/ltlast/unop.hh

@@ -42,8 +42,6 @@ namespace spot
       enum type {
 	// LTL
 	Not, X, F, G,
-	// ELTL
-	Finish,
 	// Closure
 	Closure, NegClosure, NegClosureMarked
 	};

src/ltlvisit/lbt.cc

@@ -160,7 +160,6 @@ namespace spot
 	    case unop::G:
 	      os_ << 'G';
 	      break;
-	    case unop::Finish:
 	    case unop::Closure:
 	    case unop::NegClosure:
 	    case unop::NegClosureMarked:

src/ltlvisit/mark.cc

@@ -142,7 +142,6 @@ namespace spot
 			  case unop::X:
 			  case unop::F:
 			  case unop::G:
-			  case unop::Finish:
 			  case unop::Closure:
 			    res->push_back(recurse(f));
 			    break;
@@ -236,7 +235,6 @@ namespace spot
 	    case unop::X:
 	    case unop::F:
 	    case unop::G:
-	    case unop::Finish:
 	    case unop::Closure:
 	    case unop::NegClosureMarked:
 	      result_ = uo->clone();

src/ltlvisit/simplify.cc

@@ -516,12 +516,6 @@ namespace spot
 				       unop::Closure : op,
 				       recurse_(f, false));
 	      return;
-	      /* !Finish(x), is not simplified */
-	    case unop::Finish:
-	      result_ = unop::instance(uo->op(), recurse_(f, false));
-	      if (negated_)
-		result_ = unop::instance(unop::Not, result_);
-	      return;
 	    }
 	  SPOT_UNREACHABLE();
 	}
@@ -1737,9 +1731,6 @@ namespace spot
 		      }
 		  }
 	      break;
-	    case unop::Finish:
-	      // No simplification
-	      break;
 	    }
 	  result_ = unop::instance(op, result_);
 	}

src/ltlvisit/tostring.cc

@@ -712,10 +712,6 @@ namespace spot
 	    case unop::G:
 	      emit(KG);
 	      break;
-	    case unop::Finish:
-	      os_ << "finish";
-	      need_parent = true;
-	      break;
 	    case unop::Closure:
 	      os_ << '{';
 	      in_ratexp_ = true;

src/ltlvisit/tunabbrev.cc

@@ -1,7 +1,8 @@
-// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -39,7 +40,6 @@ namespace spot
     {
       switch (uo->op())
 	{
-	case unop::Finish:
 	case unop::X:
 	case unop::Not:
 	case unop::Closure:

src/tgba/formula2bdd.cc

@@ -79,7 +79,6 @@ namespace spot
       {
 	switch (node->op())
 	  {
-	  case unop::Finish:
 	  case unop::F:
 	  case unop::G:
 	  case unop::X:

src/tgbaalgos/ltl2taa.cc

@@ -70,15 +70,10 @@ namespace spot
 	  to_free_.push_back(f);
 	}
 	init_ = f;
-	std::vector<const formula*> dst;
+	std::vector<const formula*> empty;
-	std::vector<const formula*> a;
+	taa_tgba::transition* t = res_->create_transition(init_, empty);
-
-	// A little hack to define a sink
-	dst.push_back(unop::instance(unop::Finish, constant::true_instance()));
-	to_free_.push_back(dst[0]);
-	taa_tgba::transition* t = res_->create_transition(init_, dst);
 	res_->add_condition(t, f->clone());
-	succ_state ss = { dst, f, a };
+	succ_state ss = { empty, f, empty };
 	succ_.push_back(ss);
       }
 
@@ -90,15 +85,10 @@ namespace spot
 	{
 	  case constant::True:
 	  {
-	    std::vector<const formula*> dst;
+	    std::vector<const formula*> empty;
-	    std::vector<const formula*> a;
+	    res_->create_transition(init_, empty);
-	    // A little hack to define a sink
+	    succ_state ss = { empty, node, empty };
-	    dst.push_back(unop::instance(unop::Finish,
-					 constant::true_instance()));
-	    res_->create_transition(init_, dst);
-	    succ_state ss = { dst, node, a };
 	    succ_.push_back(ss);
-	    to_free_.push_back(dst[0]);
 	    return;
 	  }
 	  case constant::False:
@@ -139,7 +129,6 @@ namespace spot
 	    // Done in recurse
 	    succ_ = v.succ_;
 	    return;
-	  case unop::Finish:
 	  case unop::Closure:
 	  case unop::NegClosure:
 	  case unop::NegClosureMarked:

src/tgbaalgos/ltl2tgba_fm.cc

@@ -682,7 +682,6 @@ namespace spot
 	  case unop::F:
 	  case unop::G:
 	  case unop::X:
-	  case unop::Finish:
 	  case unop::Closure:
 	  case unop::NegClosure:
 	  case unop::NegClosureMarked:
@@ -1484,9 +1483,6 @@ namespace spot
 	      //trace_ltl_bdd(dict_, res_);
 	    }
 	    break;
-
-	  case unop::Finish:
-	    SPOT_UNIMPLEMENTED();
 	  }
       }