diff --git a/tests/Makefile.am b/tests/Makefile.am index a219c431d..8fe314b19 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -62,6 +62,7 @@ core/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in # Keep this sorted alphabetically. check_PROGRAMS = \ core/acc \ + core/bdddict \ core/bitvect \ core/checkpsl \ core/checkta \ @@ -100,6 +101,7 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. core_acc_SOURCES = core/acc.cc +core_bdddict_SOURCES = core/bdddict.cc core_bitvect_SOURCES = core/bitvect.cc core_checkpsl_SOURCES = core/checkpsl.cc core_checkta_SOURCES = core/checkta.cc @@ -204,6 +206,7 @@ TESTS_misc = \ TESTS_twa = \ core/acc.test \ core/acc2.test \ + core/bdddict.test \ core/alternating.test \ core/ltlcross3.test \ core/taatgba.test \ diff --git a/tests/core/.gitignore b/tests/core/.gitignore index 8e6b5f689..bdea8cd42 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -1,5 +1,6 @@ acc apcollect +bdddict bddprod bitvect blue_counter @@ -45,6 +46,7 @@ nenoform ngraph output1 output2 +parity parse_print powerset *.ps diff --git a/tests/core/bdddict.cc b/tests/core/bdddict.cc new file mode 100644 index 000000000..ac848baa0 --- /dev/null +++ b/tests/core/bdddict.cc @@ -0,0 +1,31 @@ +// -*- coding: utf-8 -*-x +// Copyright (C) 2017 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 . + +#include +#include +#include + +int main() +{ + spot::formula f = spot::parse_formula("& & G p0 p1 p2"); + spot::translator trans; + spot::twa_graph_ptr aut = trans.run(f); + aut->get_dict()->assert_emptiness(); // Should fail. + return 0; +} diff --git a/tests/core/bdddict.test b/tests/core/bdddict.test new file mode 100755 index 000000000..3dd380af1 --- /dev/null +++ b/tests/core/bdddict.test @@ -0,0 +1,29 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 + +# Exercise bdd_dict::assert_emptiness() +../bdddict 2>stderr && exit 1 +grep 'some maps are not empty' stderr +grep 'Var\[p0\] x2' stderr +grep 'Var\[p1\] x2' stderr +grep 'Var\[p2\] x2' stderr