From be4f139757fac58c12450d2d5fc45266a8fa039b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 7 Mar 2017 16:01:14 +0100
Subject: [PATCH] tests: remove ltlprod

This very old test did not do anything useful today.

* tests/core/ltlprod.cc, tests/core/ltlprod.test: Delete.
* tests/Makefile.am: Adjust.
---
 tests/Makefile.am       |  3 --
 tests/core/ltlprod.cc   | 68 -----------------------------------------
 tests/core/ltlprod.test | 39 -----------------------
 3 files changed, 110 deletions(-)
 delete mode 100644 tests/core/ltlprod.cc
 delete mode 100755 tests/core/ltlprod.test

diff --git a/tests/Makefile.am b/tests/Makefile.am
index 03a3be83f..1e1336f9a 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -74,7 +74,6 @@ check_PROGRAMS = \
   core/intvcomp \
   core/intvcmp2 \
   core/kripkecat \
-  core/ltlprod \
   core/ltl2dot \
   core/ltl2text \
   core/ltlrel \
@@ -108,7 +107,6 @@ core_ikwiad_SOURCES = core/ikwiad.cc
 core_intvcomp_SOURCES = core/intvcomp.cc
 core_intvcmp2_SOURCES = core/intvcmp2.cc
 core_kripkecat_SOURCES = core/kripkecat.cc
-core_ltlprod_SOURCES  = core/ltlprod.cc
 core_ngraph_SOURCES = core/ngraph.cc
 core_randtgba_SOURCES = core/randtgba.cc
 core_readsat_SOURCES = core/readsat.cc
@@ -229,7 +227,6 @@ TESTS_twa = \
   core/ltl2tgba2.test \
   core/ltl2neverclaim.test \
   core/ltl2neverclaim-lbtt.test \
-  core/ltlprod.test \
   core/explprod.test \
   core/explpro2.test \
   core/explpro3.test \
diff --git a/tests/core/ltlprod.cc b/tests/core/ltlprod.cc
deleted file mode 100644
index 0aa0d1243..000000000
--- a/tests/core/ltlprod.cc
+++ /dev/null
@@ -1,68 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2014, 2015, 2016 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 <spot/tl/parse.hh>
-#include <spot/twaalgos/product.hh>
-#include <spot/twaalgos/ltl2tgba_fm.hh>
-#include <spot/twaalgos/dot.hh>
-
-static void
-syntax(char* prog)
-{
-  std::cerr << prog << " formula1 formula2" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-
-  if (argc != 3)
-    syntax(argv[0]);
-
-  {
-    spot::environment& env(spot::default_environment::instance());
-
-    auto pf1 = spot::parse_infix_psl(argv[1], env);
-    if (pf1.format_errors(std::cerr))
-      return 2;
-    auto f1 = pf1.f;
-
-    auto pf2 = spot::parse_infix_psl(argv[2], env);
-    if (pf2.format_errors(std::cerr))
-      return 2;
-    auto f2 = pf2.f;
-
-    auto dict = spot::make_bdd_dict();
-    {
-      auto a1 = spot::ltl_to_tgba_fm(f1, dict);
-      auto a2 = spot::ltl_to_tgba_fm(f2, dict);
-      spot::print_dot(std::cout, product(a1, a2));
-    }
-  }
-  assert(spot::fnode::instances_check());
-  return exit_code;
-}
diff --git a/tests/core/ltlprod.test b/tests/core/ltlprod.test
deleted file mode 100755
index 21e286619..000000000
--- a/tests/core/ltlprod.test
+++ /dev/null
@@ -1,39 +0,0 @@
-#!/bin/sh
-# -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2015 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/>.
-
-
-. ./defs
-
-set -e
-
-# We don't check the output, but just running these might be enough to
-# trigger assertions.
-
-run 0 ../ltlprod a b
-run 0 ../ltlprod a a
-run 0 ../ltlprod 'a U b' 'X f'
-run 0 ../ltlprod 'X a' 'X a'
-run 0 ../ltlprod 'X a' 'a U b'
-run 0 ../ltlprod 'a & b & c' 'b & d & c'
-run 0 ../ltlprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
-run 0 ../ltlprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'