reduc.test 1.52 KB
Newer Older
martinez's avatar
martinez committed
1
#! /bin/sh
2
3
4
5
6
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
# Pierre et Marie Curie.
martinez's avatar
martinez committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
#
# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.


26
# Check for the reduc visitor.
27
. ./defs || exit 1
martinez's avatar
martinez committed
28

29
set -e
martinez's avatar
martinez committed
30

31
32
FILE=formulae
: > $FILE
33
34
# for i in 10 11 12 13 14 15 16 17 18 19 20; do
for i in 10 12 14 16 18 20; do
35
36
  run 0 ../randltl -u -s 0   -f $i a b c -F 100 >> $FILE
  run 0 ../randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
37
done
martinez's avatar
martinez committed
38

39
40
41
42
43
44
45
for opt in 0 1 2 3 7; do
  run 0 ../reduc -f -h $opt "$FILE"
done
# Running the above through valgrind is quite slow already.
# Don't use valgrind for the next reductions (even slower).
for opt in 8 9; do
  ../reduc -f -h $opt "$FILE"
46
done