diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e2cefcdb4..13cf35a0a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -121,7 +121,6 @@ TESTS = \ emptchk.test \ emptchke.test \ dfs.test \ - stutter_invariant.test \ ltlcrossce.test \ emptchkr.test \ ltlcounter.test \ diff --git a/src/tgbatest/stutter_invariant.test b/src/tgbatest/stutter_invariant.test deleted file mode 100755 index 4c0a8d348..000000000 --- a/src/tgbatest/stutter_invariant.test +++ /dev/null @@ -1,47 +0,0 @@ -#!/bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2008, 2009, 2010, 2014 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). -# Copyright (C) 2003, 2004, 2005 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 . - - -. ./defs - -set -e - -check_stutter() -{ - FORMULAS=$1 - SPOT_STUTTER_CHECK=$2 - run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >exp - for i in `seq $3 $4` - do - SPOT_STUTTER_CHECK=$i - run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >out - diff out exp - done -} - -cat >ltl <