From a0a035e0e1ce0ef6d956416f44435b33cfc86c14 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 31 Jan 2015 17:55:38 +0100
Subject: [PATCH] tgbatest: remove the unused powerset source

* src/tgbatest/powerset.cc: Delete.
* src/tgbatest/Makefile.am: Adjust.
---
 src/tgbatest/Makefile.am |  5 ---
 src/tgbatest/powerset.cc | 71 ----------------------------------------
 2 files changed, 76 deletions(-)
 delete mode 100644 src/tgbatest/powerset.cc

diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 7a5e82431..7f51380be 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -37,12 +37,10 @@ check_PROGRAMS = \
   checkpsl \
   checkta \
   emptchk \
-  expldot \
   intvcomp \
   intvcmp2 \
   ltlprod \
   maskacc \
-  powerset \
   readsat \
   taatgba
 
@@ -53,14 +51,11 @@ checkpsl_SOURCES = checkpsl.cc
 checkta_SOURCES = checkta.cc
 complement_SOURCES = complementation.cc
 emptchk_SOURCES  = emptchk.cc
-expldot_SOURCES  = powerset.cc
-expldot_CXXFLAGS = -DDOTTY
 intvcomp_SOURCES = intvcomp.cc
 intvcmp2_SOURCES = intvcmp2.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
 ltlprod_SOURCES  = ltlprod.cc
 maskacc_SOURCES  = maskacc.cc
-powerset_SOURCES = powerset.cc
 randtgba_SOURCES = randtgba.cc
 readsat_SOURCES = readsat.cc
 taatgba_SOURCES = taatgba.cc
diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc
deleted file mode 100644
index 5aeab8f3c..000000000
--- a/src/tgbatest/powerset.cc
+++ /dev/null
@@ -1,71 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
-// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include <iostream>
-#include <cassert>
-#include <cstdlib>
-#include "tgbaalgos/powerset.hh"
-#include "tgbaparse/public.hh"
-#include "tgbaalgos/save.hh"
-#include "ltlast/allnodes.hh"
-#include "tgbaalgos/dotty.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " file" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-
-  if (argc != 2)
-    syntax(argv[0]);
-
-  {
-    auto dict = spot::make_bdd_dict();
-
-    spot::ltl::environment& env(spot::ltl::default_environment::instance());
-    spot::tgba_parse_error_list pel;
-    auto a = spot::tgba_parse(argv[1], pel, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel))
-      return 2;
-
-
-#ifndef DOTTY
-    auto e = spot::tgba_powerset(a);
-    spot::tgba_save_reachable(std::cout, e);
-#else
-    spot::dotty_reachable(std::cout, a);
-#endif
-  }
-
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  assert(spot::ltl::atomic_prop::instance_count() != 0);
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  return exit_code;
-}