Fix return of is_deterministic(), it was inverted.
Reported by Étienne Renault. * src/tgbaalgos/isdet.cc (is_deterministic): Invert return code. * src/tgbatest/nondet.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it.
This commit is contained in:
parent
7854f629e5
commit
4ed4e4d2a8
3 changed files with 42 additions and 1 deletions
40
src/tgbatest/nondet.test
Executable file
40
src/tgbatest/nondet.test
Executable file
|
|
@ -0,0 +1,40 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
../../bin/ltl2tgba FGa GFa --stats='%f %d' >out.1
|
||||
cat >expected.1<<EOF
|
||||
FGa 0
|
||||
GFa 1
|
||||
EOF
|
||||
|
||||
cmp out.1 expected.1
|
||||
|
||||
../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s' >out.2
|
||||
cat >expected.2<<EOF
|
||||
FGa 0 1 2
|
||||
GFa 1 0 1
|
||||
EOF
|
||||
|
||||
cmp out.2 expected.2
|
||||
Loading…
Add table
Add a link
Reference in a new issue