diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc index be80419e6..d9ca3b0eb 100644 --- a/src/tgbaalgos/isdet.cc +++ b/src/tgbaalgos/isdet.cc @@ -106,6 +106,6 @@ namespace spot bool is_deterministic(const tgba* aut) { - return !!count_nondet_states_aux(aut, false); + return !count_nondet_states_aux(aut, false); } } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index f9d95a427..3ddfa30f6 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -77,6 +77,7 @@ TESTS = \ taatgba.test \ tgbaread.test \ renault.test \ + nondet.test \ neverclaimread.test \ readsave.test \ ltl2tgba.test \ diff --git a/src/tgbatest/nondet.test b/src/tgbatest/nondet.test new file mode 100755 index 000000000..1cc7decd4 --- /dev/null +++ b/src/tgbatest/nondet.test @@ -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<out.2 +cat >expected.2<