diff --git a/tests/Makefile.am b/tests/Makefile.am index 84f541387..537a487a4 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -248,6 +248,7 @@ TESTS_twa = \ core/dra2dba.test \ core/unambig.test \ core/ltlcross4.test \ + core/streett.test \ core/ltl3dra.test \ core/ltl2dstar.test \ core/ltl2dstar2.test \ diff --git a/tests/core/streett.test b/tests/core/streett.test new file mode 100755 index 000000000..7551ed37b --- /dev/null +++ b/tests/core/streett.test @@ -0,0 +1,115 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 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 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 + +## Save the output of ltl2dstar, so that we can exercise the +## conversion from Streett to TGBA regardless of whether ltl2dstar is +## installed. +# ltldo 'ltl2dstar --automata=streett' -f 'GFa & GFb & FGc' > streett.hoa +cat >streett.hoa < out.hoa +autfilt -q --equivalent-to streett.hoa out.hoa +grep 'generalized-Buchi 2' out.hoa